Commit 9c1eff28 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

WhyML: switch Mlw_typing to the new Mlw_dexpr-based API

parent 9ebe7ff1
module M
use import int.Int
let rec f (x:int) = f (x-1)
end
......@@ -99,13 +99,13 @@ module Treedel
forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
inorder (zip (Node l x r) z) = inorder l ++ Cons x (inorder (zip r z))
let ghost left (t: tree loc) : tree loc
let ghost tree_left (t: tree loc) : tree loc
requires { t <> Empty }
ensures { match t with Empty -> false | Node l _ _ -> result = l end }
=
match t with Empty -> absurd | Node l _ _ -> l end
let ghost right (t: tree loc) : tree loc
let ghost tree_right (t: tree loc) : tree loc
requires { t <> Empty }
ensures { match t with Empty -> false | Node _ _ r -> result = r end }
=
......@@ -142,8 +142,8 @@ module Treedel
let pp = ref t in
let tt = ref (get_left !p) in
let ghost zipper = ref Top in
let ghost ppr = ref (right it) in
let ghost subtree = ref (left it) in
let ghost ppr = ref (tree_right it) in
let ghost subtree = ref (tree_left it) in
while !tt <> null do
invariant { !pp <> null /\ !mem[!pp].left = !p }
invariant { !p <> null /\ !mem[!p].left = !tt }
......@@ -151,8 +151,8 @@ module Treedel
istree !mem !pp pt /\ zip pt !zipper = it }
assert { istree !mem !p !subtree };
ghost zipper := Left !zipper !pp !ppr;
ghost ppr := right !subtree;
ghost subtree := left !subtree;
ghost ppr := tree_right !subtree;
ghost subtree := tree_left !subtree;
pp := !p;
p := !tt;
tt := get_left !p
......@@ -162,8 +162,8 @@ module Treedel
let m = get_data !p in
tt := get_right !p;
mem := set !mem !pp { !mem[!pp] with left = !tt };
let ghost pl = left !subtree in assert { pl = Empty };
ghost ot := zip (right !subtree) (Left !zipper !pp !ppr);
let ghost pl = tree_left !subtree in assert { pl = Empty };
ghost ot := zip (tree_right !subtree) (Left !zipper !pp !ppr);
(t, m)
end
......
......@@ -1236,7 +1236,7 @@ expr:
(Eloop ($4,
mk_expr (Eif ($2, $5,
mk_expr (Eraise (exit_exn (), None)))))),
[exit_exn (), mk_pat (PPptuple []), mk_expr (Etuple [])])) }
[exit_exn (), None, mk_expr (Etuple [])])) }
| FOR lident EQUAL expr for_direction expr DO for_loop_invariant expr DONE
{ mk_expr (Efor ($2, $4, $5, $6, $8, $9)) }
| ABSURD
......@@ -1327,9 +1327,9 @@ list1_handler_sep_bar:
handler:
| uqualid ARROW expr
{ ($1, { pat_desc = PPptuple []; pat_loc = floc_i 1 }, $3) }
{ ($1, None, $3) }
| uqualid pat_arg ARROW expr
{ ($1, $2, $4) }
{ ($1, Some $2, $4) }
;
program_match_cases:
......
......@@ -239,7 +239,7 @@ and expr_desc =
| Ematch of expr * (pattern * expr) list
| Eabsurd
| Eraise of qualid * expr option
| Etry of expr * (qualid * pattern * expr) list
| Etry of expr * (qualid * pattern option * expr) list
| Efor of ident * expr * for_direction * expr * invariant * expr
(* annotations *)
| Eassert of assertion_kind * lexpr
......
This diff is collapsed.
......@@ -23,9 +23,8 @@ val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val fs_at : Term.lsymbol
(* unused
val fs_old : Term.lsymbol
*)
val t_at_old : Term.term -> Term.term
val th_mark_at : Theory.theory
......
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