Add support for abstract/free types

src/inputParser.ml

@@ -218,7 +218,8 @@ let rec read_val scope name indexes arr_indexes json =
           | LustreIndex.ArrayIntIndex _ -> false
           | LustreIndex.RecordIndex _
           | LustreIndex.TupleIndex _
-          | LustreIndex.ListIndex _ -> true)
+          | LustreIndex.ListIndex _
+          | LustreIndex.AbstractTypeIndex _ -> true)
       |>
       Format.asprintf "%s%a" name (LustreIndex.pp_print_index true) 
     in

src/lustre/lustreAst.ml

@@ -160,6 +160,7 @@ and lustre_type =
   | IntRange of position * expr * expr
   | Real of position
   | UserType of position * ident
+  | AbstractType of position * ident
   | TupleType of position * lustre_type list
   | RecordType of position * typed_ident list
   | ArrayType of position * (lustre_type * expr)
@@ -664,6 +665,10 @@ and pp_print_lustre_type ppf = function
 
     Format.fprintf ppf "%a" pp_print_ident s
 
+  | AbstractType (pos, s) ->
+
+    Format.fprintf ppf "%a" pp_print_ident s
+
   | TupleType (pos, l) -> 
 
     Format.fprintf ppf 

src/lustre/lustreAst.mli

@@ -155,6 +155,7 @@ and lustre_type =
   | IntRange of position * expr * expr
   | Real of position
   | UserType of position * ident
+  | AbstractType of position * ident
   | TupleType of position * lustre_type list
   | RecordType of position * typed_ident list
   | ArrayType of position * (lustre_type * expr)

src/lustre/lustreContext.ml

@@ -635,7 +635,8 @@ let mk_state_var
            | D.ArrayIntIndex _ -> false
            | D.RecordIndex _
            | D.TupleIndex _
-           | D.ListIndex _ -> true)
+           | D.ListIndex _
+           | D.AbstractTypeIndex _ -> true)
          index)
   in
 

src/lustre/lustreDeclarations.ml

@@ -1003,7 +1003,10 @@ let rec expand_tuple' pos accum bounds lhs rhs = match lhs, rhs with
 
   (* Record index on left-hand and right-hand side *)
   | (D.RecordIndex i :: lhs_index_tl, state_var) :: lhs_tl,
-    (D.RecordIndex j :: rhs_index_tl, expr) :: rhs_tl -> 
+    (D.RecordIndex j :: rhs_index_tl, expr) :: rhs_tl
+  (* Abstract type index works like record except program cannot project field *)
+  | (D.AbstractTypeIndex i :: lhs_index_tl, state_var) :: lhs_tl,
+    (D.AbstractTypeIndex j :: rhs_index_tl, expr) :: rhs_tl -> 
 
     (* Indexes are sorted, must match *)
     if i = j then 
