Proposition 1.
This commit is contained in:
parent
7918332353
commit
d58e83a985
|
@ -17,10 +17,14 @@
|
||||||
open Names
|
open Names
|
||||||
open Format
|
open Format
|
||||||
|
|
||||||
type op = | Splus | Sminus | Stimes | Sdiv
|
type static_exp =
|
||||||
|
| Sint of int
|
||||||
type size_exp =
|
| Sfloat of float
|
||||||
| Sconst of int | Svar of name | Sop of op * size_exp * size_exp
|
| 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. *)
|
(** Constraints on size expressions. *)
|
||||||
type size_constraint =
|
type size_constraint =
|
||||||
|
@ -66,7 +70,7 @@ let rec simplify env =
|
||||||
in Sconst n
|
in Sconst n
|
||||||
| (_, _) -> Sop (op, e1, e2))
|
| (_, _) -> 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
|
[e] in the environment [env], mapping vars to integers. Raises
|
||||||
Instanciation_failed if it cannot be computed (if a var has no value).*)
|
Instanciation_failed if it cannot be computed (if a var has no value).*)
|
||||||
let int_of_size_exp env e =
|
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
|
(** Substitutes variables in the size exp with their value
|
||||||
in the map (mapping vars to size exps). *)
|
in the map (mapping vars to size exps). *)
|
||||||
let rec size_exp_subst m =
|
let rec static_exp_subst m =
|
||||||
function
|
function
|
||||||
| Svar n -> (try List.assoc n m with | Not_found -> Svar n)
|
| 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)
|
| 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 =
|
let op_to_string =
|
||||||
function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/"
|
function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/"
|
||||||
|
|
||||||
let rec print_size_exp ff =
|
let rec print_static_exp ff =
|
||||||
function
|
function
|
||||||
| Sconst i -> fprintf ff "%d" i
|
| Sconst i -> fprintf ff "%d" i
|
||||||
| Svar id -> fprintf ff "%s" id
|
| Svar id -> fprintf ff "%s" id
|
||||||
| Sop (op, e1, e2) ->
|
| Sop (op, e1, e2) ->
|
||||||
fprintf ff "@[(%a %s %a)@]"
|
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
|
let print_size_constraint ff = function
|
||||||
| Cequal (e1, e2) ->
|
| Cequal (e1, e2) ->
|
||||||
|
|
|
@ -10,7 +10,7 @@ open Static
|
||||||
open Names
|
open Names
|
||||||
|
|
||||||
type ty =
|
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 []
|
let invalid_type = Tprod []
|
||||||
|
|
||||||
|
@ -24,4 +24,4 @@ let rec print_type ff = function
|
||||||
fprintf ff "@[<hov2>%a@]" (print_list_r print_type "(" " *" ")") ty_list
|
fprintf ff "@[<hov2>%a@]" (print_list_r print_type "(" " *" ")") ty_list
|
||||||
| Tid id -> print_longname ff id
|
| Tid id -> print_longname ff id
|
||||||
| Tarray (ty, n) ->
|
| Tarray (ty, n) ->
|
||||||
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_size_exp n
|
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_static_exp n
|
||||||
|
|
|
@ -200,7 +200,7 @@ let element_type ty =
|
||||||
| Tarray (ty, _) -> ty
|
| Tarray (ty, _) -> ty
|
||||||
| _ -> error (Esubscripted_value_not_an_array ty)
|
| _ -> error (Esubscripted_value_not_an_array ty)
|
||||||
|
|
||||||
let size_exp ty =
|
let static_exp ty =
|
||||||
match ty with
|
match ty with
|
||||||
| Tarray (_, e) -> e
|
| Tarray (_, e) -> e
|
||||||
| _ -> error (Esubscripted_value_not_an_array ty)
|
| _ -> 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)
|
Instanciation_failed -> message loc (Etype_should_be_static ty)
|
||||||
|
|
||||||
let rec subst_type_vars m = function
|
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)
|
| Tprod l -> Tprod (List.map (subst_type_vars m) l)
|
||||||
| t -> t
|
| t -> t
|
||||||
|
|
||||||
|
@ -605,7 +605,7 @@ and typing_array_op statefull h op e_list =
|
||||||
match op, e_list with
|
match op, e_list with
|
||||||
| Erepeat, [e1; e2] ->
|
| Erepeat, [e1; e2] ->
|
||||||
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
|
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
|
let typed_e1, t1 = typing statefull h e1 in
|
||||||
add_size_constraint (Clequal (Sconst 1, e2));
|
add_size_constraint (Clequal (Sconst 1, e2));
|
||||||
Tarray (t1, e2), op, [typed_e1; typed_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_idx2 = expect statefull h (Tid Initial.pint) idx2 in
|
||||||
let typed_e, t1 = typing statefull h e in
|
let typed_e, t1 = typing statefull h e in
|
||||||
(*Create the expression to compute the size of the array *)
|
(*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 e1 = SOp (SMinus, static_exp_of_exp idx2, static_exp_of_exp idx1) in
|
||||||
let e2 = Sop (Splus, e1, Sconst 1) in
|
let e2 = SOp (SPlus, e1, SConst 1) in
|
||||||
add_size_constraint (Clequal (Sconst 1, e2));
|
add_size_constr (LEqual (SConst 1, e2));
|
||||||
Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
|
Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
|
||||||
| Econcat, [e1; e2] ->
|
| Econcat, [e1; e2] ->
|
||||||
let typed_e1, t1 = typing statefull h e1 in
|
let typed_e1, t1 = typing statefull h e1 in
|
||||||
|
@ -640,7 +640,7 @@ and typing_array_op statefull h op e_list =
|
||||||
with
|
with
|
||||||
TypingError(kind) -> message e1.e_loc kind
|
TypingError(kind) -> message e1.e_loc kind
|
||||||
end;
|
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]
|
Tarray (element_type t1, n), op, [typed_e1; typed_e2]
|
||||||
| Eiterator (it, ({ op_name = f; op_params = params;
|
| Eiterator (it, ({ op_name = f; op_params = params;
|
||||||
op_kind = k } as op_desc), reset),
|
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
|
instanciate_constr m ty_desc.node_params_constraints in
|
||||||
let result_ty_list = List.map (subst_type_vars m) result_ty_list 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 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
|
let ty, typed_e_list = typing_iterator statefull h it e
|
||||||
expected_ty_list result_ty_list e_list in
|
expected_ty_list result_ty_list e_list in
|
||||||
add_size_constraint (Clequal (Sconst 1, e));
|
add_size_constraint (Clequal (Sconst 1, e));
|
||||||
|
|
|
@ -41,7 +41,7 @@ and print_c ff = function
|
||||||
| Carray (n, c) ->
|
| Carray (n, c) ->
|
||||||
print_c ff c;
|
print_c ff c;
|
||||||
fprintf ff "^";
|
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 } =
|
and print_vd ff { v_ident = n; v_type = ty; v_last = last } =
|
||||||
fprintf ff "@[<v>";
|
fprintf ff "@[<v>";
|
||||||
|
@ -83,7 +83,7 @@ and print_exp ff e =
|
||||||
|
|
||||||
and print_call_params ff = function
|
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 =
|
and print_op ff op e_list =
|
||||||
match op, e_list with
|
match op, e_list with
|
||||||
|
@ -123,7 +123,7 @@ and print_array_op ff op e_list =
|
||||||
print_exp ff e2
|
print_exp ff e2
|
||||||
| Eselect idx_list, [e] ->
|
| Eselect idx_list, [e] ->
|
||||||
print_exp ff 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 ->
|
| Eselect_dyn, e::defe::idx_list ->
|
||||||
fprintf ff "@[(";
|
fprintf ff "@[(";
|
||||||
print_exp ff e;
|
print_exp ff e;
|
||||||
|
@ -134,7 +134,7 @@ and print_array_op ff op e_list =
|
||||||
fprintf ff "(@[";
|
fprintf ff "(@[";
|
||||||
print_exp ff e1;
|
print_exp ff e1;
|
||||||
fprintf ff " with ";
|
fprintf ff " with ";
|
||||||
print_list_r print_size_exp "[" "][" "]" ff idx_list;
|
print_list_r print_static_exp "[" "][" "]" ff idx_list;
|
||||||
fprintf ff " = ";
|
fprintf ff " = ";
|
||||||
print_exp ff e2;
|
print_exp ff e2;
|
||||||
fprintf ff ")@]"
|
fprintf ff ")@]"
|
||||||
|
@ -293,7 +293,7 @@ let print_const_dec ff c =
|
||||||
fprintf ff " : ";
|
fprintf ff " : ";
|
||||||
print_type ff c.c_type;
|
print_type ff c.c_type;
|
||||||
fprintf ff " = ";
|
fprintf ff " = ";
|
||||||
print_size_exp ff c.c_value;
|
print_static_exp ff c.c_value;
|
||||||
fprintf ff "@.@]"
|
fprintf ff "@.@]"
|
||||||
|
|
||||||
let print_contract ff {c_local = l;
|
let print_contract ff {c_local = l;
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
(**************************************************************************)
|
(**************************************************************************)
|
||||||
(* *)
|
(* *)
|
||||||
(* Heptagon *)
|
(* Heptagon *)
|
||||||
(* *)
|
(* *)
|
||||||
|
@ -26,50 +26,39 @@ and desc =
|
||||||
| Econst of const
|
| Econst of const
|
||||||
| Evar of ident
|
| Evar of ident
|
||||||
| Econstvar of name
|
| Econstvar of name
|
||||||
| Elast of ident
|
|
||||||
| Etuple of exp list
|
| 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
|
| Efield of exp * longname
|
||||||
| Estruct of (longname * exp) list
|
| Estruct of (longname * exp) list
|
||||||
| Earray of 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 =
|
and op =
|
||||||
| Epre of const option
|
| Efun of longname
|
||||||
| Efby
|
| Enode of longname
|
||||||
| Earrow
|
|
||||||
| Eifthenelse
|
| Eifthenelse
|
||||||
| Earray_op of array_op
|
| Earrow
|
||||||
| Efield_update of longname
|
| Efield_update of longname (* field name args would be [record ; value] *)
|
||||||
| Ecall of op_desc * exp option (** [op_desc] is the function called [exp
|
| Earray
|
||||||
option] is the optional reset condition *)
|
|
||||||
|
|
||||||
and array_op =
|
|
||||||
| Erepeat
|
| Erepeat
|
||||||
| Eselect of size_exp list
|
| Eselect
|
||||||
| Eselect_dyn
|
| Eselect_dyn
|
||||||
| Eupdate of size_exp list
|
| Eupdate
|
||||||
| Eselect_slice
|
| Eselect_slice
|
||||||
| Econcat
|
| 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 =
|
and pat =
|
||||||
| Etuplepat of pat list | Evarpat of ident
|
| Etuplepat of pat list
|
||||||
|
| Evarpat of ident
|
||||||
|
|
||||||
type eq =
|
type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
|
||||||
{ eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
|
|
||||||
|
|
||||||
and eqdesc =
|
and eqdesc =
|
||||||
| Eautomaton of state_handler list
|
| Eautomaton of state_handler list
|
||||||
|
@ -128,7 +117,7 @@ type node_dec = {
|
||||||
}
|
}
|
||||||
|
|
||||||
type const_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 = {
|
type program = {
|
||||||
p_pragmas : (name * string) list; p_opened : name list;
|
p_pragmas : (name * string) list; p_opened : name list;
|
||||||
|
@ -193,13 +182,13 @@ let op_from_app app =
|
||||||
| _ -> raise Not_static
|
| _ -> raise Not_static
|
||||||
|
|
||||||
(** Translates a Heptagon exp into a static size exp. *)
|
(** 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
|
match e.e_desc with
|
||||||
| Econstvar n -> Svar n
|
| Econstvar n -> Svar n
|
||||||
| Econst (Cint i) -> Sconst i
|
| Econst (Cint i) -> Sconst i
|
||||||
| Eapp (app, [ e1; e2 ]) ->
|
| Eapp (app, [ e1; e2 ]) ->
|
||||||
let op = op_from_app app
|
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
|
| _ -> raise Not_static
|
||||||
|
|
||||||
(** @return the set of variables defined in [pat]. *)
|
(** @return the set of variables defined in [pat]. *)
|
||||||
|
|
|
@ -114,7 +114,7 @@ let op_from_app loc app =
|
||||||
| _ -> Error.message loc Error.Estatic_exp_expected
|
| _ -> Error.message loc Error.Estatic_exp_expected
|
||||||
|
|
||||||
let check_const_vars = ref true
|
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 ->
|
| Evar n ->
|
||||||
if !check_const_vars & not (NamesEnv.mem n const_env) then
|
if !check_const_vars & not (NamesEnv.mem n const_env) then
|
||||||
Error.message e.e_loc (Error.Econst_var n)
|
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
|
| Econst (Cint i) -> Sconst i
|
||||||
| Eapp(app, [e1;e2]) ->
|
| Eapp(app, [e1;e2]) ->
|
||||||
let op = op_from_app e.e_loc app in
|
let op = op_from_app e.e_loc app in
|
||||||
Sop(op, translate_size_exp const_env e1,
|
Sop(op, translate_static_exp const_env e1,
|
||||||
translate_size_exp const_env e2)
|
translate_static_exp const_env e2)
|
||||||
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
|
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
|
||||||
|
|
||||||
let rec translate_type const_env = function
|
let rec translate_type const_env = function
|
||||||
|
@ -132,7 +132,7 @@ let rec translate_type const_env = function
|
||||||
| Tid ln -> Types.Tid ln
|
| Tid ln -> Types.Tid ln
|
||||||
| Tarray (ty, e) ->
|
| Tarray (ty, e) ->
|
||||||
let ty = translate_type const_env ty in
|
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 =
|
and translate_exp const_env env e =
|
||||||
{ Heptagon.e_desc = translate_desc e.e_loc const_env env e.e_desc;
|
{ 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 =
|
and translate_op_desc const_env desc =
|
||||||
{ Heptagon.op_name = desc.op_name;
|
{ Heptagon.op_name = desc.op_name;
|
||||||
Heptagon.op_params =
|
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 }
|
Heptagon.op_kind = translate_op_kind desc.op_kind }
|
||||||
|
|
||||||
and translate_array_op const_env env = function
|
and translate_array_op const_env env = function
|
||||||
| Eselect e_list ->
|
| 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 ->
|
| 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
|
| Erepeat -> Heptagon.Erepeat
|
||||||
| Eselect_slice -> Heptagon.Eselect_slice
|
| Eselect_slice -> Heptagon.Eselect_slice
|
||||||
| Econcat -> Heptagon.Econcat
|
| 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
|
let e_list = List.map (translate_exp const_env env) e_list in
|
||||||
(match e_list with
|
(match e_list with
|
||||||
| [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
|
| [{ 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)
|
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
|
||||||
)
|
)
|
||||||
| Eapp (app, e_list) ->
|
| Eapp (app, e_list) ->
|
||||||
|
@ -310,7 +310,7 @@ let translate_typedec const_env ty =
|
||||||
let translate_const_dec const_env cd =
|
let translate_const_dec const_env cd =
|
||||||
{ Heptagon.c_name = cd.c_name;
|
{ Heptagon.c_name = cd.c_name;
|
||||||
Heptagon.c_type = translate_type const_env cd.c_type;
|
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; }
|
Heptagon.c_loc = cd.c_loc; }
|
||||||
|
|
||||||
let translate_program p =
|
let translate_program p =
|
||||||
|
|
|
@ -8,7 +8,6 @@
|
||||||
(**************************************************************************)
|
(**************************************************************************)
|
||||||
(* removing reset statements *)
|
(* removing reset statements *)
|
||||||
|
|
||||||
(* $Id$ *)
|
|
||||||
|
|
||||||
open Misc
|
open Misc
|
||||||
open Ident
|
open Ident
|
||||||
|
|
|
@ -222,7 +222,7 @@ let rec application env { Heptagon.a_op = op; } e_list =
|
||||||
and translate_array_op env op e_list =
|
and translate_array_op env op e_list =
|
||||||
match op, e_list with
|
match op, e_list with
|
||||||
| Heptagon.Erepeat, [e; idx] ->
|
| Heptagon.Erepeat, [e; idx] ->
|
||||||
Erepeat (size_exp_of_exp idx, e)
|
Erepeat (static_exp_of_exp idx, e)
|
||||||
| Heptagon.Eselect idx_list, [e] ->
|
| Heptagon.Eselect idx_list, [e] ->
|
||||||
Eselect (idx_list, e)
|
Eselect (idx_list, e)
|
||||||
| Heptagon.Eselect_dyn, e::defe::idx_list ->
|
| 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] ->
|
| Heptagon.Eupdate idx_list, [e1;e2] ->
|
||||||
Eupdate (idx_list, e1, e2)
|
Eupdate (idx_list, e1, e2)
|
||||||
| Heptagon.Eselect_slice, [e; idx1; idx2] ->
|
| 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] ->
|
| Heptagon.Econcat, [e1; e2] ->
|
||||||
Econcat (e1, e2)
|
Econcat (e1, e2)
|
||||||
| Heptagon.Eiterator(it, op_desc, reset), idx::e_list ->
|
| Heptagon.Eiterator(it, op_desc, reset), idx::e_list ->
|
||||||
Eiterator(translate_iterator_type it,
|
Eiterator(translate_iterator_type it,
|
||||||
translate_op_desc op_desc,
|
translate_op_desc op_desc,
|
||||||
size_exp_of_exp idx, e_list,
|
static_exp_of_exp idx, e_list,
|
||||||
translate_reset reset)
|
translate_reset reset)
|
||||||
|
|
||||||
let rec translate env
|
let rec translate env
|
||||||
|
|
|
@ -38,41 +38,35 @@ and exp =
|
||||||
e_loc: location }
|
e_loc: location }
|
||||||
|
|
||||||
and edesc =
|
and edesc =
|
||||||
| Econst of const
|
| Econst of static_exp
|
||||||
| Evar of ident
|
| Evar of ident
|
||||||
| Econstvar of name
|
| Econstvar of name
|
||||||
| Efby of const option * exp
|
|
||||||
| Etuple of exp list
|
| Etuple of exp list
|
||||||
| Ecall of op_desc * exp list * ident option (** [op_desc] is the function
|
| Efby of static_exp option * exp
|
||||||
called [exp list] is the
|
| Eapp of app * exp list * ident option
|
||||||
passed arguments [ident
|
(** ident option is the optional reset *)
|
||||||
option] is the optional reset
|
|
||||||
condition *)
|
|
||||||
|
|
||||||
| Ewhen of exp * longname * ident
|
| Ewhen of exp * longname * ident
|
||||||
| Emerge of ident * (longname * exp) list
|
| Emerge of ident * (longname * exp) list
|
||||||
| Eifthenelse of exp * exp * exp
|
|
||||||
| Efield of exp * longname
|
| Efield of exp * longname
|
||||||
| Efield_update of longname * exp * exp (*field, record, value*)
|
|
||||||
| Estruct of (longname * exp) list
|
| Estruct of (longname * exp) list
|
||||||
| Earray of exp list
|
| Eiterator of iterator_type * app * static_exp * exp list * ident option
|
||||||
| 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 * 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 app = { a_op: op; a_params: static_exp list }
|
||||||
and op_kind = | Efun | Enode
|
|
||||||
|
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 =
|
and ct =
|
||||||
| Ck of ck
|
| Ck of ck
|
||||||
|
@ -91,7 +85,8 @@ and const =
|
||||||
| Cint of int
|
| Cint of int
|
||||||
| Cfloat of float
|
| Cfloat of float
|
||||||
| Cconstr of longname
|
| Cconstr of longname
|
||||||
| Carray of size_exp * const
|
| Carray of static_exp * const
|
||||||
|
| Cop of
|
||||||
|
|
||||||
and pat =
|
and pat =
|
||||||
| Etuplepat of pat list
|
| Etuplepat of pat list
|
||||||
|
@ -129,7 +124,7 @@ type node_dec =
|
||||||
|
|
||||||
type const_dec =
|
type const_dec =
|
||||||
{ c_name : name;
|
{ c_name : name;
|
||||||
c_value : size_exp;
|
c_value : static_exp;
|
||||||
c_loc : location; }
|
c_loc : location; }
|
||||||
|
|
||||||
type program =
|
type program =
|
||||||
|
|
|
@ -51,10 +51,10 @@ let rec print_c ff = function
|
||||||
| Cint i -> fprintf ff "%d" i
|
| Cint i -> fprintf ff "%d" i
|
||||||
| Cfloat f -> fprintf ff "%f" f
|
| Cfloat f -> fprintf ff "%f" f
|
||||||
| Cconstr tag -> print_longname ff tag
|
| 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 =
|
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 =
|
and print_node_params ff l =
|
||||||
fprintf ff "@[<2>%a@]" (print_list_r print_param "<<"","">>") 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
|
fprintf ff "@[<2>%a@]" (print_list_r print_vd "("","")") l
|
||||||
|
|
||||||
and print_index ff idx =
|
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 =
|
and print_dyn_index ff idx =
|
||||||
fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") 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
|
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 (idx, e) -> fprintf ff "%a%a" print_exp e print_index idx
|
||||||
| Eselect_dyn (idx, e1, e2) ->
|
| Eselect_dyn (idx, e1, e2) ->
|
||||||
fprintf ff "%a%a default %a"
|
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
|
print_exp e1 print_index idx print_exp e2
|
||||||
| Eselect_slice (idx1, idx2, e) ->
|
| Eselect_slice (idx1, idx2, e) ->
|
||||||
fprintf ff "%a[%a..%a]"
|
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
|
| Econcat (e1, e2) -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2
|
||||||
| Eiterator (it, f, n, e_list, r) ->
|
| Eiterator (it, f, n, e_list, r) ->
|
||||||
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
|
fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a"
|
||||||
(iterator_to_string it)
|
(iterator_to_string it)
|
||||||
print_op f
|
print_op f
|
||||||
print_size_exp n
|
print_static_exp n
|
||||||
print_exp_tuple e_list
|
print_exp_tuple e_list
|
||||||
print_every r
|
print_every r
|
||||||
|
|
||||||
|
@ -175,7 +175,7 @@ and print_field ff field =
|
||||||
|
|
||||||
let print_const_dec ff c =
|
let print_const_dec ff c =
|
||||||
fprintf ff "const %a = %a" print_name c.c_name
|
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
|
let print_contract ff
|
||||||
{ c_local = l; c_eq = eqs;
|
{ c_local = l; c_eq = eqs;
|
||||||
|
|
|
@ -9,22 +9,22 @@ open Types
|
||||||
open Misc
|
open Misc
|
||||||
|
|
||||||
(** Error Kind *)
|
(** Error Kind *)
|
||||||
type err_kind = | Enot_size_exp
|
type err_kind = | Enot_static_exp
|
||||||
|
|
||||||
let err_message ?(exp=void) ?(loc=exp.e_loc) = function
|
let err_message ?(exp=void) ?(loc=exp.e_loc) = function
|
||||||
| Enot_size_exp ->
|
| Enot_static_exp ->
|
||||||
Printf.eprintf "The expression %a should be a size_exp.@."
|
Printf.eprintf "The expression %a should be a static_exp.@."
|
||||||
print_exp exp;
|
print_exp exp;
|
||||||
raise Error
|
raise Error
|
||||||
|
|
||||||
let rec size_exp_of_exp e =
|
let rec static_exp_of_exp e =
|
||||||
match e.e_desc with
|
match e.e_desc with
|
||||||
| Econstvar n -> Svar n
|
| Econstvar n -> Svar n
|
||||||
| Econst (Cint i) -> Sconst i
|
| Econst (Cint i) -> Sconst i
|
||||||
| Ecall(op, [e1;e2], _) ->
|
| Ecall(op, [e1;e2], _) ->
|
||||||
let sop = op_from_app_name op.op_name in
|
let sop = op_from_app_name op.op_name in
|
||||||
Sop(sop, size_exp_of_exp e1, size_exp_of_exp e2)
|
Sop(sop, static_exp_of_exp e1, static_exp_of_exp e2)
|
||||||
| _ -> err_message ~exp:e Enot_size_exp
|
| _ -> err_message ~exp:e Enot_static_exp
|
||||||
|
|
||||||
(** @return the list of bounds of an array type*)
|
(** @return the list of bounds of an array type*)
|
||||||
let rec bounds_list ty =
|
let rec bounds_list ty =
|
||||||
|
|
|
@ -189,7 +189,7 @@ array_op:
|
||||||
{ Eselect_slice(i1, i2, e) }
|
{ Eselect_slice(i1, i2, e) }
|
||||||
| e1=exp AROBASE e2=exp { Econcat(e1,e2) }
|
| e1=exp AROBASE e2=exp { Econcat(e1,e2) }
|
||||||
| LPAREN f=iterator LPAREN op=funop RPAREN
|
| 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) }
|
RPAREN a=exps r=reset { Eiterator(f,op,p,a,r) }
|
||||||
|
|
||||||
/* Static indexes [p1][p2]... */
|
/* 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 }
|
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 }
|
n_param: n=NAME { mk_param n }
|
||||||
params(param):
|
params(param):
|
||||||
| /*empty*/ { [] }
|
| /*empty*/ { [] }
|
||||||
|
|
|
@ -59,7 +59,7 @@ let rec translate_type const_env = function
|
||||||
| Types.Tid id when id = Initial.pbool -> Tbool
|
| Types.Tid id when id = Initial.pbool -> Tbool
|
||||||
| Types.Tid id -> Tid id
|
| Types.Tid id -> Tid id
|
||||||
| Types.Tarray (ty, n) ->
|
| 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
|
| Types.Tprod ty -> assert false
|
||||||
|
|
||||||
let rec translate_const const_env = function
|
let rec translate_const const_env = function
|
||||||
|
@ -67,7 +67,7 @@ let rec translate_const const_env = function
|
||||||
| Minils.Cfloat v -> Cfloat v
|
| Minils.Cfloat v -> Cfloat v
|
||||||
| Minils.Cconstr c -> Cconstr c
|
| Minils.Cconstr c -> Cconstr c
|
||||||
| Minils.Carray (n, 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
|
let rec translate_pat map = function
|
||||||
| Minils.Evarpat x -> [ var_from_name map x ]
|
| 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
|
match desc with
|
||||||
| Minils.Econst v -> Const (translate_const const_env v)
|
| Minils.Econst v -> Const (translate_const const_env v)
|
||||||
| Minils.Evar n -> Lhs (var_from_name map n)
|
| 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 },
|
| Minils.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Efun },
|
||||||
e_list, _) when Mls_utils.is_op n ->
|
e_list, _) when Mls_utils.is_op n ->
|
||||||
Op (n, List.map (translate const_env map (m, si, j, s)) e_list)
|
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)) ->
|
| Minils.Earray_op (Minils.Eselect (idx, e)) ->
|
||||||
let e = translate const_env map (m, si, j, s) e in
|
let e = translate const_env map (m, si, j, s) e in
|
||||||
let idx_list =
|
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
|
in
|
||||||
Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list)
|
Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list)
|
||||||
| _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false
|
| _ -> (*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
|
(match op_kind with
|
||||||
| Minils.Enode -> (Reinit o) :: si
|
| Minils.Enode -> (Reinit o) :: si
|
||||||
| Minils.Efun -> si) in
|
| 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 j = (o, (encode_longname_params n params), 1) :: j in
|
||||||
let action = Step_ap (name_list, Context o, c_list) in
|
let action = Step_ap (name_list, Context o, c_list) in
|
||||||
let s = (match r, op_kind with
|
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.Evarpat x,
|
||||||
Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) ->
|
Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) ->
|
||||||
let idx1 = int_of_size_exp const_env idx1 in
|
let idx1 = int_of_static_exp const_env idx1 in
|
||||||
let idx2 = int_of_size_exp const_env idx2 in
|
let idx2 = int_of_static_exp const_env idx2 in
|
||||||
let cpt = Ident.fresh "i" in
|
let cpt = Ident.fresh "i" in
|
||||||
let e = translate const_env map (m, si, j, s) e in
|
let e = translate const_env map (m, si, j, s) e in
|
||||||
let idx =
|
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 x = var_from_name map x in
|
||||||
let bounds = Mls_utils.bounds_list e1.Minils.e_ty 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 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 idx = List.map (translate const_env map (m, si, j, s)) idx in
|
||||||
let true_act =
|
let true_act =
|
||||||
Assgn (x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in
|
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 x = var_from_name map x in
|
||||||
let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in
|
let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in
|
||||||
let idx =
|
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
|
idx in
|
||||||
let action = Assgn (lhs_of_idx_list x idx,
|
let action = Assgn (lhs_of_idx_list x idx,
|
||||||
translate const_env map (m, si, j, s) e2)
|
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)) ->
|
Minils.Earray_op (Minils.Erepeat (n, e)) ->
|
||||||
let cpt = Ident.fresh "i" in
|
let cpt = Ident.fresh "i" in
|
||||||
let action =
|
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)),
|
Assgn (Array (var_from_name map x, Lhs (Var cpt)),
|
||||||
translate const_env map (m, si, j, s) e))
|
translate const_env map (m, si, j, s) e))
|
||||||
in
|
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) ->
|
| Types.Tarray (_, n1), Types.Tarray (_, n2) ->
|
||||||
let e1 = translate const_env map (m, si, j, s) e1 in
|
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 e2 = translate const_env map (m, si, j, s) e2 in
|
||||||
let n1 = int_of_size_exp const_env n1 in
|
let n1 = int_of_static_exp const_env n1 in
|
||||||
let n2 = int_of_size_exp const_env n2 in
|
let n2 = int_of_static_exp const_env n2 in
|
||||||
let a1 =
|
let a1 =
|
||||||
For (cpt1, 0, n1,
|
For (cpt1, 0, n1,
|
||||||
Assgn (Array (x, Lhs (Var cpt1)),
|
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 =
|
let c_list =
|
||||||
List.map (translate const_env map (m, si, j, s)) e_list in
|
List.map (translate const_env map (m, si, j, s)) e_list in
|
||||||
let o = gen_obj_name f 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 =
|
let si =
|
||||||
(match k with
|
(match k with
|
||||||
| Minils.Efun -> si
|
| Minils.Efun -> si
|
||||||
| Minils.Enode -> (Reinit o) :: si) in
|
| 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 j = (o, (encode_longname_params f params), n) :: j in
|
||||||
let x = Ident.fresh "i" in
|
let x = Ident.fresh "i" in
|
||||||
let action =
|
let action =
|
||||||
|
|
|
@ -57,7 +57,7 @@ let rec collect_exp nodes env e =
|
||||||
| Ecall( { op_name = ln; op_params = params; op_kind = _ },
|
| Ecall( { op_name = ln; op_params = params; op_kind = _ },
|
||||||
e_list, _) ->
|
e_list, _) ->
|
||||||
List.iter (collect_exp nodes env) 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
|
call_node_instance nodes ln params
|
||||||
| Earray_op op ->
|
| Earray_op op ->
|
||||||
collect_array_exp nodes env op
|
collect_array_exp nodes env op
|
||||||
|
@ -74,7 +74,7 @@ and collect_array_exp nodes env = function
|
||||||
collect_exp nodes env e
|
collect_exp nodes env e
|
||||||
| Eiterator (_, { op_name = ln; op_params = params }, _, e_list, _) ->
|
| Eiterator (_, { op_name = ln; op_params = params }, _, e_list, _) ->
|
||||||
List.iter (collect_exp nodes env) 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
|
call_node_instance nodes ln params
|
||||||
|
|
||||||
and collect_eqs nodes env eq =
|
and collect_eqs nodes env eq =
|
||||||
|
|
Loading…
Reference in a new issue