Heptagon and Types mapfold.
This commit is contained in:
parent
226ddd5c28
commit
000dc91d69
|
@ -8,6 +8,7 @@
|
||||||
(**************************************************************************)
|
(**************************************************************************)
|
||||||
|
|
||||||
open Names
|
open Names
|
||||||
|
open Misc
|
||||||
open Location
|
open Location
|
||||||
|
|
||||||
type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location }
|
type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location }
|
||||||
|
@ -31,6 +32,60 @@ let invalid_type = Tprod []
|
||||||
let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc =
|
let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc =
|
||||||
{ se_desc = desc; se_ty = ty; se_loc = loc }
|
{ 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 Pp_tools
|
||||||
open Format
|
open Format
|
||||||
|
|
||||||
|
|
264
compiler/heptagon/hept_mapfold.ml
Normal file
264
compiler/heptagon/hept_mapfold.ml
Normal file
|
@ -0,0 +1,264 @@
|
||||||
|
(**************************************************************************)
|
||||||
|
(* *)
|
||||||
|
(* Heptagon *)
|
||||||
|
(* *)
|
||||||
|
(* Author : Marc Pouzet *)
|
||||||
|
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||||
|
(* *)
|
||||||
|
(**************************************************************************)
|
||||||
|
(* Generic mapred over Heptagon Ast *)
|
||||||
|
|
||||||
|
|
||||||
|
(* /!\ do never, never put in your funs record one
|
||||||
|
of the generic iterator function (_omega),
|
||||||
|
either yours either the _default version *)
|
||||||
|
|
||||||
|
|
||||||
|
open Misc
|
||||||
|
open Types
|
||||||
|
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;
|
||||||
|
edesc: 'a hept_it_funs -> 'a -> Heptagon.desc -> Heptagon.desc * 'a;
|
||||||
|
eq: 'a hept_it_funs -> 'a -> Heptagon.eq -> Heptagon.eq * 'a;
|
||||||
|
eqdesc: 'a hept_it_funs -> 'a -> Heptagon.eqdesc -> Heptagon.eqdesc * 'a;
|
||||||
|
escape_unless :
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
|
||||||
|
escape_until:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
|
||||||
|
exp: 'a hept_it_funs -> 'a -> Heptagon.exp -> Heptagon.exp * 'a;
|
||||||
|
pat: 'a hept_it_funs -> 'a -> pat -> Heptagon.pat * 'a;
|
||||||
|
present_handler:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.present_handler
|
||||||
|
-> Heptagon.present_handler * 'a;
|
||||||
|
state_handler:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.state_handler
|
||||||
|
-> Heptagon.state_handler * 'a;
|
||||||
|
switch_handler:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.switch_handler
|
||||||
|
-> Heptagon.switch_handler * 'a;
|
||||||
|
var_dec: 'a hept_it_funs -> 'a -> Heptagon.var_dec -> Heptagon.var_dec * 'a;
|
||||||
|
last: 'a hept_it_funs -> 'a -> Heptagon.last -> Heptagon.last * 'a;
|
||||||
|
contract:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.contract -> Heptagon.contract * 'a;
|
||||||
|
node_dec:
|
||||||
|
'a hept_it_funs -> 'a -> Heptagon.node_dec -> Heptagon.node_dec * 'a;
|
||||||
|
const_dec:
|
||||||
|
'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 }
|
||||||
|
|
||||||
|
|
||||||
|
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.ty_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 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
|
||||||
|
Efby (e1,e2), acc
|
||||||
|
| Efield (e, n) ->
|
||||||
|
let e, acc = exp_it funs acc e in
|
||||||
|
Efield(e, n), 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
|
||||||
|
| Eapp (app, args, reset) ->
|
||||||
|
let app, acc = app_it funs acc app in
|
||||||
|
let args, acc = mapfold (exp_it funs) acc args in
|
||||||
|
let reset, acc = optional_wacc (exp_it funs) acc reset in
|
||||||
|
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 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
|
||||||
|
|
||||||
|
|
||||||
|
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
|
||||||
|
{ 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 eqdesc, acc = eqdesc_it funs acc eq.eq_desc in
|
||||||
|
{ eq with eq_desc = eqdesc }, acc
|
||||||
|
|
||||||
|
|
||||||
|
and eqdesc_it funs acc eqd =
|
||||||
|
try funs.eqdesc funs acc eqd
|
||||||
|
with Fallback -> eqdesc funs acc eqd
|
||||||
|
and eqdesc funs acc eqd = match eqd with
|
||||||
|
| Eautomaton st_h_l ->
|
||||||
|
let st_h_l, acc = mapfold (state_handler_it funs) acc st_h_l in
|
||||||
|
Eautomaton st_h_l, acc
|
||||||
|
| Eswitch (e, sw_h_l) ->
|
||||||
|
let e, acc = exp_it funs acc e in
|
||||||
|
let sw_h_l, acc = mapfold (switch_handler_it funs) acc sw_h_l in
|
||||||
|
Eswitch (e, sw_h_l), acc
|
||||||
|
| Epresent (p_h_l, b) ->
|
||||||
|
let p_h_l, acc = mapfold (present_handler_it funs) acc p_h_l in
|
||||||
|
let b, acc = block_it funs acc b in
|
||||||
|
Epresent (p_h_l, b), acc
|
||||||
|
| Ereset (eq_l, e) ->
|
||||||
|
let eq_l, acc = mapfold (eq_it funs) acc eq_l in
|
||||||
|
let e, acc = exp_it funs acc e in
|
||||||
|
Ereset (eq_l, e), acc
|
||||||
|
| Eeq (p, e) ->
|
||||||
|
let p, acc = pat_it funs acc p in
|
||||||
|
let e, acc = exp_it funs acc e in
|
||||||
|
Eeq (p, e), acc
|
||||||
|
|
||||||
|
|
||||||
|
and block_it funs acc b = funs.block funs acc b
|
||||||
|
and block funs acc b =
|
||||||
|
let b_local, acc = mapfold (var_dec_it funs) acc b.b_local in
|
||||||
|
let b_equs, acc = mapfold (eq_it funs) acc b.b_equs in
|
||||||
|
{ b with b_local = b_local; b_equs = b_equs }, acc
|
||||||
|
|
||||||
|
|
||||||
|
and state_handler_it funs acc s = funs.state_handler funs acc s
|
||||||
|
and state_handler funs acc s =
|
||||||
|
let s_unless, acc = mapfold (escape_unless_it funs) acc s.s_unless in
|
||||||
|
let s_block, acc = block_it funs acc s.s_block in
|
||||||
|
let s_until, acc = mapfold (escape_until_it funs) acc s.s_until in
|
||||||
|
{ s with s_block = s_block; s_until = s_until; s_unless = s_unless }, acc
|
||||||
|
|
||||||
|
|
||||||
|
(** escape is a generic function to deal with the automaton state escapes,
|
||||||
|
still the iterator function record differentiate until and unless
|
||||||
|
with escape_until_it and escape_unless_it *)
|
||||||
|
and escape_unless_it funs acc esc = funs.escape_unless funs acc esc
|
||||||
|
and escape_until_it funs acc esc = funs.escape_until funs acc esc
|
||||||
|
and escape funs acc esc =
|
||||||
|
let e_cond, acc = exp_it funs acc esc.e_cond in
|
||||||
|
{ esc with e_cond = e_cond }, acc
|
||||||
|
|
||||||
|
|
||||||
|
and switch_handler_it funs acc sw = funs.switch_handler funs acc sw
|
||||||
|
and switch_handler funs acc sw =
|
||||||
|
let w_block, acc = block_it funs acc sw.w_block in
|
||||||
|
{ sw with w_block = w_block }, acc
|
||||||
|
|
||||||
|
|
||||||
|
and present_handler_it funs acc ph = funs.present_handler funs acc ph
|
||||||
|
and present_handler funs acc ph =
|
||||||
|
let p_cond, acc = exp_it funs acc ph.p_cond in
|
||||||
|
let p_block, acc = block_it funs acc ph.p_block in
|
||||||
|
{ ph with p_cond = p_cond; p_block = p_block }, acc
|
||||||
|
|
||||||
|
and var_dec_it funs acc vd = funs.var_dec funs acc vd
|
||||||
|
and var_dec funs acc vd =
|
||||||
|
let v_last, acc = last_it funs acc vd.v_last in
|
||||||
|
{ vd with v_last = v_last }, acc
|
||||||
|
|
||||||
|
|
||||||
|
and last_it funs acc l =
|
||||||
|
try funs.last funs acc l
|
||||||
|
with Fallback -> last 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
|
||||||
|
Last sto, 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_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 }
|
||||||
|
, 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
|
||||||
|
{ 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;
|
||||||
|
edesc = edesc;
|
||||||
|
eq = eq;
|
||||||
|
eqdesc = eqdesc;
|
||||||
|
escape_unless = escape;
|
||||||
|
escape_until = escape;
|
||||||
|
exp = exp;
|
||||||
|
pat = pat;
|
||||||
|
present_handler = present_handler;
|
||||||
|
state_handler = state_handler;
|
||||||
|
switch_handler = switch_handler;
|
||||||
|
var_dec = var_dec;
|
||||||
|
last = last;
|
||||||
|
contract = contract;
|
||||||
|
node_dec = node_dec;
|
||||||
|
const_dec = const_dec;
|
||||||
|
program = program;
|
||||||
|
ty_funs = Types.types_funs_default }
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -1,149 +0,0 @@
|
||||||
(**************************************************************************)
|
|
||||||
(* *)
|
|
||||||
(* Heptagon *)
|
|
||||||
(* *)
|
|
||||||
(* Author : Marc Pouzet *)
|
|
||||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
|
||||||
(* *)
|
|
||||||
(**************************************************************************)
|
|
||||||
(* Generic mapred over Heptagon Ast *)
|
|
||||||
|
|
||||||
open Misc
|
|
||||||
open Heptagon
|
|
||||||
|
|
||||||
exception Fall_back
|
|
||||||
|
|
||||||
type exp = { e_desc : edesc }
|
|
||||||
|
|
||||||
and edesc =
|
|
||||||
| Econst of static_exp
|
|
||||||
| Evar of var_ident
|
|
||||||
| Elast of var_ident
|
|
||||||
| Epre of static_exp option * exp
|
|
||||||
| Efby of exp * exp
|
|
||||||
| Efield of exp * field_name
|
|
||||||
| Estruct of (field_name * exp) list
|
|
||||||
| Eapp of app * exp list * exp option
|
|
||||||
| Eiterator of iterator_type * app * static_exp * exp list * exp option
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
let exp_it funs acc e =
|
|
||||||
let ed, acc = funs.edesc_it funs acc e.edesc in
|
|
||||||
{ e with e_desc = ed }, acc
|
|
||||||
|
|
||||||
let edesc_it_default funs acc ed = match ed with
|
|
||||||
| Econst se -> let se, acc = funs.static_exp_it funs acc se in Econst se, acc
|
|
||||||
| Evar _ | Elast _ -> ed, acc
|
|
||||||
| Epre (None, e) -> let e, acc = funs.exp_it funs acc e in Epre (None, e), acc
|
|
||||||
| Epre (Some se, e) ->
|
|
||||||
let se, acc = funs.static_exp_it funs acc se in
|
|
||||||
let e, acc = funs.exp_it funs acc e in Epre (Some se, e), acc
|
|
||||||
| Efby (e1, e2) ->
|
|
||||||
let e1, acc = funs.exp_it funs acc e1 in
|
|
||||||
let e2, acc = funs.exp_it funs acc e2 in Efby (e1,e2), acc
|
|
||||||
| Efby of exp * exp
|
|
||||||
| Efield of exp * field_name
|
|
||||||
| Estruct of (field_name * exp) list
|
|
||||||
| Eapp of app * exp list * exp option
|
|
||||||
| Eiterator of iterator_type * app * static_exp * exp list * exp option
|
|
||||||
|
|
||||||
let edesc_it funs acc e =
|
|
||||||
try funs.edesc_it funs acc e
|
|
||||||
with Fall_back -> edesc_it_default funs acc e
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(** const_dec : traverse static_exps *)
|
|
||||||
let const_it funs acc c =
|
|
||||||
let se, acc = funs.static_exp_it funs acc c.c_value in
|
|
||||||
{ c with c_value = se }, acc
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
|
|
||||||
|
|
||||||
and pat =
|
|
||||||
| Etuplepat of pat list
|
|
||||||
| Evarpat of var_ident
|
|
||||||
|
|
||||||
type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
|
|
||||||
|
|
||||||
and eqdesc =
|
|
||||||
| Eautomaton of state_handler list
|
|
||||||
| Eswitch of exp * switch_handler list
|
|
||||||
| Epresent of present_handler list * block
|
|
||||||
| Ereset of eq list * exp
|
|
||||||
| Eeq of pat * exp
|
|
||||||
|
|
||||||
and block = {
|
|
||||||
b_local : var_dec list;
|
|
||||||
b_equs : eq list;
|
|
||||||
mutable b_defnames : ty Env.t;
|
|
||||||
mutable b_statefull : bool;
|
|
||||||
b_loc : location }
|
|
||||||
|
|
||||||
and state_handler = {
|
|
||||||
s_state : state_name;
|
|
||||||
s_block : block;
|
|
||||||
s_until : escape list;
|
|
||||||
s_unless : escape list }
|
|
||||||
|
|
||||||
and escape = {
|
|
||||||
e_cond : exp;
|
|
||||||
e_reset : bool;
|
|
||||||
e_next_state : state_name }
|
|
||||||
|
|
||||||
and switch_handler = { w_name : constructor_name; w_block : block }
|
|
||||||
|
|
||||||
and present_handler = { p_cond : exp; p_block : block }
|
|
||||||
|
|
||||||
and var_dec = {
|
|
||||||
v_ident : var_ident;
|
|
||||||
mutable v_type : ty;
|
|
||||||
v_last : last;
|
|
||||||
v_loc : location }
|
|
||||||
|
|
||||||
and last = Var | Last of static_exp option
|
|
||||||
|
|
||||||
|
|
||||||
type contract = {
|
|
||||||
c_assume : exp;
|
|
||||||
c_enforce : exp;
|
|
||||||
c_local : var_dec list;
|
|
||||||
c_eq : eq list }
|
|
||||||
|
|
||||||
type node_dec = {
|
|
||||||
n_input : var_dec list;
|
|
||||||
n_output : var_dec list;
|
|
||||||
n_local : var_dec list;
|
|
||||||
n_equs : eq list }
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(** const_dec : traverse static_exps *)
|
|
||||||
let const_it funs acc c =
|
|
||||||
let se, acc = funs.static_exp_it funs acc c.c_value in
|
|
||||||
{ c with c_value = se }, acc
|
|
||||||
|
|
||||||
(** program : traverse const_dec chained to node_dec *)
|
|
||||||
let program_it funs acc p =
|
|
||||||
let cd_list, acc = mapfold (funs.const_it funs) acc p.p_consts in
|
|
||||||
let nd_list, acc = mapfold (funs.node_it funs) acc p.p_nodes in
|
|
||||||
{ p with p_consts = cd_list; p_nodes = nd_list }, acc
|
|
||||||
|
|
||||||
|
|
||||||
let hept_mapfolds = { program_it .... }
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -100,6 +100,10 @@ let optional f = function
|
||||||
| None -> None
|
| None -> None
|
||||||
| Some x -> Some (f x)
|
| Some x -> Some (f x)
|
||||||
|
|
||||||
|
let optional_wacc f acc = function
|
||||||
|
| None -> None, acc
|
||||||
|
| Some x -> let x, acc = f acc x in Some x, acc
|
||||||
|
|
||||||
let optunit f = function
|
let optunit f = function
|
||||||
| None -> ()
|
| None -> ()
|
||||||
| Some x -> f x
|
| Some x -> f x
|
||||||
|
@ -193,6 +197,10 @@ let rec assocd value = function
|
||||||
else
|
else
|
||||||
assocd value l
|
assocd value l
|
||||||
|
|
||||||
|
|
||||||
|
(** Compiler iterators *)
|
||||||
|
exception Fallback
|
||||||
|
|
||||||
(** Mapfold *)
|
(** Mapfold *)
|
||||||
let mapfold f acc l =
|
let mapfold f acc l =
|
||||||
let l,acc = List.fold_left (fun (l,acc) e -> let e,acc = f acc e in e::l, acc)
|
let l,acc = List.fold_left (fun (l,acc) e -> let e,acc = f acc e in e::l, acc)
|
||||||
|
|
|
@ -106,6 +106,8 @@ val use_new_reset_encoding : bool ref
|
||||||
|
|
||||||
(* Misc. functions *)
|
(* Misc. functions *)
|
||||||
val optional : ('a -> 'b) -> 'a option -> 'b option
|
val optional : ('a -> 'b) -> 'a option -> 'b option
|
||||||
|
(** Optional with accumulator *)
|
||||||
|
val optional_wacc : ('a -> 'b -> 'c*'a) -> 'a -> 'b option -> ('c option * 'a)
|
||||||
val optunit : ('a -> unit) -> 'a option -> unit
|
val optunit : ('a -> unit) -> 'a option -> unit
|
||||||
val split_string : string -> char -> string list
|
val split_string : string -> char -> string list
|
||||||
|
|
||||||
|
@ -153,5 +155,10 @@ val memd_assoc : 'b -> ('a * 'b) list -> bool
|
||||||
(** Same as List.assoc but searching for a data and returning the key. *)
|
(** Same as List.assoc but searching for a data and returning the key. *)
|
||||||
val assocd: 'b -> ('a * 'b) list -> 'a
|
val assocd: 'b -> ('a * 'b) list -> 'a
|
||||||
|
|
||||||
|
|
||||||
|
(** Ast iterators *)
|
||||||
|
exception Fallback
|
||||||
|
|
||||||
|
|
||||||
(** Mapfold *)
|
(** Mapfold *)
|
||||||
val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a
|
val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a
|
Loading…
Reference in a new issue