diff --git a/compiler/global/static.ml b/compiler/global/static.ml index a0d3f9b..501a168 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -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 diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index dad5c7e..f9a1547 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -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) diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 5a696fb..cb61fd8 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -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]. *) diff --git a/compiler/heptagon/parsing/scoping.ml b/compiler/heptagon/parsing/scoping.ml index 519ebcb..ec670b5 100644 --- a/compiler/heptagon/parsing/scoping.ml +++ b/compiler/heptagon/parsing/scoping.ml @@ -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 diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 0b3a95d..b6caf3d 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -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*)