From 88497a2da3fc9c42bdaab3916f687e405a1e1ffd Mon Sep 17 00:00:00 2001 From: Leonard Gerard Date: Tue, 10 May 2011 21:55:53 +0200 Subject: [PATCH] parsing clocks. --- compiler/heptagon/parsing/hept_lexer.mll | 2 + compiler/heptagon/parsing/hept_parser.mly | 45 +++-- .../heptagon/transformations/normalize.ml | 5 - compiler/main/hept2mls.ml | 10 +- compiler/minils/minils.ml | 4 +- test/bad/when_merge1.ept | 11 ++ test/good/when_merge1.ept | 168 +----------------- 7 files changed, 53 insertions(+), 192 deletions(-) create mode 100644 test/bad/when_merge1.ept diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 6663ac2..e9891e6 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -54,6 +54,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "enforce", ENFORCE; "with", WITH; "when", WHEN; + "whenot", WHENOT; "merge", MERGE; "on", ON; "map", MAP; @@ -130,6 +131,7 @@ rule token = parse | "{" {LBRACE} | "}" {RBRACE} | ":" {COLON} + | "::" {COLONCOLON} | ";" {SEMICOL} | "=" {EQUAL} | "==" {EQUALEQUAL} diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 9db93af..c90ca7c 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -9,7 +9,7 @@ open Hept_parsetree %} -%token DOT LPAREN LPAREN_LESS RPAREN GREATER_RPAREN LBRACE RBRACE COLON SEMICOL +%token DOT LPAREN LPAREN_LESS RPAREN GREATER_RPAREN LBRACE RBRACE COLON COLONCOLON SEMICOL %token EQUAL EQUALEQUAL LESS_GREATER BARBAR COMMA BAR ARROW LET TEL %token Constructor %token IDENT @@ -39,7 +39,7 @@ open Hept_parsetree %token ASSUME %token ENFORCE %token WITH -%token WHEN MERGE ON +%token WHEN WHENOT MERGE ON %token POWER %token LBRACKET LBRACKETGREATER %token RBRACKET LESSRBRACKET @@ -65,7 +65,7 @@ open Hept_parsetree %left AMPERSAND %left INFIX0 EQUAL LESS_GREATER %right INFIX1 -%right WHEN +%right WHEN WHENOT %left INFIX2 SUBTRACTIVE %left STAR INFIX3 %left INFIX4 @@ -193,7 +193,7 @@ nonmt_params: ; param: - | idl=ident_list COLON ty=ty_ident ck=ck + | idl=ident_list COLON ty=ty_ident ck=ck_annot { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl } ; @@ -248,11 +248,11 @@ loc_params: var_last: - | idl=ident_list COLON ty=ty_ident ck=ck + | idl=ident_list COLON ty=ty_ident ck=ck_annot { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl } - | LAST id=IDENT COLON ty=ty_ident ck=ck EQUAL e=exp + | LAST id=IDENT COLON ty=ty_ident ck=ck_annot EQUAL e=exp { [ mk_var_dec id ty ck (Last(Some(e))) (Loc($startpos,$endpos)) ] } - | LAST id=IDENT COLON ty=ty_ident ck=ck + | LAST id=IDENT COLON ty=ty_ident ck=ck_annot { [ mk_var_dec id ty ck (Last(None)) (Loc($startpos,$endpos)) ] } ; @@ -268,13 +268,26 @@ ty_ident: { Tarray ($1, $3) } ; -ck: - | /*empty */ { None } - | ON ck=on_ck { Some ck } +ct_annot: + | /*empty */ { None } + | COLONCOLON ck=ck + | ON ck=on_ck { Some(Ck ck) } + + +ck_annot: + | /*empty */ { None } + | COLONCOLON ck=ck + | ON ck=on_ck { Some ck } + +ck: + | DOT { Cbase } + | ck=on_ck { ck } + on_ck: | c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) } - | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(b,c,x) } + | b=ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(b,c,x) } + equs: | /* empty */ { [] } @@ -427,7 +440,7 @@ merge_handler: | LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) } exp: - | e=simple_exp { e } + | e=simple_exp ct=ct_annot { { e with e_ct_annot = ct } } | e=_exp { mk_exp e (Loc($startpos,$endpos)) } _exp: | simple_exp FBY exp @@ -447,6 +460,10 @@ _exp: { mk_op_call $2 [$1; $3] } | e=exp WHEN c=constructor_or_bool LPAREN ce=IDENT RPAREN { Ewhen (e, c, ce) } + | e=exp WHEN ce=IDENT + { Ewhen (e, Q Initial.ptrue, ce) } + | e=exp WHENOT ce=IDENT + { Ewhen (e, Q Initial.pfalse, ce) } | MERGE n=IDENT hs=merge_handlers { Emerge (n, hs) } | exp INFIX1 exp @@ -634,8 +651,8 @@ nonmt_params_signature: ; param_signature: - | IDENT COLON ty_ident ck=ck { mk_arg (Some $1) $3 ck } - | ty_ident ck=ck { mk_arg None $1 ck } + | IDENT COLON ty_ident ck=ck_annot { mk_arg (Some $1) $3 ck } + | ty_ident ck=ck_annot { mk_arg None $1 ck } ; %% diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 27608c5..ec99352 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -34,11 +34,6 @@ struct raise Errors.Error end -let is_stateful e = match e.e_desc with - | Efby _ | Epre _ -> true - | Eapp({ a_op = Enode _ }, _, _) -> true - | _ -> false - let exp_list_of_static_exp_list se_list = let mk_one_const se = mk_exp (Econst se) se.se_ty diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 13db8cf..c9bc74a 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -44,16 +44,10 @@ struct raise Errors.Error end -(* add an equation *) -let equation locals eqs e = - let n = Idents.gen_var "hept2mls" "ck" in - n, - (mk_var_dec n e.e_ty) :: locals, - (mk_equation (Evarpat n) e):: eqs let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty; - Heptagon.v_loc = loc } = - mk_var_dec ~loc:loc n ty + Heptagon.v_loc = loc; Heptagon.v_clock = ck } = + mk_var_dec ~loc:loc n ty ck let translate_reset = function | Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 4ffcd2f..eefcb9a 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -153,8 +153,8 @@ let mk_extvalue ~ty ?(clock = fresh_clock()) ?(loc = no_location) desc = let mk_exp level_ck ty ?(ck = Cbase) ?(ct = fresh_ct ty) ?(loc = no_location) desc = { e_desc = desc; e_ty = ty; e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc } -let mk_var_dec ?(loc = no_location) ?(clock = fresh_clock()) ident ty = - { v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc } +let mk_var_dec ?(loc = no_location) ident ty ck = + { v_ident = ident; v_type = ty; v_clock = ck; v_loc = loc } let mk_equation ?(loc = no_location) pat exp = { eq_lhs = pat; eq_rhs = exp; eq_loc = loc } diff --git a/test/bad/when_merge1.ept b/test/bad/when_merge1.ept new file mode 100644 index 0000000..50984f0 --- /dev/null +++ b/test/bad/when_merge1.ept @@ -0,0 +1,11 @@ +(* pour debugger ../../compiler/hec.byte -i -v -I ../../lib t1.ept *) +(* pour debugger + directory parsing global analysis dataflow sequential sigali simulation translation main + set arguments -v ../test/good/t1.ept *) + +type t = A | B + +node fusion(x1:int on B(c); x2:int; c:t) returns (y :int) + let + y = merge c (A -> x1) (B -> x2) + tel diff --git a/test/good/when_merge1.ept b/test/good/when_merge1.ept index 2449542..c34d117 100644 --- a/test/good/when_merge1.ept +++ b/test/good/when_merge1.ept @@ -15,170 +15,12 @@ node t2bool(x: t) returns (b: bool) b = merge x (A-> true) (B-> false) tel -(* -node mm(x: int) returns (o: int) - var last m: int = 0; +node filter(x:int; c:t) returns (y:int on A(c)) let - switch (x = 0) - | true do m = last m + 1; o = m - | false do m = 2; o = m - end + y = x when A(c) tel -node mmm(x: int) returns (o2: int) - var last m: int = 1; o: int; +node fusion(x1:int; x2:int; c:t) returns (y :int) let - automaton - state I - do m = 0; o = last m + 1 until (o = 1) then J - state J - do m = last m + 1; o = 0 - end; - o2 = 1 -> pre o - tel - -node m(x: int) returns (o: int) - var last o2 : int = 1; - let - automaton - state I - do o2 = 1 - unless (last o2 = 2) then J - state J - do o2 = 3 - unless (last o2 = 1) then I - end; - o = o2; - tel - -node h(z: int; x, y: int) returns (o2: int) - var o1, o: int; - let - (o1, o2) = if z<0 then (1, 2) else (3, 4); - o = 0 -> pre o + 2 - tel - -node i(x, y: int) returns (o: int) - var z, k: int; - let - reset - o = 0 + x + y; - reset - z = 1 + o + 3; - k = z + o + 2 - every (x = x) - every (x = y) - tel - -node j(x, y: int) returns (o: int) - let - automaton - state I - var z: int; - do o = 1; z = 2 - until (o = 2) then J - state J - do o = 2 - until (o = 1) then I - end - tel - -node (++)(up, down: int) returns (o: int) - var last cpt: int = 42; - let - o = last cpt; - automaton - state Init - var k : int; - do k = 0 -> pre k + 2; - cpt = 0 - until - (up = 1) then Up - state Up - do cpt = last cpt + 1 - until (down = 1) then Down - | (down = 0) then Up - state Down - do cpt = (last cpt) + 1 - until (up = 1) then Up - end; - tel - -node f(x: bool) returns (y: bool) - var z: bool; - let - y = x or x & x; - z = true -> if y then not (pre z) else pre z; - tel - -(* -let increasing(x) returns (o) - do true -> x >= pre(x) + 1 done - -modes(v0) = - last o = v0 - when up(x) returns (w) - assume (x >= 0) ensure (w >= 0) - do w = x + last o + 2; o = w + 4 done - when down(x) returns (w) - do w = x - last o + 2; o = w + 2 done - end - -val gain : int > - modes last o : int when up: int -> int when down: int -> int - end with { up # down } - -let node gain(v0)(up, down) returns (o) - assume (v0 >= 0) & (increasing up) - guaranty (deacreasing o) - last o = 0 in - automaton - state Await - do - unless down then Down(1) | up then Up(1) - state Down(d) - let rec cpt = 1 -> pre cpt + 1 in - do o = last o - d - until (cpt >= 5) then Down(d-5) - until up then Up(1) - state Up(d) - let rec cpt = 1 -> pre cpt + 1 in - do o = last o + d - until (cpt >= 5) then Up(d+5) - until down then Down(1) - state Unreachable - let rec c = 0 + 2 in - var m in - do o = m + 2; m = 3 + c done - end - -node g(x, y: int) returns (o: int) - let - o = x ++ y; - tel - -node dfby(x)(y) returns (o) - let - o = x fby (x fby y) - tel - -node f(x)(y) returns (o) - var last o = x; - let - o = last o + y - tel - -val f : int > (int => int) - -static x = e in ... - -(if c then (fun x -> x + 2) else (fun k -> k + 3))(x+2) - -let M(x1,..., xn) = - let y1 = ... in ... let yk = ... in - modes - mem m1 = ...; mem ml = ...; - step (...) returns (...) ... - reset = ... - end -*) *) + y = merge c (A -> x1) (B -> x2) + tel