mergesort_list.mlw 2.77 KB
 Jean-Christophe Filliatre committed Apr 03, 2011 1 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2014 2 3 4 5 ``````(** Sorting a list of integers using mergesort Author: Jean-Christophe Filliâtre (CNRS) *) `````` Jean-Christophe Filliatre committed Apr 03, 2011 6 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 7 ``````module Elt `````` 8 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 9 10 11 12 `````` use export int.Int use export list.Length use export list.Append use export list.Permut `````` 13 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 14 15 16 17 18 19 20 `````` type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le clone export list.Sorted with type t = elt, predicate le = le end `````` Jean-Christophe Filliatre committed Mar 29, 2014 21 ``````module Merge (* : MergeSpec *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 22 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2014 23 `````` clone export Elt `````` Jean-Christophe Filliatre committed Mar 28, 2014 24 25 26 `````` let rec merge (l1 l2: list elt) : list elt requires { sorted l1 /\ sorted l2 } `````` Jean-Christophe Filliatre committed Mar 29, 2014 27 28 `````` ensures { sorted result } ensures { permut result (l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 29 30 31 32 33 34 35 36 37 38 `````` variant { length l1 + length l2 } = match l1, l2 with | Nil, _ -> l2 | _, Nil -> l1 | Cons x1 r1, Cons x2 r2 -> if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) end end `````` Jean-Christophe Filliatre committed Mar 29, 2014 39 ``````(** tail recursive implementation *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 40 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2014 41 42 43 ``````module EfficientMerge (* : MergeSpec *) clone export Elt `````` Jean-Christophe Filliatre committed Mar 28, 2014 44 45 46 47 `````` use import list.Mem use import list.Reverse use import list.RevAppend `````` Jean-Christophe Filliatre committed Mar 29, 2014 48 49 50 51 `````` lemma sorted_reverse_cons: forall acc x1. sorted (reverse acc) -> (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc)) `````` Jean-Christophe Filliatre committed Mar 28, 2014 52 53 54 55 `````` let rec merge_aux (acc l1 l2: list elt) : list elt requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 } requires { forall x y: elt. mem x acc -> mem y l1 -> le x y } requires { forall x y: elt. mem x acc -> mem y l2 -> le x y } `````` Jean-Christophe Filliatre committed Mar 29, 2014 56 57 `````` ensures { sorted result } ensures { permut result (acc ++ l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 `````` variant { length l1 + length l2 } = match l1, l2 with | Nil, _ -> rev_append acc l2 | _, Nil -> rev_append acc l1 | Cons x1 r1, Cons x2 r2 -> if le x1 x2 then merge_aux (Cons x1 acc) r1 l2 else merge_aux (Cons x2 acc) l1 r2 end let merge (l1 l2: list elt) : list elt requires { sorted l1 /\ sorted l2 } ensures { sorted result /\ permut result (l1 ++ l2) } = merge_aux Nil l1 l2 end module Mergesort `````` Jean-Christophe Filliatre committed Mar 29, 2014 77 `````` clone import Merge `````` Jean-Christophe Filliatre committed Mar 28, 2014 78 79 `````` let split (l0: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 80 `````` requires { length l0 >= 2 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 81 `````` ensures { let (l1, l2) = result in `````` Andrei Paskevich committed Oct 13, 2012 82 `````` 1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 83 `````` = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 84 `````` requires { length l2 = length l1 \/ length l2 = length l1 + 1 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 85 `````` ensures { let r1, r2 = result in `````` Andrei Paskevich committed Oct 13, 2012 86 87 `````` (length r2 = length r1 \/ length r2 = length r1 + 1) /\ permut (r1 ++ r2) (l1 ++ (l2 ++ l)) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 88 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 89 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 90 91 92 93 94 `````` | Nil -> (l1, l2) | Cons x r -> split_aux l2 (Cons x l1) r end in split_aux Nil Nil l0 `````` Jean-Christophe Filliatre committed May 20, 2011 95 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 96 `````` let rec mergesort (l: list elt) : list elt `````` Andrei Paskevich committed Oct 13, 2012 97 `````` ensures { sorted result /\ permut result l } `````` Jean-Christophe Filliatre committed Mar 28, 2014 98 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 99 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 100 101 `````` | Nil | Cons _ Nil -> l | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2) `````` 102 103 `````` end `````` Jean-Christophe Filliatre committed Dec 29, 2010 104 ``end``