summaryrefslogtreecommitdiff
path: root/abstract/transform.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/transform.ml')
-rw-r--r--abstract/transform.ml76
1 files changed, 48 insertions, 28 deletions
diff --git a/abstract/transform.ml b/abstract/transform.ml
index d9b20d8..ff2374e 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -21,7 +21,7 @@ type transform_data = {
(* Numerical types / Enumerated types *)
type ne_expr =
| EE of enum_expr
- | NE of num_expr
+ | NE of num_expr * bool (* bool: true -> real, false -> int *)
(* f_of_neexpr :
transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr
@@ -34,31 +34,38 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
| AST_identifier(id, _) ->
let qid = node^"/"^id in
begin match type_var td.rp node id with
- | TInt | TReal -> where [NE (NIdent qid)]
+ | TInt -> where [NE (NIdent qid, false)]
+ | TReal -> where [NE (NIdent qid, true)]
| TEnum _ -> where [EE (EIdent qid)]
end
| AST_idconst(id, _) ->
begin let x = VarMap.find ("cst/"^id) td.consts in
- try where [NE (NIntConst (I.as_int x))]
- with _ -> try where [NE (NRealConst (I.as_real x))]
+ try where [NE (NIntConst (I.as_int x), false)]
+ with _ -> try where [NE (NRealConst (I.as_real x), true)]
with _ -> try where [EE (EItem (if I.as_bool x then bool_true else bool_false))]
with _ -> le error "Invalid data for supposedly numerical/boolean constant."
end
(* numerical *)
- | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i))]
- | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r))]
+ | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i), false)]
+ | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r), true)]
| AST_bool_const b -> where [EE(EItem (if b then bool_true else bool_false))]
| AST_unary(op, e) ->
sub (function
- | [NE x] -> where [NE(NUnary(op, x))]
+ | [NE (x, r)] -> where [NE(NUnary(op, x, r), r)]
| _ -> le invalid_arity "Unary operator") e
| AST_binary(op, a, b) ->
sub (function
- | [NE x] ->
- sub (function
- | [NE y] -> where [NE(NBinary(op, x, y))]
- | _ -> le invalid_arity "binary operator") b
- | _ -> le invalid_arity "binary operator") a
+ | [NE (x, r1); NE (y, r2)] ->
+ let r = r1 || r2 in
+ where [NE(NBinary(op, x, y, r), r)]
+ | _ -> le invalid_arity "binary operator")
+ (AST_tuple([a; b]), snd expr)
+ | AST_cast(e, ty) ->
+ let is_real = (ty = AST_TREAL) in
+ sub (function
+ | [NE (x, _)] -> where [NE(NUnary(AST_UPLUS, x, is_real), is_real)]
+ | _ -> le invalid_arity "Cast.")
+ e
(* temporal *)
| AST_pre(expr, id) ->
let id = node^"/"^id in
@@ -67,7 +74,8 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
(List.mapi
(fun i t -> let x = id^"."^(string_of_int i) in
match t with
- | TInt | TReal -> NE(NIdent x)
+ | TInt -> NE(NIdent x, false)
+ | TReal -> NE(NIdent x, true)
| TEnum _ -> EE(EIdent x))
typ)
| AST_arrow(a, b) ->
@@ -81,9 +89,9 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
else if not (td.rp.no_time_scope clock_scope)
then
f_or
- (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
+ (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false))
(sub where a))
- (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
+ (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
(sub where b))
else
f_or (sub where a) (sub where b)
@@ -98,7 +106,8 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr =
(List.map
(fun (_, id, t) -> let x = node^"/"^nid^"/"^id in
match t with
- | AST_TINT | AST_TREAL -> NE(NIdent x)
+ | AST_TINT -> NE(NIdent x, false)
+ | AST_TREAL -> NE(NIdent x, true)
| _ -> EE(EIdent x))
n.ret)
| AST_tuple l ->
@@ -135,7 +144,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
where
(f_of_neexpr td (node, prefix, clock_scope)
(function
- | [NE x; NE y] -> BRel(rel, x, y)
+ | [NE (x, r1); NE (y, r2)] -> BRel(rel, x, y, r1 || r2)
| [EE x; EE y] ->
let eop = match rel with
| AST_EQ -> E_EQ
@@ -156,9 +165,9 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr =
else if not (td.rp.no_time_scope clock_scope)
then
f_or
- (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0))
+ (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false))
(sub where a))
- (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1))
+ (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
(sub where b))
else
f_or (sub where a) (sub where b)
@@ -192,7 +201,8 @@ let gen_clock td (node, prefix, _) active =
f_and
(if not (td.rp.no_time_scope clock_scope)
then BRel(AST_EQ, NIdent("N"^clock_scope^"time"),
- NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time")))
+ NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false),
+ false)
else BConst true)
(if td.rp.init_scope clock_scope
then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false)
@@ -202,7 +212,7 @@ let gen_clock td (node, prefix, _) active =
(if not (td.rp.no_time_scope clock_scope)
then BRel(AST_EQ,
NIdent("N"^clock_scope^"time"),
- NIdent(clock_scope^"time"))
+ NIdent(clock_scope^"time"), false)
else BConst true)
(if td.rp.init_scope clock_scope
then f_e_eq (EIdent("N"^clock_scope^"init"))
@@ -216,9 +226,13 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
let instance_eq (_, id, eqs, args) =
let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in
if active then
- let arg_eq ((_,argname,_), expr) =
+ let arg_eq ((_,argname,ty), expr) =
f_of_neexpr td (node, prefix, clock_scope) (function
- | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
+ | [NE (v, r)] ->
+ let need_r = (ty = AST_TREAL) in
+ if r <> need_r then error "Invalid type for numerical argument.";
+ BRel(AST_EQ,
+ NIdent(node^"/"^id^"/"^argname), v, r)
| [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
| _ -> invalid_arity "in argument")
expr
@@ -236,7 +250,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
(List.mapi
(fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
match v with
- | NE v -> BRel(AST_EQ, NIdent x, v)
+ | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r)
| EE v -> f_e_eq (EIdent x) v)
elist))
expr
@@ -246,7 +260,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
(List.mapi
(fun i t -> let x = string_of_int i in
match t with
- | TInt | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x))
+ | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false)
+ | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true)
| TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
typ)
in
@@ -260,8 +275,13 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees =
if active then
let apply_f vs =
let rels =
- List.map2 (fun (id, _) -> function
- | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
+ List.map2 (fun (id, _) ->
+ let need_r = (type_var td.rp node id = TReal) in
+ function
+ | NE (v, r) ->
+ if r <> need_r then error "Invalid type in numerical assign";
+ BRel(AST_EQ, NIdent (node^"/"^id),
+ v, r)
| EE v -> f_e_eq (EIdent (node^"/"^id)) v)
ids vs
in
@@ -380,7 +400,7 @@ let gen_clock_init rp (node, prefix, _) =
then
BRel(AST_EQ,
NIdent(clock_scope^"time"),
- NIntConst 0)
+ NIntConst 0, false)
else BConst true)
(if rp.init_scope clock_scope
then
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:11:33 +0000