Commit adaf9119 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: same fringe; syntax ++ for append

parent 5e956b50
...@@ -153,4 +153,6 @@ why.conf ...@@ -153,4 +153,6 @@ why.conf
/examples/programs/insertion_sort_list/ /examples/programs/insertion_sort_list/
/examples/programs/mergesort_list/ /examples/programs/mergesort_list/
/examples/programs/binary_search/ /examples/programs/binary_search/
/examples/programs/same_fringe/
...@@ -8,11 +8,11 @@ module M ...@@ -8,11 +8,11 @@ module M
lemma Permut_append: lemma Permut_append:
forall l1 l2 k1 k2 : list 'a. forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (append l1 l2) (append k1 k2) permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
lemma Permut_cons_append: lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a. forall x : 'a, l1 l2 : list 'a.
permut (append (Cons x l1) l2) (append l1 (Cons x l2)) permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
let split l0 = let split l0 =
{ length l0 >= 2 } { length l0 >= 2 }
...@@ -24,11 +24,11 @@ let split l0 = ...@@ -24,11 +24,11 @@ let split l0 =
end end
{ let r1, r2 = result in { let r1, r2 = result in
(length r2 = length r1 or length r2 = length r1 + 1) and (length r2 = length r1 or length r2 = length r1 + 1) and
permut (append r1 r2) (append l1 (append l2 l)) } permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
in in
split_aux Nil Nil l0 split_aux Nil Nil l0
{ let (l1, l2) = result in { let (l1, l2) = result in
1 <= length l1 and 1 <= length l2 and permut l0 (append l1 l2) } 1 <= length l1 and 1 <= length l2 and permut l0 (l1 ++ l2) }
let rec merge l1 l2 variant { length l1 + length l2 } = let rec merge l1 l2 variant { length l1 + length l2 } =
{ sorted l1 and sorted l2 } { sorted l1 and sorted l2 }
...@@ -38,7 +38,7 @@ let rec merge l1 l2 variant { length l1 + length l2 } = ...@@ -38,7 +38,7 @@ let rec merge l1 l2 variant { length l1 + length l2 } =
| Cons x1 r1, Cons x2 r2 -> | Cons x1 r1, Cons x2 r2 ->
if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
end end
{ sorted result and permut result (append l1 l2) } { sorted result and permut result (l1 ++ l2) }
let rec mergesort l variant { length l } = let rec mergesort l variant { length l } =
{ } { }
......
(*
``Same fringe'' is a famous problem.
Given two binary search trees, you must decide whether they contain the
same elements. See for instance http://www.c2.com/cgi/wiki?SameFringeProblem
*)
module SameFringe
use import list.List
use import list.Append
(* binary trees with elements at the nodes *)
type elt
type tree =
| Empty
| Node tree elt tree
logic elements (t : tree) : list elt = match t with
| Empty -> Nil
| Node l x r -> elements l ++ Cons x (elements r)
end
(* the left spine of a tree, as a bottom-up list *)
type enum =
| Done
| Next elt tree enum
logic enum_elements (e : enum) : list elt = match e with
| Done -> Nil
| Next x r e -> Cons x (elements r ++ enum_elements e)
end
(* the enum of a tree [t], prepended to a given enum [e] *)
let rec enum t e =
{ }
match t with
| Empty -> e
| Node l x r -> enum l (Next x r e)
end
{ enum_elements result = elements t ++ enum_elements e }
let rec eq_enum e1 e2 =
{ }
match e1, e2 with
| Done, Done ->
True
| Next x1 r1 e1, Next x2 r2 e2 ->
x1 = x2 && eq_enum (enum r1 e1) (enum r2 e2)
| _ ->
False
end
{ result=True <-> enum_elements e1 = enum_elements e2 }
let same_fringe t1 t2 =
{ }
eq_enum (enum t1 Done) (enum t2 Done)
{ result=True <-> elements t1 = elements t2 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/same_fringe.gui"
End:
*)
...@@ -15,17 +15,17 @@ module M ...@@ -15,17 +15,17 @@ module M
lenf q >= lenr q lenf q >= lenr q
logic model (q : queue 'a) : list 'a = logic model (q : queue 'a) : list 'a =
append (front q) (reverse (rear q)) front q ++ reverse (rear q)
let create f lf r lr = let create f lf r lr =
{ lf = length f and lr = length r } { lf = length f and lr = length r }
if lf >= lr then if lf >= lr then
Q f lf r lr Q f lf r lr
else else
let f = append f (reverse r) in let f = f ++ reverse r in
Q f (lf + lr) Nil 0 Q f (lf + lr) Nil 0
: queue 'a : queue 'a
{ inv result and model result = append f (reverse r) } { inv result and model result = f ++ reverse r }
let empty () = let empty () =
{} {}
...@@ -51,7 +51,7 @@ let tail (q : queue 'a) = ...@@ -51,7 +51,7 @@ let tail (q : queue 'a) =
let enqueue (x : 'a) (q : queue 'a) = let enqueue (x : 'a) (q : queue 'a) =
{ inv q } { inv q }
create (front q) (lenf q) (Cons x (rear q)) (lenr q + 1) create (front q) (lenf q) (Cons x (rear q)) (lenr q + 1)
{ inv result and model result = append (model q) (Cons x Nil) } { inv result and model result = model q ++ Cons x Nil }
end end
......
...@@ -79,23 +79,23 @@ end ...@@ -79,23 +79,23 @@ end
theory Append theory Append
use export List use export List
logic append (l1 l2 : list 'a) : list 'a = match l1 with logic (++) (l1 l2 : list 'a) : list 'a = match l1 with
| Nil -> l2 | Nil -> l2
| Cons x1 r1 -> Cons x1 (append r1 l2) | Cons x1 r1 -> Cons x1 (r1 ++ l2)
end end
lemma Append_assoc : lemma Append_assoc :
forall l1 l2 l3 : list 'a. forall l1 l2 l3 : list 'a.
append l1 (append l2 l3) = append (append l1 l2) l3 l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
lemma Append_l_nil : lemma Append_l_nil :
forall l : list 'a. append l Nil = l forall l : list 'a. l ++ Nil = l
use import Length use import Length
use import int.Int use import int.Int
lemma Append_length : lemma Append_length :
forall l1 l2 : list 'a. length (append l1 l2) = length l1 + length l2 forall l1 l2 : list 'a. length (l1 ++ l2) = length l1 + length l2
end end
...@@ -106,7 +106,7 @@ theory Reverse ...@@ -106,7 +106,7 @@ theory Reverse
logic reverse (l : list 'a) : list 'a = match l with logic reverse (l : list 'a) : list 'a = match l with
| Nil -> Nil | Nil -> Nil
| Cons x r -> append (reverse r) (Cons x Nil) | Cons x r -> reverse r ++ Cons x Nil
end end
use import Length use import Length
......
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