From 99e3cfccdebb3088de36107546c6175ddf44356e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 16 Jun 2010 17:03:45 +0200 Subject: [PATCH] Ported scoping --- global/signature.ml | 3 + global/types.ml | 4 +- heptagon/heptagon.ml | 18 ++-- heptagon/parsing/parser.mly | 5 +- heptagon/parsing/parsetree.ml | 4 +- heptagon/parsing/scoping.ml | 153 +++++++++++++++++----------------- utilities/misc.mli | 7 -- 7 files changed, 93 insertions(+), 101 deletions(-) diff --git a/global/signature.ml b/global/signature.ml index fa8b7af..22a1a5a 100644 --- a/global/signature.ml +++ b/global/signature.ml @@ -39,3 +39,6 @@ let types_of_arg_list l = List.map (fun ad -> ad.a_type) l let mk_arg name ty = { a_type = ty; a_name = name } +let mk_param name = + { p_name = name } + diff --git a/global/types.ml b/global/types.ml index 4489d1c..952d294 100644 --- a/global/types.ml +++ b/global/types.ml @@ -12,6 +12,6 @@ open Names type ty = | Tprod of ty list | Tid of longname | Tarray of ty * size_exp +let invalid_type = Tprod [] - -let const_array_of ty n = Tarray (ty, SConst n) \ No newline at end of file +let const_array_of ty n = Tarray (ty, SConst n) diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml index 8fae310..f1892b2 100644 --- a/heptagon/heptagon.ml +++ b/heptagon/heptagon.ml @@ -13,7 +13,7 @@ open Names open Ident open Static open Signature - +open Types type iterator_type = | Imap @@ -163,9 +163,10 @@ let mk_type_dec name desc = let mk_equation desc = { eq_desc = desc; eq_statefull = true; eq_loc = no_location; } -let cfalse = Cconstr pfalse +(* +let cfalse = Cconstr Initial.pfalse -let ctrue = Cconstr ptrue +let ctrue = Cconstr Initial.ptrue let make_bool desc = emake desc tybool @@ -180,9 +181,9 @@ let bool_param n = v_linearity = NotLinear; } -let dfalse = make_bool (Econst (Cconstr pfalse)) +let dfalse = make_bool (Econst (Cconstr Initial.pfalse)) -let dtrue = make_bool (Econst (Cconstr ptrue)) +let dtrue = make_bool (Econst (Cconstr Initial.ptrue)) let var n ty = emake (Evar n) ty @@ -224,19 +225,18 @@ let eq pat e = eqmake (Eeq (pat, e)) let reset eq_list e = eqmake (Ereset (eq_list, e)) let switch e l = eqmake (Eswitch (e, l)) - -let varpat n = Evarpat n + *) let op_from_app app = match app.a_op with - | Eop (n, _) -> op_from_app_name n + | Ecall ((op, _, Eop), _) -> op_from_app_name op | _ -> raise Not_static let rec size_exp_of_exp e = match e.e_desc with | Econstvar n -> SVar n | Econst (Cint i) -> SConst i - | Eapp (app, ([ e1; e2 ])) -> + | Eapp (app, [ e1; e2 ]) -> let op = op_from_app app in SOp (op, size_exp_of_exp e1, size_exp_of_exp e2) | _ -> raise Not_static diff --git a/heptagon/parsing/parser.mly b/heptagon/parsing/parser.mly index 0fe28ff..69fa7e5 100644 --- a/heptagon/parsing/parser.mly +++ b/heptagon/parsing/parser.mly @@ -562,8 +562,9 @@ interface_decl: | OPEN Constructor { mk_interface_decl (Iopen $2) } | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN - { mk_interface_decl (Isignature({ sig_name = $4; sig_inputs = $6; sig_outputs = $10; - sig_node = $3; sig_params = $4; })) } + { mk_interface_decl (Isignature({ sig_name = $4; sig_inputs = $6; + sig_outputs = $10; + sig_params = $4; })) } ; params_signature: diff --git a/heptagon/parsing/parsetree.ml b/heptagon/parsing/parsetree.ml index 959e5ca..8ba4dd4 100644 --- a/heptagon/parsing/parsetree.ml +++ b/heptagon/parsing/parsetree.ml @@ -116,7 +116,7 @@ type type_dec = and type_desc = | Type_abs | Type_enum of name list - | Type_struct of structure + | Type_struct of (name * ty) list type contract = { c_assume : exp; @@ -154,8 +154,6 @@ type signature = { sig_name : name; sig_inputs : arg list; sig_outputs : arg list; - sig_node : bool; - sig_safe : bool; sig_params : name list; } type interface = interface_decl list diff --git a/heptagon/parsing/scoping.ml b/heptagon/parsing/scoping.ml index 9309e10..e9f6572 100644 --- a/heptagon/parsing/scoping.ml +++ b/heptagon/parsing/scoping.ml @@ -94,10 +94,14 @@ let build_id_list loc env l = List.fold_left build_id env l (* Translate the AST into Heptagon. *) -let translate_inlining_policy = function - | Ino -> Heptagon.Ino - | Ione -> Heptagon.Ione - | Irec -> Heptagon.Irec +let translate_iterator_type = function + | Imap -> Heptagon.Imap + | Ifold -> Heptagon.Ifold + | Imapfold -> Heptagon.Imapfold + +let translate_op_kind = function + | Eop -> Heptagon.Eop + | Enode -> Heptagon.Enode let translate_const = function | Cint i -> Heptagon.Cint i @@ -106,7 +110,7 @@ let translate_const = function let op_from_app loc app = match app.a_op with - | Eop (op,_) -> op_from_app_name op + | Ecall (op, _, Eop) -> op_from_app_name op | _ -> Error.message loc Error.Estatic_exp_expected let check_const_vars = ref true @@ -114,27 +118,25 @@ let rec translate_size_exp const_env e = match e.e_desc with | Evar n -> if !check_const_vars & not (NamesEnv.mem n const_env) then - Error.message e.e_loc (Error.Econst_var n) + Error.message e.e_loc (Error.Econst_var n) else - SVar n + SVar n | Econst (Cint i) -> SConst i | Eapp(app, [e1;e2]) -> let op = op_from_app e.e_loc app in - SOp(op, translate_size_exp const_env e1, translate_size_exp const_env e2) + SOp(op, translate_size_exp const_env e1, translate_size_exp const_env e2) | _ -> Error.message e.e_loc Error.Estatic_exp_expected let rec translate_type const_env = function - | Tprod ty_list -> - Heptagon.Tprod(List.map (translate_type const_env) ty_list) - | Tid ln -> Heptagon.Tbase (Heptagon.Tid ln) + | Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list) + | Tid ln -> Types.Tid ln | Tarray (ty, e) -> - let ty = Heptagon.type (translate_type const_env ty) in - Heptagon.Tbase (Heptagon.Tarray (ty, translate_size_exp const_env e)) + let ty = translate_type const_env ty in + Types.Tarray (ty, translate_size_exp const_env e) and translate_exp const_env env e = { Heptagon.e_desc = translate_desc e.e_loc const_env env e.e_desc; - Heptagon.e_ty = Heptagon.Tprod []; - Heptagon.e_linearity = Linearity.NotLinear; + Heptagon.e_ty = Types.invalid_type; Heptagon.e_loc = e.e_loc } and translate_app const_env env app = @@ -144,50 +146,51 @@ and translate_app const_env env app = | Efby -> Heptagon.Efby | Earrow -> Heptagon.Earrow | Eifthenelse -> Heptagon.Eifthenelse - | Erepeat -> Heptagon.Erepeat - | Eselect_slice -> Heptagon.Eselect_slice - | Econcat -> Heptagon.Econcat - | Ecopy -> Heptagon.Ecopy - | Eselect_dyn -> Heptagon.Eselect_dyn - | Enode (ln, params) -> Heptagon.Enode (ln, List.map (translate_size_exp const_env) params) - | Eevery (ln, params) -> Heptagon.Eevery (ln, List.map (translate_size_exp const_env) params) - | Eop (ln, params) -> Heptagon.Eop (ln, List.map (translate_size_exp const_env) params) - | Eselect e_list -> Heptagon.Eselect (List.map (translate_size_exp const_env) e_list) - | Eupdate e_list -> Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list) - | Eiterator (it, ln, params) -> - Heptagon.Eiterator (it, ln, List.map (translate_size_exp const_env) params, None) + | Ecall (ln, params, k) -> + let params = List.map (translate_size_exp const_env) params in + Heptagon.Ecall ((ln, params, translate_op_kind k), None) | Efield_update f -> Heptagon.Efield_update f - | Emake f -> Heptagon.Emake f - | Eflatten f -> Heptagon.Eflatten f + | Earray_op op -> Heptagon.Earray_op (translate_array_op const_env env op) in - { Heptagon.a_op = op; - Heptagon.a_inlined = translate_inlining_policy app.a_inlined } + { Heptagon.a_op = op; } +and translate_array_op const_env env = function + | Eselect e_list -> Heptagon.Eselect (List.map (translate_size_exp const_env) e_list) + | Eupdate e_list -> Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list) + | Erepeat -> Heptagon.Erepeat + | Eselect_slice -> Heptagon.Eselect_slice + | Econcat -> Heptagon.Econcat + | Eselect_dyn -> Heptagon.Eselect_dyn + | Eiterator (it, (ln, params, k)) -> + let params = List.map (translate_size_exp const_env) params in + Heptagon.Eiterator (translate_iterator_type it, + (ln, params, translate_op_kind k), None) + and translate_desc loc const_env env = function | Econst c -> Heptagon.Econst (translate_const c) | Evar x -> if Rename.mem x env then - Heptagon.Evar (Rename.name loc env x) + Heptagon.Evar (Rename.name loc env x) else if NamesEnv.mem x const_env then (* var not defined, maybe a const var*) - Heptagon.Econstvar x + Heptagon.Econstvar x else - Error.message loc (Error.Evar x) + Error.message loc (Error.Evar x) | Elast x -> Heptagon.Elast (Rename.name loc env x) | Etuple e_list -> Heptagon.Etuple (List.map (translate_exp const_env env) e_list) - | Eapp ({ a_op = Erepeat} as app, e_list) -> + | Eapp ({ a_op = (Earray_op Erepeat)} as app, e_list) -> let e_list = List.map (translate_exp const_env env) e_list in - (match e_list with - | [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] -> - Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c)) - | _ -> Heptagon.Eapp (translate_app const_env env app, e_list) - ) + (match e_list with + | [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] -> + Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c)) + | _ -> Heptagon.Eapp (translate_app const_env env app, e_list) + ) | Eapp (app, e_list) -> let e_list = List.map (translate_exp const_env env) e_list in - Heptagon.Eapp (translate_app const_env env app, e_list) + Heptagon.Eapp (translate_app const_env env app, e_list) | Efield (e, field) -> Heptagon.Efield (translate_exp const_env env e, field) | Estruct f_e_list -> let f_e_list = List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in - Heptagon.Estruct f_e_list + Heptagon.Estruct f_e_list | Earray e_list -> Heptagon.Earray (List.map (translate_exp const_env env) e_list) and translate_pat loc env = function @@ -201,33 +204,35 @@ let rec translate_eq const_env env eq = and translate_eq_desc loc const_env env = function | Eswitch(e, switch_handlers) -> - Heptagon.Eswitch (translate_exp const_env env e, - List.map (translate_switch_handler loc const_env env) switch_handlers) + let sh = List.map + (translate_switch_handler loc const_env env) + switch_handlers in + Heptagon.Eswitch (translate_exp const_env env e, sh) | Eeq(p, e) -> - Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e) + Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e) | Epresent (present_handlers, b) -> - Heptagon.Epresent (List.map (translate_present_handler const_env env) present_handlers, - translate_block const_env env b) + Heptagon.Epresent (List.map (translate_present_handler const_env env) + present_handlers, + fst (translate_block const_env env b)) | Eautomaton state_handlers -> - Heptagon.Eautomaton (List.map (translate_state_handler const_env env) state_handlers) + Heptagon.Eautomaton (List.map (translate_state_handler const_env env) + state_handlers) | Ereset (eq_list, e) -> - Heptagon.Ereset (List.map (translate_eq const_env env) eq_list, - translate_exp const_env env e) + Heptagon.Ereset (List.map (translate_eq const_env env) eq_list, + translate_exp const_env env e) and translate_block const_env env b = let env = build_vd_list env b.b_local in - { Heptagon.b_local = translate_vd_list const_env env b.b_local; Heptagon.b_equs = List.map (translate_eq const_env env) b.b_equs; Heptagon.b_defnames = Env.empty ; Heptagon.b_statefull = false; - Heptagon.b_loc = b.b_loc } + Heptagon.b_loc = b.b_loc }, env and translate_state_handler const_env env sh = - let b = translate_block const_env env sh.s_block in - let env = build_vd_list env sh.s_block.b_local in + let b, env = translate_block const_env env sh.s_block in { Heptagon.s_state = sh.s_state; - Heptagon.s_block = b; + Heptagon.s_block = b; Heptagon.s_until = List.map (translate_escape const_env env) sh.s_until; Heptagon.s_unless = List.map (translate_escape const_env env) sh.s_unless; } @@ -238,16 +243,15 @@ and translate_escape const_env env esc = and translate_present_handler const_env env ph = { Heptagon.p_cond = translate_exp const_env env ph.p_cond; - Heptagon.p_block = translate_block const_env env ph.p_block } + Heptagon.p_block = fst (translate_block const_env env ph.p_block) } and translate_switch_handler loc const_env env sh = { Heptagon.w_name = sh.w_name; - Heptagon.w_block = translate_block const_env env sh.w_block } + Heptagon.w_block = fst (translate_block const_env env sh.w_block) } and translate_var_dec const_env env vd = { Heptagon.v_name = Rename.name vd.v_loc env vd.v_name; - Heptagon.v_type = Heptagon.type (translate_type const_env vd.v_type); - Heptagon.v_linearity = vd.v_linearity; + Heptagon.v_type = translate_type const_env vd.v_type; Heptagon.v_last = translate_last env vd.v_last; Heptagon.v_loc = vd.v_loc } @@ -274,10 +278,10 @@ let translate_node const_env env node = Heptagon.n_input = translate_vd_list const_env env node.n_input; Heptagon.n_output = translate_vd_list const_env env node.n_output; Heptagon.n_local = translate_vd_list const_env env node.n_local; - Heptagon.n_contract = Misc.optional (translate_contract const_env env) node.n_contract; + Heptagon.n_contract = Misc.optional + (translate_contract const_env env) node.n_contract; Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs; Heptagon.n_loc = node.n_loc; - Heptagon.n_states_graph = Interference_graph.mk_graph [] ""; Heptagon.n_params = node.n_params; Heptagon.n_params_constraints = []; } @@ -286,10 +290,10 @@ let translate_typedec const_env ty = | Type_abs -> Heptagon.Type_abs | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list) | Type_struct(field_ty_list) -> - let translate_field_type (f,ty) = - f, Heptagon.type (translate_type const_env ty) - in - Heptagon.Type_struct (List.map translate_field_type field_ty_list) + let translate_field_type (f,ty) = + f, translate_type const_env ty + in + Heptagon.Type_struct (List.map translate_field_type field_ty_list) in { Heptagon.t_name = ty.t_name; Heptagon.t_desc = onetype ty.t_desc; @@ -297,7 +301,7 @@ let translate_typedec const_env ty = let translate_const_dec const_env cd = { Heptagon.c_name = cd.c_name; - Heptagon.c_type = Heptagon.type (translate_type const_env cd.c_type); + Heptagon.c_type = translate_type const_env cd.c_type; Heptagon.c_value = translate_size_exp const_env cd.c_value; Heptagon.c_loc = cd.c_loc; } @@ -309,23 +313,16 @@ let translate_program p = Heptagon.p_nodes = List.map (translate_node const_env Rename.empty) p.p_nodes; Heptagon.p_consts = List.map (translate_const_dec const_env) p.p_consts; } -let translate_signature const_env s = - let translate_field_type (f,(ty,lin)) = - f, Heptagon.type (translate_type const_env ty), lin - in - - let const_env = build_id_list no_location const_env s.sig_params in +let translate_signature s = { Heptagon.sig_name = s.sig_name; - Heptagon.sig_inputs = List.map translate_field_type s.sig_inputs; - Heptagon.sig_outputs = List.map translate_field_type s.sig_outputs; - Heptagon.sig_node = s.sig_node; - Heptagon.sig_safe = s.sig_safe; - Heptagon.sig_params = s.sig_params; } + Heptagon.sig_inputs = s.sig_inputs; + Heptagon.sig_outputs = s.sig_outputs; + Heptagon.sig_params = List.map Signature.mk_param s.sig_params; } let translate_interface_desc const_env = function | Iopen n -> Heptagon.Iopen n | Itypedef tydec -> Heptagon.Itypedef (translate_typedec const_env tydec) - | Isignature s -> Heptagon.Isignature (translate_signature const_env s) + | Isignature s -> Heptagon.Isignature (translate_signature s) let translate_interface_decl const_env idecl = { Heptagon.interf_desc = translate_interface_desc const_env idecl.interf_desc; diff --git a/utilities/misc.mli b/utilities/misc.mli index 425c7a5..df78d23 100644 --- a/utilities/misc.mli +++ b/utilities/misc.mli @@ -118,13 +118,6 @@ exception Error val gen_symbol : unit -> string val reset_symbol : unit -> unit -type iterator_name = - Imap - | Ifold - | Imapfold - -val iterator_to_string : iterator_name -> string - (** [unique l] returns the [l] list without duplicates. O([length l]). *) val unique : 'a list -> 'a list