diff --git a/compiler/global/static.ml b/compiler/global/static.ml index bf572fb..06ad6f4 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -17,10 +17,14 @@ open Names open Format -type op = | Splus | Sminus | Stimes | Sdiv - -type size_exp = - | Sconst of int | Svar of name | Sop of op * size_exp * size_exp +type static_exp = + | Sint of int + | Sfloat of float + | Sbool of bool + | Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *) + | Sarray of static_exp list (** [ e1, e2, e3 ] *) + | Svar of name + | Sop of longname * static_exp list (** defined ops for now pervasives *) (** Constraints on size expressions. *) type size_constraint = @@ -66,7 +70,7 @@ let rec simplify env = in Sconst n | (_, _) -> Sop (op, e1, e2)) -(** [int_of_size_exp env e] returns the value of the expression +(** [int_of_static_exp env e] returns the value of the expression [e] in the environment [env], mapping vars to integers. Raises Instanciation_failed if it cannot be computed (if a var has no value).*) let int_of_size_exp env e = @@ -114,7 +118,7 @@ let rec solve const_env = (** Substitutes variables in the size exp with their value in the map (mapping vars to size exps). *) -let rec size_exp_subst m = +let rec static_exp_subst m = function | Svar n -> (try List.assoc n m with | Not_found -> Svar n) | Sop (op, e1, e2) -> Sop (op, size_exp_subst m e1, size_exp_subst m e2) @@ -132,13 +136,13 @@ let instanciate_constr m constr = let op_to_string = function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/" -let rec print_size_exp ff = +let rec print_static_exp ff = function | Sconst i -> fprintf ff "%d" i | Svar id -> fprintf ff "%s" id | Sop (op, e1, e2) -> fprintf ff "@[(%a %s %a)@]" - print_size_exp e1 (op_to_string op) print_size_exp e2 + print_static_exp e1 (op_to_string op) print_static_exp e2 let print_size_constraint ff = function | Cequal (e1, e2) -> diff --git a/compiler/global/types.ml b/compiler/global/types.ml index ab66efd..7637d63 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -10,7 +10,7 @@ open Static open Names type ty = - | Tprod of ty list | Tid of longname | Tarray of ty * size_exp + | Tprod of ty list | Tid of longname | Tarray of ty * static_exp let invalid_type = Tprod [] @@ -24,4 +24,4 @@ let rec print_type ff = function fprintf ff "@[%a@]" (print_list_r print_type "(" " *" ")") ty_list | Tid id -> print_longname ff id | Tarray (ty, n) -> - fprintf ff "@[%a^%a@]" print_type ty print_size_exp n + fprintf ff "@[%a^%a@]" print_type ty print_static_exp n diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index f4b3cfd..99b485c 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -200,7 +200,7 @@ let element_type ty = | Tarray (ty, _) -> ty | _ -> error (Esubscripted_value_not_an_array ty) -let size_exp ty = +let static_exp ty = match ty with | Tarray (_, e) -> e | _ -> error (Esubscripted_value_not_an_array ty) @@ -354,7 +354,7 @@ let simplify_type loc const_env ty = Instanciation_failed -> message loc (Etype_should_be_static ty) let rec subst_type_vars m = function - | Tarray(ty, e) -> Tarray(subst_type_vars m ty, size_exp_subst m e) + | Tarray(ty, e) -> Tarray(subst_type_vars m ty, static_exp_subst m e) | Tprod l -> Tprod (List.map (subst_type_vars m) l) | t -> t @@ -605,7 +605,7 @@ and typing_array_op statefull h op e_list = match op, e_list with | Erepeat, [e1; e2] -> let typed_e2 = expect statefull h (Tid Initial.pint) e2 in - let e2 = size_exp_of_exp e2 in + let e2 = static_exp_of_exp e2 in let typed_e1, t1 = typing statefull h e1 in add_size_constraint (Clequal (Sconst 1, e2)); Tarray (t1, e2), op, [typed_e1; typed_e2] @@ -628,9 +628,9 @@ and typing_array_op statefull h op e_list = let typed_idx2 = expect statefull h (Tid Initial.pint) idx2 in let typed_e, t1 = typing statefull h e in (*Create the expression to compute the size of the array *) - let e1 = Sop (Sminus, size_exp_of_exp idx2, size_exp_of_exp idx1) in - let e2 = Sop (Splus, e1, Sconst 1) in - add_size_constraint (Clequal (Sconst 1, e2)); + let e1 = SOp (SMinus, static_exp_of_exp idx2, static_exp_of_exp idx1) in + let e2 = SOp (SPlus, e1, SConst 1) in + add_size_constr (LEqual (SConst 1, e2)); Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2] | Econcat, [e1; e2] -> let typed_e1, t1 = typing statefull h e1 in @@ -640,7 +640,7 @@ and typing_array_op statefull h op e_list = with TypingError(kind) -> message e1.e_loc kind end; - let n = Sop (Splus, size_exp t1, size_exp t2) in + let n = SOp (SPlus, static_exp t1, static_exp t2) in Tarray (element_type t1, n), op, [typed_e1; typed_e2] | Eiterator (it, ({ op_name = f; op_params = params; op_kind = k } as op_desc), reset), @@ -655,7 +655,7 @@ and typing_array_op statefull h op e_list = instanciate_constr m ty_desc.node_params_constraints in let result_ty_list = List.map (subst_type_vars m) result_ty_list in let typed_e = expect statefull h (Tid Initial.pint) e in - let e = size_exp_of_exp e in + let e = static_exp_of_exp e in let ty, typed_e_list = typing_iterator statefull h it e expected_ty_list result_ty_list e_list in add_size_constraint (Clequal (Sconst 1, e)); diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index a1f5f11..41cb8a6 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -41,7 +41,7 @@ and print_c ff = function | Carray (n, c) -> print_c ff c; fprintf ff "^"; - print_size_exp ff n + print_static_exp ff n and print_vd ff { v_ident = n; v_type = ty; v_last = last } = fprintf ff "@["; @@ -83,7 +83,7 @@ and print_exp ff e = and print_call_params ff = function | [] -> () - | l -> print_list_r print_size_exp "<<" "," ">>" ff l + | l -> print_list_r print_static_exp "<<" "," ">>" ff l and print_op ff op e_list = match op, e_list with @@ -123,7 +123,7 @@ and print_array_op ff op e_list = print_exp ff e2 | Eselect idx_list, [e] -> print_exp ff e; - print_list_r print_size_exp "[" "][" "]" ff idx_list + print_list_r print_static_exp "[" "][" "]" ff idx_list | Eselect_dyn, e::defe::idx_list -> fprintf ff "@[("; print_exp ff e; @@ -134,7 +134,7 @@ and print_array_op ff op e_list = fprintf ff "(@["; print_exp ff e1; fprintf ff " with "; - print_list_r print_size_exp "[" "][" "]" ff idx_list; + print_list_r print_static_exp "[" "][" "]" ff idx_list; fprintf ff " = "; print_exp ff e2; fprintf ff ")@]" @@ -293,7 +293,7 @@ let print_const_dec ff c = fprintf ff " : "; print_type ff c.c_type; fprintf ff " = "; - print_size_exp ff c.c_value; + print_static_exp ff c.c_value; fprintf ff "@.@]" let print_contract ff {c_local = l; diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 1c2f911..67ad86d 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -1,4 +1,4 @@ -(**************************************************************************) + (**************************************************************************) (* *) (* Heptagon *) (* *) @@ -26,50 +26,39 @@ and desc = | Econst of const | Evar of ident | Econstvar of name - | Elast of ident | Etuple of exp list - | Eapp of app * exp list + | Elast of ident + | Epre of static_exp option * exp + | Efby of exp * exp | Efield of exp * longname | Estruct of (longname * exp) list | Earray of exp list + | Eapp of app * exp list * exp option + | Eiterator of iterator_type * app * static_exp * exp list * exp option -and app = - { a_op : op; } + +and app = { a_op: op; a_params: static_exp list } and op = - | Epre of const option - | Efby - | Earrow + | Efun of longname + | Enode of longname | Eifthenelse - | Earray_op of array_op - | Efield_update of longname - | Ecall of op_desc * exp option (** [op_desc] is the function called [exp - option] is the optional reset condition *) - -and array_op = + | Earrow + | Efield_update of longname (* field name args would be [record ; value] *) + | Earray | Erepeat - | Eselect of size_exp list + | Eselect | Eselect_dyn - | Eupdate of size_exp list + | Eupdate | Eselect_slice | Econcat - | Eiterator of iterator_type * op_desc * exp option (** [op_desc] node to map - [exp option] reset *) -and op_desc = { op_name : longname; op_params: size_exp list; op_kind: op_kind } -and op_kind = | Efun | Enode - -and const = - | Cint of int - | Cfloat of float - | Cconstr of longname - | Carray of size_exp * const and pat = - | Etuplepat of pat list | Evarpat of ident + | Etuplepat of pat list + | Evarpat of ident -type eq = - { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location } +type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location } and eqdesc = | Eautomaton of state_handler list @@ -128,7 +117,7 @@ type node_dec = { } type const_dec = { - c_name : name; c_type : ty; c_value : size_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; @@ -193,13 +182,13 @@ let op_from_app app = | _ -> raise Not_static (** Translates a Heptagon exp into a static size exp. *) -let rec size_exp_of_exp e = +let rec static_exp_of_exp e = match e.e_desc with | Econstvar n -> Svar n | Econst (Cint i) -> Sconst i | Eapp (app, [ e1; e2 ]) -> let op = op_from_app app - in Sop (op, size_exp_of_exp e1, size_exp_of_exp e2) + in Sop (op, static_exp_of_exp e1, static_exp_of_exp e2) | _ -> raise Not_static (** @return the set of variables defined in [pat]. *) diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml index bb42c25..3117407 100644 --- a/compiler/heptagon/parsing/scoping.ml +++ b/compiler/heptagon/parsing/scoping.ml @@ -114,7 +114,7 @@ let op_from_app loc app = | _ -> Error.message loc Error.Estatic_exp_expected let check_const_vars = ref true -let rec translate_size_exp const_env e = match e.e_desc with +let rec translate_static_exp const_env e = match e.e_desc with | Evar n -> if !check_const_vars & not (NamesEnv.mem n const_env) then Error.message e.e_loc (Error.Econst_var n) @@ -123,8 +123,8 @@ let rec translate_size_exp const_env e = match e.e_desc with | Econst (Cint i) -> Sconst i | Eapp(app, [e1;e2]) -> let op = op_from_app e.e_loc app in - Sop(op, translate_size_exp const_env e1, - translate_size_exp const_env e2) + Sop(op, translate_static_exp const_env e1, + translate_static_exp const_env e2) | _ -> Error.message e.e_loc Error.Estatic_exp_expected let rec translate_type const_env = function @@ -132,7 +132,7 @@ let rec translate_type const_env = function | Tid ln -> Types.Tid ln | Tarray (ty, e) -> let ty = translate_type const_env ty in - Types.Tarray (ty, translate_size_exp const_env e) + Types.Tarray (ty, translate_static_exp const_env e) and translate_exp const_env env e = { Heptagon.e_desc = translate_desc e.e_loc const_env env e.e_desc; @@ -155,14 +155,14 @@ and translate_app const_env env app = and translate_op_desc const_env desc = { Heptagon.op_name = desc.op_name; Heptagon.op_params = - List.map (translate_size_exp const_env) desc.op_params; + List.map (translate_static_exp const_env) desc.op_params; Heptagon.op_kind = translate_op_kind desc.op_kind } and translate_array_op const_env env = function | Eselect e_list -> - Heptagon.Eselect (List.map (translate_size_exp const_env) e_list) + Heptagon.Eselect (List.map (translate_static_exp const_env) e_list) | Eupdate e_list -> - Heptagon.Eupdate (List.map (translate_size_exp const_env) e_list) + Heptagon.Eupdate (List.map (translate_static_exp const_env) e_list) | Erepeat -> Heptagon.Erepeat | Eselect_slice -> Heptagon.Eselect_slice | Econcat -> Heptagon.Econcat @@ -187,7 +187,7 @@ and translate_desc loc const_env env = function let e_list = List.map (translate_exp const_env env) e_list in (match e_list with | [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] -> - Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c)) + Heptagon.Econst (Heptagon.Carray (Heptagon.static_exp_of_exp e1, c)) | _ -> Heptagon.Eapp (translate_app const_env env app, e_list) ) | Eapp (app, e_list) -> @@ -310,7 +310,7 @@ let translate_typedec const_env ty = let translate_const_dec const_env cd = { Heptagon.c_name = cd.c_name; Heptagon.c_type = translate_type const_env cd.c_type; - Heptagon.c_value = translate_size_exp const_env cd.c_value; + Heptagon.c_value = translate_static_exp const_env cd.c_value; Heptagon.c_loc = cd.c_loc; } let translate_program p = diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 0418f03..a8d36f8 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -8,7 +8,6 @@ (**************************************************************************) (* removing reset statements *) -(* $Id$ *) open Misc open Ident diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 138be14..bf78ad5 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -222,7 +222,7 @@ let rec application env { Heptagon.a_op = op; } e_list = and translate_array_op env op e_list = match op, e_list with | Heptagon.Erepeat, [e; idx] -> - Erepeat (size_exp_of_exp idx, e) + Erepeat (static_exp_of_exp idx, e) | Heptagon.Eselect idx_list, [e] -> Eselect (idx_list, e) | Heptagon.Eselect_dyn, e::defe::idx_list -> @@ -230,13 +230,13 @@ and translate_array_op env op e_list = | Heptagon.Eupdate idx_list, [e1;e2] -> Eupdate (idx_list, e1, e2) | Heptagon.Eselect_slice, [e; idx1; idx2] -> - Eselect_slice (size_exp_of_exp idx1, size_exp_of_exp idx2, e) + Eselect_slice (static_exp_of_exp idx1, static_exp_of_exp idx2, e) | Heptagon.Econcat, [e1; e2] -> Econcat (e1, e2) | Heptagon.Eiterator(it, op_desc, reset), idx::e_list -> Eiterator(translate_iterator_type it, translate_op_desc op_desc, - size_exp_of_exp idx, e_list, + static_exp_of_exp idx, e_list, translate_reset reset) let rec translate env diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index eaf4d3f..ebf92d8 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -38,41 +38,35 @@ and exp = e_loc: location } and edesc = - | Econst of const + | Econst of static_exp | Evar of ident | Econstvar of name - | Efby of const option * exp | Etuple of exp list - | 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 *) - + | Efby of static_exp option * exp + | Eapp of app * exp list * ident option + (** ident option is the optional reset *) | 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 - | Earray of exp list - | Earray_op of array_op + | Eiterator of iterator_type * app * static_exp * exp list * ident option -and array_op = - | Erepeat of size_exp * exp - | Eselect of size_exp list * exp (*indices, array*) - | Eselect_dyn of exp list * exp * exp (* indices, array, default*) - | Eupdate of size_exp list * exp * exp (*indices, array, value*) - | Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, - array*) - | Econcat of exp * exp - | Eiterator of iterator_type * op_desc * size_exp * exp list * ident option - (** [op_desc] is the function iterated, [size_exp] is the size of the - iteration, [exp list] is the passed arguments, [ident option] is the - optional reset condition *) -and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind } -and op_kind = | Efun | Enode +and app = { a_op: op; a_params: static_exp list } + +and op = + | Efun of longname + | Enode of longname + | Eifthenelse + | Efield_update of longname (* field name args would be [record ; value] *) + | Earray + | Erepeat + | Eselect + | Eselect_dyn + | Eupdate + | Eselect_slice + | Econcat + and ct = | Ck of ck @@ -91,7 +85,8 @@ and const = | Cint of int | Cfloat of float | Cconstr of longname - | Carray of size_exp * const + | Carray of static_exp * const + | Cop of and pat = | Etuplepat of pat list @@ -129,7 +124,7 @@ type node_dec = type const_dec = { c_name : name; - c_value : size_exp; + c_value : static_exp; c_loc : location; } type program = diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index a29c825..a3d33b1 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -51,10 +51,10 @@ let rec print_c ff = function | Cint i -> fprintf ff "%d" i | Cfloat f -> fprintf ff "%f" f | Cconstr tag -> print_longname ff tag - | Carray (n, c) -> fprintf ff "%a^%a" print_c c print_size_exp n + | Carray (n, c) -> fprintf ff "%a^%a" print_c c print_static_exp n let rec print_params ff l = - fprintf ff "@[<2>%a@]" (print_list_r print_size_exp "<<"","">>") l + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "<<"","">>") l and print_node_params ff l = fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") l @@ -66,7 +66,7 @@ and print_vd_tuple ff l = fprintf ff "@[<2>%a@]" (print_list_r print_vd "("","")") l and print_index ff idx = - fprintf ff "@[<2>%a@]" (print_list print_size_exp "[""][""]") idx + fprintf ff "@[<2>%a@]" (print_list print_static_exp "[""][""]") idx and print_dyn_index ff idx = fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx @@ -116,7 +116,7 @@ and print_exp_desc ff = function and print_array_op ff = function - | Erepeat (n, e) -> fprintf ff "%a^%a" print_exp e print_size_exp n + | Erepeat (n, e) -> fprintf ff "%a^%a" print_exp e print_static_exp n | Eselect (idx, e) -> fprintf ff "%a%a" print_exp e print_index idx | Eselect_dyn (idx, e1, e2) -> fprintf ff "%a%a default %a" @@ -126,13 +126,13 @@ and print_array_op ff = function print_exp e1 print_index idx print_exp e2 | Eselect_slice (idx1, idx2, e) -> fprintf ff "%a[%a..%a]" - print_exp e print_size_exp idx1 print_size_exp idx2 + print_exp e print_static_exp idx1 print_static_exp idx2 | Econcat (e1, e2) -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 | Eiterator (it, f, n, e_list, r) -> fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" (iterator_to_string it) print_op f - print_size_exp n + print_static_exp n print_exp_tuple e_list print_every r @@ -175,7 +175,7 @@ and print_field ff field = let print_const_dec ff c = fprintf ff "const %a = %a" print_name c.c_name - print_size_exp c.c_value + print_static_exp c.c_value let print_contract ff { c_local = l; c_eq = eqs; diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 67d3bc5..e71e2c5 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -9,22 +9,22 @@ open Types open Misc (** Error Kind *) -type err_kind = | Enot_size_exp +type err_kind = | Enot_static_exp let err_message ?(exp=void) ?(loc=exp.e_loc) = function - | Enot_size_exp -> - Printf.eprintf "The expression %a should be a size_exp.@." + | Enot_static_exp -> + Printf.eprintf "The expression %a should be a static_exp.@." print_exp exp; raise Error -let rec size_exp_of_exp e = +let rec static_exp_of_exp e = match e.e_desc with | Econstvar n -> Svar n | Econst (Cint i) -> Sconst i | Ecall(op, [e1;e2], _) -> let sop = op_from_app_name op.op_name in - Sop(sop, size_exp_of_exp e1, size_exp_of_exp e2) - | _ -> err_message ~exp:e Enot_size_exp + Sop(sop, static_exp_of_exp e1, static_exp_of_exp e2) + | _ -> err_message ~exp:e Enot_static_exp (** @return the list of bounds of an array type*) let rec bounds_list ty = diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index c7d8fe3..be107df 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -189,7 +189,7 @@ array_op: { Eselect_slice(i1, i2, e) } | e1=exp AROBASE e2=exp { Econcat(e1,e2) } | LPAREN f=iterator LPAREN op=funop RPAREN - DOUBLE_LESS p=e_param DOUBLE_GREATER /* une seule dimension ? */ + DOUBLE_LESS p=e_param DOUBLE_GREATER RPAREN a=exps r=reset { Eiterator(f,op,p,a,r) } /* Static indexes [p1][p2]... */ @@ -214,7 +214,7 @@ reset: r=option(RESET,ident) { r } funop: ln=longname p=params(e_param) { mk_op ~op_kind:Enode ~op_params:p ln } -e_param: e=exp { size_exp_of_exp e } +e_param: e=exp { static_exp_of_exp e } n_param: n=NAME { mk_param n } params(param): | /*empty*/ { [] } diff --git a/compiler/minils/sequential/mls2obc.ml b/compiler/minils/sequential/mls2obc.ml index 7f37d91..1d4a04c 100644 --- a/compiler/minils/sequential/mls2obc.ml +++ b/compiler/minils/sequential/mls2obc.ml @@ -59,7 +59,7 @@ let rec translate_type const_env = function | Types.Tid id when id = Initial.pbool -> Tbool | Types.Tid id -> Tid id | Types.Tarray (ty, n) -> - Tarray (translate_type const_env ty, int_of_size_exp const_env n) + Tarray (translate_type const_env ty, int_of_static_exp const_env n) | Types.Tprod ty -> assert false let rec translate_const const_env = function @@ -67,7 +67,7 @@ let rec translate_const const_env = function | Minils.Cfloat v -> Cfloat v | Minils.Cconstr c -> Cconstr c | Minils.Carray (n, c) -> - Carray (int_of_size_exp const_env n, translate_const const_env c) + Carray (int_of_static_exp const_env n, translate_const const_env c) let rec translate_pat map = function | Minils.Evarpat x -> [ var_from_name map x ] @@ -81,7 +81,7 @@ let rec translate const_env map (m, si, j, s) match desc with | Minils.Econst v -> Const (translate_const const_env v) | Minils.Evar n -> Lhs (var_from_name map n) - | Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (Svar n))) + | Minils.Econstvar n -> Const (Cint (int_of_static_exp const_env (Svar n))) | Minils.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Efun }, e_list, _) when Mls_utils.is_op n -> Op (n, List.map (translate const_env map (m, si, j, s)) e_list) @@ -105,7 +105,7 @@ let rec translate const_env map (m, si, j, s) | Minils.Earray_op (Minils.Eselect (idx, e)) -> let e = translate const_env map (m, si, j, s) e in let idx_list = - List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx + List.map (fun e -> Const (Cint (int_of_static_exp const_env e))) idx in Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list) | _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false @@ -163,7 +163,7 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } (match op_kind with | Minils.Enode -> (Reinit o) :: si | Minils.Efun -> si) in - let params = List.map (int_of_size_exp const_env) params in + let params = List.map (int_of_static_exp const_env) params in let j = (o, (encode_longname_params n params), 1) :: j in let action = Step_ap (name_list, Context o, c_list) in let s = (match r, op_kind with @@ -192,8 +192,8 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } | Minils.Evarpat x, Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) -> - let idx1 = int_of_size_exp const_env idx1 in - let idx2 = int_of_size_exp const_env idx2 in + let idx1 = int_of_static_exp const_env idx1 in + let idx2 = int_of_static_exp const_env idx2 in let cpt = Ident.fresh "i" in let e = translate const_env map (m, si, j, s) e in let idx = @@ -210,7 +210,7 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } let x = var_from_name map x in let bounds = Mls_utils.bounds_list e1.Minils.e_ty in let e1 = translate const_env map (m, si, j, s) e1 in - let bounds = List.map (int_of_size_exp const_env) bounds in + let bounds = List.map (int_of_static_exp const_env) bounds in let idx = List.map (translate const_env map (m, si, j, s)) idx in let true_act = Assgn (x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in @@ -228,7 +228,7 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } let x = var_from_name map x in let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in let idx = - List.map (fun se -> Const (Cint (int_of_size_exp const_env se))) + List.map (fun se -> Const (Cint (int_of_static_exp const_env se))) idx in let action = Assgn (lhs_of_idx_list x idx, translate const_env map (m, si, j, s) e2) @@ -239,7 +239,7 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } Minils.Earray_op (Minils.Erepeat (n, e)) -> let cpt = Ident.fresh "i" in let action = - For (cpt, 0, int_of_size_exp const_env n, + For (cpt, 0, int_of_static_exp const_env n, Assgn (Array (var_from_name map x, Lhs (Var cpt)), translate const_env map (m, si, j, s) e)) in @@ -254,8 +254,8 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } | Types.Tarray (_, n1), Types.Tarray (_, n2) -> let e1 = translate const_env map (m, si, j, s) e1 in let e2 = translate const_env map (m, si, j, s) e2 in - let n1 = int_of_size_exp const_env n1 in - let n2 = int_of_size_exp const_env n2 in + let n1 = int_of_static_exp const_env n1 in + let n2 = int_of_static_exp const_env n2 in let a1 = For (cpt1, 0, n1, Assgn (Array (x, Lhs (Var cpt1)), @@ -279,12 +279,12 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } let c_list = List.map (translate const_env map (m, si, j, s)) e_list in let o = gen_obj_name f in - let n = int_of_size_exp const_env n in + let n = int_of_static_exp const_env n in let si = (match k with | Minils.Efun -> si | Minils.Enode -> (Reinit o) :: si) in - let params = List.map (int_of_size_exp const_env) params in + let params = List.map (int_of_static_exp const_env) params in let j = (o, (encode_longname_params f params), n) :: j in let x = Ident.fresh "i" in let action = diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index 2ae30e4..12bcadf 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -57,7 +57,7 @@ let rec collect_exp nodes env e = | Ecall( { op_name = ln; op_params = params; op_kind = _ }, e_list, _) -> List.iter (collect_exp nodes env) e_list; - let params = List.map (int_of_size_exp env) params in + let params = List.map (int_of_static_exp env) params in call_node_instance nodes ln params | Earray_op op -> collect_array_exp nodes env op @@ -74,7 +74,7 @@ and collect_array_exp nodes env = function collect_exp nodes env e | Eiterator (_, { op_name = ln; op_params = params }, _, e_list, _) -> List.iter (collect_exp nodes env) e_list; - let params = List.map (int_of_size_exp env) params in + let params = List.map (int_of_static_exp env) params in call_node_instance nodes ln params and collect_eqs nodes env eq =