Toccata

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

(* 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.
*)

module Convolution

  use int.Int
  use list.List
  use list.Length
  use list.Append
  use list.Reverse
  use list.Combine

  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.
               y = y0 ++ ys && length y0 = length x &&
               r = combine x (reverse y0) }
  = match x with
    | Nil ->
        Nil, y
    | Cons x0 xs ->
        match convolution_rec xs y with
        | r, Cons y0 ys -> Cons (x0, y0) r, ys
        | _ -> absurd end
    end

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

  use int.Int
  use option.Option
  use list.List
  use list.Length
  use list.Append
  use list.Nth
  use list.NthLength
  use list.NthLengthAppend

  predicate pal (x: list 'a) (n: int) =
    forall i: int. 0 <= i < n -> nth i x = nth (n - 1 - i) x

  exception Exit

  type elt
  val predicate eq (x y: elt)
    ensures { result <-> x = y }

  let rec palindrome_rec (x y: list elt): list elt
    requires { length x >= length y }
    variant { x }
    ensures { exists x0: list elt. length x0 = length y && x = x0 ++ result }
    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 };
            if eq x0 x1 then xs else raise Exit
        | Nil -> absurd
        end
    | _ -> absurd
    end

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

end