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 ?)
This commit is contained in:
parent
87cb705fcb
commit
e7bd251b35
5 changed files with 281 additions and 69 deletions
79
compiler/global/global_mapfold.ml
Normal file
79
compiler/global/global_mapfold.ml
Normal file
|
@ -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;
|
||||
}
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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 }
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -119,6 +119,7 @@ type node_dec = {
|
|||
|
||||
type const_dec = {
|
||||
c_name : name;
|
||||
c_type : ty;
|
||||
c_value : static_exp;
|
||||
c_loc : location }
|
||||
|
||||
|
|
181
compiler/minils/mls_mapfold.ml
Normal file
181
compiler/minils/mls_mapfold.ml
Normal file
|
@ -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 }
|
Loading…
Reference in a new issue