[aslspec] type parameter refactoring and type inference

asllib/aslspec/AST.ml

@@ -214,7 +214,7 @@ module Term = struct
     | Parameter of { loc : source_location; name : string }
         (** A named type parameter. The parser constructs an instance of
             [Label], which is later substituted by an instance of [Parameter] in
-            [SubstituteTypeParameters]. *)
+            [ResolveTypeParameters]. *)
     | TypeOperator of {
         loc : source_location;
         op : type_operator;

asllib/aslspec/aslspec.md

@@ -64,6 +64,20 @@ aslspec supports the following type constructors:
 - `fun A -> B`: the type of total functions from `A` to `B`.
 - `partial T -> T`: the type of partial functions from `A` to `B`.
 
+Type definitions can declare a type parameter in double brackets. References
+to the parameter are scoped to the definition. For example:
+```
+typedef Tree[[T]] =
+    | Leaf(value: T)
+    | Node(left: Tree[[T]], right: Tree[[T]])
+;
+```
+An application such as `Tree[[Z]]` instantiates `T` with `Z`.
+When a parameterized variant is used in an expression, its parameter is
+inferred from the types of the variant's components. Repeated occurrences of
+the parameter must unify to a single type. For example, `Node(left, right)`
+requires the types inferred for `left` and `right` to be compatible.
+
 Complex type definitions can also use *variants* where by a union of different type constructors
 is used to define the domain of values.
 For example:

asllib/aslspec/error.ml

@@ -260,32 +260,35 @@ let type_instantiation_length_failure formal_type arg_type ~expected_length
        PP.pp_type_term formal_type PP.pp_type_term arg_type expected_length
        actual_length
 
-let type_operator_instantiation_failure ~relation_name formal_type arg_type =
+let type_operator_instantiation_failure ~owner formal_type arg_type =
   spec_error_loc_of_term arg_type
   @@ Format.asprintf
-       "The type term `%a` cannot be instantiated with `%a` for operator `%s` \
-        since there are incompatible argument types for it"
-       PP.pp_type_term formal_type PP.pp_type_term arg_type relation_name
+       "The type term `%a` cannot be instantiated with `%a` for %s since there \
+        are incompatible argument types for it"
+       PP.pp_type_term formal_type PP.pp_type_term arg_type owner
 
-let param_type_instantiation_failure ~relation_name formal_type arg_type =
+let param_type_instantiation_failure ~owner formal_type arg_type =
   spec_error_loc_of_term arg_type
   @@ Format.asprintf
-       "The type term `%a` cannot be instantiated with `%a` in relation `%s` \
-        since the parameterized types do not match"
-       PP.pp_type_term formal_type PP.pp_type_term arg_type relation_name
+       "The type term `%a` cannot be instantiated with `%a` for %s since the \
+        parameterized types do not match"
+       PP.pp_type_term formal_type PP.pp_type_term arg_type owner
 
-let uninstantiated_parameter_in_relation param relation_name ~context_expr =
-  spec_error_loc_of_expr context_expr
-  @@ Format.asprintf
-       "The type parameter %s of relation %s could not be instantiated in %a"
-       param relation_name PP.pp_expr context_expr
+let uninstantiated_parameter loc param ~owner =
+  spec_error loc
+  @@ Format.asprintf "The type parameter %s of %s could not be instantiated"
+       param owner
 
-let parameter_type_unification_failure loc ~relation_name parameter_name term1
-    term2 =
+let parameter_type_unification_failure loc ~owner parameter_name term1 term2 =
   spec_error loc
-  @@ Format.asprintf
-       "Could not unify types %a and %a for parameter %s of relation %s"
-       PP.pp_type_term term1 PP.pp_type_term term2 parameter_name relation_name
+  @@ Format.asprintf "Could not unify types %a and %a for parameter %s of %s"
+       PP.pp_type_term term1 PP.pp_type_term term2 parameter_name owner
+
+(** Raises a specification error because [owner] declares [parameter] more than
+    once. *)
+let duplicate_type_parameter loc ~owner parameter =
+  spec_error loc
+  @@ Format.asprintf "Duplicate type parameter %s in %s" parameter owner
 
 let only_single_output_relations_supported name ~context_expr =
   spec_error_loc_of_expr context_expr