Adapt for real type with Apron ; not very efficient ATM.

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