jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Updated ast for Static

Browse source 
- Static are used for consts in Heptagon and Minils.
For now, node static parameters remain int only
(ie they are type parameters). Do we need more ?
- Also updated Parsetree AST to the recent changes
in API
This commit is contained in:
Cédric Pasteur 2010-07-02 13:50:18 +02:00
parent c46896ca55
commit 769cb1d881
11 changed files with 248 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

117
compiler/global/static.ml
View file

@ -22,12 +22,12 @@ type static_exp =
| Sint of int
| Sfloat of float
| Sbool of bool
| Sconstructor of
| Sconstructor of longname
| 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 ] *)
| Sop of longname * static_exp list (** defined ops for now in pervasives *)
(** Constraints on size expressions. *)
type size_constraint =
| Cequal of static_exp * static_exp (* e1 = e2*)
@ -40,67 +40,70 @@ exception Instanciation_failed
exception Not_static
(** Returns the op from an operator full name. *)
let op_from_app_name n =
match n with
| Modname { qual = "Pervasives"; id = "+" } | Name "+" -> Splus
| Modname { qual = "Pervasives"; id = "-" } | Name "-" -> Sminus
| Modname { qual = "Pervasives"; id = "*" } | Name "*" -> Stimes
| Modname { qual = "Pervasives"; id = "/" } | Name "/" -> Sdiv
let op_from_app_name ln =
match ln with
| Modname { qual = "Pervasives" } -> ln
| _ -> raise Not_static
(** Applies the operator [op] to the two integers [n1] and [n2]
and returns the reslt as a static exp. *)
let apply_int_op op n1 n2 =
match op with
| Modname { qual = "Pervasives"; id = "+" } -> Sint (n1 + n2)
| Modname { qual = "Pervasives"; id = "-" } -> Sint (n1 - n2)
| Modname { qual = "Pervasives"; id = "*" } -> Sint (n1 * n2)
| Modname { qual = "Pervasives"; id = "/" } ->
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)
(** [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 =
function
| Sconst n -> Sconst n
let rec simplify env se =
match se with
| Sint _ | Sfloat _ | Sbool _ | Sconstructor -> se
| Svar id -> (try simplify env (NamesEnv.find id env) with | _ -> Svar id)
| Sop (op, e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
| (Sconst n1, Sconst n2) ->
let n =
(match op with
| Splus -> n1 + n2
| Sminus -> n1 - n2
| Stimes -> n1 * n2
| Sdiv ->
if n2 = 0 then raise Instanciation_failed else n1 / n2)
in Sconst n
| (_, _) -> Sop (op, e1, e2))
| Sop (op, [e1; e2]) ->
(match simplify env e1, simplify env e2 with
| Sint n1, Sint n2 -> apply_int_op op n1 n2
| e1, e2 -> Sop (op, [e1; e2])
)
| Sop (op, se_list) -> Sop (op, List.map (simplify env) se_list)
| Sarray se_list -> Sarray (List.map (simplify env) se_list)
| Sarray_power (se, n) -> Sarray_power (simplify env se, simplify env n)
| Stuple se_list -> Stuple (List.map (simplify env) se_list)
(** [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 =
match simplify env e with | Sconst n -> n | _ -> raise Instanciation_failed
let int_of_static_exp env e =
match simplify env e 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 ->
((Some true), (Cequal (simplify env e1, simplify env 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, e2) with
| (Sconst n1, Sconst n2) -> ((Some (n1 = n2)), (Cequal (e1, e2)))
| (_, _) -> (None, (Cequal (e1, e2))))
(match e1, e2 with
| SConst n1, SConst 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, e2) with
| (Sconst n1, Sconst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
| (_, _) -> (None, (Clequal (e1, e2))))
| Cfalse -> (None, Cfalse)
(match e1, e2 with
| SConst n1, SConst n2 -> Some (n1 <= n2), Clequal (e1, e2)
| _, _ -> None, Clequal (e1, e2))
| Cfalse -> None, Cfalse
exception Solve_failed of size_constraint
@ -120,11 +123,14 @@ 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 =
function
| Svar n -> (try List.assoc n m with | Not_found -> Svar n)
| Sop (op, e1, e2) -> Sop (op, static_exp_subst m e1, static_exp_subst m e2)
| s -> s
let rec static_exp_subst m = function
| 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)
| s -> s
(** Substitutes variables in the constraint list with their value
in the map (mapping vars to size exps). *)
@ -135,16 +141,23 @@ let instanciate_constr m constr =
| Cfalse -> Cfalse
in List.map (replace_one m) constr
let op_to_string =
function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/"
let rec print_static_exp ff = function
| 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
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_static_exp e1 (op_to_string op) print_static_exp e2
and print_static_exp_tuple ff l =
fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l
let print_size_constraint ff = function
| Cequal (e1, e2) ->

5
compiler/heptagon/analysis/interface.ml
View file

@ -21,7 +21,8 @@ module Type =
struct
let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull;
sig_outputs = o_list; sig_params = params } =
let check_arg a = { a with a_type = check_type a.a_type } in
let const_env = build_node_params NamesEnv.empty node_params in
let check_arg a = { a with a_type = check_type const_env a.a_type } in
name, { node_inputs = List.map check_arg i_list;
node_outputs = List.map check_arg o_list;
node_statefull = statefull;
@ -32,7 +33,7 @@ struct
try
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
| Itypedef(tydesc) -> deftype NamesEnv.empty NamesEnv.empty tydesc
| Isignature(s) ->
let name, s = sigtype s in
add_value name s

159
compiler/heptagon/analysis/typing.ml
View file

@ -226,7 +226,7 @@ let less_than statefull = if not statefull then error Estate_clash
let rec is_statefull_exp e =
match e.e_desc with
| Econst _ | Econstvar _ | Evar _-> false
| Econst _ | Evar _-> false
| Elast _ -> true
| Etuple e_list -> List.exists is_statefull_exp e_list
| Eapp({ a_op = (Efby | Epre _ | Earrow) }, _) -> true
@ -281,15 +281,41 @@ let prod = function
| [ty] -> ty
| ty_list -> Tprod ty_list
let rec typing_const c = match c with
| Cint _ -> c, Tid(pint)
| Cfloat _ -> c, Tid(pfloat)
let typing_static_exp const_env se =
match se with
| Sint -> Initial.pint
| Sbool -> Initial.pbool
| Sfloat -> Initial.pfloat
| Svar n ->
(try
NamesEnv.find n const_env
with
Not_found -> message no_location (Eundefined_const n))
| Sconstructor ln ->
| Cconstr(c) ->
let { qualid = q; info = ty } = find_constr c in
Cconstr(Modname q), ty
| Carray(n, c) ->
let c, ty = typing_const c in
Carray(n,c), Tarray(ty, n)
| Sop (op, se_list) ->
| Sarray_power (se, n) ->
expect_static_exp const_env no_location (Tid Initial.pint) n;
let ty = typing_static_exp const_env se in
Tarray(ty, n)
| Sarray [] ->
message no_location Eempty_array
| Sarray se::se_list ->
let ty = typing_static_exp const_env se in
List.iter (expect_static_exp const_env ty) se_list;
Tarray(ty, Sint ((List.length se_list) + 1))
| Stuple se_list ->
prod (List.map (typing_static_exp const_env) se_list)
and expect_static_exp const_env loc exp_ty se =
try
let ty = typing_static_exp const_env se in
unify ty exp_ty
with
Unify -> message loc (Etype_clash(ty, exp_ty))
let typ_of_name h x =
try
@ -331,25 +357,26 @@ let name_mem n env =
Env.fold check_one env false
(** [check_type t] checks that t exists *)
let rec check_type = function
let rec check_type const_env = function
| Tarray(ty, e) ->
Tarray(check_type ty, e)
expect_static_exp const_env (Tid Initial.pint) e;
Tarray(check_type const_env ty, e)
| Tid(ty_name) ->
(try Tid(Modname((find_type ty_name).qualid))
with Not_found -> error (Eundefined(fullname ty_name)))
| Tprod l ->
Tprod (List.map check_type l)
Tprod (List.map (check_type const_env) l)
let rec simplify_type const_env = function
let rec simplify_type const_value_env = function
| Tid _ as t -> t
| Tarray(ty, e) ->
Tarray(simplify_type const_env ty, simplify const_env e)
Tarray(simplify_type const_value_env ty, simplify const_value_env e)
| Tprod l ->
Tprod (List.map (simplify_type const_env) l)
Tprod (List.map (simplify_type const_value_env) l)
let simplify_type loc const_env ty =
let simplify_type loc const_value_env ty =
try
simplify_type const_env ty
simplify_type const_value_env ty
with
Instanciation_failed -> message loc (Etype_should_be_static ty)
@ -466,9 +493,9 @@ let struct_info_from_field loc f =
(** @return the type of the field with name [f] in the list
[fields]. [t1] is the corresponding record type and [loc] is
the location, both used for error reporting. *)
let field_type f fields t1 loc =
let field_type const_env f fields t1 loc =
try
check_type (field_assoc f fields)
check_type const_env (field_assoc f fields)
with
Not_found -> message loc (Eno_such_field (t1, f))
@ -476,10 +503,9 @@ let rec typing statefull h e =
try
let typed_desc,ty = match e.e_desc with
| Econst(c) ->
let typed_c, ty = typing_const c in
let typed_c, ty = typing_static_exp const_env c in
Econst(c),
ty
| Econstvar(x) -> Econstvar x, Tid Initial.pint
| Evar(x) ->
Evar(x),
typ_of_varname h x
@ -529,30 +555,30 @@ let rec typing statefull h e =
with
TypingError(kind) -> message e.e_loc kind
and typing_field statefull h fields t1 (f, e) =
and typing_field statefull const_env h fields t1 (f, e) =
try
let ty = check_type (field_assoc f fields) in
let typed_e = expect statefull h ty e in
let ty = check_type const_env (field_assoc f fields) in
let typed_e = expect statefull const_env h ty e in
f, typed_e
with
Not_found -> message e.e_loc (Eno_such_field (t1, f))
and expect statefull h expected_ty e =
let typed_e, actual_ty = typing statefull h e in
and expect statefull const_env h expected_ty e =
let typed_e, actual_ty = typing statefull const_env h e in
try
unify actual_ty expected_ty;
typed_e
with TypingError(kind) -> message e.e_loc kind
and typing_app statefull h op e_list =
and typing_app statefull const_env h op e_list =
match op, e_list with
| Epre(None), [e] ->
less_than statefull;
let typed_e,ty = typing statefull h e in
ty,op,[typed_e]
| Epre(Some(c)), [e] ->
| Epre(Some c), [e] ->
less_than statefull;
let typed_c, t1 = typing_const c in
let typed_c, t1 = typing_static_exp const_env c in
let typed_e = expect statefull h t1 e in
t1, Epre(Some(typed_c)), [typed_e]
| (Efby | Earrow), [e1;e2] ->
@ -603,7 +629,7 @@ and typing_app statefull h op e_list =
(*Array operators*)
and typing_array_op statefull h op e_list =
match op, e_list with
| Erepeat, [e1; e2] ->
| Earray_fill, [e1; e2] ->
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
let e2 = static_exp_of_exp e2 in
let typed_e1, t1 = typing statefull h e1 in
@ -642,24 +668,23 @@ and typing_array_op statefull h op e_list =
end;
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),
e::e_list ->
| Eiterator (it, app, n, e_list, reset),
let { qualid = q; info = ty_desc } = find_value f in
let f = Modname(q) in
let k, expected_ty_list, result_ty_list = kind f statefull k ty_desc in
let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params)
params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let size_constrs =
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 = 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 n
expected_ty_list result_ty_list e_list in
add_size_constraint (Clequal (Sconst 1, e));
(* add size constraints *)
let size_constrs =
instanciate_constr m ty_desc.node_params_constraints in
add_size_constraint (Clequal (SConst 1, e));
List.iter add_size_constraint size_constrs;
(* return the type *)
ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
typed_e::typed_e_list
@ -714,12 +739,13 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
end;
prod result_ty_list, typed_e_list
and typing_array_subscript statefull h idx_list ty =
and typing_array_subscript statefull const_env h idx_list ty =
match ty, idx_list with
| ty, [] -> ty
| Tarray(ty, exp), idx::idx_list ->
add_size_constraint (Clequal (Sconst 0, idx));
add_size_constraint (Clequal (idx, Sop(Sminus, exp, Sconst 1)));
expect_static_exp const_env (Tid Initial.pint) exp;
add_size_constraint (Clequal (SConst 0, idx));
add_size_constraint (Clequal (idx, Sop(SMinus, exp, SConst 1)));
typing_array_subscript statefull h idx_list ty
| _, _ -> error (Esubscripted_value_not_an_array ty)
@ -886,12 +912,12 @@ and typing_block statefull h
with
| TypingError(kind) -> message loc kind
and build h h0 dec =
and build const_env h h0 dec =
List.fold_left
(fun (acc_dec, acc_defined, h)
({ v_ident = n; v_type = btype; v_last = l; v_loc = loc } as v) ->
try
let ty = check_type btype in
let ty = check_type const_env btype in
(* update type longname with module name from check_type *)
v.v_type <- ty;
if (Env.mem n h0) or (Env.mem n h)
@ -904,14 +930,6 @@ and build h h0 dec =
| TypingError(kind) -> message loc kind)
([], Env.empty, h) dec
let build_params h params =
let add_one h param =
if Env.mem param h then
error (Ealready_defined(name param));
Env.add param { ty = Tid Initial.pint; last = false } h
in
List.fold_left add_one h params
let typing_contract statefull h contract =
match contract with
@ -942,9 +960,9 @@ let typing_contract statefull h contract =
c_enforce = typed_e_g },
controllable_names, h
let signature const_env statefull inputs returns params constraints =
let signature const_value_env statefull inputs returns params constraints =
let arg_dec_of_var_dec vd =
mk_arg (Some (name vd.v_ident)) (check_type vd.v_type)
mk_arg (Some (name vd.v_ident)) (simplify_type const_value_env vd.v_type)
in
{ node_inputs = List.map arg_dec_of_var_dec inputs;
node_outputs = List.map arg_dec_of_var_dec returns;
@ -958,22 +976,28 @@ let solve loc env cl =
with
Solve_failed c -> message loc (Econstraint_solve_failed c)
let node const_env ({ n_name = f; n_statefull = statefull;
let build_node_params const_env l =
List.fold_left (fun env n -> NamesEnv.add n (Tid Initial.pint) env)
const_env l
let node const_env const_value_env ({ n_name = f; n_statefull = statefull;
n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc;
n_params = node_params; } as n) =
try
let typed_i_list, input_names, h = build Env.empty Env.empty i_list in
let typed_o_list, output_names, h = build h h o_list in
let const_env = build_node_params const_env node_params in
let typed_i_list, input_names, h = build const_env Env.empty Env.empty i_list in
let typed_o_list, output_names, h = build const_env h h o_list in
(* typing contract *)
let typed_contract, controllable_names, h =
typing_contract statefull h contract in
let typed_l_list, local_names, h = build h h l_list in
let typed_l_list, local_names, h = build const_env h h l_list in
let typed_eq_list, defined_names =
typing_eq_list statefull h Env.empty eq_list in
typing_eq_list statefull const_env h Env.empty eq_list in
(* if not (statefull) & (List.length o_list <> 1)
then error (Etoo_many_outputs);*)
let expected_names = add local_names output_names in
@ -981,8 +1005,8 @@ let node const_env ({ n_name = f; n_statefull = statefull;
included_env defined_names expected_names;
let cl = get_size_constraint () in
let cl = solve loc const_env cl in
add_value f (signature const_env statefull i_list o_list node_params cl);
let cl = solve loc const_value_env cl in
add_value f (signature const_value_env statefull i_list o_list node_params cl);
{ n with
n_input = List.rev typed_i_list;
@ -993,7 +1017,7 @@ let node const_env ({ n_name = f; n_statefull = statefull;
with
| TypingError(error) -> message loc error
let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
let deftype const_env const_value_env { t_name = n; t_desc = tdesc; t_loc = loc } =
try
match tdesc with
| Type_abs -> add_type n Tabstract
@ -1004,7 +1028,8 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
let field_ty_list =
List.map (fun f ->
mk_field f.f_name
(simplify_type loc const_env f.f_type))
(simplify_type loc const_value_env
(check_type const_env f.f_type))
field_ty_list in
add_type n (Tstruct field_ty_list);
add_struct n field_ty_list;
@ -1013,15 +1038,23 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
with
TypingError(error) -> message loc error
let build_const_env cd_list =
let build_const_value_env cd_list =
List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env)
NamesEnv.empty cd_list
let build_const_env cd_list =
let typing_const_dec const_envenv cd =
expect_static_exp const_env cd.c_loc cd.c_type cd.c_value;
NamesEnv.add cd.c_name cd.c_type env
in
List.fold_left typing_const_env NamesEnv.empty cd_list
let program
({ p_opened = opened; p_types = p_type_list;
p_nodes = p_node_list; p_consts = p_consts_list } as p) =
let const_env = build_const_env p_consts_list in
let const_value_env = build_const_value_env p_consts_list in
List.iter open_module opened;
List.iter (deftype const_env) p_type_list;
let typed_node_list = List.map (node const_env) p_node_list in
List.iter (deftype const_env const_value_env) p_type_list;
let typed_node_list = List.map (node const_env const_value_env) p_node_list in
{ p with p_nodes = typed_node_list }

3
compiler/heptagon/heptagon.ml
View file

@ -182,9 +182,6 @@ let op_from_app app =
let rec static_exp_of_exp e =
match e.e_desc with
| Econst se -> se
| Eapp (app, [ e1; e2 ]) ->
let op = op_from_app app
in Sop (op, static_exp_of_exp e1, static_exp_of_exp e2)
| _ -> raise Not_static
(** @return the set of variables defined in [pat]. *)

14
compiler/heptagon/parsing/hept_parser.mly
View file

@ -216,7 +216,7 @@ opt_equs:
;
opt_assume:
| /* empty */ { mk_exp (Econst (Cconstr Initial.ptrue)) }
| /* empty */ { mk_exp (Econst (Sconstructor Initial.ptrue)) }
| ASSUME exp { $2 }
;
@ -242,7 +242,7 @@ loc_params:
var_last:
| ident_list COLON ty_ident
{ List.map (fun id -> mk_var_dec id $3 Var) $1 }
| LAST IDENT COLON ty_ident EQUAL const
| LAST IDENT COLON ty_ident EQUAL exp
{ [ mk_var_dec $2 $4 (Last(Some($6))) ] }
| LAST IDENT COLON ty_ident
{ [ mk_var_dec $2 $4 (Last(None)) ] }
@ -442,7 +442,7 @@ exp:
{ mk_exp (Efield ($1, $3)) }
/*Array operations*/
| exp POWER simple_exp
{ mk_exp (mk_array_op_call Erepeat [$1; $3]) }
{ mk_exp (mk_call Erepeat [$1; $3]) }
| simple_exp indexes
{ mk_exp (mk_array_op_call (Eselect $2) [$1]) }
| simple_exp DOT indexes DEFAULT exp
@ -483,7 +483,6 @@ indexes:
constructor:
| Constructor { Name($1) } %prec prec_ident
| Constructor DOT Constructor { Modname({qual = $1; id = $3}) }
| BOOL { Name(if $1 then "true" else "false") }
;
longname:
@ -492,9 +491,10 @@ longname:
;
const:
| INT { Cint($1) }
| FLOAT { Cfloat($1) }
| constructor { Cconstr($1) }
| INT { Sint $1 }
| FLOAT { Sfloat $1 }
| BOOL { Sbool $1 }
| constructor { Sconstructor $1 }
;
tuple_exp:

60
compiler/heptagon/parsing/parsetree.ml
View file

@ -27,39 +27,31 @@ and exp =
e_loc: location }
and desc =
| Econst of const
| Econst of static_exp
| Evar of name
| Elast of name
| Etuple of exp list
| Eapp of app * exp list
| Epre of 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
| Eiterator of iterator_type * app * static_exp * exp list
and app =
{ a_op : op; }
and app = { a_op: op; a_params: static_exp list; }
and op =
| Epre of const option
| Efby | Earrow | Eifthenelse
| Earray_op of array_op
| Efield_update of longname
| Ecall of op_desc
and array_op =
| Erepeat | Eselect of exp list | Eselect_dyn
| Eupdate of exp list
| Etuple
| Enode of longname
| Eifthenelse
| Earrow
| Efield_update of longname (* field name args would be [record ; value] *)
| Earray
| Earray_fill
| Eselect
| Eselect_dyn
| Eselect_slice
| Eupdate
| Econcat
| Eiterator of iterator_type * op_desc
and op_desc = { op_name : longname; op_params: exp list; op_kind: op_kind }
and op_kind = | Efun | Enode
and const =
| Cint of int
| Cfloat of float
| Cconstr of longname
and pat =
| Etuplepat of pat list
@ -106,7 +98,7 @@ and var_dec =
v_last : last;
v_loc : location; }
and last = Var | Last of const option
and last = Var | Last of exp option
type type_dec =
{ t_name : name;
@ -174,20 +166,14 @@ and interface_desc =
let mk_exp desc =
{ e_desc = desc; e_loc = Location.current_loc () }
let mk_app op =
{ a_op = op; }
let mk_app op params =
{ a_op = op; a_params = params }
let mk_op_desc ln params kind =
{ op_name = ln; op_params = params; op_kind = kind }
let mk_call ?(params=[]) op exps =
Eapp (mk_app op params, exps)
let mk_call desc exps =
Eapp (mk_app (Ecall desc), exps)
let mk_op_call s params exps =
mk_call (mk_op_desc (Name s) params Efun) exps
let mk_array_op_call op exps =
Eapp (mk_app (Earray_op op), exps)
let mk_op_call ?(params=[])s exps =
mk_call (Efun (Name s)) params exps
let mk_iterator_call it ln params exps =
mk_array_op_call (Eiterator (it, mk_op_desc ln params Enode)) exps

64
compiler/heptagon/parsing/scoping.ml
View file

@ -103,46 +103,59 @@ let translate_op_kind = function
| Efun -> Heptagon.Efun
| Enode -> Heptagon.Enode
let translate_const = function
| Cint i -> Heptagon.Cint i
| Cfloat f -> Heptagon.Cfloat f
| Cconstr ln -> Heptagon.Cconstr ln
let op_from_app loc app =
match app.a_op with
| Ecall { op_name = op; op_kind = Efun } -> op_from_app_name op
| _ -> Error.message loc Error.Estatic_exp_expected
let check_const_vars = ref true
let rec translate_static_exp const_env e = match e.e_desc with
let rec static_exp_of_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)
else
Svar n
| Econst (Cint i) -> Sconst i
| Eapp(app, [e1;e2]) ->
| Econst se -> se
| Eapp({ a_op = Earray_fill }, [e;n]) ->
Sarray_power (static_exp_of_exp const_env e,
static_exp_of_exp const_env n)
| Eapp({ a_op = Earray }, [e;n]) ->
Sarray (List.map (static_exp_of_exp const_env) e_list)
| Eapp({ a_op = Etuple }, [e;n]) ->
Stuple (List.map (static_exp_of_exp const_env) e_list)
| Eapp(app, e_list) ->
let op = op_from_app e.e_loc app in
Sop(op, translate_static_exp const_env e1,
translate_static_exp const_env e2)
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
Sop(op, List.map (static_exp_of_exp const_env) e_list)
| _ -> raise Not_static
let expect_static_exp const_env e =
try
static_exp_of_exp const_env e
with
Not_static -> Error.message e.e_loc Error.Estatic_exp_expected
let rec translate_type const_env = function
| Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list)
| Tid ln -> Types.Tid ln
| Tarray (ty, e) ->
let ty = translate_type const_env ty in
Types.Tarray (ty, translate_static_exp const_env e)
Types.Tarray (ty, expect_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;
let desc =
try (* try to see if the exp is a constant *)
Econst (translate_static_exp const_env e)
with
Not_static -> translate_desc e.e_loc const_env env e.e_desc in
{ Heptagon.e_desc = desc;
Heptagon.e_ty = Types.invalid_type;
Heptagon.e_loc = e.e_loc }
and translate_app const_env env app =
let op = match app.a_op with
| Epre None -> Heptagon.Epre None
| Epre (Some c) -> Heptagon.Epre (Some (translate_const c))
| Epre (Some e) ->
Heptagon.Epre (Some (expect_static_exp const_env e))
| Efby -> Heptagon.Efby
| Earrow -> Heptagon.Earrow
| Eifthenelse -> Heptagon.Eifthenelse
@ -155,14 +168,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_static_exp const_env) desc.op_params;
List.map (expect_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_static_exp const_env) e_list)
Heptagon.Eselect (List.map (expect_static_exp const_env) e_list)
| Eupdate e_list ->
Heptagon.Eupdate (List.map (translate_static_exp const_env) e_list)
Heptagon.Eupdate (List.map (expect_static_exp const_env) e_list)
| Erepeat -> Heptagon.Erepeat
| Eselect_slice -> Heptagon.Eselect_slice
| Econcat -> Heptagon.Econcat
@ -172,7 +185,7 @@ and translate_array_op const_env env = function
translate_op_desc const_env desc, None)
and translate_desc loc const_env env = function
| Econst c -> Heptagon.Econst (translate_const c)
| Econst c -> Heptagon.Econst c
| Evar x ->
if Rename.mem x env then (* defined var *)
Heptagon.Evar (Rename.name loc env x)
@ -183,13 +196,6 @@ and translate_desc loc const_env env = function
| Elast x -> Heptagon.Elast (Rename.name loc env x)
| Etuple e_list ->
Heptagon.Etuple (List.map (translate_exp const_env env) e_list)
| Eapp ({ a_op = (Earray_op Erepeat)} as app, e_list) ->
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.static_exp_of_exp e1, c))
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
)
| Eapp (app, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
Heptagon.Eapp (translate_app const_env env app, e_list)
@ -260,16 +266,16 @@ and translate_switch_handler loc const_env env sh =
and translate_var_dec const_env env vd =
{ Heptagon.v_ident = Rename.name vd.v_loc env vd.v_name;
Heptagon.v_type = translate_type const_env vd.v_type;
Heptagon.v_last = translate_last env vd.v_last;
Heptagon.v_last = translate_last const_env env vd.v_last;
Heptagon.v_loc = vd.v_loc }
and translate_vd_list const_env env =
List.map (translate_var_dec const_env env)
and translate_last env = function
and translate_last const_env env = function
| Var -> Heptagon.Var
| Last (None) -> Heptagon.Last None
| Last (Some c) -> Heptagon.Last (Some (translate_const c))
| Last (Some e) -> Heptagon.Last (Some (expect_static_exp const_env e))
let translate_contract const_env env ct =
{ Heptagon.c_assume = translate_exp const_env env ct.c_assume;
@ -310,7 +316,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_static_exp const_env cd.c_value;
Heptagon.c_value = expect_static_exp const_env cd.c_value;
Heptagon.c_loc = cd.c_loc; }
let translate_program p =

14
compiler/main/hept2mls.ml
View file

@ -182,12 +182,6 @@ let switch x ci_eqs_list =
check ci_eqs_list;
distribute ci_eqs_list
let rec const = function
| Heptagon.Cint i -> Cint i
| Heptagon.Cfloat f -> Cfloat f
| Heptagon.Cconstr t -> Cconstr t
| Heptagon.Carray(n, c) -> Carray(n, const c)
let translate_op_kind = function
| Heptagon.Efun -> Efun
| Heptagon.Enode -> Enode
@ -210,8 +204,8 @@ let translate_iterator_type = function
let rec application env { Heptagon.a_op = op; } e_list =
match op, e_list with
| Heptagon.Epre(None), [e] -> Efby(None, e)
| Heptagon.Epre(Some(c)), [e] -> Efby(Some(const c), e)
| Heptagon.Efby, [{ e_desc = Econst(c) } ; e] -> Efby(Some(c), e)
| Heptagon.Epre(Some c), [e] -> Efby(Some c, e)
| Heptagon.Efby, [{ e_desc = Econst c } ; e] -> Efby(Some c, e)
| Heptagon.Eifthenelse, [e1;e2;e3] -> Eifthenelse(e1, e2, e3)
| Heptagon.Ecall(op_desc, r), e_list ->
Ecall(translate_op_desc op_desc, e_list, translate_reset r)
@ -243,12 +237,10 @@ let rec translate env
{ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
Heptagon.e_loc = loc } =
match desc with
| Heptagon.Econst(c) ->
| Heptagon.Econst c ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst (const c)))
| Heptagon.Evar x ->
Env.con env x (mk_exp ~loc:loc ~exp_ty:ty (Evar x))
| Heptagon.Econstvar(x) ->
Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econstvar x))
| Heptagon.Etuple(e_list) ->
mk_exp ~loc:loc ~exp_ty:ty (Etuple (List.map (translate env) e_list))
| Heptagon.Eapp(app, e_list) ->

