Merge pull request #1115 from daniel-larraz/call-with-qvar-arg

Add support for function calls with arguments containing quantified vars

src/lustre/generatedIdentifiers.ml

@@ -39,6 +39,7 @@ type t = {
   locals : 
   (LustreAst.lustre_type)
     StringMap.t;
+  asserts : (Lib.position * LustreAst.expr) list;
   contract_calls :
     (Lib.position
     * (Lib.position * HString.t) list (* contract scope *)
@@ -52,7 +53,8 @@ type t = {
     * LustreAst.expr (* restart expression *)
     * HString.t (* node name *)
     * (LustreAst.expr list) (* node arguments *)
-    * (LustreAst.expr list option)) (* node argument defaults *)
+    * (LustreAst.expr list option) (* node argument defaults *)
+    * bool) (* Was call inlined? *)
     list;
   subrange_constraints : (source
     * (Lib.position * HString.t) list (* contract scope  *)
@@ -104,6 +106,7 @@ let union_keys key id1 id2 = match key, id1, id2 with
 
 let union ids1 ids2 = {
     locals = StringMap.merge union_keys ids1.locals ids2.locals;
+    asserts = ids1.asserts @ ids2.asserts;
     array_constructors = StringMap.merge union_keys
       ids1.array_constructors ids2.array_constructors;
     node_args = ids1.node_args @ ids2.node_args;
@@ -130,6 +133,7 @@ let union_keys2 key id1 id2 = match key, id1, id2 with
 
 let empty () = {
   locals = StringMap.empty;
+  asserts = [];
   array_constructors = StringMap.empty;
   node_args = [];
   oracles = [];

src/lustre/generatedIdentifiers.mli

@@ -39,6 +39,7 @@ type t = {
   locals : 
   (LustreAst.lustre_type)
     StringMap.t;
+  asserts : (Lib.position * LustreAst.expr) list;
   contract_calls :
     (Lib.position
     * (Lib.position * HString.t) list (* contract scope *)
@@ -52,7 +53,8 @@ type t = {
     * LustreAst.expr (* restart expression *)
     * HString.t (* node name *)
     * (LustreAst.expr list) (* node arguments *)
-    * (LustreAst.expr list option)) (* node argument defaults *)
+    * (LustreAst.expr list option) (* node argument defaults *)
+    * bool) (* Was call inlined? *)
     list;
   subrange_constraints : (source
     * (Lib.position * HString.t) list (* contract scope  *)

src/lustre/lustreAstHelpers.mli

@@ -55,6 +55,11 @@ val substitute_naive : HString.t -> expr -> expr -> expr
 (** Substitute second param for first param in third param. 
     AnyOp and Quantifier are not supported due to introduction of bound variables. *)
 
+val apply_subst_in_expr : (HString.t * expr) list -> expr -> expr
+(** [apply_subst_in_expr s e] applies the substitution defined by association list [s]
+    to the expression [e]
+    AnyOp and Quantifier are not supported due to introduction of bound variables. *)
+
 val apply_subst_in_type : (HString.t * expr) list -> lustre_type -> lustre_type
 (** [apply_subst_in_type s t] applies the substitution defined by association list [s]
     to the expressions of (possibly dependent) type [t]
@@ -187,4 +192,4 @@ val rename_contract_vars : expr -> expr
 val name_of_prop : Lib.position -> HString.t option -> LustreAst.prop_kind -> HString.t
 (** Get the name associated with a property *)
 
-val get_const_num_value : expr -> int option
+val get_const_num_value : expr -> int option