there_and_back_again.mlw 2.59 KB
Newer Older
1

2
(* Two puzzles from Danvy and Goldberg's ``There and back again''
3
   http://www.brics.dk/RS/02/12/BRICS-RS-02-12.pdf‎
4
*)
5

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.
12 13
*)

14
module Convolution
15

16 17 18 19 20 21
  use int.Int
  use list.List
  use list.Length
  use list.Append
  use list.Reverse
  use list.Combine
22

23
  let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a)
24 25
    variant  { x }
    requires { length x <= length y }
26
    ensures  { let r, ys = result in exists y0: list 'a.
27 28 29 30
               y = y0 ++ ys && length y0 = length x &&
               r = combine x (reverse y0) }
  = match x with
    | Nil ->
31
        Nil, y
32
    | Cons x0 xs ->
33
        match convolution_rec xs y with
34
        | r, Cons y0 ys -> Cons (x0, y0) r, ys
35 36 37
        | _ -> absurd end
    end

38
  let convolution (x y: list 'a) : list ('a, 'a)
39 40
    requires { length x = length y }
    ensures  { result = combine x (reverse y) }
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

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
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

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
72 73
    requires { length x >= length y }
    variant { x }
74
    ensures { exists x0: list elt. length x0 = length y && x = x0 ++ result }
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 };
87
            if eq x0 x1 then xs else raise Exit
88 89 90 91 92
        | Nil -> absurd
        end
    | _ -> absurd
    end

93
  let palindrome (x: list elt) : bool
94
    ensures { result=True <-> pal x (length x) }
95 96
  = match palindrome_rec x x with _ -> True
    | exception Exit -> False end
97 98

end