diff --git a/compiler/heptagon/main/heptcheck.ml b/compiler/heptagon/main/heptcheck.ml index b3e2d5a..6ca9460 100644 --- a/compiler/heptagon/main/heptcheck.ml +++ b/compiler/heptagon/main/heptcheck.ml @@ -31,6 +31,9 @@ let check_implementation modname filename = (* Parsing of the file *) let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in + (* Fuse static exps together *) + let p = do_silent_pass "Static Scoping" + Hept_static_scoping.program p in (* Convert the parse tree to Heptagon AST *) let p = do_pass "Scoping" Hept_scoping.translate_program p pp in diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 422b87c..10789ad 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -127,6 +127,15 @@ and edesc funs acc ed = match ed with (n,e), acc in let n_e_list, acc = mapfold aux acc n_e_list in Estruct n_e_list, acc + | Emerge (x, c_e_list) -> + let aux acc (c,e) = + let e, acc = exp_it funs acc e in + (c,e), acc in + let c_e_list, acc = mapfold aux acc c_e_list in + Emerge(x, c_e_list), acc + | Ewhen (e, c, x) -> + let e, acc = exp_it funs acc e in + Ewhen (e, c, x), acc | Eapp (app, args) -> let app, acc = app_it funs acc app in let args, acc = mapfold (exp_it funs) acc args in diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index d0dbc48..a21f235 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -114,7 +114,6 @@ let qualify_const local_const c = match c with with Not_found -> error (Equal_unbound ("constant",c ))) | Q q -> if check_const q then q else raise Not_static - module Rename = struct open Error @@ -178,17 +177,18 @@ let static_app_from_app app args= q, (app.a_params @ args) | _ -> raise Not_static -let rec translate_static_exp local_const se = +let rec translate_static_exp se = try - let se_d = translate_static_exp_desc local_const se.se_desc in + let se_d = translate_static_exp_desc se.se_desc in Types.mk_static_exp ~loc:se.se_loc se_d with | ScopingError err -> message se.se_loc err -and translate_static_exp_desc local_const ed = - let t = translate_static_exp local_const in +and translate_static_exp_desc ed = + let t = translate_static_exp in match ed with - | Svar q -> Types.Svar (qualify_const local_const q) + | Svar (Q q) -> Types.Svar q + | Svar (ToQ _) -> assert false | Sint i -> Types.Sint i | Sfloat f -> Types.Sfloat f | Sbool b -> Types.Sbool b @@ -202,91 +202,58 @@ and translate_static_exp_desc local_const ed = Types.Srecord (List.map qualf se_f_list) | Sop (fn, se_list) -> Types.Sop (qualify_value fn, List.map t se_list) -let rec static_exp_of_exp local_const e = - try - let t = static_exp_of_exp local_const in - let desc = match e.e_desc with - | Evar n -> Types.Svar (qualify_const local_const (ToQ n)) - | Econst se -> translate_static_exp_desc local_const se.se_desc - | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) -> - Types.Sarray_power (t e, t n) - | Eapp({ a_op = Earray }, e_list) -> - Types.Sarray (List.map t e_list) - | Eapp({ a_op = Etuple }, e_list) -> - Types.Stuple (List.map t e_list) - | Eapp(app, e_list) -> - let op, args = static_app_from_app app e_list in - Types.Sop (op, List.map t args) - | Estruct e_list -> - Types.Srecord (List.map (fun (f,e) -> qualify_field f, t e) e_list) - | _ -> raise Not_static in - Types.mk_static_exp ~loc:e.e_loc desc - with - | ScopingError err -> message e.e_loc err +let expect_static_exp e = match e.e_desc with + | Econst se -> translate_static_exp se + | _ -> message e.e_loc Estatic_exp_expected -let expect_static_exp local_const e = - try static_exp_of_exp local_const e - with Not_static -> message e.e_loc Estatic_exp_expected - -let rec translate_type loc local_const ty = +let rec translate_type loc ty = try (match ty with | Tprod ty_list -> - Types.Tprod(List.map (translate_type loc local_const) ty_list) + Types.Tprod(List.map (translate_type loc) ty_list) | Tid ln -> Types.Tid (qualify_type ln) | Tarray (ty, e) -> - let ty = translate_type loc local_const ty in - Types.Tarray (ty, expect_static_exp local_const e)) + let ty = translate_type loc ty in + Types.Tarray (ty, expect_static_exp e)) with | ScopingError err -> message loc err - -and translate_exp local_const env e = +let rec translate_exp env e = try - let desc = - (*try (* try to see if the exp is a constant *) - Heptagon.Econst (static_exp_of_exp local_const e) - with - Not_static -> *) translate_desc e.e_loc local_const env e.e_desc in - { Heptagon.e_desc = desc; + { Heptagon.e_desc = translate_desc e.e_loc env e.e_desc; Heptagon.e_ty = Types.invalid_type; Heptagon.e_loc = e.e_loc } with ScopingError(error) -> message e.e_loc error -and translate_desc loc local_const env = function - | Econst c -> Heptagon.Econst (translate_static_exp local_const c) - | Evar x -> ( - try (* First check if it is a const var *) - Heptagon.Econst - (Types.mk_static_exp - ~loc:loc (Types.Svar (qualify_var_as_const local_const x))) - with Not_found -> Heptagon.Evar (Rename.var loc env x)) +and translate_desc loc env = function + | Econst c -> Heptagon.Econst (translate_static_exp c) + | Evar x -> Heptagon.Evar (Rename.var loc env x) | Elast x -> Heptagon.Elast (Rename.last loc env x) - | Epre (None, e) -> Heptagon.Epre (None, translate_exp local_const env e) + | Epre (None, e) -> Heptagon.Epre (None, translate_exp env e) | Epre (Some c, e) -> - Heptagon.Epre (Some (expect_static_exp local_const c), - translate_exp local_const env e) - | Efby (e1, e2) -> Heptagon.Efby (translate_exp local_const env e1, - translate_exp local_const env e2) + Heptagon.Epre (Some (expect_static_exp c), + translate_exp env e) + | Efby (e1, e2) -> Heptagon.Efby (translate_exp env e1, + translate_exp env e2) | Estruct f_e_list -> let f_e_list = - List.map (fun (f,e) -> qualify_field f, translate_exp local_const env e) + List.map (fun (f,e) -> qualify_field f, translate_exp env e) f_e_list in Heptagon.Estruct f_e_list | Eapp ({ a_op = op; a_params = params }, e_list) -> - let e_list = List.map (translate_exp local_const env) e_list in - let params = List.map (expect_static_exp local_const) params in + let e_list = List.map (translate_exp env) e_list in + let params = List.map (expect_static_exp) params in let app = Heptagon.mk_op ~params:params (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, e_list) -> - let e_list = List.map (translate_exp local_const env) e_list in - let n = expect_static_exp local_const n in - let params = List.map (expect_static_exp local_const) params in + let e_list = List.map (translate_exp env) e_list in + let n = expect_static_exp n in + let params = List.map (expect_static_exp) params in let app = Heptagon.mk_op ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, app, n, e_list, None) | Ewhen (e, c, n) -> - let e = translate_exp local_const env e in + let e = translate_exp env e in let c = qualify_constrs c in let n = Rename.var loc env n in Heptagon.Ewhen (e, c, n) @@ -294,7 +261,7 @@ and translate_desc loc local_const env = function let n = Rename.var loc env n in let c_e_list = let fun_c_e (c, e) = - let e = translate_exp local_const env e in + let e = translate_exp env e in let c = qualify_constrs c in (c, e) in List.map fun_c_e c_e_list in @@ -321,112 +288,110 @@ and translate_pat loc env = function | Evarpat x -> Heptagon.Evarpat (Rename.var loc env x) | Etuplepat l -> Heptagon.Etuplepat (List.map (translate_pat loc env) l) -let rec translate_eq local_const env eq = - { Heptagon.eq_desc = translate_eq_desc eq.eq_loc local_const env eq.eq_desc ; +let rec translate_eq env eq = + { Heptagon.eq_desc = translate_eq_desc eq.eq_loc env eq.eq_desc ; Heptagon.eq_statefull = false; Heptagon.eq_loc = eq.eq_loc } -and translate_eq_desc loc local_const env = function +and translate_eq_desc loc env = function | Eswitch(e, switch_handlers) -> let sh = List.map - (translate_switch_handler loc local_const env) + (translate_switch_handler loc env) switch_handlers in - Heptagon.Eswitch (translate_exp local_const env e, sh) + Heptagon.Eswitch (translate_exp env e, sh) | Eeq(p, e) -> - Heptagon.Eeq (translate_pat loc env p, translate_exp local_const env e) + Heptagon.Eeq (translate_pat loc env p, translate_exp env e) | Epresent (present_handlers, b) -> Heptagon.Epresent - (List.map (translate_present_handler local_const env) present_handlers - , fst (translate_block local_const env b)) + (List.map (translate_present_handler env) present_handlers + , fst (translate_block env b)) | Eautomaton state_handlers -> - Heptagon.Eautomaton (List.map (translate_state_handler local_const env) + Heptagon.Eautomaton (List.map (translate_state_handler env) state_handlers) | Ereset (b, e) -> - let b, _ = translate_block local_const env b in - Heptagon.Ereset (b, translate_exp local_const env e) + let b, _ = translate_block env b in + Heptagon.Ereset (b, translate_exp env e) -and translate_block local_const env b = +and translate_block env b = let env = Rename.append env b.b_local in - { Heptagon.b_local = translate_vd_list local_const env b.b_local; - Heptagon.b_equs = List.map (translate_eq local_const env) b.b_equs; + { Heptagon.b_local = translate_vd_list env b.b_local; + Heptagon.b_equs = List.map (translate_eq env) b.b_equs; Heptagon.b_defnames = Env.empty; Heptagon.b_statefull = false; Heptagon.b_loc = b.b_loc }, env -and translate_state_handler local_const env sh = - let b, env = translate_block local_const env sh.s_block in +and translate_state_handler env sh = + let b, env = translate_block env sh.s_block in { Heptagon.s_state = sh.s_state; Heptagon.s_block = b; - Heptagon.s_until = List.map (translate_escape local_const env) sh.s_until; + Heptagon.s_until = List.map (translate_escape env) sh.s_until; Heptagon.s_unless = - List.map (translate_escape local_const env) sh.s_unless; } + List.map (translate_escape env) sh.s_unless; } -and translate_escape local_const env esc = - { Heptagon.e_cond = translate_exp local_const env esc.e_cond; +and translate_escape env esc = + { Heptagon.e_cond = translate_exp env esc.e_cond; Heptagon.e_reset = esc.e_reset; Heptagon.e_next_state = esc.e_next_state } -and translate_present_handler local_const env ph = - { Heptagon.p_cond = translate_exp local_const env ph.p_cond; - Heptagon.p_block = fst (translate_block local_const env ph.p_block) } +and translate_present_handler env ph = + { Heptagon.p_cond = translate_exp env ph.p_cond; + Heptagon.p_block = fst (translate_block env ph.p_block) } -and translate_switch_handler loc local_const env sh = +and translate_switch_handler loc env sh = try { Heptagon.w_name = qualify_constrs sh.w_name; - Heptagon.w_block = fst (translate_block local_const env sh.w_block) } + Heptagon.w_block = fst (translate_block env sh.w_block) } with | ScopingError err -> message loc err -and translate_var_dec local_const env vd = +and translate_var_dec env vd = (* env is initialized with the declared vars before their translation *) { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name; - Heptagon.v_type = translate_type vd.v_loc local_const vd.v_type; - Heptagon.v_last = translate_last local_const vd.v_last; + Heptagon.v_type = translate_type vd.v_loc vd.v_type; + Heptagon.v_last = translate_last vd.v_last; Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *) Heptagon.v_loc = vd.v_loc } -and translate_vd_list local_const env = - List.map (translate_var_dec local_const env) +and translate_vd_list env = + List.map (translate_var_dec env) -and translate_last local_const = function +and translate_last = function | Var -> Heptagon.Var | Last (None) -> Heptagon.Last None - | Last (Some e) -> Heptagon.Last (Some (expect_static_exp local_const e)) + | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e)) -let translate_contract local_const env ct = - let b, _ = translate_block local_const env ct.c_block in - { Heptagon.c_assume = translate_exp local_const env ct.c_assume; - Heptagon.c_enforce = translate_exp local_const env ct.c_enforce; +let translate_contract env ct = + let b, _ = translate_block env ct.c_block in + { Heptagon.c_assume = translate_exp env ct.c_assume; + Heptagon.c_enforce = translate_exp env ct.c_enforce; Heptagon.c_block = b } -let params_of_var_decs local_const = +let params_of_var_decs = List.map (fun vd -> Signature.mk_param vd.v_name - (translate_type vd.v_loc local_const vd.v_type)) + (translate_type vd.v_loc vd.v_type)) -let args_of_var_decs local_const = +let args_of_var_decs = List.map (fun vd -> Signature.mk_arg (Some vd.v_name) - (translate_type vd.v_loc local_const vd.v_type)) + (translate_type vd.v_loc vd.v_type)) let translate_node node = Idents.new_function (); - (* Node's params go to local_const env *) - let local_const = build_const node.n_loc node.n_params in (* Inputs and outputs define the initial local env *) let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in - let params = params_of_var_decs local_const node.n_params in - let inputs = translate_vd_list local_const env0 node.n_input in - let outputs = translate_vd_list local_const env0 node.n_output in - let b, env = translate_block local_const env0 node.n_block in + let params = params_of_var_decs node.n_params in + let inputs = translate_vd_list env0 node.n_input in + let outputs = translate_vd_list env0 node.n_output in + let b, env = translate_block env0 node.n_block in let contract = - Misc.optional (translate_contract local_const env) node.n_contract in + Misc.optional (translate_contract env) node.n_contract in (* the env of the block is used in the contract translation *) let n = current_qual node.n_name in (* add the node signature to the environment *) - let i = args_of_var_decs local_const node.n_input in - let o = args_of_var_decs local_const node.n_output in - let p = params_of_var_decs local_const node.n_params in + let i = args_of_var_decs node.n_input in + let o = args_of_var_decs node.n_output in + let p = params_of_var_decs node.n_params in add_value n (Signature.mk_node i o node.n_statefull p); { Heptagon.n_name = n; Heptagon.n_statefull = node.n_statefull; @@ -445,7 +410,7 @@ let translate_typedec ty = add_type n Signature.Tabstract; Heptagon.Type_abs | Type_alias t -> - let t = translate_type ty.t_loc S.empty t in + let t = translate_type ty.t_loc t in add_type n (Signature.Talias t); Heptagon.Type_alias t | Type_enum(tag_list) -> @@ -456,7 +421,7 @@ let translate_typedec ty = | Type_struct(field_ty_list) -> let translate_field_type (f,t) = let f = current_qual f in - let t = translate_type ty.t_loc S.empty t in + let t = translate_type ty.t_loc t in add_field f n; Signature.mk_field f t in let field_list = List.map translate_field_type field_ty_list in @@ -469,9 +434,8 @@ let translate_typedec ty = let translate_const_dec cd = let c_name = current_qual cd.c_name in - let c_type = translate_type cd.c_loc S.empty cd.c_type in - let c_value = expect_static_exp S.empty cd.c_value in - add_const c_name (Signature.mk_const_def c_type c_value); + let c_type = translate_type cd.c_loc cd.c_type in + let c_value = expect_static_exp cd.c_value in { Heptagon.c_name = c_name; Heptagon.c_type = c_type; Heptagon.c_value = c_value; @@ -489,13 +453,12 @@ let translate_program p = Heptagon.p_consts = consts; } let translate_signature s = - let local_const = build_const s.sig_loc s.sig_params in let translate_arg a = - Signature.mk_arg a.a_name (translate_type s.sig_loc local_const a.a_type) in + Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type) in let n = current_qual s.sig_name in let i = List.map translate_arg s.sig_inputs in let o = List.map translate_arg s.sig_outputs in - let p = params_of_var_decs local_const s.sig_params in + let p = params_of_var_decs s.sig_params in add_value n (Signature.mk_node i o s.sig_statefull p); Heptagon.mk_signature n i o s.sig_statefull p s.sig_loc diff --git a/compiler/heptagon/parsing/hept_static_scoping.ml b/compiler/heptagon/parsing/hept_static_scoping.ml new file mode 100644 index 0000000..e0d1f54 --- /dev/null +++ b/compiler/heptagon/parsing/hept_static_scoping.ml @@ -0,0 +1,68 @@ +open Modules +open Hept_parsetree +open Hept_parsetree_mapfold +open Hept_scoping + +(* Convert expressions that should be static to the corresponding + static expression. After this pass, all the static expressions + (including variables) are of type Econst se. *) + +exception Not_static + +let assert_se e = match e.e_desc with + | Econst se -> se + | _ -> raise Not_static + +(** convention : static params are set as the first static args, + op (a3) == op (a2,a3) == op (a1,a2,a3) *) +let static_app_from_app app args = + match app.a_op with + | Efun ((Q { Names.qual = "Pervasives" }) as q) + | Enode ((Q { Names.qual = "Pervasives" }) as q) -> + q, (app.a_params @ args) + | _ -> raise Not_static + +let exp funs local_const e = + let e, _ = Hept_parsetree_mapfold.exp funs local_const e in + try + let sed = + match e.e_desc with + | Evar n -> + (try + Svar (Q (qualify_const local_const (ToQ n))) + with + | Error.ScopingError _ -> raise Not_static) + | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) -> + Sarray_power (assert_se e, assert_se n) + | Eapp({ a_op = Earray }, e_list) -> + Sarray (List.map assert_se e_list) + | Eapp({ a_op = Etuple }, e_list) -> + Stuple (List.map assert_se e_list) + | Eapp(app, e_list) -> + let op, e_list = static_app_from_app app e_list in + Sop (op, List.map assert_se e_list) + | Estruct e_list -> + Srecord (List.map (fun (f,e) -> f, assert_se e) e_list) + | _ -> raise Not_static + in + { e with e_desc = Econst (mk_static_exp sed e.e_loc) }, local_const + with + Not_static -> e, local_const + +let node funs _ n = + let local_const = Hept_scoping.build_const n.n_loc n.n_params in + Hept_parsetree_mapfold.node_dec funs local_const n + +let const_dec funs local_const cd = + let cd, _ = Hept_parsetree_mapfold.const_dec funs local_const cd in + let c_name = current_qual cd.c_name in + let c_type = Hept_scoping.translate_type cd.c_loc cd.c_type in + let c_value = Hept_scoping.expect_static_exp cd.c_value in + add_const c_name (Signature.mk_const_def c_type c_value); + cd, local_const + +let program p = + let funs = { Hept_parsetree_mapfold.defaults + with node_dec = node; exp = exp; const_dec = const_dec } in + let p, _ = Hept_parsetree_mapfold.program_it funs Names.S.empty p in + p diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index eecb1e0..a31cce0 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -40,6 +40,9 @@ let compile_impl modname filename = (* Parsing of the file *) let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in + (* Fuse static exps together *) + let p = do_silent_pass "Static Scoping" + Hept_static_scoping.program p in (* Convert the parse tree to Heptagon AST *) let p = do_pass "Scoping" Hept_scoping.translate_program p pp in