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

5 files changed, 19 insertions, 4 deletions

diff --git a/frontend/ast.ml b/frontend/ast.ml
index ae11064..d55626d 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -46,6 +46,7 @@ type expr =
     | AST_real_const  of string ext
     | AST_unary       of unary_op * (expr ext)
     | AST_binary      of binary_op * (expr ext) * (expr ext)
+    | AST_cast        of (expr ext) * typ
     (* on boolean values *)
     | AST_bool_const  of bool
     | AST_binary_rel  of binary_rel_op * (expr ext) * (expr ext)
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 9a4d62d..3ca2ff6 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -103,6 +103,9 @@ let rec print_expr fmt e =
       if expr_precedence e1 <= expr_precedence e
       then Format.fprintf fmt "(%a)" print_expr e1
       else Format.fprintf fmt "%a" print_expr e1
+  | AST_cast ((e1,_), ty) ->
+      Format.fprintf fmt "%s (%a)"
+          (string_of_typ ty) print_expr e1;
 
   | AST_binary (op,(e1,_),(e2,_)) ->
       if expr_precedence e1 < expr_precedence e
diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml
index d229f2f..d687d95 100644
--- a/frontend/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -43,7 +43,8 @@ let extract_const_decls =
 let rec extract_instances p e = match fst e with
   | AST_idconst _ | AST_identifier _
   | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> extract_instances p e'
+  | AST_unary (_, e') | AST_pre (e', _)
+  | AST_not e' | AST_cast(e', _) -> extract_instances p e'
   | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
   | AST_arrow(e1, e2) ->
     extract_instances p e1 @ extract_instances p e2
@@ -62,7 +63,7 @@ let rec extract_instances p e = match fst e with
 let rec extract_pre e = match fst e with
   | AST_identifier _ | AST_idconst _
   | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_not e' -> extract_pre e'
+  | AST_unary (_, e') | AST_not e' | AST_cast(e', _) -> extract_pre e'
   | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
   | AST_arrow(e1, e2) ->
     extract_pre e1 @ extract_pre e2
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 4301a05..4e010ec 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -61,6 +61,10 @@ primary_expr:
 | FALSE                     { AST_bool_const false }
 | e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN 
                             { AST_instance (e, l, fst e ^ uid ()) }
+| INT LPAREN e=ext(expr) RPAREN
+                            { AST_cast(e, AST_TINT) }
+| REAL LPAREN e=ext(expr) RPAREN
+                            { AST_cast(e, AST_TREAL) }
 
 unary_expr:
 | e=primary_expr                   { e }
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 9fe2c8f..46458f2 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -71,6 +71,12 @@ let rec type_expr_vl p vl cvl node expr =
         | [TInt], [TReal] | [TReal], [TInt] -> [TReal]
         | _ -> err "Invalid argument for binary."
         end
+    | AST_cast(e, ty) ->
+      begin match sub e, ty with
+      | [x], AST_TINT -> [TInt]
+      | [y], AST_TREAL -> [TReal]
+      | _ -> err "Invalid arity for cast."
+      end
     (* On boolean values *)
     | AST_bool_const _ -> [bool_type]
     | AST_binary_rel _ -> [bool_type] (* do not check subtypes... TODO? *)
@@ -94,8 +100,8 @@ let rec type_expr_vl p vl cvl node expr =
     | AST_tuple x -> List.flatten (List.map sub x)
 
 
-(* type_expr : tp -> string -> expr -> typ list *)
-let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars
+(* type_expr : rp -> string -> expr -> typ list *)
+let type_expr rp = type_expr_vl rp.p rp.all_vars rp.const_vars
 
 let type_var tp node id =
     let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) tp.all_vars in t