Rebase done : Mls re-ported. Mls_mapfold and mls_utils updated.
This commit is contained in:
parent
be7bdc7f27
commit
57751992c0
4 changed files with 53 additions and 89 deletions
|
@ -16,24 +16,19 @@ open Minils
|
|||
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 }
|
||||
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
|
||||
|
@ -165,7 +160,7 @@ and program funs acc p =
|
|||
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 = {
|
||||
let defaults = {
|
||||
app = app;
|
||||
edesc = edesc;
|
||||
eq = eq;
|
||||
|
@ -178,4 +173,4 @@ let mls_funs_default = {
|
|||
type_dec = type_dec;
|
||||
tdesc = tdesc;
|
||||
program = program;
|
||||
global_funs = Global_mapfold.global_funs_default }
|
||||
global_funs = Global_mapfold.defaults }
|
||||
|
|
|
@ -210,7 +210,7 @@ let print oc { p_opened = pm; p_types = pt; p_nodes = pn; p_consts = pc } =
|
|||
let ff = formatter_of_out_channel oc
|
||||
in (
|
||||
List.iter (print_open_module ff) pm;
|
||||
List.iter (print_type_def ff) pt;
|
||||
List.iter (print_type_dec ff) pt;
|
||||
List.iter (print_const_dec ff) pc;
|
||||
List.iter (print_node ff) pn;
|
||||
fprintf ff "@?" )
|
||||
|
|
|
@ -55,8 +55,7 @@ let is_op = function
|
|||
|
||||
module Vars =
|
||||
struct
|
||||
let add x acc =
|
||||
if List.mem x acc then acc else x :: acc
|
||||
let add x acc = if List.mem x acc then acc else x :: acc
|
||||
|
||||
let rec vars_pat acc = function
|
||||
| Evarpat x -> x :: acc
|
||||
|
@ -67,54 +66,26 @@ struct
|
|||
| Cbase | Cvar { contents = Cindex _ } -> acc
|
||||
| Cvar { contents = Clink ck } -> vars_ck acc ck
|
||||
|
||||
let rec read is_left acc e =
|
||||
let acc =
|
||||
match e.e_desc with
|
||||
| Evar n -> add n acc
|
||||
| Emerge(x, c_e_list) ->
|
||||
let acc = add x acc in
|
||||
List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list
|
||||
| Eifthenelse(e1, e2, e3) ->
|
||||
read is_left (read is_left (read is_left acc e1) e2) e3
|
||||
| Ewhen(e, c, x) ->
|
||||
let acc = add x acc in
|
||||
read is_left acc e
|
||||
| Etuple(e_list) -> List.fold_left (read is_left) acc e_list
|
||||
| Ecall(_, e_list, None) ->
|
||||
List.fold_left (read is_left) acc e_list
|
||||
| Ecall(_, e_list, Some x) ->
|
||||
let acc = add x acc in
|
||||
List.fold_left (read is_left) acc e_list
|
||||
| Efby(_, e) ->
|
||||
if is_left then vars_ck acc e.e_ck else read is_left acc e
|
||||
| Efield(e, _) -> read is_left acc e
|
||||
| Estruct(f_e_list) ->
|
||||
List.fold_left (fun acc (_, e) -> read is_left acc e) acc f_e_list
|
||||
| Econst _ | Econstvar _ -> acc
|
||||
| Efield_update (_, e1, e2) ->
|
||||
read is_left (read is_left acc e1) e2
|
||||
(*Array operators*)
|
||||
| Earray e_list -> List.fold_left (read is_left) acc e_list
|
||||
| Earray_op op -> read_array_op is_left acc op
|
||||
let read_exp read_funs (is_left, acc) e =
|
||||
(* recursive call *)
|
||||
let _,(_, acc) = Mls_mapfold.exp read_funs (is_left, acc) e in
|
||||
(* special cases *)
|
||||
let acc = match e.e_desc with
|
||||
| Evar x | Emerge(x,_) | Ewhen(_, _, x)
|
||||
| Eapp(_, _, Some x) | Eiterator (_, _, _, _, Some x) ->
|
||||
add x acc
|
||||
| Efby(_, e) ->
|
||||
if is_left then vars_ck acc e.e_ck else acc
|
||||
| _ -> acc
|
||||
in
|
||||
vars_ck acc e.e_ck
|
||||
e, (is_left, vars_ck acc e.e_ck)
|
||||
|
||||
and read_array_op is_left acc = function
|
||||
| Erepeat (_,e) -> read is_left acc e
|
||||
| Eselect (_,e) -> read is_left acc e
|
||||
| Eselect_dyn (e_list, e1, e2) ->
|
||||
let acc = List.fold_left (read is_left) acc e_list in
|
||||
read is_left (read is_left acc e1) e2
|
||||
| Eupdate (_, e1, e2) ->
|
||||
read is_left (read is_left acc e1) e2
|
||||
| Eselect_slice (_ , _, e) -> read is_left acc e
|
||||
| Econcat (e1, e2) ->
|
||||
read is_left (read is_left acc e1) e2
|
||||
| Eiterator (_, _, _, e_list, None) ->
|
||||
List.fold_left (read is_left) acc e_list
|
||||
| Eiterator (_, _, _, e_list, Some x) ->
|
||||
let acc = add x acc in
|
||||
List.fold_left (read is_left) acc e_list
|
||||
let read_exp is_left acc e =
|
||||
let _, (_, acc) =
|
||||
Mls_mapfold.exp_it
|
||||
{ Mls_mapfold.defaults with Mls_mapfold.exp = read_exp }
|
||||
(is_left, acc) e in
|
||||
acc
|
||||
|
||||
let rec remove x = function
|
||||
| [] -> []
|
||||
|
@ -122,21 +93,19 @@ struct
|
|||
|
||||
let def acc { eq_lhs = pat } = vars_pat acc pat
|
||||
|
||||
let read is_left { eq_lhs = pat; eq_rhs = e } =
|
||||
match pat, e.e_desc with
|
||||
| Evarpat(n), Efby(_, e1) ->
|
||||
if is_left
|
||||
then remove n (read is_left [] e1)
|
||||
else read is_left [] e1
|
||||
| _ -> read is_left [] e
|
||||
let read is_left { eq_lhs = pat; eq_rhs = e } = match pat, e.e_desc with
|
||||
| Evarpat(n), Efby(_, e1) ->
|
||||
if is_left
|
||||
then remove n (read_exp is_left [] e1)
|
||||
else read_exp is_left [] e1
|
||||
| _ -> read_exp is_left [] e
|
||||
|
||||
let antidep { eq_rhs = e } =
|
||||
match e.e_desc with Efby _ -> true | _ -> false
|
||||
|
||||
let clock { eq_rhs = e } =
|
||||
match e.e_desc with
|
||||
| Emerge(_, (_, e) :: _) -> e.e_ck
|
||||
| _ -> e.e_ck
|
||||
let clock { eq_rhs = e } = match e.e_desc with
|
||||
| Emerge(_, (_, e) :: _) -> e.e_ck
|
||||
| _ -> e.e_ck
|
||||
|
||||
let head ck =
|
||||
let rec headrec ck l =
|
||||
|
@ -149,10 +118,9 @@ struct
|
|||
|
||||
(** Returns a list of memory vars (x in x = v fby e)
|
||||
appearing in an equation. *)
|
||||
let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) =
|
||||
match e.e_desc with
|
||||
| Efby(_, _) -> def [] eq
|
||||
| _ -> []
|
||||
let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) = match e.e_desc with
|
||||
| Efby(_, _) -> def [] eq
|
||||
| _ -> []
|
||||
end
|
||||
|
||||
|
||||
|
|
|
@ -89,7 +89,7 @@ let collect_node_calls ln =
|
|||
| _ -> ed, (ln, params)::acc)
|
||||
| _ -> raise Misc.Fallback
|
||||
in
|
||||
let funs = { Mls_mapfold.mls_funs_default with
|
||||
let funs = { Mls_mapfold.defaults with
|
||||
edesc = edesc } in
|
||||
let n = node_by_longname ln in
|
||||
let _, acc = Mls_mapfold.node_dec funs [] n in
|
||||
|
@ -165,9 +165,9 @@ struct
|
|||
| _ -> assert false)
|
||||
|
||||
let node_dec_instance modname n params =
|
||||
let global_funs = { global_funs_default with
|
||||
let global_funs = { Global_mapfold.defaults with
|
||||
static_exp = static_exp } in
|
||||
let funs = { Mls_mapfold.mls_funs_default with
|
||||
let funs = { Mls_mapfold.defaults with
|
||||
edesc = edesc;
|
||||
global_funs = global_funs } in
|
||||
let m = build NamesEnv.empty n.n_params params in
|
||||
|
@ -185,7 +185,8 @@ struct
|
|||
List.map (node_dec_instance modname n) (get_node_instances ln)
|
||||
|
||||
let program p =
|
||||
{ p with p_nodes = List.flatten (List.map (node_dec p.p_modname) p.p_nodes) }
|
||||
{ p
|
||||
with p_nodes = List.flatten (List.map (node_dec p.p_modname) p.p_nodes) }
|
||||
end
|
||||
|
||||
let check_no_static_var se =
|
||||
|
@ -193,7 +194,7 @@ let check_no_static_var se =
|
|||
| Svar (Name n) -> Error.message se.se_loc (Error.Evar_unbound n)
|
||||
| _ -> raise Misc.Fallback
|
||||
in
|
||||
let funs = { Global_mapfold.global_funs_default with
|
||||
let funs = { Global_mapfold.defaults with
|
||||
static_exp_desc = static_exp_desc } in
|
||||
ignore (Global_mapfold.static_exp_it funs false se)
|
||||
|
||||
|
|
Loading…
Reference in a new issue