From e7bd251b359b04137c248af404554409938b27d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 9 Jul 2010 11:33:17 +0200 Subject: [PATCH] Added Global_mapfold and Mls_mapfold - Global_mapfold is used to iterate over types defined in Types or Signature (the iterators from Types were moved here) - Mls_mapfold to iterate over Minils AST (we do not iterate over clocks yet: is it useful ?) --- compiler/global/global_mapfold.ml | 79 +++++++++++++ compiler/global/types.ml | 53 --------- compiler/heptagon/hept_mapfold.ml | 36 +++--- compiler/minils/minils.ml | 1 + compiler/minils/mls_mapfold.ml | 181 ++++++++++++++++++++++++++++++ 5 files changed, 281 insertions(+), 69 deletions(-) create mode 100644 compiler/global/global_mapfold.ml create mode 100644 compiler/minils/mls_mapfold.ml diff --git a/compiler/global/global_mapfold.ml b/compiler/global/global_mapfold.ml new file mode 100644 index 0000000..31c9cde --- /dev/null +++ b/compiler/global/global_mapfold.ml @@ -0,0 +1,79 @@ +open Misc +open Types +open Signature + +type 'a global_it_funs = { + static_exp : 'a global_it_funs -> 'a -> static_exp -> static_exp * 'a; + static_exp_desc : + 'a global_it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a; + ty : 'a global_it_funs -> 'a -> ty -> ty * 'a; + param: 'a global_it_funs -> 'a -> param -> param * 'a; + structure: 'a global_it_funs -> 'a -> structure -> structure * 'a; + field: 'a global_it_funs -> 'a -> field -> field * 'a; +} + +let rec static_exp_it funs acc se = funs.static_exp funs acc se +and static_exp funs acc se = + let se_desc, acc = static_exp_desc_it funs acc se.se_desc in + let se_ty, acc = ty_it funs acc se.se_ty in + { se with se_desc = se_desc; se_ty = se_ty }, acc + +and static_exp_desc_it funs acc sd = + try funs.static_exp_desc funs acc sd + with Fallback -> static_exp_desc funs acc sd + +and static_exp_desc funs acc sd = match sd with + | Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> sd, acc + | Stuple se_l -> + let se_l, acc = mapfold (static_exp_it funs) acc se_l in + Stuple se_l, acc + | Sarray se_l -> + let se_l, acc = mapfold (static_exp_it funs) acc se_l in + Sarray se_l, acc + | Sop (n, se_l) -> + let se_l, acc = mapfold (static_exp_it funs) acc se_l in + Sop (n, se_l), acc + | Sarray_power (se1, se2) -> + let se1, acc = static_exp_it funs acc se1 in + let se2, acc = static_exp_it funs acc se2 in + Sarray_power(se1, se2), acc + | Srecord f_se_l -> + let aux acc (f,se) = let se,acc = static_exp_it funs acc se in + (f, se), acc in + let f_se_l, acc = mapfold aux acc f_se_l in + Srecord f_se_l, acc + +and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t +and ty funs acc t = match t with + | Tid _ -> t, acc + | Tprod t_l -> let t_l, acc = mapfold (ty_it funs) acc t_l in Tprod t_l, acc + | Tarray (t, se) -> + let t, acc = ty_it funs acc t in + let se, acc = static_exp_it funs acc se in + Tarray (t, se), acc + +and structure_it funs acc s = funs.structure funs acc s +and structure funs acc s = + mapfold (field_it funs) acc s + + +and field_it funs acc f = funs.field funs acc f +and field funs acc f = + let ty, acc = ty_it funs acc f.f_type in + { f with f_type = ty }, acc + + +and param_it funs acc p = funs.param funs acc p +and param funs acc p = + let p_type, acc = ty_it funs acc p.p_type in + { p with p_type = p_type }, acc + + +let global_funs_default = { + static_exp = static_exp; + static_exp_desc = static_exp_desc; + ty = ty; + structure = structure; + field = field; + param = param; +} diff --git a/compiler/global/types.ml b/compiler/global/types.ml index 45940d0..d24f4db 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -33,59 +33,6 @@ let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = { se_desc = desc; se_ty = ty; se_loc = loc } -(**Iterators*) - -type 'a types_it_funs = { - static_exp : 'a types_it_funs -> 'a -> static_exp -> static_exp * 'a; - static_exp_desc : - 'a types_it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a; - ty : 'a types_it_funs -> 'a -> ty -> ty * 'a } - -let rec static_exp_it funs acc se = funs.static_exp funs acc se -and static_exp funs acc se = - let se_desc, acc = static_exp_desc_it funs acc se.se_desc in - let se_ty, acc = ty_it funs acc se.se_ty in - { se with se_desc = se_desc; se_ty = se_ty }, acc - -and static_exp_desc_it funs acc sd = - try funs.static_exp_desc funs acc sd - with Fallback -> static_exp_desc funs acc sd - -and static_exp_desc funs acc sd = match sd with - | Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> sd, acc - | Stuple se_l -> - let se_l, acc = mapfold (static_exp_it funs) acc se_l in - Stuple se_l, acc - | Sarray se_l -> - let se_l, acc = mapfold (static_exp_it funs) acc se_l in - Sarray se_l, acc - | Sop (n, se_l) -> - let se_l, acc = mapfold (static_exp_it funs) acc se_l in - Sop (n, se_l), acc - | Sarray_power (se1, se2) -> - let se1, acc = static_exp_it funs acc se1 in - let se2, acc = static_exp_it funs acc se2 in - Sarray_power(se1, se2), acc - | Srecord f_se_l -> - let aux acc (f,se) = let se,acc = static_exp_it funs acc se in - (f, se), acc in - let f_se_l, acc = mapfold aux acc f_se_l in - Srecord f_se_l, acc - -and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t -and ty funs acc t = match t with - | Tid _ -> t, acc - | Tprod t_l -> let t_l, acc = mapfold (ty_it funs) acc t_l in Tprod t_l, acc - | Tarray (t, se) -> - let t, acc = ty_it funs acc t in - let se, acc = static_exp_it funs acc se in - Tarray (t, se), acc - -let types_funs_default = { - static_exp = static_exp; - static_exp_desc = static_exp_desc; - ty = ty } - open Pp_tools open Format diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index c89d33c..ac72a47 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -15,10 +15,9 @@ open Misc -open Types +open Global_mapfold open Heptagon - type 'a hept_it_funs = { app: 'a hept_it_funs -> 'a -> Heptagon.app -> Heptagon.app * 'a; block: 'a hept_it_funs -> 'a -> Heptagon.block -> Heptagon.block * 'a; @@ -50,7 +49,7 @@ type 'a hept_it_funs = { 'a hept_it_funs -> 'a -> Heptagon.const_dec -> Heptagon.const_dec * 'a; program: 'a hept_it_funs -> 'a -> Heptagon.program -> Heptagon.program * 'a; - ty_funs: 'a Types.types_it_funs } + global_funs: 'a Global_mapfold.global_it_funs } let rec exp_it funs acc e = funs.exp funs acc e @@ -64,17 +63,13 @@ and edesc_it funs acc ed = with Fallback -> edesc funs acc ed and edesc funs acc ed = match ed with | Econst se -> - let se, acc = static_exp_it funs.ty_funs acc se in + let se, acc = static_exp_it funs.global_funs acc se in Econst se, acc | Evar _ | Elast _ -> ed, acc | Epre (se, e) -> - let se, acc = optional_wacc (static_exp_it funs.ty_funs) acc se in + let se, acc = optional_wacc (static_exp_it funs.global_funs) acc se in let e, acc = exp_it funs acc e in Epre (se, e), acc - | Epre (Some se, e) -> - let se, acc = static_exp_it funs.ty_funs acc se in - let e, acc = exp_it funs acc e in - Epre (Some se, e), acc | Efby (e1, e2) -> let e1, acc = exp_it funs acc e1 in let e2, acc = exp_it funs acc e2 in @@ -95,7 +90,7 @@ and edesc funs acc ed = match ed with Eapp (app, args, reset), acc | Eiterator (i, app, param, args, reset) -> let app, acc = app_it funs acc app in - let param, acc = static_exp_it funs.ty_funs acc param in + let param, acc = static_exp_it funs.global_funs acc param in let args, acc = mapfold (exp_it funs) acc args in let reset, acc = optional_wacc (exp_it funs) acc reset in Eiterator (i, app, param, args, reset), acc @@ -103,7 +98,7 @@ and edesc funs acc ed = match ed with and app_it funs acc a = funs.app funs acc a and app funs acc a = - let p, acc = mapfold (static_exp_it funs.ty_funs) acc a.a_params in + let p, acc = mapfold (static_exp_it funs.global_funs) acc a.a_params in { a with a_params = p }, acc @@ -197,7 +192,7 @@ and last_it funs acc l = and last funs acc l = match l with | Var -> l, acc | Last sto -> - let sto, acc = optional_wacc (static_exp_it funs.ty_funs) acc sto in + let sto, acc = optional_wacc (static_exp_it funs.global_funs) acc sto in Last sto, acc @@ -211,30 +206,39 @@ and contract funs acc c = c_assume = c_assume; c_enforce = c_enforce; c_local = c_local; c_eq = c_eq } , acc +and param_it funs acc vd = funs.param funs acc vd +and param funs acc vd = + let v_last, acc = last_it funs acc vd.v_last in + { vd with v_last = v_last }, acc and node_dec_it funs acc nd = funs.node_dec funs acc nd and node_dec funs acc nd = let n_input, acc = mapfold (var_dec_it funs) acc nd.n_input in let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in let n_local, acc = mapfold (var_dec_it funs) acc nd.n_local in + let n_params, acc = mapfold (param_it funs.global_funs) acc nd.n_params in + let n_contract, acc = optional_wacc (contract_it funs) acc nd.n_contract in let n_equs, acc = mapfold (eq_it funs) acc nd.n_equs in { nd with - n_input = n_input; n_output = n_output; n_local = n_local; n_equs = n_equs } + n_input = n_input; n_output = n_output; + n_local = n_local; n_params = n_params; + n_contract = n_contract; n_equs = n_equs; } , acc - and const_dec_it funs acc c = funs.const_dec funs acc c and const_dec funs acc c = - let se, acc = static_exp_it funs.ty_funs acc c.c_value in + let se, acc = static_exp_it funs.global_funs acc c.c_value in { c with c_value = se }, acc + and program_it funs acc p = funs.program funs acc p and program funs acc p = let cd_list, acc = mapfold (const_dec_it funs) acc p.p_consts in let nd_list, acc = mapfold (node_dec_it funs) acc p.p_nodes in { p with p_consts = cd_list; p_nodes = nd_list }, acc + let hept_funs_default = { app = app; block = block; @@ -254,7 +258,7 @@ let hept_funs_default = { node_dec = node_dec; const_dec = const_dec; program = program; - ty_funs = Types.types_funs_default } + global_funs = Global_mapfold.global_funs_default } diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index a3aff13..ffd118b 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -119,6 +119,7 @@ type node_dec = { type const_dec = { c_name : name; + c_type : ty; c_value : static_exp; c_loc : location } diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml new file mode 100644 index 0000000..e32d090 --- /dev/null +++ b/compiler/minils/mls_mapfold.ml @@ -0,0 +1,181 @@ + (**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +(* Generic mapred over Minils Ast *) +open Misc +open Global_mapfold +open Minils + +(* /!\ do never, never put in your funs record one + of the generic iterator function (_omega), + either yours either the _default version *) + +type 'a mls_it_funs = { + app: 'a mls_it_funs -> 'a -> Minils.app -> Minils.app * 'a; + edesc: 'a mls_it_funs -> 'a -> Minils.edesc -> Minils.edesc * 'a; + eq: 'a mls_it_funs -> 'a -> Minils.eq -> Minils.eq * 'a; + exp: 'a mls_it_funs -> 'a -> Minils.exp -> Minils.exp * 'a; + pat: 'a mls_it_funs -> 'a -> Minils.pat -> Minils.pat * 'a; + var_dec: 'a mls_it_funs -> 'a -> Minils.var_dec -> Minils.var_dec * 'a; + contract: + 'a mls_it_funs -> 'a -> Minils.contract -> Minils.contract * 'a; + node_dec: + 'a mls_it_funs -> 'a -> Minils.node_dec -> Minils.node_dec * 'a; + const_dec: + 'a mls_it_funs -> 'a -> Minils.const_dec -> Minils.const_dec * 'a; + type_dec: + 'a mls_it_funs -> 'a -> Minils.type_dec -> Minils.type_dec * 'a; + tdesc: 'a mls_it_funs -> 'a -> Minils.tdesc -> Minils.tdesc * 'a; + program: + 'a mls_it_funs -> 'a -> Minils.program -> Minils.program * 'a; + global_funs: 'a Global_mapfold.global_it_funs } + + +let rec exp_it funs acc e = funs.exp funs acc e +and exp funs acc e = + let ed, acc = edesc_it funs acc e.e_desc in + { e with e_desc = ed }, acc + + +and edesc_it funs acc ed = + try funs.edesc funs acc ed + with Fallback -> edesc funs acc ed +and edesc funs acc ed = match ed with + | Econst se -> + let se, acc = static_exp_it funs.global_funs acc se in + Econst se, acc + | Evar x -> ed, acc + | Efby (se, e) -> + let se, acc = optional_wacc (static_exp_it funs.global_funs) acc se in + let e, acc = exp_it funs acc e in + Efby (se, e), acc + | Eapp(app, args, reset) -> + let app, acc = app_it funs acc app in + let args, acc = mapfold (exp_it funs) acc args in + Eapp (app, args, reset), acc + | Ewhen(e, c, x) -> + let e, acc = exp_it funs acc e in + Ewhen(e, c, x), 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 + | Estruct n_e_list -> + let aux acc (n,e) = + let e, acc = exp_it funs acc e in + (n,e), acc in + let n_e_list, acc = mapfold aux acc n_e_list in + Estruct n_e_list, acc + | Eiterator (i, app, param, args, reset) -> + let app, acc = app_it funs acc app in + let param, acc = static_exp_it funs.global_funs acc param in + let args, acc = mapfold (exp_it funs) acc args in + Eiterator (i, app, param, args, reset), acc + + +and app_it funs acc a = funs.app funs acc a +and app funs acc a = + let p, acc = mapfold (static_exp_it funs.global_funs) acc a.a_params in + { a with a_params = p }, acc + + +and pat_it funs acc p = + try funs.pat funs acc p + with Fallback -> pat funs acc p +and pat funs acc p = match p with + | Etuplepat pl -> + let pl, acc = mapfold (pat_it funs) acc pl in + Etuplepat pl, acc + | Evarpat _ -> p, acc + + +and eq_it funs acc eq = funs.eq funs acc eq +and eq funs acc eq = + let eq_lhs, acc = pat_it funs acc eq.eq_lhs in + let eq_rhs, acc = exp_it funs acc eq.eq_rhs in + { eq with eq_lhs = eq_lhs; eq_rhs = eq_rhs }, acc + + +and var_dec_it funs acc vd = funs.var_dec funs acc vd +and var_dec funs acc vd = + let v_type, acc = ty_it funs.global_funs acc vd.v_type in + { vd with v_type = v_type }, acc + + +and contract_it funs acc c = funs.contract funs acc c +and contract funs acc c = + let c_assume, acc = exp_it funs acc c.c_assume in + let c_enforce, acc = exp_it funs acc c.c_enforce in + let c_local, acc = mapfold (var_dec_it funs) acc c.c_local in + let c_eq, acc = mapfold (eq_it funs) acc c.c_eq in + { c with + c_assume = c_assume; c_enforce = c_enforce; c_local = c_local; c_eq = c_eq } + , acc + + +and node_dec_it funs acc nd = funs.node_dec funs acc nd +and node_dec funs acc nd = + let n_input, acc = mapfold (var_dec_it funs) acc nd.n_input in + let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in + let n_local, acc = mapfold (var_dec_it funs) acc nd.n_local in + let n_params, acc = mapfold (param_it funs.global_funs) acc nd.n_params in + let n_contract, acc = optional_wacc (contract_it funs) acc nd.n_contract in + let n_equs, acc = mapfold (eq_it funs) acc nd.n_equs in + { nd with + n_input = n_input; n_output = n_output; + n_local = n_local; n_params = n_params; + n_contract = n_contract; n_equs = n_equs } + , acc + + +and const_dec_it funs acc c = funs.const_dec funs acc c +and const_dec funs acc c = + let ty, acc = ty_it funs.global_funs acc c.c_type in + let se, acc = static_exp_it funs.global_funs acc c.c_value in + { c with c_type = ty; c_value = se }, acc + + +and type_dec_it funs acc t = funs.type_dec funs acc t +and type_dec funs acc t = + let tdesc, acc = tdesc_it funs acc t.t_desc in + { t with t_desc = tdesc }, acc + + +and tdesc_it funs acc td = + try funs.tdesc funs acc td + with Fallback -> tdesc funs acc td +and tdesc funs acc td = match td with + | Type_struct s -> + let s, acc = structure_it funs.global_funs acc s in + Type_struct s, acc + | _ -> td, acc + + +and program_it funs acc p = funs.program funs acc p +and program funs acc p = + let td_list, acc = mapfold (type_dec_it funs) acc p.p_types in + let cd_list, acc = mapfold (const_dec_it funs) acc p.p_consts in + let nd_list, acc = mapfold (node_dec_it funs) acc p.p_nodes in + { p with p_types = td_list; p_consts = cd_list; p_nodes = nd_list }, acc + +let mls_funs_default = { + app = app; + edesc = edesc; + eq = eq; + exp = exp; + pat = pat; + var_dec = var_dec; + contract = contract; + node_dec = node_dec; + const_dec = const_dec; + type_dec = type_dec; + tdesc = tdesc; + program = program; + global_funs = Global_mapfold.global_funs_default }