there_and_back_again.mlw 2.59 KB
 Jean-Christophe Filliatre committed Jun 12, 2013 1 `````` `````` Jean-Christophe Filliatre committed Jun 12, 2013 2 ``````(* Two puzzles from Danvy and Goldberg's ``There and back again'' `````` Jean-Christophe Filliatre committed Jun 12, 2013 3 `````` http://www.brics.dk/RS/02/12/BRICS-RS-02-12.pdf‎ `````` Jean-Christophe Filliatre committed Jun 12, 2013 4 ``````*) `````` Jean-Christophe Filliatre committed Jun 12, 2013 5 `````` `````` Jean-Christophe Filliatre committed Jun 12, 2013 6 7 8 9 10 11 ``````(* Computing a symbolic convolution: Given two lists [x1 , x2 , ..., xn−1 , xn ] and [y1 , y2 , ..., yn−1 , yn ], where n is not known in advance, write a function that constructs [(x1 , yn ), (x2 , yn−1 ), ..., (xn−1 , y2 ), (xn , y1 )] in n recursive calls and with no auxiliary list. `````` Jean-Christophe Filliatre committed Jun 12, 2013 12 13 ``````*) `````` Jean-Christophe Filliatre committed Jun 12, 2013 14 ``````module Convolution `````` Jean-Christophe Filliatre committed Jun 12, 2013 15 `````` `````` Andrei Paskevich committed Jun 15, 2018 16 17 18 19 20 21 `````` use int.Int use list.List use list.Length use list.Append use list.Reverse use list.Combine `````` Jean-Christophe Filliatre committed Jun 12, 2013 22 `````` `````` Jean-Christophe Filliatre committed Jun 12, 2013 23 `````` let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a) `````` Jean-Christophe Filliatre committed Jun 12, 2013 24 25 `````` variant { x } requires { length x <= length y } `````` Andrei Paskevich committed Jun 11, 2017 26 `````` ensures { let r, ys = result in exists y0: list 'a. `````` Jean-Christophe Filliatre committed Jun 12, 2013 27 28 29 30 `````` y = y0 ++ ys && length y0 = length x && r = combine x (reverse y0) } = match x with | Nil -> `````` Andrei Paskevich committed Jun 11, 2017 31 `````` Nil, y `````` Jean-Christophe Filliatre committed Jun 12, 2013 32 `````` | Cons x0 xs -> `````` Jean-Christophe Filliatre committed Jun 12, 2013 33 `````` match convolution_rec xs y with `````` Andrei Paskevich committed Jun 11, 2017 34 `````` | r, Cons y0 ys -> Cons (x0, y0) r, ys `````` Jean-Christophe Filliatre committed Jun 12, 2013 35 36 37 `````` | _ -> absurd end end `````` Jean-Christophe Filliatre committed Jun 12, 2013 38 `````` let convolution (x y: list 'a) : list ('a, 'a) `````` Jean-Christophe Filliatre committed Jun 12, 2013 39 40 `````` requires { length x = length y } ensures { result = combine x (reverse y) } `````` Jean-Christophe Filliatre committed Jun 12, 2013 41 42 43 44 45 46 47 48 49 50 51 52 `````` = let r, _ = convolution_rec x y in r end (* Detecting a palindrome: Given a list of length n, where n is not known in advance, determine whether this list is a palindrome in ceil(n/2) recursive calls and with no auxiliary list. *) module Palindrome `````` Andrei Paskevich committed Jun 15, 2018 53 54 55 56 57 58 59 60 `````` use int.Int use option.Option use list.List use list.Length use list.Append use list.Nth use list.NthLength use list.NthLengthAppend `````` Jean-Christophe Filliatre committed Jun 12, 2013 61 62 63 64 65 66 `````` predicate pal (x: list 'a) (n: int) = forall i: int. 0 <= i < n -> nth i x = nth (n - 1 - i) x exception Exit `````` Guillaume Melquiond committed Mar 29, 2016 67 68 69 70 71 `````` type elt val predicate eq (x y: elt) ensures { result <-> x = y } let rec palindrome_rec (x y: list elt): list elt `````` Jean-Christophe Filliatre committed Jun 12, 2013 72 73 `````` requires { length x >= length y } variant { x } `````` Guillaume Melquiond committed Mar 29, 2016 74 `````` ensures { exists x0: list elt. length x0 = length y && x = x0 ++ result } `````` Jean-Christophe Filliatre committed Jun 12, 2013 75 76 77 78 79 80 81 82 83 84 85 86 `````` ensures { pal x (length y) } raises { Exit -> exists i: int. 0 <= i < length y && nth i x <> nth (length y - 1 - i) x } = match x, y with | _, Nil -> x | Cons _ xs, Cons _ Nil -> xs | Cons x0 xs, Cons _ (Cons _ ys) -> match palindrome_rec xs ys with | Cons x1 xs -> assert { nth (length y - 1) x = Some x1 }; `````` Guillaume Melquiond committed Mar 29, 2016 87 `````` if eq x0 x1 then xs else raise Exit `````` Jean-Christophe Filliatre committed Jun 12, 2013 88 89 90 91 92 `````` | Nil -> absurd end | _ -> absurd end `````` Guillaume Melquiond committed Mar 29, 2016 93 `````` let palindrome (x: list elt) : bool `````` Jean-Christophe Filliatre committed Jun 12, 2013 94 `````` ensures { result=True <-> pal x (length x) } `````` Andrei Paskevich committed Jun 11, 2017 95 96 `````` = match palindrome_rec x x with _ -> True | exception Exit -> False end `````` Jean-Christophe Filliatre committed Jun 12, 2013 97 98 `````` end``````