From 4b3c3ba8b591a8c7ce2096768954f6e1dd283b66 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Tue, 3 Aug 2010 22:38:42 +0200 Subject: [PATCH] Revert "Fixed problem in clocking" e3676d1e3cb851c0041758c2a60f93e26b4933c7 Fixing the actual bug : * static_exp should not be created without type after or during the typing pass. --- compiler/global/clocks.ml | 6 +-- compiler/global/initial.ml | 12 ++++++ compiler/global/types.ml | 3 +- compiler/heptagon/analysis/causality.ml | 2 - compiler/heptagon/analysis/typing.ml | 37 +++++++++---------- compiler/heptagon/heptagon.ml | 9 ++--- compiler/heptagon/transformations/automata.ml | 13 +++++-- compiler/heptagon/transformations/reset.ml | 4 +- compiler/main/hept2mls.ml | 2 +- compiler/main/mls2obc.ml | 19 ++++++---- compiler/minils/analysis/clocking.ml | 4 +- compiler/minils/main/mls_compiler.ml | 2 +- compiler/minils/parsing/mls_parser.mly | 2 + 13 files changed, 65 insertions(+), 50 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index b048982..0b183e5 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -95,9 +95,9 @@ let rec skeleton ck = function | Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list) | Tarray _ | Tid _ -> Ck ck -let rec const_skeleton se = match se.se_desc with - | Stuple se_list -> Cprod (List.map const_skeleton se_list) - | _ -> Ck (new_var ()) +let rec const_skeleton ck se = match se.se_desc with + | Stuple se_list -> Cprod (List.map (const_skeleton ck) se_list) + | _ -> Ck ck let ckofct = function | Ck ck -> ck_repr ck | Cprod ct_list -> Cbase diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml index 26d61ec..bc4756b 100644 --- a/compiler/global/initial.ml +++ b/compiler/global/initial.ml @@ -9,6 +9,7 @@ (* initialization of the typing environment *) open Names +open Types let tglobal = [] let cglobal = [] @@ -22,6 +23,17 @@ let pfloat = Modname({ qual = "Pervasives"; id = "float" }) let mk_pervasives s = Modname({ qual = "Pervasives"; id = s }) +let mk_static_int_op op args = + mk_static_exp ~ty:(Tid pint) (Sop (op,args)) + +let mk_static_int i = + mk_static_exp ~ty:(Tid pint) (Sint i) + +let mk_static_bool b = + mk_static_exp ~ty:(Tid pbool) (Sbool b) + + + (* 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 474af30..0a3681b 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -34,11 +34,10 @@ let prod = function | [ty] -> ty | ty_list -> Tprod ty_list +(** DO NOT use this after the typing, since it gives invalid_type *) let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = { se_desc = desc; se_ty = ty; se_loc = loc } -let static_exp_of_int i = - mk_static_exp (Sint i) open Pp_tools open Format diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index d9aa932..708d610 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -9,8 +9,6 @@ (* causality check *) -(* $Id: causality.ml 615 2009-11-20 17:43:14Z pouzet $ *) - open Misc open Names open Idents diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 1398109..c00e48e 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -477,7 +477,7 @@ and typing_static_exp const_env se = let typed_se, ty = typing_static_exp const_env se in let typed_se_list = List.map (expect_static_exp const_env ty) se_list in Sarray (typed_se::typed_se_list), - Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1))) + Tarray(ty, mk_static_int ((List.length se_list) + 1)) | Stuple se_list -> let typed_se_list, ty_list = List.split (List.map (typing_static_exp const_env) se_list) in @@ -596,7 +596,7 @@ let rec typing const_env h e = (* add size constraints *) let size_constrs = instanciate_constr m ty_desc.node_params_constraints in - add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n)); + add_size_constraint (Clequal (mk_static_int 1, typed_n)); List.iter add_size_constraint size_constrs; (* return the type *) Eiterator(it, { app with a_op = op; a_params = typed_params } @@ -666,8 +666,7 @@ and typing_app const_env h op e_list = | { a_op = Earray }, exp::e_list -> let typed_exp, t1 = typing const_env h exp in let typed_e_list = List.map (expect const_env h t1) e_list in - let n = mk_static_exp ~ty:(Tid Initial.pint) - (Sint (List.length e_list + 1)) in + let n = mk_static_int (List.length e_list + 1) in Tarray(t1, n), op, typed_exp::typed_e_list | { a_op = Efield; a_params = [f] }, [e] -> @@ -698,7 +697,7 @@ and typing_app const_env h op e_list = | { a_op = Earray_fill; a_params = [n] }, [e1] -> let typed_n = expect_static_exp const_env (Tid Initial.pint) n in let typed_e1, t1 = typing const_env h e1 in - add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n)); + add_size_constraint (Clequal (mk_static_int 1, typed_n)); Tarray (t1, typed_n), { op with a_params = [typed_n] }, [typed_e1] | { a_op = Eselect; a_params = idx_list }, [e1] -> @@ -726,11 +725,11 @@ and typing_app const_env h op e_list = let typed_idx2 = expect_static_exp const_env (Tid Initial.pint) idx2 in let typed_e, t1 = typing const_env h e in (*Create the expression to compute the size of the array *) - let e1 = mk_static_exp (Sop (mk_pervasives "-", - [typed_idx2; typed_idx1])) in - let e2 = mk_static_exp (Sop (mk_pervasives "+", - [e1;mk_static_exp (Sint 1) ])) in - add_size_constraint (Clequal (mk_static_exp (Sint 1), e2)); + let e1 = + mk_static_int_op (mk_pervasives "-") [typed_idx2; typed_idx1] in + let e2 = + mk_static_int_op (mk_pervasives "+") [e1;mk_static_int 1 ] in + add_size_constraint (Clequal (mk_static_int 1, e2)); Tarray (element_type t1, e2), { op with a_params = [typed_idx1; typed_idx2] }, [typed_e] @@ -742,8 +741,8 @@ and typing_app const_env h op e_list = with TypingError(kind) -> message e1.e_loc kind end; - let n = mk_static_exp (Sop (mk_pervasives "+", - [array_size t1; array_size t2])) in + let n = + mk_static_int_op (mk_pervasives "+") [array_size t1; array_size t2] in Tarray (element_type t1, n), op, [typed_e1; typed_e2] (*Arity problems*) @@ -823,13 +822,13 @@ and typing_array_subscript const_env h idx_list ty = | Tarray(ty, exp), idx::idx_list -> ignore (expect_static_exp const_env (Tid Initial.pint) exp); let typed_idx = expect_static_exp const_env (Tid Initial.pint) idx in - 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)); - let typed_idx_list, ty = - typing_array_subscript const_env h idx_list ty in - typed_idx::typed_idx_list, ty + add_size_constraint (Clequal (mk_static_int 0, idx)); + let bound = + mk_static_int_op (mk_pervasives "-") [exp; mk_static_int 1] in + add_size_constraint (Clequal (idx,bound)); + let typed_idx_list, ty = + typing_array_subscript const_env h idx_list ty in + typed_idx::typed_idx_list, ty | _, _ -> error (Esubscripted_value_not_an_array ty) (* This function checks that the array dimensions matches diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 72e1be8..d9af65a 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -14,6 +14,7 @@ open Idents open Static open Signature open Types +open Initial type state_name = name @@ -175,12 +176,8 @@ let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs = { b_local = []; b_equs = eqs; b_defnames = defnames; b_statefull = statefull; b_loc = no_location } -let dfalse = - mk_exp (Econst (mk_static_exp (Sconstructor Initial.pfalse))) - (Tid Initial.pbool) -let dtrue = - mk_exp (Econst (mk_static_exp (Sconstructor Initial.ptrue))) - (Tid Initial.pbool) +let dfalse = mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) +let dtrue = mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) let mk_ifthenelse e1 e2 e3 = { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] } diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml index fb6c641..67ed26a 100644 --- a/compiler/heptagon/transformations/automata.ml +++ b/compiler/heptagon/transformations/automata.ml @@ -14,6 +14,7 @@ open Names open Idents open Heptagon open Hept_mapfold +open Initial let mk_var_exp n ty = mk_exp (Evar n) ty @@ -28,11 +29,15 @@ let mk_switch_equation e l = mk_equation (Eswitch (e, l)) let mk_exp_fby_false e = - mk_exp (Epre (Some (mk_static_exp (Sconstructor Initial.pfalse)), e)) + mk_exp (Epre (Some (mk_static_bool false), e)) (Tid Initial.pbool) +let mk_constructor constr ty = + mk_static_exp ~ty:ty (Sconstructor constr) + +(* Be sure that [initial] is of the right type [e.e_ty] before using this *) let mk_exp_fby_state initial e = - { e with e_desc = Epre (Some (mk_static_exp (Sconstructor initial)), e) } + { e with e_desc = Epre (Some (mk_constructor initial e.e_ty), e) } (* the list of enumerated types introduced to represent states *) let state_type_dec_list = ref [] @@ -71,8 +76,8 @@ let translate_automaton v eq_list handlers = let pre_next_resetname = Idents.fresh "pnr" in let name n = Name(NamesEnv.find n states) in - let state n = mk_exp (Econst (mk_static_exp - (Sconstructor (name n)))) tstatetype in + let state n = + mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype in let statevar n = mk_var_exp n tstatetype in let boolvar n = mk_var_exp n (Tid Initial.pbool) in diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml index 0f05765..a463970 100644 --- a/compiler/heptagon/transformations/reset.ml +++ b/compiler/heptagon/transformations/reset.ml @@ -14,6 +14,7 @@ open Idents open Heptagon open Hept_mapfold open Types +open Initial (* We introduce an initialization variable for each block *) (* Using an asynchronous reset would allow to produce *) @@ -52,8 +53,7 @@ let mk_bool_param n = let or_op_call e_list = mk_op_app (Efun Initial.por) e_list let pre_true e = - { e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool) - (Sconstructor Initial.ptrue)), e) } + { e with e_desc = Epre (Some (mk_static_bool true), e) } let init e = pre_true { dfalse with e_loc = e.e_loc } let add_resets res e = diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index cff50ae..e929cb4 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -178,7 +178,7 @@ let switch x ci_eqs_list = | [] | (_, []) :: _ -> [] | (ci, (y, { e_ty = ty; e_loc = loc }) :: _) :: _ -> let ci_e_list, ci_eqs_list = split ci_eqs_list in - (y, mk_exp ~exp_ty:ty (Emerge(x, ci_e_list))) :: + (y, mk_exp ~exp_ty:ty ~loc:loc (Emerge(x, ci_e_list))) :: distribute ci_eqs_list in check ci_eqs_list; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index eadebfd..ae22871 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -17,6 +17,11 @@ open Types open Control open Static open Obc_mapfold +open Initial + +(** Not giving any type and called after typing, DO NOT use it anywhere else *) +let static_exp_of_int i = + Types.mk_static_exp (Types.Sint i) let gen_obj_name n = (shortname n) ^ "_mem" ^ (gen_symbol ()) @@ -197,13 +202,11 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } [mk_evar cpt; mk_exp (Econst idx1) ])) in (* bound = (idx2 - idx1) + 1*) - let bound = - mk_static_exp (Sop(op_from_string "+", - [ mk_static_exp (Sint 1); - mk_static_exp (Sop (op_from_string "-", - [idx2;idx1])) ])) in + let bound = mk_static_int_op (op_from_string "+") + [ mk_static_int 1; + mk_static_int_op (op_from_string "-") [idx2;idx1] ] in let action = - Afor (cpt, mk_static_exp (Sint 0), bound, + Afor (cpt, mk_static_int 0, bound, mk_block [Aassgn (mk_lhs (Larray (var_from_name map x, mk_evar cpt)), mk_lhs_exp (Larray (lhs_of_exp e, idx)))] ) @@ -242,7 +245,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } Minils.a_params = [n] }, [e], _) -> let cpt = Idents.fresh "i" in let action = - Afor (cpt, mk_static_exp (Sint 0), n, + Afor (cpt, mk_static_int 0, n, mk_block [Aassgn (mk_lhs (Larray (var_from_name map x, mk_evar cpt)), translate map (si, j, s) e) ]) @@ -259,7 +262,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } let e1 = translate map (si, j, s) e1 in let e2 = translate map (si, j, s) e2 in let a1 = - Afor (cpt1, mk_static_exp (Sint 0), n1, + Afor (cpt1, mk_static_int 0, n1, mk_block [Aassgn (mk_lhs (Larray (x, mk_evar cpt1)), mk_lhs_exp (Larray (lhs_of_exp e1, mk_evar cpt1)))] ) in diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 18dfbc5..9dc82c5 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -35,7 +35,7 @@ let typ_of_name h x = Env.find x h let rec typing h e = let ct = match e.e_desc with - | Econst se -> const_skeleton se + | Econst se -> skeleton (new_var ()) se.se_ty | Evar x -> Ck (typ_of_name h x) | Efby (c, e) -> typing h e | Eapp({a_op = op}, args, r) -> @@ -94,7 +94,7 @@ and expect h expected_ty e = let actual_ty = typing h e in try unify actual_ty expected_ty with - | Unify -> eprintf "e %a : " print_exp e; + | Unify -> eprintf "%a : " print_exp e; error_message e.e_loc (Etypeclash (actual_ty, expected_ty)) and typing_c_e_list h ck_c n c_e_list = diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 4a8133c..1f4489b 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -14,7 +14,7 @@ let pp p = if !verbose then Mls_printer.print stdout p let compile pp p = (* Clocking *) - let p = do_pass Clocking.program "Clocking" p pp false in + let p = do_pass Clocking.program "Clocking" p pp true in (* Check that the dataflow code is well initialized *) (*let p = do_silent_pass Init.program "Initialization check" p !init in *) diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 159b2d9..05b5b67 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -147,9 +147,11 @@ constructor: /* of type longname */ | ln=qualified(CONSTRUCTOR) { ln } | b=BOOL { Name(if b then "true" else "false") } +/* TODO donner un type !! Phase de typing. */ field: | ln=longname { mk_static_exp ~loc:(Loc($startpos,$endpos)) (Sconstructor ln)} +/* TODO donner un type !! Phase de typing. */ const : c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c } _const: | i=INT { Sint i }