Commit a1e032f6 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: tuple terms/expressions do not require parentheses

This makes the syntax cleaner and brings us closer to OCaml.

One incompatibility with the previous grammar is that "ghost"
binds stronger than the left arrow of assignment, and thus
ghost assignments have to be written as "ghost (x.f <- v)".

This is unavoidable, because assignment has to be weaker than
the tuple comma (think "x.f, y.g <- y.g, x.f" or "a[i] <- u,v"),
and "ghost" has to be stronger than comma, for consistency with
our patterns and our return types.

The "return" construction is weaker than comma, for "return a,b".
It is also weaker than assignment, though "return x.f <- b" does
not make much sense either way.

This change does not concern type expressions, where a tuple
type must always have its clothes^Wparentheses on: (int, int).
It might be nice to write "constant pair: int, bool", but on
the other hand this would break casts like "42: int, true".
parent 566a5e90
......@@ -33,12 +33,12 @@ let rec sum (l: list or_integer_float) : (int, real) =
variant { l }
returns { si, sf -> si = add_int l /\ sf = add_real l }
match l with
| Nil -> (0, 0.0)
| Nil -> 0, 0.0
| Cons h t ->
let (a,b) = sum t in
let a,b = sum t in
match h with
| Integer n -> (n + a,b)
| Real x -> (a,x +. b)
| Integer n -> n + a, b
| Real x -> a, x +. b
end
end
......@@ -47,7 +47,7 @@ let main () =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
in
let (s,f) = sum l in
let s,f = sum l in
assert { s = 22 };
assert { f = 4.7 }
......@@ -69,7 +69,7 @@ let sum (l: list or_integer_float) : (int, real) =
!sf +. add_real !ll = add_real l }
variant { !ll }
match !ll with
| Nil -> return (!si, !sf)
| Nil -> return !si, !sf
| Cons (Integer n) t ->
si := !si + n; ll := t
| Cons (Real x) t ->
......@@ -84,7 +84,7 @@ let main () =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
in
let (s,f) = sum l in
let s,f = sum l in
assert { s = 22 };
assert { f = 4.7 }
......
......@@ -46,6 +46,6 @@ module Division
r := !r - y;
q := !q + 1
done;
(!q, !r)
!q, !r
end
......@@ -116,18 +116,18 @@ module Puzzle12
match balance (balls[0] + balls[8]) (balls[9] + balls[10]) with
| Equal -> (* 0,8 = 9,10 *)
match balance balls[0] balls[11] with
| Right -> (11, False) | _ -> (11, True) end
| Right -> 11, False | _ -> 11, True end
| Right -> (* 0,8 < 9,10 *)
match balance balls[9] balls[10] with
| Equal -> (8, True)
| Right -> (10, False)
| Left -> (9, False)
| Equal -> 8, True
| Right -> 10, False
| Left -> 9, False
end
| Left -> (* 0,8 > 9,10 *)
match balance balls[9] balls[10] with
| Equal -> (8, False)
| Right -> (9, True)
| Left -> (10, True)
| Equal -> 8, False
| Right -> 9, True
| Left -> 10, True
end
end
| Right -> (* 0,1,2,3 < 4,5,6,7 *)
......@@ -135,20 +135,20 @@ module Puzzle12
(balls[2] + balls[5] + balls[8]) with
| Equal -> (* 0,1,4 = 2,5,8 *)
match balance balls[6] balls[7] with
| Equal -> (3, True)
| Right -> (7, False)
| Left -> (6, False)
| Equal -> 3, True
| Right -> 7, False
| Left -> 6, False
end
| Right -> (* 0,1,4 < 2,5,8 *)
match balance balls[0] balls[1] with
| Equal -> (5, False)
| Right -> (0, True)
| Left -> (1, True)
| Equal -> 5, False
| Right -> 0, True
| Left -> 1, True
end
| Left -> (* 0,1,4 > 2,5,8 *)
match balance balls[4] balls[8] with
| Equal -> (2, True)
| _ -> (4, False)
| Equal -> 2, True
| _ -> 4, False
end
end
| Left -> (* 0,1,2,3 > 4,5,6,7 *)
......@@ -156,21 +156,21 @@ module Puzzle12
(balls[2] + balls[5] + balls[8]) with
| Equal -> (* 0,1,4 = 2,5,8 *)
match balance balls[6] balls[7] with
| Equal -> (3, False)
| Right -> (6, True)
| Left -> (7, True)
| Equal -> 3, False
| Right -> 6, True
| Left -> 7, True
end
| Right -> (* 0,1,4 < 2,5,8 *)
match balance balls[2] balls[5] with
| Equal -> (4, True)
| Right -> (5, False)
| Left -> (2, False)
| Equal -> 4, True
| Right -> 5, False
| Left -> 2, False
end
| Left -> (* 0,1,4 > 2,5,8 *)
match balance balls[0] balls[1] with
| Equal -> (5, True)
| Right -> (1, False)
| Left -> (0, False)
| Equal -> 5, True
| Right -> 1, False
| Left -> 0, False
end
end
end
......
......@@ -257,7 +257,7 @@ module BinomialHeap
requires { inv k h }
requires { h <> Nil }
variant { h }
ensures { let (t, h') = result in
ensures { let t, h' = result in
heaps (Cons t Nil) && heaps h' && inv k h' &&
le_roots t.elem h && binomial_tree t &&
forall x. occ x h = occ x (Cons t Nil) + occ x h' }
......@@ -266,10 +266,10 @@ module BinomialHeap
| Nil ->
absurd
| Cons t Nil ->
(t, Nil)
t, Nil
| Cons t tl ->
let (t', tl') = extract_min_tree (rank t + 1) tl in
if le t.elem t'.elem then (t, tl) else (t', Cons t tl')
let t', tl' = extract_min_tree (rank t + 1) tl in
if le t.elem t'.elem then t, tl else t', Cons t tl'
end
let rec extract_min (h: heap) : (elt, heap)
......@@ -277,13 +277,13 @@ module BinomialHeap
requires { inv 0 h }
requires { h <> Nil }
variant { h }
ensures { let (e, h') = result in
ensures { let e, h' = result in
heaps h' && inv 0 h' &&
occ e h' = occ e h - 1 &&
forall x. x <> e -> occ x h' = occ x h }
=
let (t, h') = extract_min_tree 0 h in
(t.elem, merge 0 (reverse t.children) h')
let t, h' = extract_min_tree 0 h in
t.elem, merge 0 (reverse t.children) h'
(** Complexity analysis. *)
......
......@@ -100,7 +100,7 @@ module BraunHeaps
requires { inv t }
requires { 0 < size t }
variant { t }
ensures { let (e, t') = result in
ensures { let e, t' = result in
heap t' && inv t' && size t' = size t - 1 &&
occ e t' = occ e t - 1 &&
forall x. x <> e -> occ x t' = occ x t }
......@@ -110,10 +110,10 @@ module BraunHeaps
absurd
| Node Empty y r ->
assert { r = Empty };
(y, Empty)
y, Empty
| Node l y r ->
let (x, l) = extract l in
(x, Node r y l)
let x, l = extract l in
x, Node r y l
end
let rec replace_min (x: elt) (t: tree elt)
......@@ -162,7 +162,7 @@ module BraunHeaps
if le lx ly then
Node r lx (merge ll lr)
else
let (x, l) = extract l in
let x, l = extract l in
Node (replace_min x r) ly l
| Empty, _ ->
absurd
......
......@@ -115,11 +115,11 @@ let function interpret_0 (p:prog) : int = eval_0 p
*)
let test () =
(interpret_0 p0,
interpret_0 p0,
interpret_0 p1,
interpret_0 p2,
interpret_0 p3,
interpret_0 p4)
interpret_0 p4
constant v3 : int = eval_0 p3
......@@ -269,11 +269,11 @@ let interpret_2 (p:prog) : int
= eval_2 p I
let test () =
(interpret_2 p0,
interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4)
interpret_2 p4
end
......@@ -379,11 +379,11 @@ let interpret_2 (p:prog) : int
= eval_2 p I
let test () =
(interpret_2 p0,
interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4)
interpret_2 p4
end
......@@ -715,11 +715,11 @@ let interpret_4 (p:prog) : value
let test () =
(interpret_4 p0,
interpret_4 p0,
interpret_4 p1,
interpret_4 p2,
interpret_4 p3,
interpret_4 p4)
interpret_4 p4
end
......@@ -902,7 +902,7 @@ lemma size_c_pos: forall c: context. size_c c >= 0
let rec decompose_term (e:expr) (c:context) : (context, expr)
variant { size_e e + size_c c }
ensures { let (c1,e1) = result in
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c /\ is_a_value e }
......@@ -915,7 +915,7 @@ let rec decompose_term (e:expr) (c:context) : (context, expr)
with decompose_cont (c:context) (n:int) : (context, expr)
variant { size_c c }
ensures { let (c1,e1) = result in
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c (Cte n) /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c }
......@@ -924,11 +924,11 @@ with decompose_cont (c:context) (n:int) : (context, expr)
match c with
| Empty -> raise Stuck
| Left c e -> decompose_term e (Right n c)
| Right n1 c -> (c, Sub (Cte n1) (Cte n))
| Right n1 c -> c, Sub (Cte n1) (Cte n)
end
let decompose (e:expr) : (context, expr)
ensures { let (c1,e1) = result in recompose c1 e1 = e /\
ensures { let c1,e1 = result in recompose c1 e1 = e /\
is_a_redex e1 }
raises { Stuck -> is_a_value e }
=
......@@ -961,7 +961,7 @@ let reduce (e:expr) : expr
ensures { eval_0 result = eval_0 e }
raises { Stuck -> is_a_value e }
=
let (c,r) = decompose e in
let c,r = decompose e in
recompose c (contract r)
(**
......@@ -1000,7 +1000,7 @@ let rec itere (e:expr) : int
let refocus c e
ensures { let (c1,e1) = result in
ensures { let c1,e1 = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { Stuck -> is_empty_context c /\ is_a_value e }
......@@ -1063,11 +1063,11 @@ let interpret p
= eval_1 Empty p
let test () =
(interpret p0,
interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4)
interpret p4
end
......@@ -1164,11 +1164,11 @@ let interpret p
= eval_1 Empty p
let test () =
(interpret p0,
interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4)
interpret p4
end
......@@ -73,8 +73,8 @@ module Esterel
in
assert {
forall x. mem x res.mdl ->
let (y,z) =
if mem x a.mdl then (x,min_elt b.mdl) else (min_elt a.mdl,x)
let y,z =
if mem x a.mdl then x, min_elt b.mdl else min_elt a.mdl, x
in
mem y a.mdl /\ mem z b.mdl /\ x = max y z };
res
......
......@@ -145,7 +145,7 @@ module Zeckendorf
let greatest_fib (x: int) : (int, int)
requires { 0 < x }
ensures { let (k, fk) = result in
ensures { let k, fk = result in
2 <= k /\ 1 <= fk = fib k <= x < fib (k + 1) }
=
let a = ref 1 in
......@@ -160,7 +160,7 @@ module Zeckendorf
b := f;
k := !k + 1
done;
(!k, !a)
!k, !a
let zeckendorf (n: int) : list int
requires { 0 <= n }
......@@ -175,7 +175,7 @@ module Zeckendorf
invariant { !x + sum !l = n }
invariant { match !l with Nil -> true | Cons k _ -> !x < fib (k-1) end }
variant { !x }
let (k, fk) = greatest_fib !x in
let k, fk = greatest_fib !x in
x := !x - fk;
l := Cons k !l
done;
......@@ -239,19 +239,19 @@ module Zeckendorf
requires { wf k lc }
requires { k >= 2 /\ lc <> Nil }
requires { 0 <= acc = sum lb - sum lc < fib (k-1) }
returns { (x,p) -> fib x <= sum lb = acc + fib x + sum p < fib (x+1) }
returns { (x,p) -> wf k p /\ x >= k /\ lc = snoc p x }
returns { x,p -> fib x <= sum lb = acc + fib x + sum p < fib (x+1) }
returns { x,p -> wf k p /\ x >= k /\ lc = snoc p x }
variant { lc }
= match lc with
| Nil -> absurd
| Cons x Nil -> (x,Nil)
| Cons x q -> let (y,p) = decomp (x+2) (acc+fib x) q lb in (y,Cons x p)
| Cons x Nil -> x,Nil
| Cons x q -> let y,p = decomp (x+2) (acc+fib x) q lb in y,Cons x p
end in
match l1 , l2 with
| Nil , Nil -> ()
| Nil , l | l , Nil -> let _ = decomp 2 0 l l in absurd
| _ , _ -> let (_,q1) = decomp 2 0 l1 l1 in
let (_,q2) = decomp 2 0 l2 l2 in
| _ , _ -> let _,q1 = decomp 2 0 l1 l1 in
let _,q2 = decomp 2 0 l2 l2 in
zeckendorf_unique q1 q2
end
......@@ -299,7 +299,7 @@ module FibonacciLogarithmic
ensures { let a, b = result in
power m1110 n = { a11 = a+b; a12 = b; a21 = b; a22 = a } }
= if n = 0 then
(1, 0)
1, 0
else begin
assert { 0 <= div n 2 };
let a, b = logfib (div n 2) in
......@@ -307,12 +307,12 @@ module FibonacciLogarithmic
if mod n 2 = 0 then
begin
assert { 2 * (div n 2) = (div n 2) + (div n 2) };
(a*a+ b*b, b*(a + c))
a*a+ b*b, b*(a + c)
end
else
begin
assert { 2 * (div n 2) + 1 = (div n 2) + (div n 2) + 1 };
(b*(a + c), c*c + b*b)
b*(a + c), c*c + b*b
end
end
......
module FingerTrees
use import int.Int
use import list.List
use import list.Length
use import list.Append
type digit 'a =
| One 'a
| Two 'a 'a
| Three 'a 'a 'a
| Four 'a 'a 'a 'a
function d_m (b:digit 'a) : list 'a = match b with
| One x -> Cons x Nil
| Two y x -> Cons y (Cons x Nil)
| Three z y x -> Cons z (Cons y (Cons x Nil))
| Four u z y x -> Cons u (Cons z (Cons y (Cons x Nil)))
end
type node 'a =
| Node2 'a 'a
| Node3 'a 'a 'a
function node_cons (nd:node 'a) (l:list 'a) : list 'a = match nd with
| Node2 x y -> Cons x (Cons y l)
| Node3 x y z -> Cons x (Cons y (Cons z l))
end
let lemma node_cons_app (nd:node 'a) (p q:list 'a)
ensures { node_cons nd (p++q) = node_cons nd p ++ q }
= match nd with Node2 _ _ -> "keep_on_simp" () | _ -> () end
function flatten (l:list (node 'a)) : list 'a = match l with
| Nil -> Nil
| Cons nd q -> node_cons nd (flatten q)
end
type t 'a =
| Empty
| Single (digit 'a)
| Deep (digit 'a) (t (node 'a)) (digit 'a)
function t_m (t:t 'a) : list 'a = match t with
| Empty -> Nil
| Single x -> d_m x
| Deep l m r -> d_m l ++ flatten (t_m m) ++ d_m r
end
let d_cons (x:'a) (d:digit 'a) : (digit 'a,list (node 'a))
returns { (b,o) -> Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 }
returns { b,o -> Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 }
= match d with
| One y -> (Two x y , Nil)
| Two y z -> (Three x y z , Nil)
| Three y z t -> (Four x y z t , Nil)
| Four y z t u -> (Two x y , Cons (Node3 z t u) Nil)
| One y -> Two x y , Nil
| Two y z -> Three x y z , Nil
| Three y z t -> Four x y z t , Nil
| Four y z t u -> Two x y , Cons (Node3 z t u) Nil
end
let rec cons (x:'a) (t:t 'a) : t 'a
ensures { t_m result = Cons x (t_m t) }
variant { t }
= match t with
| Empty -> Single (One x)
| Single d -> Deep (One x) Empty d
| Deep lf md rg -> let (lf2 , rem) = d_cons x lf in
| Deep lf md rg -> let lf2 , rem = d_cons x lf in
match rem with
| Nil -> Deep lf2 md rg
| Cons x q -> assert { q = Nil };
Deep lf2 (cons x md) rg
end
end
end
......@@ -102,6 +102,6 @@ module SimpleQueue
*)
q.data[q.n] <- x;
q.n <- q.n + 1;
ghost q.contents <- q.contents ++ Cons x Nil
ghost (q.contents <- q.contents ++ Cons x Nil)
end
......@@ -88,7 +88,7 @@ module Mergesort
let split (l0: list 'a) : (list 'a, list 'a)
requires { length l0 >= 2 }
ensures { let (l1, l2) = result in
ensures { let l1, l2 = result in
1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) }
= let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a)
requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
......@@ -97,7 +97,7 @@ module Mergesort
permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
variant { length l }
= match l with
| Nil -> (l1, l2)
| Nil -> l1, l2
| Cons x r -> split_aux l2 (Cons x l1) r
end
in
......
......@@ -267,7 +267,7 @@ module PatienceAbstract
0 <= s.stacks[i][j] < s.num_elts)
(** contents of stacks are valid card indexes *)
/\ (forall i. 0 <= i < s.num_elts ->
let (is,ip) = s.positions[i] in
let is,ip = s.positions[i] in
0 <= is < s.num_stacks &&
let st = s.stacks[is] in
0 <= ip < s.stack_sizes[is] &&
......@@ -296,7 +296,7 @@ module PatienceAbstract
(** the predecessor is a valid index or [-1] *)
pred < i /\
(** predecessor is always a smaller index *)
let (is,_ip) = s.positions[i] in
let is,_ip = s.positions[i] in
if pred < 0 then is = 0
(** if predecessor is [-1] then [i] is in leftmost stack *)
else
......@@ -304,7 +304,7 @@ module PatienceAbstract
(** if predecessor is not [-1], it denotes a card with smaller value... *)
is > 0 &&
(** ...the card is not on the leftmost stack... *)
let (ps,_pp) = s.positions[pred] in
let ps,_pp = s.positions[pred] in
ps = is - 1)
(** ...and predecessor is in the stack on the immediate left *)
......@@ -333,7 +333,7 @@ module PatienceAbstract
!pred = top_stack_im1 /\
c > s.values[!pred] /\
0 <= !pred < s.num_elts /\
let (ps,_pp) = s.positions[!pred] in
let ps,_pp = s.positions[!pred] in
ps = i - 1
}
let stack_i = s.stacks[i] in
......@@ -341,7 +341,7 @@ module PatienceAbstract
let top_stack_i = stack_i[stack_i_size - 1] in
if c <= s.values[top_stack_i] then raise (Return i);
assert { 0 <= top_stack_i < s.num_elts };
assert { let (is,ip) = s.positions[top_stack_i] in
assert { let is,ip = s.positions[top_stack_i] in
0 <= is < s.num_stacks &&
0 <= ip < s.stack_sizes[is] &&
s.stacks[is][ip] = top_stack_i &&
......@@ -359,7 +359,7 @@ module PatienceAbstract
s.num_stacks <- s.num_stacks + 1;
s.stack_sizes <- s.stack_sizes[i <- 1];
s.stacks <- s.stacks[i <- new_stack_i];
s.positions <- s.positions[idx <- (i,0)];
s.positions <- s.positions[idx <- i,0];
s.preds <- s.preds[idx <- !pred]
with Return i ->
let stack_i = s.stacks[i] in
......@@ -372,7 +372,7 @@ module PatienceAbstract
(* s.num_stacks unchanged *)
s.stack_sizes <- s.stack_sizes[i <- stack_i_size + 1];
s.stacks <- s.stacks[i <- new_stack_i];
s.positions <- s.positions[idx <- (i,stack_i_size)];
s.positions <- s.positions[idx <- i,stack_i_size];
s.preds <- s.preds[idx <- !pred];
end
......@@ -471,7 +471,7 @@ module PatienceAbstract
for i = ns-1 downto 0 do
invariant { -1 <= !idx < s.num_elts }
invariant { i >= 0 -> !idx >= 0 &&
let (is,_) = s.positions[!idx] in is = i }
let is,_ = s.positions[!idx] in is = i }
invariant { i+1 < ns -> !idx < !seq[i+1] }
invariant { 0 <= i < ns-1 -> s.values[!idx] < s.values[!seq[i+1]] }
invariant { forall j. i < j < ns -> 0 <= !seq[j] < s.num_elts }
......@@ -496,7 +496,7 @@ module PatienceAbstract
increasing_subsequence sigma input /\ sigma.seqlen > s.num_stacks ->
let f = fun i ->
let si = sigma.seqval[i] in
let (stack_i,_) = s.positions[si] in
let stack_i,_ = s.positions[si] in
stack_i
in range f sigma.seqlen s.num_stacks &&
not (injective f sigma.seqlen s.num_stacks)
......@@ -509,8 +509,8 @@ module PatienceAbstract
0 <= i < j < sigma.seqlen &&
let si = sigma.seqval[i] in
let sj = sigma.seqval[j] in
let (stack_i,_pi) = s.positions[si] in
let (stack_j,_pj) = s.positions[sj] in
let stack_i,_pi = s.positions[si] in
let stack_j,_pj = s.positions[sj] in
stack_i = stack_j
};
assert { (* contradiction from non-injectivity *)
......@@ -520,8 +520,8 @@ module PatienceAbstract
0 <= i < j < sigma.seqlen ->
let si = sigma.seqval[i] in
let sj = sigma.seqval[j] in
let (stack_i,pi) = s.positions[si] in
let (stack_j,pj) = s.positions[sj] in
let stack_i,pi = s.positions[si] in
let stack_j,pj = s.positions[sj] in
stack_i = stack_j ->
si < sj && pi < pj && s.values[si] < s.values[sj]
};
......@@ -596,7 +596,7 @@ module PatienceFull
!pred = top_stack_im1 /\
c > state.values[!pred] /\
0 <= !pred < state.num_elts /\
let (ps,_pp) = state.positions[!pred] in
let ps,_pp = state.positions[!pred] in
ps = !i - 1
}
invariant { old_stacks = rev_append !acc !rem_stacks }
......@@ -626,7 +626,7 @@ module PatienceFull
let ghost stack_i_size = state.stack_sizes[!i] in
let ghost top_stack_i = stack_i[stack_i_size - 1] in
assert { 0 <= top_stack_i < state.num_elts };
assert { let (is,ip) = state.positions[top_stack_i] in
assert { let is,ip = state.positions[top_stack_i] in
0 <= is < state.num_stacks &&
0 <= ip < state.stack_sizes[is] &&
state.stacks[is][ip] = top_stack_i &&
......@@ -648,7 +648,7 @@ module PatienceFull
state.num_stacks <- state.num_stacks + 1;
state.stack_sizes <- state.stack_sizes[i <- 1];
state.stacks <- state.stacks[i <- new_stack_i];
state.positions <- state.positions[idx <- (i,0)];
state.positions <- state.positions[idx <- i,0];
state.preds <- state.preds[idx <- !pred];
(* we put card [c] in a new stack *)
rev_append (Cons (Cons c Nil) !acc) Nil
......@@ -665,7 +665,7 @@ module PatienceFull
(* state.num_stacks unchanged *)
state.stack_sizes <- state.stack_sizes[!i <- stack_i_size + 1];
state.stacks <- state.stacks[!i <- new_stack_i];
state.positions <- state.positions[idx <- (!i,stack_i_size)];
state.positions <- state.positions[idx <- !i,stack_i_size];
state.preds <- state.preds[idx <- !pred];
(* card is placed on the leftmost stack where its card
value is no greater than the topmost card on that
......@@ -824,7 +824,7 @@ module PatienceFull
for i = ns-1 downto 0 do
invariant { -1 <= !idx < state.num_elts }
invariant { i >= 0 -> !idx >= 0 &&
let (is,_) = state.positions[!idx] in is = i }
let is,_ = state.positions[!idx] in is = i }
invariant { i+1 < ns -> !idx < !seq[i+1] }
invariant { 0 <= i < ns-1 -> state.values[!idx] < state.values[!seq[i+1]] }
invariant { forall j. i < j < ns -> 0 <= !seq[j] < state.num_elts }
......@@ -848,7 +848,7 @@ module PatienceFull
increasing_subsequence sigma input /\ sigma.seqlen > state.num_stacks ->
let f = fun i ->
let si = sigma.seqval[i] in
let (stack_i,_) = state.positions[si] in
let stack_i,_ = state.positions[si] in
stack_i
in range f sigma.seqlen state.num_stacks &&
not (injective f sigma.seqlen state.num_stacks)
......@@ -860,8 +860,8 @@ module PatienceFull
0 <= i < j < sigma.seqlen &&
let si = sigma.seqval[i] in
let sj = sigma.seqval[j] in
let (stack_i,_pi) = state.positions[si] in
let (stack_j,_pj) = state.positions[sj] in
let stack_i,_pi = state.positions[si] in
let stack_j,_pj = state.positions[sj] in
stack_i = stack_j
};
assert { (* contradiction from non-injectivity *)
......@@ -871,8 +871,8 @@ module PatienceFull
0 <= i < j < sigma.seqlen ->
let si = sigma.seqval[i] in
let sj = sigma.seqval[j] in
let (stack_i,pi) = state.positions[si] in
let (stack_j,pj) = state.positions[sj] in
let stack_i,pi = state.positions[si] in
let stack_j,pj = state.positions[sj] in
stack_i = stack_j ->
si < sj && pi < pj && state.values[si] < state.values[sj]
};
......
......@@ -102,10 +102,10 @@ module DFA
function exec (a:t) (q:state) (w:word) : state =
match w with
| Nil -> q
| Cons c r -> let q' = a.transition[(q,c)] in exec a q' r
| Cons c r -> let q' = a.transition[q,c] in exec a q' r
end
function accepts (a:t) (w:word) : bool =
a.is_final_state[exec a 0 w]
end
\ No newline at end of file
end
......@@ -52,13 +52,13 @@ module SwapInt32
let swap (a b: int32) : (int32, int32)
requires { in_bounds a /\ in_bounds b }
ensures { let (x,y) = result in
returns { x,y ->
to_int x = to_int b /\ to_int y = to_int a }
=
let a = a + b in
let b = a - b in
let a = a - b in
(a, b)
a, b
(* then rephrased with mutable variables *)
......
......@@ -23,15 +23,15 @@ module Convolution
let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a)
variant { x }
requires { length x <= length y }
ensures { let (r, ys) = result in exists y0: list 'a.
ensures { let r, ys = result in exists y0: list 'a.
y = y0 ++ ys && length y0 = length x &&
r = combine x (reverse y0) }
= match x with
| Nil ->
(Nil, y)
Nil, y
| Cons x0 xs ->
match convolution_rec xs y with
| r, Cons y0 ys -> (Cons (x0, y0) r, ys)
| r, Cons y0 ys -> Cons (x0, y0) r, ys
| _ -> absurd end
end
......
</
......@@ -219,8 +219,8 @@ module LinearProbing
assert { numofd h.data 0 (i+1) =
numofd (h.data at L) 0 (i+1) - 1 }
end;
ghost h.view <- Map.set h.view (keym x) True;
ghost h.loc <- Map.set h.loc (keym x) i
ghost (h.view <- Map.set h.view (keym x) True);
ghost (h.loc <- Map.set h.loc (keym x) i)
let copy (h: t) : t
ensures { result.view = h.view }
......@@ -313,11 +313,11 @@ module LinearProbing
h.data[j] <- dummy;
assert { numofd h.data 0 (j+1) =
numofd (h.data at L) 0 (j+1) + 1 };
ghost h.view <- Map.set h.view (keym x) False;
ghost (h.view <- Map.set h.view (keym x) False);
let l = ref h.loc in