diff options
Diffstat (limited to 'abstract/transform.ml')
| -rw-r--r-- | abstract/transform.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml index b6781a8..82b6731 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -70,7 +70,7 @@ let rec f_of_neexpr td (node, prefix) where expr = | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> - if List.mem (node^"/") td.rp.init_scope + if td.rp.init_scope (node^"/") then f_or (f_and (f_e_eq (EIdent (node^"/"^prefix^"init")) (EItem bool_true)) @@ -306,21 +306,21 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = let time_incr_eq = if active then f_and - (if not (List.mem (node^"/") td.rp.no_time_scope) + (if not (td.rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) else BConst true) - (if List.mem (node^"/") td.rp.init_scope + (if td.rp.init_scope (node^"/") then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) else BConst true) else f_and - (if not (List.mem (node^"/") td.rp.no_time_scope) + (if not (td.rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NIdent(node^"/"^prefix^"time")) else BConst true) - (if List.mem (node^"/") td.rp.init_scope + (if td.rp.init_scope (node^"/") then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EIdent (node^"/"^prefix^"init")) else BConst true) @@ -373,13 +373,13 @@ let rec init_f_of_scope rp (node, prefix, eqs) = in let time_eq = f_and - (if not (List.mem (node^"/") rp.no_time_scope) + (if not (rp.no_time_scope (node^"/")) then BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0) else BConst true) - (if List.mem (node^"/") rp.init_scope + (if rp.init_scope (node^"/") then f_e_eq (EIdent(node^"/"^prefix^"init")) (EItem bool_true) else BConst true) |