From fed52e5130486b63a3eccd1b0776ce50eca7b64a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Tue, 15 Jun 2010 15:08:14 +0200 Subject: [PATCH] minils "done" --- global/location.ml | 2 - heptagon/heptagon.ml | 5 +- main/hept2mls.ml | 8 +-- minils/analysis/clocking.ml | 2 +- minils/analysis/init.ml | 4 +- minils/minils.ml | 101 ++++++++-------------------- minils/sequential/mls2obc.ml | 4 +- minils/transformations/callgraph.ml | 2 +- minils/transformations/normalize.ml | 8 +-- 9 files changed, 46 insertions(+), 90 deletions(-) diff --git a/global/location.ml b/global/location.ml index 0056108..991ca44 100644 --- a/global/location.ml +++ b/global/location.ml @@ -1,8 +1,6 @@ (* Printing a location in the source program *) (* taken from the source of the Caml Light 0.73 compiler *) -(* $Id$ *) - open Lexing open Parsing diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml index 7a23909..182015d 100644 --- a/heptagon/heptagon.ml +++ b/heptagon/heptagon.ml @@ -15,7 +15,7 @@ open Static open Signature -type iterator_name = +type iterator_type = | Imap | Ifold | Imapfold @@ -53,7 +53,8 @@ type exp = | Eupdate of size_exp list | Eselect_slice | Econcat - | Eiterator of iterator_name * op_desc * exp option + | Eiterator of iterator_type * op_desc * exp option (** [op_desc] node to map + [exp option] reset *) and op_desc = longname * size_exp list * op_kind and op_kind = | Eop | Enode diff --git a/main/hept2mls.ml b/main/hept2mls.ml index 91de560..f6fe111 100644 --- a/main/hept2mls.ml +++ b/main/hept2mls.ml @@ -76,7 +76,7 @@ let equation locals l_eqs e = n, { v_name = n; v_copy_of = None; v_type = exp_type e; v_linearity = NotLinear; v_clock = Cbase } :: locals, - { p_lhs = Evarpat(n); p_rhs = e } :: l_eqs + { eq_lhs = Evarpat(n); eq_rhs = e } :: l_eqs (* inserts the definition [x,e] into the set of shared equations *) let rec add x e shared = @@ -92,7 +92,7 @@ let add_locals ni l_eqs s_eqs s_handlers = | (x, e) :: s_handlers -> if IdentSet.mem x ni then addrec l_eqs (add x e s_eqs) s_handlers else - addrec ({ p_lhs = Evarpat(x); p_rhs = e } :: l_eqs) + addrec ({ eq_lhs = Evarpat(x); eq_rhs = e } :: l_eqs) s_eqs s_handlers in addrec l_eqs s_eqs s_handlers @@ -338,14 +338,14 @@ let rec translate_eq env ni (locals, l_eqs, s_eqs) eq = | Heptagon.Eeq(p, e) when all_locals ni p -> (* all vars from [p] are local *) locals, - { p_lhs = translate_pat p; p_rhs = translate env e } :: l_eqs, + { eq_lhs = translate_pat p; eq_rhs = translate env e } :: l_eqs, s_eqs | Heptagon.Eeq(p, e) (* some are local *) -> (* transforms [p = e] into [p' = e; p = p'] *) let p', locals, s_eqs = rename_pat ni locals s_eqs (p,e.Heptagon.e_ty) in locals, - { p_lhs = p'; p_rhs = translate env e } :: l_eqs, + { eq_lhs = p'; eq_rhs = translate env e } :: l_eqs, s_eqs | Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ -> assert false diff --git a/minils/analysis/clocking.ml b/minils/analysis/clocking.ml index e1ef1a2..2724273 100644 --- a/minils/analysis/clocking.ml +++ b/minils/analysis/clocking.ml @@ -228,7 +228,7 @@ let rec typing_pat h = function let typing_eqs h eq_list = List.iter - (fun { p_lhs = pat; p_rhs = e } -> + (fun { eq_lhs = pat; eq_rhs = e } -> (match e.e_desc with | Ereset_mem (_, _, x) -> let ck = typ_of_name h x in diff --git a/minils/analysis/init.ml b/minils/analysis/init.ml index a355e1d..0f36d09 100644 --- a/minils/analysis/init.ml +++ b/minils/analysis/init.ml @@ -262,7 +262,7 @@ let rec typing_pat h = function let typing_eqs h eq_list = List.iter - (fun { p_lhs = pat; p_rhs = e } -> + (fun { eq_lhs = pat; eq_rhs = e } -> let ty_pat = typing_pat h pat in expect h e ty_pat) eq_list @@ -270,7 +270,7 @@ let build h eq_list = let rec build_pat h = function | Evarpat(x) -> Env.add x { t_init = new_var (); t_value = None } h | Etuplepat(pat_list) -> List.fold_left build_pat h pat_list in - let build_equation h { p_lhs = pat; p_rhs = e } = + let build_equation h { eq_lhs = pat; eq_rhs = e } = match pat, e.e_desc with | Evarpat(x), Efby(Some(Cconstr c), _) -> (* we keep the initial value of state variables *) diff --git a/minils/minils.ml b/minils/minils.ml index 3fa34ac..4db8658 100644 --- a/minils/minils.ml +++ b/minils/minils.ml @@ -9,19 +9,15 @@ (* The internal MiniLustre representation *) -(* $Id$ *) - open Location open Dep open Misc open Names open Ident -open Linearity -open Interference_graph -open Global +open Signature open Static -type iterator_name = +type iterator_type = | Imap | Ifold | Imapfold @@ -34,14 +30,13 @@ type type_dec = and tdesc = | Type_abs | Type_enum of name list - | Type_struct of (name * ty) list + | Type_struct of structure and exp = { e_desc: desc; (* its descriptor *) mutable e_ck: ck; mutable e_ty: ty; - mutable e_linearity : linearity; - e_loc: location } + e_loc: location } and desc = | Econst of const @@ -49,16 +44,20 @@ and desc = | Econstvar of name | Efby of const option * exp | Etuple of exp list - | Eop of longname * size_exp list * exp list - | Eapp of app * size_exp list * exp list - | Eevery of app * size_exp list * exp list * ident + | Ecall of op_desc * exp list * ident option (** [op_desc] is the function called + [exp list] is the passed arguments + [ident option] is the optional reset condition *) + | Ewhen of exp * longname * ident | Emerge of ident * (longname * exp) list | Eifthenelse of exp * exp * exp | Efield of exp * longname + | Efield_update of longname * exp * exp (*field, record, value*) | Estruct of (longname * exp) list -(*Array operators*) | Earray of exp list + | Earray_op of array_op + +and array_op = | Erepeat of size_exp * exp | Eselect of size_exp list * exp (*indices, array*) | Eselect_dyn of exp list * size_exp list * exp * exp (*indices, bounds, array, default*) @@ -66,12 +65,9 @@ and desc = | Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*) | Econcat of exp * exp | Eiterator of iterator_name * longname * size_exp list * size_exp * exp list * ident option - | Efield_update of longname * exp * exp (*field, record, value*) - -and app = - { a_op: longname; - a_inlined: inlining_policy - } + +and op_desc = longname * size_exp list * op_kind +and op_kind = | Eop | Enode and ct = | Ck of ck @@ -86,15 +82,6 @@ and link = | Cindex of int | Clink of ck -and ty = - | Tbase of ty - | Tprod of ty list - -and ty = - | Tint | Tfloat - | Tid of longname - | Tarray of ty * size_exp - and const = | Cint of int | Cfloat of float @@ -106,14 +93,13 @@ and pat = | Evarpat of ident type eq = - { p_lhs : pat; - p_rhs : exp; } + { eq_lhs : pat; + eq_rhs : exp; + eq_loc : loc } type var_dec = { v_name : ident; - v_copy_of : ident option; v_type : ty; - v_linearity : linearity; v_clock : ck } type contract = @@ -131,13 +117,10 @@ type node_dec = n_contract : contract option; n_local : var_dec list; n_equs : eq list; - n_loc : location; - n_targeting : (int*int) list; - n_mem_alloc : (ty * ivar list) list; - n_states_graph : (name,name) interf_graph; - n_params : name list; + n_loc : location; + n_params : param list; n_params_constraints : size_constr list; - n_params_instances : (int list) list; } + n_params_instances : (int list) list; }(*TODO commenter ou passer en env*) type const_dec = { c_name : name; @@ -159,26 +142,6 @@ let make_dummy_exp desc ty = { e_desc = desc; e_ty = ty; e_linearity = NotLinear; e_ck = Cbase; e_loc = no_location } -(* Helper functions to work with types *) -let type = function - | Tbase(bty) -> bty - | Tprod _ -> assert false - -(*TODO Cedric *) -type ivar = | IVar of ident | IField of ident * longname - -(** [filter_vars l] returns a list of variables identifiers from - a list of ivar.*) -let rec filter_vars = - function - | [] -> [] - | IVar id :: l -> id :: (filter_vars l) - | _ :: l -> filter_vars l - -(* get the type of an expression ; assuming that this type is a base type *) -let exp_type e = - type e.e_ty - let rec size_exp_of_exp e = match e.e_desc with | Econstvar n -> SVar n @@ -207,12 +170,6 @@ let rec vd_mem n = function | [] -> false | vd::l -> vd.v_name = n or (vd_mem n l) -(** Same as vd_mem but for an ivar value. *) -let ivar_vd_mem var vds = - match var with - | IVar id -> vd_mem id vds - | _ -> false - (** [is_record_type ty] returns whether ty corresponds to a record type. *) let is_record_type ty = match ty with @@ -288,9 +245,9 @@ struct | [] -> [] | y :: l -> if x = y then l else y :: remove x l - let def acc { p_lhs = pat } = vars_pat acc pat + let def acc { eq_lhs = pat } = vars_pat acc pat - let read is_left { p_lhs = pat; p_rhs = e } = + let read is_left { eq_lhs = pat; eq_rhs = e } = match pat, e.e_desc with | Evarpat(n), Efby(_, e1) -> if is_left @@ -311,9 +268,9 @@ struct let read is_left eq = filter_vars (read is_left eq) - let antidep { p_rhs = e } = + let antidep { eq_rhs = e } = match e.e_desc with Efby _ -> true | _ -> false - let clock { p_rhs = e } = + let clock { eq_rhs = e } = match e.e_desc with | Emerge(_, (_, e) :: _) -> e.e_ck | _ -> e.e_ck @@ -354,7 +311,7 @@ struct | Econcat (e1, e2) -> linear_use (linear_use acc e1) e2 - let mem_reset { p_rhs = e } = + let mem_reset { eq_rhs = e } = match e.e_desc with | Ereset_mem (y, _, _) -> [y] | _ -> [] @@ -366,7 +323,7 @@ module DataFlowDep = Make type equation = eq let read eq = Vars.read true eq let def = Vars.def - let linear_read eq = Vars.linear_use [] eq.p_rhs + let linear_read eq = Vars.linear_use [] eq.eq_rhs let mem_reset = Vars.mem_reset let antidep = Vars.antidep end) @@ -376,7 +333,7 @@ module AllDep = Make (struct type equation = eq let read eq = Vars.read false eq - let linear_read eq = Vars.linear_use [] eq.p_rhs + let linear_read eq = Vars.linear_use [] eq.eq_rhs let mem_reset = Vars.mem_reset let def = Vars.def let antidep eq = false @@ -650,7 +607,7 @@ struct fprintf ff ")@]@,") "" tag_e_list - let print_eq ff { p_lhs = p; p_rhs = e } = + let print_eq ff { eq_lhs = p; eq_rhs = e } = fprintf ff "@["; print_pat ff p; (* (\* DEBUG *\) *) diff --git a/minils/sequential/mls2obc.ml b/minils/sequential/mls2obc.ml index fda05df..0c07e8a 100644 --- a/minils/sequential/mls2obc.ml +++ b/minils/sequential/mls2obc.ml @@ -132,7 +132,7 @@ and translate_c_act_list const_env map context pat c_act_list = and comp s_list = List.fold_right (fun s rest -> Comp(s, rest)) s_list Nothing -let rec translate_eq const_env map { Minils.p_lhs = pat; Minils.p_rhs = e } (m, si, j, s) = +let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } (m, si, j, s) = let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e in match pat, desc with | Minils.Evarpat(n), Minils.Efby(opt_c, e) -> @@ -175,7 +175,7 @@ let rec translate_eq const_env map { Minils.p_lhs = pat; Minils.p_rhs = e } (m, (m, si, j, s) | Minils.Etuplepat(p_list), Minils.Etuple(act_list) -> List.fold_right2 - (fun pat e -> translate_eq const_env map { Minils.p_lhs = pat; Minils.p_rhs = e } ) + (fun pat e -> translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } ) p_list act_list (m, si, j, s) | Minils.Evarpat(x), Minils.Eselect_slice(idx1, idx2, e) -> let idx1 = int_of_size_exp const_env idx1 in diff --git a/minils/transformations/callgraph.ml b/minils/transformations/callgraph.ml index dae310f..b002d4b 100644 --- a/minils/transformations/callgraph.ml +++ b/minils/transformations/callgraph.ml @@ -93,7 +93,7 @@ let rec collect_exp nodes env e = ) and collect_eqs nodes env eq = - collect_exp nodes env eq.p_rhs + collect_exp nodes env eq.eq_rhs and node_call nodes n params = match params with diff --git a/minils/transformations/normalize.ml b/minils/transformations/normalize.ml index a46ae02..4afc3ba 100644 --- a/minils/transformations/normalize.ml +++ b/minils/transformations/normalize.ml @@ -21,7 +21,7 @@ let equation (d_list, eq_list) ({ e_ty = te; e_linearity = l; e_ck = ck } as e) let n = Ident.fresh "_v" in let d_list = { v_name = n; v_copy_of = None; v_type = type te; v_linearity = l; v_clock = ck } :: d_list - and eq_list = { p_lhs = Evarpat(n); p_rhs = e } :: eq_list in + and eq_list = { eq_lhs = Evarpat(n); eq_rhs = e } :: eq_list in (d_list, eq_list), n let intro context e = @@ -232,17 +232,17 @@ let rec translate_eq context pat e = | Evarpat(x), Efby _ when not (vd_mem x d_list) -> let (d_list, eq_list), n = equation context e in d_list, - { p_lhs = pat; p_rhs = { e with e_desc = Evar(n) } } :: eq_list + { eq_lhs = pat; eq_rhs = { e with e_desc = Evar(n) } } :: eq_list | Etuplepat(pat_list), Etuple(e_list) -> List.fold_left2 distribute context pat_list e_list - | _ -> d_list, { p_lhs = pat; p_rhs = e } :: eq_list in + | _ -> d_list, { eq_lhs = pat; eq_rhs = e } :: eq_list in let context, e = translate Any context e in distribute context pat e let translate_eq_list d_list eq_list = List.fold_left - (fun context { p_lhs = pat; p_rhs = e } -> translate_eq context pat e) + (fun context { eq_lhs = pat; eq_rhs = e } -> translate_eq context pat e) (d_list, []) eq_list let translate_contract ({ c_eq = eq_list; c_local = d_list } as c) =