parsing clocks.
This commit is contained in:
parent
a8215c8083
commit
88497a2da3
|
@ -54,6 +54,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
|
||||||
"enforce", ENFORCE;
|
"enforce", ENFORCE;
|
||||||
"with", WITH;
|
"with", WITH;
|
||||||
"when", WHEN;
|
"when", WHEN;
|
||||||
|
"whenot", WHENOT;
|
||||||
"merge", MERGE;
|
"merge", MERGE;
|
||||||
"on", ON;
|
"on", ON;
|
||||||
"map", MAP;
|
"map", MAP;
|
||||||
|
@ -130,6 +131,7 @@ rule token = parse
|
||||||
| "{" {LBRACE}
|
| "{" {LBRACE}
|
||||||
| "}" {RBRACE}
|
| "}" {RBRACE}
|
||||||
| ":" {COLON}
|
| ":" {COLON}
|
||||||
|
| "::" {COLONCOLON}
|
||||||
| ";" {SEMICOL}
|
| ";" {SEMICOL}
|
||||||
| "=" {EQUAL}
|
| "=" {EQUAL}
|
||||||
| "==" {EQUALEQUAL}
|
| "==" {EQUALEQUAL}
|
||||||
|
|
|
@ -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 EQUAL EQUALEQUAL LESS_GREATER BARBAR COMMA BAR ARROW LET TEL
|
||||||
%token <string> Constructor
|
%token <string> Constructor
|
||||||
%token <string> IDENT
|
%token <string> IDENT
|
||||||
|
@ -39,7 +39,7 @@ open Hept_parsetree
|
||||||
%token ASSUME
|
%token ASSUME
|
||||||
%token ENFORCE
|
%token ENFORCE
|
||||||
%token WITH
|
%token WITH
|
||||||
%token WHEN MERGE ON
|
%token WHEN WHENOT MERGE ON
|
||||||
%token POWER
|
%token POWER
|
||||||
%token LBRACKET LBRACKETGREATER
|
%token LBRACKET LBRACKETGREATER
|
||||||
%token RBRACKET LESSRBRACKET
|
%token RBRACKET LESSRBRACKET
|
||||||
|
@ -65,7 +65,7 @@ open Hept_parsetree
|
||||||
%left AMPERSAND
|
%left AMPERSAND
|
||||||
%left INFIX0 EQUAL LESS_GREATER
|
%left INFIX0 EQUAL LESS_GREATER
|
||||||
%right INFIX1
|
%right INFIX1
|
||||||
%right WHEN
|
%right WHEN WHENOT
|
||||||
%left INFIX2 SUBTRACTIVE
|
%left INFIX2 SUBTRACTIVE
|
||||||
%left STAR INFIX3
|
%left STAR INFIX3
|
||||||
%left INFIX4
|
%left INFIX4
|
||||||
|
@ -193,7 +193,7 @@ nonmt_params:
|
||||||
;
|
;
|
||||||
|
|
||||||
param:
|
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 }
|
{ List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl }
|
||||||
;
|
;
|
||||||
|
|
||||||
|
@ -248,11 +248,11 @@ loc_params:
|
||||||
|
|
||||||
|
|
||||||
var_last:
|
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 }
|
{ 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)) ] }
|
{ [ 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)) ] }
|
{ [ mk_var_dec id ty ck (Last(None)) (Loc($startpos,$endpos)) ] }
|
||||||
;
|
;
|
||||||
|
|
||||||
|
@ -268,13 +268,26 @@ ty_ident:
|
||||||
{ Tarray ($1, $3) }
|
{ Tarray ($1, $3) }
|
||||||
;
|
;
|
||||||
|
|
||||||
ck:
|
ct_annot:
|
||||||
| /*empty */ { None }
|
| /*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 }
|
| ON ck=on_ck { Some ck }
|
||||||
|
|
||||||
|
ck:
|
||||||
|
| DOT { Cbase }
|
||||||
|
| ck=on_ck { ck }
|
||||||
|
|
||||||
|
|
||||||
on_ck:
|
on_ck:
|
||||||
| c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) }
|
| 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:
|
equs:
|
||||||
| /* empty */ { [] }
|
| /* empty */ { [] }
|
||||||
|
@ -427,7 +440,7 @@ merge_handler:
|
||||||
| LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) }
|
| LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) }
|
||||||
|
|
||||||
exp:
|
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)) }
|
| e=_exp { mk_exp e (Loc($startpos,$endpos)) }
|
||||||
_exp:
|
_exp:
|
||||||
| simple_exp FBY exp
|
| simple_exp FBY exp
|
||||||
|
@ -447,6 +460,10 @@ _exp:
|
||||||
{ mk_op_call $2 [$1; $3] }
|
{ mk_op_call $2 [$1; $3] }
|
||||||
| e=exp WHEN c=constructor_or_bool LPAREN ce=IDENT RPAREN
|
| e=exp WHEN c=constructor_or_bool LPAREN ce=IDENT RPAREN
|
||||||
{ Ewhen (e, c, ce) }
|
{ 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
|
| MERGE n=IDENT hs=merge_handlers
|
||||||
{ Emerge (n, hs) }
|
{ Emerge (n, hs) }
|
||||||
| exp INFIX1 exp
|
| exp INFIX1 exp
|
||||||
|
@ -634,8 +651,8 @@ nonmt_params_signature:
|
||||||
;
|
;
|
||||||
|
|
||||||
param_signature:
|
param_signature:
|
||||||
| IDENT COLON ty_ident ck=ck { mk_arg (Some $1) $3 ck }
|
| IDENT COLON ty_ident ck=ck_annot { mk_arg (Some $1) $3 ck }
|
||||||
| ty_ident ck=ck { mk_arg None $1 ck }
|
| ty_ident ck=ck_annot { mk_arg None $1 ck }
|
||||||
;
|
;
|
||||||
|
|
||||||
%%
|
%%
|
||||||
|
|
|
@ -34,11 +34,6 @@ struct
|
||||||
raise Errors.Error
|
raise Errors.Error
|
||||||
end
|
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 exp_list_of_static_exp_list se_list =
|
||||||
let mk_one_const se =
|
let mk_one_const se =
|
||||||
mk_exp (Econst se) se.se_ty
|
mk_exp (Econst se) se.se_ty
|
||||||
|
|
|
@ -44,16 +44,10 @@ struct
|
||||||
raise Errors.Error
|
raise Errors.Error
|
||||||
end
|
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;
|
let translate_var { Heptagon.v_ident = n; Heptagon.v_type = ty;
|
||||||
Heptagon.v_loc = loc } =
|
Heptagon.v_loc = loc; Heptagon.v_clock = ck } =
|
||||||
mk_var_dec ~loc:loc n ty
|
mk_var_dec ~loc:loc n ty ck
|
||||||
|
|
||||||
let translate_reset = function
|
let translate_reset = function
|
||||||
| Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n
|
| Some { Heptagon.e_desc = Heptagon.Evar n } -> Some n
|
||||||
|
|
|
@ -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 =
|
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 }
|
{ 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 =
|
let mk_var_dec ?(loc = no_location) ident ty ck =
|
||||||
{ v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }
|
{ v_ident = ident; v_type = ty; v_clock = ck; v_loc = loc }
|
||||||
|
|
||||||
let mk_equation ?(loc = no_location) pat exp =
|
let mk_equation ?(loc = no_location) pat exp =
|
||||||
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
|
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
|
||||||
|
|
11
test/bad/when_merge1.ept
Normal file
11
test/bad/when_merge1.ept
Normal file
|
@ -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
|
|
@ -15,170 +15,12 @@ node t2bool(x: t) returns (b: bool)
|
||||||
b = merge x (A-> true) (B-> false)
|
b = merge x (A-> true) (B-> false)
|
||||||
tel
|
tel
|
||||||
|
|
||||||
(*
|
node filter(x:int; c:t) returns (y:int on A(c))
|
||||||
node mm(x: int) returns (o: int)
|
|
||||||
var last m: int = 0;
|
|
||||||
let
|
let
|
||||||
switch (x = 0)
|
y = x when A(c)
|
||||||
| true do m = last m + 1; o = m
|
|
||||||
| false do m = 2; o = m
|
|
||||||
end
|
|
||||||
tel
|
tel
|
||||||
|
|
||||||
node mmm(x: int) returns (o2: int)
|
node fusion(x1:int; x2:int; c:t) returns (y :int)
|
||||||
var last m: int = 1; o: int;
|
|
||||||
let
|
let
|
||||||
automaton
|
y = merge c (A -> x1) (B -> x2)
|
||||||
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
|
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
|
|
||||||
*) *)
|
|
||||||
|
|
Loading…
Reference in a new issue