Commit 4160347c authored by Andrei Paskevich's avatar Andrei Paskevich

one-branch match may be not ghost even if the matched expr is one

parent 056a7875
......@@ -171,8 +171,7 @@ module Tower_of_Hanoi
ensures { c.rod = old c.rod }
= if n > 0 then begin
let ghost t = c.rod in
let ghost x = match p with Cons x _ -> x | Nil -> absurd end in
let ghost r = match p with Cons _ r -> r | Nil -> absurd end in
let x,r = match p with Cons x r -> (x,r) | Nil -> absurd end in
hanoi_rec a c b (n-1) r (Cons x s);
move a b x s;
hanoi_rec c b a (n-1) r t
......
......@@ -663,7 +663,9 @@ let e_case e0 bl =
let vty = VTvalue (vty_value ~ghost bity) in
mk_expr (Ecase (e0,bl)) vty eff (add_e_vars e0 varm)
in
branch vtv0.vtv_ghost eff_empty Mid.empty bl
(* a one-branch match may be not ghost even if the matched expr is *)
let ghost = match bl with [_] -> false | _ -> vtv0.vtv_ghost in
branch ghost eff_empty Mid.empty bl
(* ghost *)
......
......@@ -753,6 +753,8 @@ and print_lexpr pri info fmt e =
| Eany _ ->
fprintf fmt "@[(%a :@ %a)@]" to_be_implemented "any"
(print_vty info) e.e_vty
| Ecase (e1, [_,e2]) when vty_ghost e1.e_vty ->
print_lexpr pri info fmt e2
| Ecase (e1, bl) ->
fprintf fmt "@[(match @[%a@] with@\n@[<hov>%a@])@]"
(print_expr info) e1 (print_list newline (print_ebranch info)) bl
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment