From 5baa30f7c13290d3b57b15f171287cc6a80e03f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Wed, 7 Jul 2010 15:11:32 +0200 Subject: [PATCH] Last refactor ? and hept_mapred shows in ! --- compiler/global/ident.ml | 2 + compiler/global/ident.mli | 3 + compiler/global/modules.ml | 5 +- compiler/global/names.ml | 11 +++ compiler/global/signature.ml | 11 ++- compiler/global/static.ml | 48 ++++------ compiler/global/types.ml | 35 ++++++-- compiler/heptagon/hept_mapred.ml | 149 +++++++++++++++++++++++++++++++ compiler/heptagon/heptagon.ml | 133 ++++++++++++++------------- compiler/minils/minils.ml | 113 +++++++++++------------ compiler/obc/java/java.ml | 4 +- compiler/obc/obc.ml | 42 ++++----- compiler/utilities/misc.ml | 7 ++ compiler/utilities/misc.mli | 2 + 14 files changed, 378 insertions(+), 187 deletions(-) create mode 100644 compiler/heptagon/hept_mapred.ml diff --git a/compiler/global/ident.ml b/compiler/global/ident.ml index e30cc19..bd7c5c1 100644 --- a/compiler/global/ident.ml +++ b/compiler/global/ident.ml @@ -16,6 +16,8 @@ type ident = { is_generated : bool; } +type var_ident = ident + let compare id1 id2 = compare id1.num id2.num let sourcename id = id.source let name id = diff --git a/compiler/global/ident.mli b/compiler/global/ident.mli index a6a512f..c2f297d 100644 --- a/compiler/global/ident.mli +++ b/compiler/global/ident.mli @@ -7,6 +7,9 @@ (** The (abstract) type of identifiers*) type ident +(** Type to be used for local variables *) +type var_ident = ident + (** Get the source name from an identifier*) val sourcename : ident -> string (** Get the full name of an identifier (it is guaranteed to be unique) *) diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 9c80a41..1a36225 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -25,8 +25,9 @@ type env = mutable values: node NamesEnv.t; mutable types: type_def NamesEnv.t; mutable constr: ty NamesEnv.t; - mutable structs : structure NamesEnv.t; - mutable fields : name NamesEnv.t; + mutable structs: structure NamesEnv.t; + mutable fields: name NamesEnv.t; + (* TODO CP mutable consts: const_def NamesEnv.t; *) format_version : string; } diff --git a/compiler/global/names.ml b/compiler/global/names.ml index d68cf4b..75ca7e0 100644 --- a/compiler/global/names.ml +++ b/compiler/global/names.ml @@ -10,6 +10,17 @@ type longname = and qualident = { qual: string; id: string } +type type_name = longname + +type fun_name = longname + +type field_name = longname + +type constructor_name = longname + +type constant_name = longname + + module NamesM = struct type t = name let compare = compare diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 3cc3563..fa41431 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -34,7 +34,6 @@ type structure = field list type type_def = | Tabstract | Tenum of name list | Tstruct of structure - let names_of_arg_list l = List.map (fun ad -> ad.a_name) l let types_of_arg_list l = List.map (fun ad -> ad.a_type) l @@ -46,9 +45,6 @@ let mk_param name ty = { p_name = name; p_type = ty } let mk_field n ty = { f_name = n; f_type = ty } -let print_param ff p = - fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type - let rec field_assoc f = function | [] -> raise Not_found | { f_name = n; f_type = ty }::l -> @@ -56,3 +52,10 @@ let rec field_assoc f = function ty else field_assoc f l + + +open Format + +let print_param ff p = + fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type + diff --git a/compiler/global/static.ml b/compiler/global/static.ml index 96434f2..e4bd165 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -16,6 +16,7 @@ open Names open Format +open Types (** Constraints on size expressions. *) @@ -46,20 +47,21 @@ let apply_int_op op n1 n2 = let n = if n2 = 0 then raise Instanciation_failed else n1 / n2 in Sint n | _ -> (* unknown operator, reconstrcut the op *) - Sop (op, Sint n1, Sint n2) + Sop (op, [mk_static_exp (Sint n1); mk_static_exp (Sint n2)]) (*TODO CP*) (** [simplify env e] returns e simplified with the variables values taken from env (mapping vars to integers). Variables are replaced with their values and every operator that can be computed is replaced with the value of the result. *) let rec simplify env se = - match se with - | Sint _ | Sfloat _ | Sbool _ | Sconstructor -> se - | Svar id -> (try simplify env (NamesEnv.find id env) with | _ -> se) + match se.se_desc with + | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> se + | Svar id -> + (try simplify env (NamesEnv.find (shortname id) env) with | _ -> se) | Sop (op, [e1; e2]) -> let e1 = simplify env e1 in let e2 = simplify env e2 in - (match e1.e_desc, e2.e_desc with + (match e1.se_desc, e2.se_desc with | Sint n1, Sint n2 -> { se with se_desc = apply_int_op op n1 n2 } | _, _ -> { se with se_desc = Sop (op, [e1; e2]) } ) @@ -80,27 +82,27 @@ let rec simplify env se = Instanciation_failed if it cannot be computed (if a var has no value).*) let int_of_static_exp env e = let e = simplify env e in - match e.e_desc with | Sint n -> n | _ -> raise Instanciation_failed + match e.se_desc with | Sint n -> n | _ -> raise Instanciation_failed (** [is_true env constr] returns whether the constraint is satisfied in the environment (or None if this can be decided) and a simplified constraint. *) let is_true env = function - | Cequal e1, e2 when e1 = e2 -> + | Cequal (e1, e2) when e1 = e2 -> Some true, Cequal (simplify env e1, simplify env e2) | Cequal (e1, e2) -> let e1 = simplify env e1 in let e2 = simplify env e2 in - (match e1.e_desc, e2.e_desc with + (match e1.se_desc, e2.se_desc with | Sint n1, Sint n2 -> Some (n1 = n2), Cequal (e1, e2) | (_, _) -> None, Cequal (e1, e2)) | Clequal (e1, e2) -> let e1 = simplify env e1 in let e2 = simplify env e2 in - (match e1.e_desc, e2.e_desc with + (match e1.se_desc, e2.se_desc with | Sint n1, Sint n2 -> Some (n1 <= n2), Clequal (e1, e2) | _, _ -> None, Clequal (e1, e2)) | Cfalse -> None, Cfalse @@ -124,15 +126,15 @@ let rec solve const_env = (** Substitutes variables in the size exp with their value in the map (mapping vars to size exps). *) let rec static_exp_subst m se = - let desc = match se.e_desc with + let desc = match se.se_desc with | Svar n -> (try List.assoc n m with | Not_found -> Svar n) | Sop (op, se_list) -> Sop (op, List.map (static_exp_subst m) se_list) | Sarray_power (se, n) -> Sarray_power (static_exp_subst m se, static_exp_subst m n) - | Sarray se_list -> Sarray (List.map (static_exp_subst env) se_list) - | Stuple se_list -> Stuple (List.map (static_exp_subst env) se_list) + | Sarray se_list -> Sarray (List.map (static_exp_subst m) se_list) + | Stuple se_list -> Stuple (List.map (static_exp_subst m) se_list) | Srecord f_se_list -> - Srecord (List.map (fun (f,se) -> f, static_exp_subst env se) f_se_list) + Srecord (List.map (fun (f,se) -> f, static_exp_subst m se) f_se_list) | s -> s in { se with se_desc = desc } @@ -146,26 +148,8 @@ let instanciate_constr m constr = | Cfalse -> Cfalse in List.map (replace_one m) constr -let rec print_static_exp ff se = match se.e_desc with - | Sint i -> fprintf ff "%d" i - | Sbool b -> fprintf ff "%b" b - | Sfloat f -> fprintf ff "%f" f - | Sconstructor ln -> print_longname ff ln - | Svar id -> fprintf ff "%s" id - | Sop (op, se_list) -> - fprintf ff "@[<2>%a@,%a@]" - print_longname op print_static_exp_tuple se_list - | Sarray_power (se, n) -> - fprintf ff "%a^%a" print_static_exp se print_static_exp n - | Sarray se_list -> - fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list - | Stuple se_list -> print_static_exp_tuple se_list - | Srecord f_se_list -> - print_record (print_couple print_longname - print_static_exp """ = """) ff f_se_list -and print_static_exp_tuple ff l = - fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l +open Format let print_size_constraint ff = function | Cequal (e1, e2) -> diff --git a/compiler/global/types.ml b/compiler/global/types.ml index 2442292..e14d669 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -13,28 +13,49 @@ open Location type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location } and static_exp_desc = - | Svar of name + | Svar of constant_name | Sint of int | Sfloat of float | Sbool of bool - | Sconstructor of longname + | Sconstructor of constructor_name | Stuple of static_exp list | Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *) | Sarray of static_exp list (** [ e1, e2, e3 ] *) - | Srecord of (longname * static_exp) list (** { f1 = e1; f2 = e2; ... } *) - | Sop of longname * static_exp list (** defined ops for now in pervasives *) + | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *) + | Sop of fun_name * static_exp list (** defined ops for now in pervasives *) -type ty = | Tprod of ty list | Tid of longname | Tarray of ty * static_exp +and ty = | Tprod of ty list | Tid of type_name | Tarray of ty * static_exp let invalid_type = Tprod [] -let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) = +let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = { se_desc = desc; se_ty = ty; se_loc = loc } open Pp_tools open Format -let rec print_type ff = function +let rec print_static_exp ff se = match se.se_desc with + | Sint i -> fprintf ff "%d" i + | Sbool b -> fprintf ff "%b" b + | Sfloat f -> fprintf ff "%f" f + | Sconstructor ln -> print_longname ff ln + | Svar id -> fprintf ff "%a" print_longname id + | Sop (op, se_list) -> + fprintf ff "@[<2>%a@,%a@]" + print_longname op print_static_exp_tuple se_list + | Sarray_power (se, n) -> + fprintf ff "%a^%a" print_static_exp se print_static_exp n + | Sarray se_list -> + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list + | Stuple se_list -> print_static_exp_tuple ff se_list + | Srecord f_se_list -> + print_record (print_couple print_longname + print_static_exp """ = """) ff f_se_list + +and print_static_exp_tuple ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l + +and print_type ff = function | Tprod ty_list -> fprintf ff "@[%a@]" (print_list_r print_type "(" " *" ")") ty_list | Tid id -> print_longname ff id diff --git a/compiler/heptagon/hept_mapred.ml b/compiler/heptagon/hept_mapred.ml new file mode 100644 index 0000000..0887222 --- /dev/null +++ b/compiler/heptagon/hept_mapred.ml @@ -0,0 +1,149 @@ + (**************************************************************************) +(* *) +(* 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 .... } + + + + + + + + + diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index b8bdc27..8d044a3 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -15,6 +15,8 @@ open Static open Signature open Types +type state_name = name + type iterator_type = | Imap | Ifold @@ -24,12 +26,12 @@ type exp = { e_desc : desc; e_ty : ty; e_loc : location } and desc = | Econst of static_exp - | Evar of ident - | Elast of ident + | Evar of var_ident + | Elast of var_ident | Epre of static_exp option * exp | Efby of exp * exp - | Efield of exp * longname - | Estruct of (longname * exp) list + | 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 @@ -38,11 +40,11 @@ and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } and op = | Etuple - | Efun of longname - | Enode of longname + | Efun of fun_name + | Enode of fun_name | Eifthenelse | Earrow - | Efield_update of longname (* field name args would be [record ; value] *) + | Efield_update of field_name (* field name args would be [record ; value] *) | Earray | Earray_fill | Eselect @@ -53,7 +55,7 @@ and op = and pat = | Etuplepat of pat list - | Evarpat of ident + | Evarpat of var_ident type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location } @@ -65,86 +67,93 @@ and eqdesc = | 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 -} + 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 : name; s_block : block; s_until : escape list; - s_unless : escape list -} + 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 : name -} + e_cond : exp; + e_reset : bool; + e_next_state : state_name } -and switch_handler = { - w_name : longname; w_block : block -} +and switch_handler = { w_name : constructor_name; w_block : block } -and present_handler = { - p_cond : exp; p_block : block -} +and present_handler = { p_cond : exp; p_block : block } and var_dec = { - v_ident : ident; mutable v_type : ty; v_last : last; v_loc : location -} + v_ident : var_ident; + mutable v_type : ty; + v_last : last; + v_loc : location } -and last = - | Var | Last of static_exp option +and last = Var | Last of static_exp option -type type_dec = { - t_name : name; t_desc : type_desc; t_loc : location -} +type type_dec = { t_name : name; t_desc : type_dec_desc; t_loc : location } -and type_desc = - | Type_abs | Type_enum of name list | Type_struct of structure +and type_dec_desc = Type_abs | Type_enum of name list | Type_struct of structure type contract = { - c_assume : exp; c_enforce : exp; c_controllables : var_dec list; - c_local : var_dec list; c_eq : eq list -} + c_assume : exp; + c_enforce : exp; + c_local : var_dec list; + c_eq : eq list } type node_dec = { - n_name : name; n_statefull : bool; n_input : var_dec list; - n_output : var_dec list; n_local : var_dec list; - n_contract : contract option; n_equs : eq list; n_loc : location; + n_name : name; + n_statefull : bool; + n_input : var_dec list; + n_output : var_dec list; + n_local : var_dec list; + n_contract : contract option; + n_equs : eq list; n_loc : location; n_params : param list; - n_params_constraints : size_constraint list -} + n_params_constraints : size_constraint list } type const_dec = { - c_name : name; c_type : ty; c_value : static_exp; c_loc : location } + c_name : name; + c_type : ty; + c_value : static_exp; + c_loc : location } type program = { - p_pragmas : (name * string) list; p_opened : name list; - p_types : type_dec list; p_nodes : node_dec list; - p_consts : const_dec list -} + p_opened : name list; + p_types : type_dec list; + p_nodes : node_dec list; + p_consts : const_dec list } type signature = { - sig_name : name; sig_inputs : arg list; sig_statefull : bool; - sig_outputs : arg list; sig_params : param list -} + sig_name : name; + sig_inputs : arg list; + sig_statefull : bool; + sig_outputs : arg list; + sig_params : param list } -type interface = - interface_decl list +type interface = interface_decl list -and interface_decl = { - interf_desc : interface_desc; interf_loc : location -} +and interface_decl = { interf_desc : interface_desc; interf_loc : location } and interface_desc = - | Iopen of name | Itypedef of type_dec | Isignature of signature + | Iopen of name + | Itypedef of type_dec + | Isignature of signature (* Helper functions to create AST. *) let mk_exp desc ty = { e_desc = desc; e_ty = ty; e_loc = no_location; } -let mk_op op = { a_op = op; } +let mk_op ?(params=[]) ?(unsafe=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe } -let mk_op_desc ln params kind = - { op_name = ln; op_params = params; op_kind = kind } +let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = + Eapp(mk_op ~params:params ~unsafe:unsafe op, args, reset) let mk_type_dec name desc = { t_name = name; t_desc = desc; t_loc = no_location; } @@ -160,11 +169,15 @@ let mk_block ?(statefull = true) defnames eqs = { b_local = []; b_equs = eqs; b_defnames = defnames; b_statefull = statefull; b_loc = no_location } -let dfalse = mk_exp (Econst (Sconstructor Initial.pfalse)) (Tid Initial.pbool) -let dtrue = mk_exp (Econst (Sconstructor Initial.ptrue)) (Tid Initial.pbool) +let dfalse = + mk_exp (Econst (mk_static_exp (Sconstructor Initial.pfalse))) + (Tid Initial.pbool) +let dtrue = + mk_exp (Econst (mk_static_exp (Sconstructor Initial.ptrue))) + (Tid Initial.pbool) let mk_ifthenelse e1 e2 e3 = - { e3 with e_desc = Eapp(mk_op Eifthenelse, [e1; e2; e3]) } + { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] } let mk_simple_equation pat e = mk_equation ~statefull:false (Eeq(pat, e)) @@ -175,7 +188,7 @@ let mk_switch_equation ?(statefull = true) e l = (** @return a size exp operator from a Heptagon operator. *) let op_from_app app = match app.a_op with - | Ecall ( { op_name = op; op_kind = Efun }, _) -> op_from_app_name op + | Efun op -> op_from_app_name op | _ -> raise Not_static (** Translates a Heptagon exp into a static size exp. *) diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 8c788e1..e999f30 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -21,36 +21,36 @@ type iterator_type = | Ifold | Imapfold -type type_dec = - { t_name: name; - t_desc: tdesc; - t_loc: location } +type type_dec = { + t_name: name; + t_desc: tdesc; + t_loc: location } and tdesc = | Type_abs | Type_enum of name list | Type_struct of structure -and exp = - { e_desc: edesc; - mutable e_ck: ck; - mutable e_ty: ty; - e_loc: location } +and exp = { + e_desc: edesc; + mutable e_ck: ck; + mutable e_ty: ty; + e_loc: location } and edesc = | Econst of static_exp - | Evar of ident + | Evar of var_ident | Efby of static_exp option * exp (** static_exp fby exp *) - | Eapp of app * exp list * ident option + | Eapp of app * exp list * var_ident option (** app ~args=(exp,exp...) reset ~r=ident *) - | Ewhen of exp * longname * ident + | Ewhen of exp * constructor_name * var_ident (** exp when Constructor(ident) *) - | Emerge of ident * (longname * exp) list + | Emerge of var_ident * (constructor_name * exp) list (** merge ident (Constructor -> exp)+ *) - | Estruct of (longname * exp) list + | Estruct of (field_name * exp) list (** { field=exp; ... } *) - | Eiterator of iterator_type * app * static_exp * exp list * ident option + | Eiterator of iterator_type * app * static_exp * exp list * var_ident option (** map f <> (exp,exp...) reset ident *) and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } @@ -59,8 +59,8 @@ and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } and op = | Etuple (** (args) *) - | Efun of longname (** "Stateless" longname <> (args) reset r *) - | Enode of longname (** "Stateful" longname <> (args) reset r *) + | Efun of fun_name (** "Stateless" longname <> (args) reset r *) + | Enode of fun_name (** "Stateful" longname <> (args) reset r *) | Eifthenelse (** if arg1 then arg2 else arg3 *) | Efield (** arg1.a_param1 *) | Efield_update (** { arg1 with a_param1 = arg2 } *) @@ -79,7 +79,7 @@ and ct = and ck = | Cbase | Cvar of link ref - | Con of ck * longname * ident + | Con of ck * constructor_name * var_ident and link = | Cindex of int @@ -87,50 +87,46 @@ and link = and pat = | Etuplepat of pat list - | Evarpat of ident + | Evarpat of var_ident -type eq = - { eq_lhs : pat; - eq_rhs : exp; - eq_loc : location } +type eq = { + eq_lhs : pat; + eq_rhs : exp; + eq_loc : location } -type var_dec = - { v_ident : ident; - v_type : ty; - v_clock : ck } +type var_dec = { + v_ident : var_ident; + v_type : ty; + v_clock : ck } -type contract = - { c_assume : exp; - c_enforce : exp; - c_controllables : var_dec list; - c_local : var_dec list; - c_eq : eq list } +type contract = { + c_assume : exp; + c_enforce : exp; + c_local : var_dec list; + c_eq : eq list } -type node_dec = - { n_name : name; - n_input : var_dec list; - n_output : var_dec list; - n_contract : contract option; - n_local : var_dec list; - n_equs : eq list; - n_loc : location; - n_params : param list; - n_params_constraints : size_constraint list; - n_params_instances : (int list) list; }(*TODO commenter ou passer en env*) - -type const_dec = - { c_name : name; - c_value : static_exp; - c_loc : location } - -type program = - { p_pragmas: (name * string) list; - p_opened : name list; - p_types : type_dec list; - p_nodes : node_dec list; - p_consts : const_dec list } +type node_dec = { + n_name : name; + n_input : var_dec list; + n_output : var_dec list; + n_contract : contract option; + n_local : var_dec list; + n_equs : eq list; + n_loc : location; + n_params : param list; (** TODO CP mettre des petits commentaires *) + n_params_constraints : size_constr list; + n_params_instances : (static_exp list) list } +type const_dec = { + c_name : name; + c_value : static_exp; + c_loc : location } +type program = { + p_opened : name list; + p_types : type_dec list; + p_nodes : node_dec list; + p_consts : const_dec list } (*Helper functions to build the AST*) @@ -138,8 +134,7 @@ let mk_exp ?(exp_ty = Tprod []) ?(clock = Cbase) ?(loc = no_location) desc = { e_desc = desc; e_ty = exp_ty; e_ck = clock; e_loc = loc } let mk_var_dec ?(clock = Cbase) ident ty = - { v_ident = ident; v_type = ty; - v_clock = clock } + { v_ident = ident; v_type = ty; v_clock = clock } let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } @@ -159,7 +154,7 @@ let mk_node n_params_instances = pinst; } let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name = - { t_name = name; t_desc = type_desc; t_loc = loc } + t_name = name; t_desc = type_desc; t_loc = loc } let mk_op ?(op_params = []) ?(op_kind = Enode) lname = { op_name = lname; op_params = op_params; op_kind = op_kind } diff --git a/compiler/obc/java/java.ml b/compiler/obc/java/java.ml index 22afc79..2ff3bf0 100644 --- a/compiler/obc/java/java.ml +++ b/compiler/obc/java/java.ml @@ -164,8 +164,8 @@ let print_types java_dir headers tps = (******************************) type answer = - | Sing of var_name - | Mult of var_name list + | Sing of var_ident + | Mult of var_ident list let print_const ff c ts = match c with diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index c80a99c..46cedc9 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -13,33 +13,31 @@ open Names open Ident open Types -type var_name = ident -type type_name = longname -type fun_name = longname + type class_name = name type instance_name = longname type obj_name = name type op_name = longname -type field_name = longname type type_dec = { t_name : name; - t_desc : tdesc } + t_desc : tdesc; + t_loc : loc } and tdesc = | Type_abs | Type_enum of name list | Type_struct of (name * ty) list -type lhs = { l_desc : lhs_desc; l_ty : ty } +type lhs = { l_desc : lhs_desc; l_ty : ty; l_loc : loc } and lhs_desc = - | Lvar of var_name - | Lmem of var_name + | Lvar of var_ident + | Lmem of var_ident | Lfield of lhs * field_name | Larray of lhs * exp -and exp = { e_desc : exp_desc; e_ty : ty } +and exp = { e_desc : exp_desc; e_ty : ty; e_loc : loc } and exp_desc = | Elhs of lhs @@ -55,24 +53,26 @@ type obj_call = type method_name = | Mreset | Mstep - | Mother of name + | Mmethod of name type act = | Aassgn of lhs * exp | Acall of lhs list * obj_call * method_name * exp list - | Acase of exp * (longname * block) list - | Afor of var_name * static_exp * static_exp * block + | Acase of exp * (constructor_name * block) list + | Afor of var_ident * static_exp * static_exp * block and block = act list type var_dec = - { v_ident : var_name; - v_type : ty; (*v_controllable : bool*) } + { v_ident : var_ident; + v_type : ty; (* TODO should be here, v_controllable : bool*) + v_loc : loc } type obj_dec = { o_name : obj_name; o_class : instance_name; - o_size : static_exp; } + o_size : static_exp; + o_loc : loc } type method_def = { f_name : fun_name; @@ -85,11 +85,11 @@ type class_def = { c_name : class_name; c_mems : var_dec list; c_objs : obj_dec list; - c_methods: method_def list; } + c_methods: method_def list; + c_loc : loc } type program = - { p_pragmas: (name * string) list; - p_opened : name list; + { p_opened : name list; p_types : type_dec list; p_defs : class_def list } @@ -102,12 +102,12 @@ let mk_exp ?(ty=invalid_type) desc = let mk_lhs ?(ty=invalid_type) desc = { l_desc = desc; l_ty = ty } -let rec var_name x = +let rec var_ident x = match x with | Lvar x -> x | Lmem x -> x - | Lfield(x,_) -> var_name x - | Larray(l, _) -> var_name l + | Lfield(x,_) -> var_ident x + | Larray(l, _) -> var_ident l (** Returns whether an object of name n belongs to a list of var_dec. *) diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index 9f5f607..de3e35b 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -192,3 +192,10 @@ let rec assocd value = function k else assocd value l + +(** Mapfold *) +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) + ([],acc) l in + List.rev l, acc + diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index 28257ba..9b22ff9 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -153,3 +153,5 @@ val memd_assoc : 'b -> ('a * 'b) list -> bool (** Same as List.assoc but searching for a data and returning the key. *) val assocd: 'b -> ('a * 'b) list -> 'a +(** Mapfold *) +val mapfold: ('a -> 'b -> 'c * 'a) -> 'a -> 'b list -> 'c list * 'a \ No newline at end of file