6
compiler/minils/mls_utils.ml
View file

@ -19,11 +19,7 @@ let err_message ?(exp=void) ?(loc=exp.e_loc) = function
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, static_exp_of_exp e1, static_exp_of_exp e2)
| Econst se -> se
| _ -> err_message ~exp:e Enot_static_exp
(** @return the list of bounds of an array type*)

17
compiler/minils/sequential/mls2obc.ml
View file

@ -63,11 +63,17 @@ let rec translate_type const_env = function
| Types.Tprod ty -> assert false
let rec translate_const const_env = function
| Minils.Cint v -> Cint v
| Minils.Cfloat v -> Cfloat v
| Minils.Cconstr c -> Cconstr c
| Minils.Carray (n, c) ->
Carray (int_of_static_exp const_env n, translate_const const_env c)
| Minils.Sint v -> Cint v
| Minils.Sbool v -> Cbool v
| Minils.Sfloat v -> Cfloat v
| Minils.Sconstructor c -> Cconstr c
| Minils.Sarray_power (n, c) ->
Carray_power (int_of_static_exp const_env n, translate_const const_env c)
| Minils.Sarray se_list ->
Carray (List.map (translate_const const_env) se_list)
| Minils.Stuple se_list ->
Ctuple (List.map (translate_const const_env) se_list)
| Minils.Svar n -> simplify const_env (SVar n)
let rec translate_pat map = function
| Minils.Evarpat x -> [ var_from_name map x ]
@ -81,7 +87,6 @@ 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_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)

5
compiler/minils/sequential/obc.ml
View file

@ -39,9 +39,12 @@ and tdesc =
type const =
| Cint of int
| Cbool of bool
| Cfloat of float
| Cconstr of longname
| Carray of int * const
| Carray_power of int * const
| Carray of const list
| Ctuple of const list
type lhs =
| Var of var_name