@@ -1024,24 +1027,35 @@ let rec expand_tuple' pos accum bounds lhs rhs = match lhs, rhs with
   | (D.RecordIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _
   | (D.RecordIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _
   | (D.RecordIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _
+  | (D.RecordIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _
 
   | (D.TupleIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _
   | (D.TupleIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _
   | (D.TupleIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _
+  | (D.TupleIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _
 
   | (D.ListIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _
   | (D.ListIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _
   | (D.ListIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _
   | (D.ListIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _
+  | (D.ListIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _
 
   | (D.ArrayIntIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _
   | (D.ArrayIntIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _
   | (D.ArrayIntIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _
   | (D.ArrayIntIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _
+  | (D.ArrayIntIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _
 
   | (D.ArrayVarIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _
   | (D.ArrayVarIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _
   | (D.ArrayVarIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _
+  | (D.ArrayVarIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _
+
+  | (D.AbstractTypeIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _
+  | (D.AbstractTypeIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _
+  | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _
+  | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _
+  | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _
 
   | (_ :: _, _) :: _, ([], _) :: _ 
   | ([], _) :: _, (_ :: _, _) :: _ ->
@@ -2589,7 +2603,15 @@ and eval_node_decl
 (** Handle declaration and return context. *)
 and declaration_to_context ctx = function
 (* Declaration of a type as alias or free *)
-| A.TypeDecl (pos, A.AliasType (_, i, type_expr)) ->
+| A.TypeDecl (pos, type_rhs) ->
+
+  let (i, type_expr) = match type_rhs with
+    (* Replace type aliases with their right-hand-side *)
+    | A.AliasType (_, i, type_expr) -> (i, type_expr)
+    (* Replace free types with an abstract type with no user-accessible
+     * representation. *)
+    | A.FreeType (_, i) -> (i, A.AbstractType (pos, i))
+  in
 
   (* Identifier of AST identifier *)
   let ident = I.mk_string_ident i in
@@ -2870,11 +2892,6 @@ and declaration_to_context ctx = function
 (* Unsupported below                                                    *)
 (* ******************************************************************** *)
 
-(* Identifier is a free type *)
-| A.TypeDecl (pos, (A.FreeType _)) ->
-
-  C.fail_at_position pos "Free types not supported"
-
 
 (* Parametric node declaration *)
 | A.NodeParamInst (pos, _)

src/lustre/lustreIndex.ml

@@ -43,6 +43,9 @@ type one_index =
   (* Array field indexed by variable *)
   | ArrayVarIndex of E.expr
 
+  (* Index to the representation field of an abstract type *)
+  | AbstractTypeIndex of string
+
 
 (* Pretty-print a single index *)
 let pp_print_one_index' db = function 
@@ -54,7 +57,8 @@ let pp_print_one_index' db = function
        | TupleIndex i -> Format.fprintf ppf "<%d>" i
        | ListIndex i -> Format.fprintf ppf "{%d}" i
        | ArrayIntIndex i -> Format.fprintf ppf "[%d]" i
-       | ArrayVarIndex v -> ()) (* Format.fprintf ppf "[X%d(%a)]" db (E.pp_print_expr false) v ) *)
+       | ArrayVarIndex v -> () (* Format.fprintf ppf "[X%d(%a)]" db (E.pp_print_expr false) v ) *)
+       | AbstractTypeIndex i -> ())
 
   | true ->
 
@@ -63,7 +67,8 @@ let pp_print_one_index' db = function
        | TupleIndex i -> Format.fprintf ppf "_%d" i
        | ListIndex i -> Format.fprintf ppf "_%d" i
        | ArrayIntIndex i -> Format.fprintf ppf "_%d" i
-       | ArrayVarIndex v ->  Format.fprintf ppf "_X%d" db)
+       | ArrayVarIndex v ->  Format.fprintf ppf "_X%d" db
+       | AbstractTypeIndex i -> Format.fprintf ppf ".%s" i)
 
 
 (* Pretty-print a list of single indexes, given the number of previously seen *)
@@ -106,7 +111,8 @@ type index = one_index list
 let compare_one_index a b = match a, b with 
 
   (* Use polymorphic comparison on strings and integers *)
-  | RecordIndex a, RecordIndex b -> Pervasives.compare a b
+  | RecordIndex a, RecordIndex b
+  | AbstractTypeIndex a, AbstractTypeIndex b -> Pervasives.compare a b
   | TupleIndex a, TupleIndex b
   | ListIndex a, ListIndex b
   | ArrayIntIndex a, ArrayIntIndex b -> Pervasives.compare a b
@@ -118,38 +124,51 @@ let compare_one_index a b = match a, b with
   | RecordIndex _, TupleIndex _
   | RecordIndex _, ListIndex _
   | RecordIndex _, ArrayIntIndex _
-  | RecordIndex _, ArrayVarIndex _ -> 1 
+  | RecordIndex _, ArrayVarIndex _
+  | RecordIndex _, AbstractTypeIndex _ -> 1 
 
   (* Tuple indexes are only smaller than record indexes *)
   | TupleIndex _, RecordIndex _ -> -1 
   | TupleIndex _, ListIndex _
   | TupleIndex _, ArrayIntIndex _
-  | TupleIndex _, ArrayVarIndex _ -> 1 
+  | TupleIndex _, ArrayVarIndex _
+  | TupleIndex _, AbstractTypeIndex _ -> 1 
 
   (* List indexes are smaller than tuple and record indexes *)
   | ListIndex _, RecordIndex _
   | ListIndex _, TupleIndex _ -> -1 
   | ListIndex _, ArrayIntIndex _
-  | ListIndex _, ArrayVarIndex _ -> 1 
+  | ListIndex _, ArrayVarIndex _
+  | ListIndex _, AbstractTypeIndex _ -> 1 
 
-  (* Intger array indexes are only greater than array variables indexes *)
+  (* Intger array indexes are greater than array variables
+   * and abstract type indexes *)
   | ArrayIntIndex _, RecordIndex _
   | ArrayIntIndex _, TupleIndex _
   | ArrayIntIndex _, ListIndex _ -> -1
-  | ArrayIntIndex _, ArrayVarIndex _ -> 1
+  | ArrayIntIndex _, ArrayVarIndex _
+  | ArrayIntIndex _, AbstractTypeIndex _ -> 1
 
-  (* Array variable indexes are smallest *)
+  (* Array variable indexes are only greater than abstract type indexes *)
   | ArrayVarIndex _, RecordIndex _
   | ArrayVarIndex _, ArrayIntIndex _
   | ArrayVarIndex _, ListIndex _
   | ArrayVarIndex _, TupleIndex _ -> -1
+  | ArrayVarIndex _, AbstractTypeIndex _ -> 1
 
+  (* Abstract type indexes are the smallest *)
+  | AbstractTypeIndex _, RecordIndex _
+  | AbstractTypeIndex _, ArrayIntIndex _
+  | AbstractTypeIndex _, ListIndex _
+  | AbstractTypeIndex _, TupleIndex _
+  | AbstractTypeIndex _, ArrayVarIndex _ -> -1
 
 (* Equality of indexes *)
 let equal_one_index a b = match a,b with 
 
   (* String indexes are equal if the strings are *)
-  | RecordIndex a, RecordIndex b -> a = b
+  | RecordIndex a, RecordIndex b
+  | AbstractTypeIndex a, AbstractTypeIndex b -> a = b
 
   (* Integer indexes are equal if the integers are *)
   | TupleIndex a, TupleIndex b 
@@ -255,6 +274,7 @@ let compatible_one_index i1 i2 = match i1, i2 with
   | ArrayIntIndex _, ArrayVarIndex _
   | ArrayVarIndex _, ArrayIntIndex _
   | ArrayVarIndex _, ArrayVarIndex _ -> true
+  | AbstractTypeIndex s1, AbstractTypeIndex s2 -> s1 = s2
   | _ -> false
 
 let compatible_indexes = List.for_all2 compatible_one_index

src/lustre/lustreIndex.mli

@@ -57,6 +57,9 @@ type one_index =
   (** Variable as index of an array of given size *)
   | ArrayVarIndex of LustreExpr.expr
 
+  (* Index to the representation field of an abstract type *)
+  | AbstractTypeIndex of string
+
 (** A sequence of indexes *)
 type index = one_index list
 

src/lustre/lustreSimplify.ml

@@ -905,9 +905,10 @@ let rec eval_ast_expr bounds ctx =
                   pos
                   "Invalid index for expression"
 
-            (* Cannot be record, list or empty index *)
+            (* Cannot be record, list, abstract type or empty index *)
             | D.RecordIndex _ :: _, _
             | D.ListIndex _ :: _, _
+            | D.AbstractTypeIndex _ :: _, _
             | [], _ ->
 
               C.fail_at_position
@@ -1210,7 +1211,8 @@ let rec eval_ast_expr bounds ctx =
       (* Projection from a tuple expression *)
         | D.TupleIndex _ :: _, _
         | D.RecordIndex _ :: _, _ 
-        | D.ListIndex _ :: _, _ ->
+        | D.ListIndex _ :: _, _
+        | D.AbstractTypeIndex _ :: _, _ ->
 
 
           (* Try again underneath *)
@@ -1625,7 +1627,8 @@ and eval_ast_projection bounds ctx pos expr = function
   (* Cannot project array field this way, need to use select
      operator *)
   | D.ListIndex _
-  | D.ArrayVarIndex _ -> raise (Invalid_argument "eval_ast_projection")
+  | D.ArrayVarIndex _
+  | D.AbstractTypeIndex _ -> raise (Invalid_argument "eval_ast_projection")
 
 
 and try_eval_node_call bounds ctx pos ident cond restart args defaults =
@@ -2118,6 +2121,14 @@ and eval_ast_type ctx = function
       Deps.Unknown_decl (Deps.Type, ident, pos) |> raise
   )
 
+  (* User-defined abstract types are represented as an integer reference
+   * to an object. This reference is wrapped inside an index for that type
+   * so it cannot be used as a raw integer.
+   * There are abstract types in Type, but using an integer reference is able
+   * to give better counterexamples. *)
+  | A.AbstractType (pos, ident) ->
+      D.singleton [D.AbstractTypeIndex ident] Type.t_int
+
   (* Record type, return trie of indexes in record *)
   | A.RecordType (pos, record_fields) -> 
 

tests/regression/error/abstract_type.lus

@@ -0,0 +1,9 @@
+(* Check type checking for abstract types*)
+type COUNTER;
+
+node test (const init : COUNTER) returns (out : int) ;
+let
+  (* Type error *)
+  out = init + 1;
+tel
+

tests/regression/falsifiable/abstract_type.lus

@@ -0,0 +1,19 @@
+(* An abstract / free type with axiomatised operations *)
+type COUNTER;
+
+(* Operation to get counter value *)
+function imported get_counter (in: COUNTER) returns (out: int) ;
+
+(* Increment a counter -- the new one is bigger than the old one *)
+function imported increment (in: COUNTER) returns (out: COUNTER) ;
+(*@contract
+  guarantee get_counter(out) = get_counter(in) + 1 ;
+*)
+
+(* Try to prove that incrementing the counter does nothing... *)
+node test (const init : COUNTER) returns (c : COUNTER) ;
+let
+  c = init -> increment(pre c);
+  --%PROPERTY true -> (get_counter(c) = get_counter(pre c));
+tel
+

tests/regression/success/abstract_type.lus

@@ -0,0 +1,29 @@
+(* An abstract / free type with axiomatised operations *)
+type COUNTER;
+
+(* Operation to get counter value *)
+function imported get_counter (in: COUNTER) returns (out: int) ;
+
+(* Increment a counter -- the new one is bigger than the old one *)
+function imported increment (in: COUNTER) returns (out: COUNTER) ;
+(*@contract
+  guarantee get_counter(out) = get_counter(in) + 1 ;
+*)
+
+(* Construct a new counter *)
+function imported zero () returns (out: COUNTER) ;
+(*@contract
+  guarantee get_counter(out) = 0 ;
+*)
+
+(* Prove that incrementing the counter works... *)
+node test (const init : COUNTER) returns (c : COUNTER) ;
+let
+  c = init -> increment(pre c);
+  --%PROPERTY true -> (get_counter(c) > get_counter(pre c));
+  --%PROPERTY get_counter(init) >= 0 => get_counter(c) >= 0;
+  (* An example of a property that fails: *)
+  (* --%PROPERTY get_counter(init) >= 0 => get_counter(c) = get_counter(init); *)
+  (* An example of a property that should not typecheck: *)
+  (* --%PROPERTY get_counter(init) >= 0 => get_counter(c) = init; *)
+tel