Merge pull request #1083 from lorchrob/abstract-type-cleanup

Disallow quantification over variables with types containing abstract types

doc/usr/source/2_input/7_abstract_types.rst

@@ -0,0 +1,34 @@
+Abstract Types
+==============
+
+Kind 2 supports Lustre's **abstract types**, 
+which are user-declared types without definitions.
+Abstract types are declared with the syntax ``type <name>``.
+Below is a simple Lustre file that declares an identity 
+node that takes an input of (abstract) type ``T`` 
+and returns an output of type ``T`` equal to the input.
+
+.. code-block::
+
+    type T;
+    function id_T (x: T) returns (y: T);
+    let
+        y = x;
+    tel
+
+In Kind 2, all abstract types have infinite domains. 
+Therefore, to maintain soundness, quantification over variables with abstract
+types is not allowed. For example, the following code block 
+is rejected by Kind 2, since the contract assumption would constrain 
+type ``T`` to have a finite domain.
+
+.. code-block::
+
+    type T;
+    function id_T (x: T) returns (y: T);
+    (*@contract
+    assume forall (x:T) (forall (y: T) x = y);
+    *)
+    let
+        y = x;
+    tel

doc/usr/source/index.rst

@@ -27,6 +27,7 @@ Table of Contents
     2_input/4_refinement_types
     2_input/5_enums
     2_input/6_history_type
+    2_input/7_abstract_types
     3_output/2_machine_readable
     3_output/3_exit_codes
 

src/lustre/lustreTypeChecker.ml

@@ -98,6 +98,7 @@ type error_kind = Unknown of string
   | IntervalMustHaveBound
   | ExpectedRecordType of tc_type
   | GlobalConstRefType of HString.t
+  | QuantifiedAbstractType of HString.t
   | InvalidPolymorphicCall of HString.t
 
 type error = [
@@ -193,6 +194,7 @@ let error_message kind = match kind with
   | IntervalMustHaveBound -> "Range should have at least one bound"
   | ExpectedRecordType ty -> "Expected record type but found " ^ string_of_tc_type ty
   | GlobalConstRefType id -> "Global constant '" ^ HString.string_of_hstring id ^ "' has refinement type (not yet supported)"
+  | QuantifiedAbstractType id -> "Variable '" ^ HString.string_of_hstring id ^ "' with type that contains an abstract type (or type variable) cannot be quantified"
   | InvalidPolymorphicCall id -> "Call to node or contract '" ^ HString.string_of_hstring id ^ "' passes an incorrect number of type parameters"
 
 type warning_kind = 
@@ -1070,6 +1072,14 @@ and check_type_expr: tc_context -> HString.t option -> LA.expr -> tc_type -> ([>
 
   (* Quantified expressions *)
   | Quantifier (_, _, qs, e) ->
+    (* Disallow quantification over abstract types *)
+    let* _ = R.seq_ (List.map (fun (pos, id, ty) -> 
+      if type_contains_abstract ctx ty 
+      then 
+        type_error pos (QuantifiedAbstractType id) 
+      else 
+        R.ok ()
+    ) qs) in
     let extn_ctx = List.fold_left union ctx
                     (List.map (fun (_, i, ty) -> singleton_ty i ty) qs) in
     check_type_expr extn_ctx nname e exp_ty

src/lustre/lustreTypeChecker.mli

@@ -83,6 +83,7 @@ type error_kind = Unknown of string
   | IntervalMustHaveBound
   | ExpectedRecordType of tc_type
   | GlobalConstRefType of HString.t
+  | QuantifiedAbstractType of HString.t
   | InvalidPolymorphicCall of HString.t
 
 type error = [

src/lustre/typeCheckerContext.ml

@@ -686,6 +686,26 @@ let rec type_contains_enum_subrange_reftype ctx = function
       | _ -> assert false)
   | _ -> false
 
+let rec type_contains_abstract ctx = function
+  | LA.UserType (_, id) -> 
+    (match lookup_ty_syn ctx id with 
+    | Some (AbstractType _) 
+    | None -> true 
+    | Some ty -> type_contains_abstract ctx ty)
+  | RefinementType (_, (_, _, ty), _) -> type_contains_abstract ctx ty
+  | TupleType (_, tys) | GroupType (_, tys) ->
+    List.fold_left (fun acc ty -> acc || type_contains_abstract ctx ty) false tys
+  | RecordType (_, _, tys) ->
+    List.fold_left (fun acc (_, _, ty) -> acc || type_contains_abstract ctx ty)
+      false tys
+  | ArrayType (_, (ty, _)) -> type_contains_abstract ctx ty
+  | TArr (_, ty1, ty2) -> type_contains_abstract ctx ty1 || type_contains_abstract ctx ty2
+  | History (_, id) -> 
+    (match lookup_ty ctx id with 
+    | Some ty -> type_contains_abstract ctx ty
+    | _ -> assert false)
+  | _ -> false
+
 let rec ty_vars_of_expr ctx node_name expr = 
   let call = ty_vars_of_expr ctx node_name in match expr with 
   (* Node calls *)

src/lustre/typeCheckerContext.mli

@@ -275,6 +275,9 @@ val type_contains_ref : tc_context -> LA.lustre_type -> bool
 val type_contains_enum_subrange_reftype : tc_context -> LA.lustre_type -> bool
 (** Returns true if the lustre type expression contains an EnumType/IntRange or if it is an EnumType/IntRange *)
 
+val type_contains_abstract : tc_context -> tc_type -> bool
+(** Returns true if the lustre type expression contains an abstract type (including polymorphic type variable) or if it is an abstract type *)
+
 val ty_vars_of_expr: tc_context -> LA.index -> LA.expr -> SI.t
 (** [ty_vars_of_type ctx node_name e] returns all type variable identifiers that appear in the expression [e] *)