diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 0558f7b..8bb2f4b 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -104,6 +104,10 @@ let prod ck_l = match ck_l with | [ck] -> Ck ck | _ -> Cprod (List.map (fun ck -> Ck ck) ck_l) +let rec root_ck_of ck = match ck_repr ck with + | Cbase | Cvar _ -> ck + | Con(ck,_,_) -> root_ck_of ck + (* let rec tuple ck = function | Tprod ty_list -> diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index a102d24..4d4a422 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -146,7 +146,7 @@ let print_ident ff id = Format.fprintf ff "%s" (name id) | Cbase -> fprintf ff "base" | Con (ck, c, n) -> fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n - | Cvar { contents = Cindex _ } -> fprintf ff "base" + | Cvar { contents = Cindex i } -> fprintf ff "'a%i" i | Cvar { contents = Clink ck } -> print_ck ff ck let rec print_ct ff = function diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index a3eac0e..74cd89e 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -139,7 +139,7 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e } = | Some(reset) -> ck_of_name h reset in let ct = typing_app h ck_r pat op args in ct, ck_r - | Eiterator (_, _, _, pargs, args, r) -> + | Eiterator (_, _, _, pargs, args, r) -> (*TODO*) (* Typed exactly as a fun or a node... *) let ck_r = match r with | None -> fresh_clock() @@ -147,7 +147,6 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e } = in List.iter (expect_extvalue h ck_r) pargs; List.iter (expect_extvalue h ck_r) args; - (*TODO*) Ck ck_r, ck_r in e.e_base_ck <- base; @@ -191,11 +190,13 @@ let typing_contract h contract = append_env h c_list let typing_node node = - let h = append_env Env.empty node.n_input in - let h = append_env h node.n_output in - let h = typing_contract h node.n_contract in + let h0 = append_env Env.empty node.n_input in + let h0 = append_env h0 node.n_output in + let h = typing_contract h0 node.n_contract in let h = append_env h node.n_local in typing_eqs h node.n_equs; + (* synchronize input and output on base : find the free vars and set them to base *) + Env.iter (fun id ck -> unify_ck (root_ck_of ck) Cbase) h0; (*update clock info in variables descriptions *) let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in let node = { node with n_input = List.map set_clock node.n_input; diff --git a/compiler/minils/analysis/level_clock.ml b/compiler/minils/analysis/level_clock.ml new file mode 100644 index 0000000..63fc0a5 --- /dev/null +++ b/compiler/minils/analysis/level_clock.ml @@ -0,0 +1,32 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) + +open Clocks +open Minils + +(* Any clock variable left after clocking is free and should be set to level_ck. + Since inputs and outputs are grounded to Cbase, this append when + no data dependance exists between an expression and the inputs/outputs.*) + +(* We are confident that it is sufficient to unify level_ck with base_ck + for expressions having a base_ck == Cvar. + The other ones are coming from one like this one, + indeed if it was Con (Cvar,c,x) x would have to be defined with an expression of clock Cvar.*) + +let exp _ acc e = + let _ = match ck_repr e.e_base_ck with + | Cvar ({contents = Cindex _}) -> unify_ck e.e_base_ck e.e_level_ck + | _ -> () + in + e,acc (* no recursion since in minils exps are not recursive *) + +let program p = + let funs = { Mls_mapfold.defaults with Mls_mapfold.exp = exp } in + let p, _ = Mls_mapfold.program_it funs [] p in + p \ No newline at end of file diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 8a42098..e30b984 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -17,6 +17,9 @@ let compile_program p = (* Clocking *) let p = pass "Clocking" true Clocking.program p pp in + (* Level clocks *) + let p = pass "Level clock" true Level_clock.program p pp in + (* Check that the dataflow code is well initialized *) (*let p = silent_pass "Initialization check" !init Init.program p in *) diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index aaa28e8..10b00f3 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -27,19 +27,7 @@ let rec print_pat ff = function | Evarpat n -> print_ident ff n | Etuplepat pat_list -> fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list -(* -let rec print_ck ff = function - | Cbase -> fprintf ff "base" - | Con (ck, c, n) -> - fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n - | Cvar { contents = Cindex _ } -> fprintf ff "base" - | Cvar { contents = Clink ck } -> print_ck ff ck -let rec print_ct ff = function - | Ck ck -> print_ck ff ck - | Cprod ct_list -> - fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list -*) let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } = if !Compiler_options.full_type_info then fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck diff --git a/test/good/current.ept b/test/good/current.ept index 77b71a9..7a31172 100644 --- a/test/good/current.ept +++ b/test/good/current.ept @@ -11,9 +11,11 @@ let y = x_cur when c tel -node use_current (c : bool; x : int) returns (y : int on c) -var x_cur :int; +node use_current (c : bool; x : int) returns (b : bool on c; y : int on c) +var x_cur, y2 :int; let x_cur = current(c,x); y = x_cur when c; + y2 = internal_current(c,x); + b = y = y2; tel diff --git a/test/good/side_effet.ept b/test/good/side_effet.ept new file mode 100644 index 0000000..f0eb3a9 --- /dev/null +++ b/test/good/side_effet.ept @@ -0,0 +1,10 @@ +node hello() returns (b:bool) +var tmp : bool; +let + tmp = (*printf("hello")*) true; + automaton + state A var ttmp :bool; do + b = true; + ttmp = (*printf("hello")*) true; + end; +tel