diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-12-14 23:40:44 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-12-14 23:40:44 +0000 |
commit | e85f690a704a4182a8ffc8b96cff71737f5c0904 (patch) | |
tree | f77ee57d4b4947d56e885eada3c65ce64354e366 /src/util | |
parent | 5b04e6f0b29be4f376ab1f306529bf8a22111bd5 (diff) |
added minor documentation for parametric datatypes, for bug 283
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.h | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/util/datatype.h b/src/util/datatype.h index 5a1d9b931..d39d7110d 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -158,7 +158,15 @@ private: throw(AssertionException, DatatypeResolutionException); friend class Datatype; - /** @FIXME document this! */ + /** Helper function for resolving parametric datatypes. + This replaces instances of the SortConstructorType produced for unresolved + parametric datatypes, with the corresponding resolved DatatypeType. For example, take + the parametric definition of a list, list[T] = cons(car : T, cdr : list[T]) | null. + If "range" is the unresolved parametric datatype: + DATATYPE list = cons(car: SORT_TAG_1, cdr: SORT_TAG_2(SORT_TAG_1)) | null END;, + this function will return the resolved type: + DATATYPE list = cons(car: SORT_TAG_1, cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END; + */ Type doParametricSubstitution(Type range, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements); @@ -350,6 +358,19 @@ public: * Datatype and request the constructor, selector, and tester terms. * See src/parser/parser.cpp for how this is done. For API usage * ideas, see test/unit/util/datatype_black.h. + * + * Datatypes may also be defined parametrically, such as this example: + * + * DATATYPE
+ * list[T] = cons(car : T, cdr : list[T]) | null,
+ * tree = node(children : list[tree]) | leaf
+ * END; + * + * Here, the definition of the parametric datatype list, where T is a type variable. + * In other words, this defines a family of types list[C] where C is any concrete + * type. Datatypes can be parameterized over multiple type variables using the + * syntax sym[ T1, ..., Tn ] = ..., + * */ class CVC4_PUBLIC Datatype { public: |