Good static Constructors names.
Conflicts: compiler/global/static.ml compiler/heptagon/analysis/typing.ml compiler/heptagon/heptagon.ml compiler/heptagon/parsing/scoping.ml compiler/minils/mls_utils.ml
This commit is contained in:
Léonard Gérard
parent
de16b4f178
commit
0ae39e8698
5 changed files with 62 additions and 53 deletions
|
|
@ -1,12 +1,20 @@
|
|||
(** This module defines static expressions, used in arrays definition
|
||||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(** This module defines static expressions, used in params and for constants.
|
||||
|
||||
and anywhere a static value is expected. For instance:
|
||||
const n: int = 3;
|
||||
var x : int^n; var y : int^(n + 2);
|
||||
x[n - 1], x[1 + 3],...
|
||||
*)
|
||||
open Names
|
||||
|
||||
open Names
|
||||
open Format
|
||||
|
||||
type op = | SPlus | SMinus | STimes | SDiv
|
||||
|
|
@ -15,10 +23,10 @@ type size_exp =
|
|||
| SConst of int | SVar of name | SOp of op * size_exp * size_exp
|
||||
|
||||
(** Constraints on size expressions. *)
|
||||
type size_constr =
|
||||
| Equal of size_exp * size_exp (* e1 = e2*)
|
||||
| LEqual of size_exp * size_exp (* e1 <= e2 *)
|
||||
| False
|
||||
type size_constraint =
|
||||
| Cequal of static_exp * static_exp (* e1 = e2*)
|
||||
| Clequal of static_exp * static_exp (* e1 <= e2 *)
|
||||
| Cfalse
|
||||
|
||||
(* unsatisfiable constraint *)
|
||||
exception Instanciation_failed
|
||||
|
|
@ -41,8 +49,8 @@ let op_from_app_name n =
|
|||
let rec simplify env =
|
||||
function
|
||||
| SConst n -> SConst n
|
||||
| SVar id -> (try simplify env (NamesEnv.find id env) with | _ -> SVar id)
|
||||
| SOp (op, e1, e2) ->
|
||||
| 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
|
||||
|
|
@ -56,7 +64,7 @@ let rec simplify env =
|
|||
| SDiv ->
|
||||
if n2 = 0 then raise Instanciation_failed else n1 / n2)
|
||||
in SConst n
|
||||
| (_, _) -> SOp (op, e1, e2))
|
||||
| (_, _) -> Sop (op, e1, e2))
|
||||
|
||||
(** [int_of_size_exp env e] returns the value of the expression
|
||||
[e] in the environment [env], mapping vars to integers. Raises
|
||||
|
|
@ -70,23 +78,23 @@ let int_of_size_exp env e =
|
|||
and a simplified constraint. *)
|
||||
let is_true env =
|
||||
function
|
||||
| Equal (e1, e2) when e1 = e2 ->
|
||||
((Some true), (Equal (simplify env e1, simplify env e2)))
|
||||
| Equal (e1, e2) ->
|
||||
| Cequal (e1, e2) when e1 = e2 ->
|
||||
((Some true), (Cequal (simplify env e1, simplify env e2)))
|
||||
| Cequal (e1, e2) ->
|
||||
let e1 = simplify env e1 in
|
||||
let e2 = simplify env e2
|
||||
in
|
||||
(match (e1, e2) with
|
||||
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
|
||||
| (_, _) -> (None, (Equal (e1, e2))))
|
||||
| LEqual (e1, e2) ->
|
||||
| (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)), (LEqual (e1, e2)))
|
||||
| (_, _) -> (None, (LEqual (e1, e2))))
|
||||
| False -> (None, False)
|
||||
| (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
|
||||
| (_, _) -> (None, (Clequal (e1, e2))))
|
||||
| Cfalse -> (None, Cfalse)
|
||||
|
||||
exception Solve_failed of size_constr
|
||||
|
||||
|
|
@ -108,18 +116,17 @@ let rec solve const_env =
|
|||
in the map (mapping vars to size exps). *)
|
||||
let rec size_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)
|
||||
| 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)
|
||||
| s -> s
|
||||
|
||||
(** Substitutes variables in the constraint list with their value
|
||||
in the map (mapping vars to size exps). *)
|
||||
let instanciate_constr m constr =
|
||||
let replace_one m =
|
||||
function
|
||||
| Equal (e1, e2) -> Equal (size_exp_subst m e1, size_exp_subst m e2)
|
||||
| LEqual (e1, e2) -> LEqual (size_exp_subst m e1, size_exp_subst m e2)
|
||||
| False -> False
|
||||
let replace_one m = function
|
||||
| Cequal (e1, e2) -> Cequal (size_exp_subst m e1, size_exp_subst m e2)
|
||||
| Clequal (e1, e2) -> Clequal (size_exp_subst m e1, size_exp_subst m e2)
|
||||
| Cfalse -> Cfalse
|
||||
in List.map (replace_one m) constr
|
||||
|
||||
let op_to_string =
|
||||
|
|
@ -128,17 +135,17 @@ let op_to_string =
|
|||
let rec print_size_exp ff =
|
||||
function
|
||||
| SConst i -> fprintf ff "%d" i
|
||||
| SVar id -> fprintf ff "%s" id
|
||||
| SOp (op, e1, e2) ->
|
||||
| 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
|
||||
|
||||
let print_size_constr ff = function
|
||||
| Equal (e1, e2) ->
|
||||
| Cequal (e1, e2) ->
|
||||
fprintf ff "@[%a = %a@]" print_size_exp e1 print_size_exp e2
|
||||
| LEqual (e1, e2) ->
|
||||
| Clequal (e1, e2) ->
|
||||
fprintf ff "@[%a <= %a@]" print_size_exp e1 print_size_exp e2
|
||||
| False -> fprintf ff "False"
|
||||
| Cfalse -> fprintf ff "False"
|
||||
|
||||
let psize_constr oc c =
|
||||
let ff = formatter_of_out_channel oc
|
||||
|
|
|
|||
|
|
@ -215,7 +215,7 @@ let rec unify t1 t2 =
|
|||
_ -> raise Unify
|
||||
)
|
||||
| Tarray (ty1, e1), Tarray (ty2, e2) ->
|
||||
add_size_constr (Equal(e1,e2));
|
||||
add_size_constr (Cequal(e1,e2));
|
||||
unify ty1 ty2
|
||||
| _ -> raise Unify
|
||||
|
||||
|
|
@ -607,7 +607,7 @@ and typing_array_op statefull h op e_list =
|
|||
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
|
||||
let e2 = size_exp_of_exp e2 in
|
||||
let typed_e1, t1 = typing statefull h e1 in
|
||||
add_size_constr (LEqual (SConst 1, e2));
|
||||
add_size_constr (Clequal (SConst 1, e2));
|
||||
Tarray (t1, e2), op, [typed_e1; typed_e2]
|
||||
| Eselect idx_list, [e1] ->
|
||||
let typed_e1, t1 = typing statefull h e1 in
|
||||
|
|
@ -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_constr (LEqual (SConst 1, e2));
|
||||
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_constr (Clequal (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, size_exp t1, size_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),
|
||||
|
|
@ -658,7 +658,7 @@ and typing_array_op statefull h op e_list =
|
|||
let e = size_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_constr (LEqual (SConst 1, e));
|
||||
add_size_constr (Clequal (SConst 1, e));
|
||||
List.iter add_size_constr size_constrs;
|
||||
ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
|
||||
typed_e::typed_e_list
|
||||
|
|
@ -718,8 +718,8 @@ and typing_array_subscript statefull h idx_list ty =
|
|||
match ty, idx_list with
|
||||
| ty, [] -> ty
|
||||
| Tarray(ty, exp), idx::idx_list ->
|
||||
add_size_constr (LEqual (SConst 0, idx));
|
||||
add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
|
||||
add_size_constr (Clequal (SConst 0, idx));
|
||||
add_size_constr (Clequal (idx, Sop(SMinus, exp, SConst 1)));
|
||||
typing_array_subscript statefull h idx_list ty
|
||||
| _, _ -> error (Esubscripted_value_not_an_array ty)
|
||||
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@ type iterator_type =
|
|||
| Ifold
|
||||
| Imapfold
|
||||
|
||||
type exp =
|
||||
{ e_desc : desc; e_ty : ty; e_loc : location }
|
||||
type exp = { e_desc : desc; e_ty : ty; e_loc : location }
|
||||
|
||||
and desc =
|
||||
| Econst of const
|
||||
|
|
@ -196,11 +195,11 @@ let op_from_app app =
|
|||
(** Translates a Heptagon exp into a static size exp. *)
|
||||
let rec size_exp_of_exp e =
|
||||
match e.e_desc with
|
||||
| Econstvar n -> SVar n
|
||||
| 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, size_exp_of_exp e1, size_exp_of_exp e2)
|
||||
| _ -> raise Not_static
|
||||
|
||||
(** @return the set of variables defined in [pat]. *)
|
||||
|
|
|
|||
|
|
@ -119,11 +119,12 @@ let rec translate_size_exp const_env e = match e.e_desc with
|
|||
if !check_const_vars & not (NamesEnv.mem n const_env) then
|
||||
Error.message e.e_loc (Error.Econst_var n)
|
||||
else
|
||||
SVar n
|
||||
Svar n
|
||||
| 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_size_exp const_env e1,
|
||||
translate_size_exp const_env e2)
|
||||
| _ -> Error.message e.e_loc Error.Estatic_exp_expected
|
||||
|
||||
let rec translate_type const_env = function
|
||||
|
|
@ -153,7 +154,8 @@ 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;
|
||||
Heptagon.op_params =
|
||||
List.map (translate_size_exp const_env) desc.op_params;
|
||||
Heptagon.op_kind = translate_op_kind desc.op_kind }
|
||||
|
||||
and translate_array_op const_env env = function
|
||||
|
|
@ -184,9 +186,9 @@ and translate_desc loc const_env env = function
|
|||
| 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.size_exp_of_exp e1, c))
|
||||
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
|
||||
| [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
|
||||
Heptagon.Econst (Heptagon.Carray (Heptagon.size_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
|
||||
|
|
|
|||
|
|
@ -13,16 +13,17 @@ type err_kind = | Enot_size_exp
|
|||
|
||||
let err_message ?(exp=void) ?(loc=exp.e_loc) = function
|
||||
| Enot_size_exp ->
|
||||
Printf.eprintf "The expression %a should be a size_exp.@." print_exp exp;
|
||||
Printf.eprintf "The expression %a should be a size_exp.@."
|
||||
print_exp exp;
|
||||
raise Error
|
||||
|
||||
let rec size_exp_of_exp e =
|
||||
match e.e_desc with
|
||||
| Econstvar n -> SVar n
|
||||
| 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)
|
||||
Sop(sop, size_exp_of_exp e1, size_exp_of_exp e2)
|
||||
| _ -> err_message ~exp:e Enot_size_exp
|
||||
|
||||
(** @return the list of bounds of an array type*)
|
||||
|
|
|
|||
Loading…
Reference in a new issue