Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for function calls with arguments containing quantified vars #1115

Merged
merged 1 commit into from
Dec 5, 2024
Merged

Add support for function calls with arguments containing quantified vars #1115

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/lustre/generatedIdentifiers.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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 *)
Expand Down Expand Up @@ -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;
Expand All @@ -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 = [];
Expand Down
4 changes: 3 additions & 1 deletion src/lustre/generatedIdentifiers.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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 *)
Expand Down
7 changes: 6 additions & 1 deletion src/lustre/lustreAstHelpers.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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
Loading
Loading