jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Add a missing case in Minils Init

Browse source 
The encoding of a reset for e1 -> e2 (in heptagon) is:
	if true fby false then e1 else e2

which is well initiliazed even in e2 = pre x.
This commit is contained in:
Cédric Pasteur 2010-06-22 15:15:51 +02:00 committed by Léonard Gérard
parent 7984917b0e
commit 744f166e12
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
compiler/minils/analysis/init.ml
View file

@ -225,7 +225,13 @@ let rec typing h e =
in skeleton i e.e_ty
| Ewhen (e, c, n) ->
let { t_init = i1 } = Env.find n h in
let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
(* result of the encoding of e1 -> e2 == if true fby false then e1 else e2 *)
| Eifthenelse(
{ e_desc = Efby(Some (Cconstr tn), { e_desc = Econst (Cconstr fn) }) },
e2, e3) when tn = Initial.ptrue & fn = Initial.pfalse ->
expect h e3 (skeleton ione e3.e_ty);
let i = itype (typing h e2) in skeleton i e.e_ty
| Eifthenelse (e1, e2, e3) ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in