From f97a886970bef9e1d6e8a1e217732d6ef8be087e Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 1 Jul 2014 15:42:57 +0200 Subject: Adapt for real type with Apron ; not very efficient ATM. --- frontend/ast.ml | 1 + frontend/ast_printer.ml | 3 +++ frontend/ast_util.ml | 5 +++-- frontend/parser.mly | 4 ++++ frontend/typing.ml | 10 ++++++++-- 5 files changed, 19 insertions(+), 4 deletions(-) (limited to 'frontend') 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 -- cgit v1.2.3