From 662e81d810c60096ed5a54e824ab657b8c6c98de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Mon, 5 Jul 2010 16:55:14 +0200 Subject: [PATCH] Add location and type to static exps --- compiler/global/initial.ml | 2 ++ compiler/global/types.ml | 9 +++++--- compiler/heptagon/analysis/typing.ml | 27 ++++++++++++++--------- compiler/heptagon/parsing/hept_parser.mly | 10 +++++---- 4 files changed, 30 insertions(+), 18 deletions(-) diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml index 5f25bb6..26d61ec 100644 --- a/compiler/global/initial.ml +++ b/compiler/global/initial.ml @@ -20,6 +20,8 @@ let por = Modname({ qual = "Pervasives"; id = "or" }) let pint = Modname({ qual = "Pervasives"; id = "int" }) let pfloat = Modname({ qual = "Pervasives"; id = "float" }) +let mk_pervasives s = Modname({ qual = "Pervasives"; id = s }) + (* build the initial environment *) let initialize () = List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal; diff --git a/compiler/global/types.ml b/compiler/global/types.ml index 53496a5..736e0c3 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -8,11 +8,13 @@ (**************************************************************************) open Names - +open Location type ty = | Tprod of ty list | Tid of longname | Tarray of ty * static_exp -type static_exp = { se_desc: static_exp_desc; se_typ: loc: location } +type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location } + +and static_exp_desc = | Svar of name | Sint of int | Sfloat of float @@ -25,7 +27,8 @@ type static_exp = { se_desc: static_exp_desc; se_typ: loc: location } let invalid_type = Tprod [] -let const_array_of ty n = Tarray (ty, SConst n) (* TODO ??? *) +let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) = + { se_desc = desc; se_ty = ty; se_loc = loc } open Pp_tools open Format diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index a1ff811..4923476 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -306,7 +306,7 @@ let typing_static_exp const_env se = | 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)) + Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1))) | Stuple se_list -> prod (List.map (typing_static_exp const_env) se_list) @@ -546,7 +546,7 @@ let rec typing statefull h e = let typed_exp, t1 = typing statefull h exp in let typed_e_list = List.map (expect statefull h t1) e_list in Earray(typed_exp::typed_e_list), - const_array_of t1 (List.length e_list + 1) + Tarray(t1, mk_static_exp (Sint (List.length e_list + 1))) (* Arity problems *) | Earray [] -> error (Earity_clash (0, 1)) @@ -635,7 +635,7 @@ and typing_array_op statefull h op e_list = 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 - add_size_constraint (Clequal (Sconst 1, e2)); + add_size_constraint (Clequal (mk_static_exp (Sint 1), e2)); Tarray (t1, e2), op, [typed_e1; typed_e2] | Eselect idx_list, [e1] -> let typed_e1, t1 = typing statefull h e1 in @@ -656,9 +656,12 @@ 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, static_exp_of_exp idx2, static_exp_of_exp idx1) in - let e2 = Sop (SPlus, e1, SConst 1) in - add_size_constr (Clequal (SConst 1, e2)); + let e1 = mk_static_exp (Sop (mk_pervasives "-", + [static_exp_of_exp idx2; + static_exp_of_exp idx1])) in + let e2 = mk_static_exp (Sop (mk_pervasives "+", e1, + mk_static_exp (Sint 1))) in + add_size_constr (Clequal (mk_static_exp (Sint 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 @@ -684,8 +687,8 @@ and typing_array_op statefull h op e_list = (* 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; + add_size_constraint (Clequal (mk_static_exp (Sint 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 @@ -746,9 +749,11 @@ and typing_array_subscript statefull const_env h idx_list ty = | ty, [] -> ty | Tarray(ty, exp), idx::idx_list -> 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 + add_size_constraint (Clequal (mk_static_exp (Sint 0), idx)); + let bound = mk_static_exp (Sop(mk_pervasives "-", + [exp; mk_static_exp (Sint 1))) in + add_size_constraint (Clequal (idx,bound)); + typing_array_subscript statefull h idx_list ty | _, _ -> error (Esubscripted_value_not_an_array ty) (* This function checks that the array dimensions matches diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index efaa590..e7c515f 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -5,6 +5,8 @@ open Location open Names open Hept_parsetree +let mk_static_exp = mk_static_exp ~loc:(current_loc()) + %} %token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL @@ -491,10 +493,10 @@ longname: ; const: - | INT { Sint $1 } - | FLOAT { Sfloat $1 } - | BOOL { Sbool $1 } - | constructor { Sconstructor $1 } + | INT { mk_static_exp (Sint $1) } + | FLOAT { mk_static_exp (Sfloat $1) } + | BOOL { mk_static_exp (Sbool $1) } + | constructor { mk_static_exp (Sconstructor $1) } ; tuple_exp: