random_access_list.mlw 2.18 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

(** Random Access Lists.

    The code below uses polymorphic recursion (both in the logic
    and in the programs).

    BUGS:
    - induction_ty_lex has no effect on a goal involving polymorphic recursion
    - a lemma function is not allowed to perform polymorphic recursion?

 *)

module RandomAccessList

  use import int.Int
  use import int.ComputerDivision
  use import list.List
  use import list.Length
  use import list.Nth
  use import option.Option

  type ral 'a =
  | Empty
  | Zero    (ral ('a, 'a))
  | One  'a (ral ('a, 'a))

  function flatten (l: list ('a , 'a)) : list 'a
  = match l with
    | Nil -> Nil
    | Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
    end

  lemma length_flatten:
    forall l: list ('a, 'a). length (flatten l) = 2 * length l

  function elements (l: ral 'a) : list 'a
    = match l with
      | Empty    -> Nil
      | Zero l1  -> flatten (elements l1)
      | One x l1 -> Cons x (flatten (elements l1))
      end

  let rec size (l: ral 'a) : int
    variant { l }
    ensures { result = length (elements l) }
  =
    match l with
    | Empty    -> 0
    | Zero  l1 ->     2 * size l1
    | One _ l1 -> 1 + 2 * size l1
    end

  let rec add (x: 'a) (l: ral 'a) : ral 'a
    variant { l }
    ensures { elements result = Cons x (elements l) }
    = match l with
      | Empty    -> One x Empty
      | Zero l1  -> One x l1
      | One y l1 -> Zero (add (x, y) l1)
      end

  let rec lemma nth_flatten (i: int) (l: list ('a, 'a))
    requires { 0 <= i < length l }
    variant  { l }
    ensures  { match nth i l with
               | None -> false
               | Some (x0, x1) -> Some x0 = nth (2 * i)     (flatten l) /\
                                  Some x1 = nth (2 * i + 1) (flatten l) end }
  = match l with
    | Nil -> ()
    | Cons _ r -> if i > 0 then nth_flatten (i-1) r
    end

  let rec get (i: int) (l: ral 'a) : 'a
    requires { 0 <= i < length (elements l) }
    variant  { i, l }
    ensures  { nth i (elements l) = Some result }
    = match l with
      | Empty    -> absurd
      | One x l1 -> if i = 0 then x else get (i-1) (Zero l1)
      | Zero l1  -> let (x0, x1) = get (div i 2) l1 in
                    if mod i 2 = 0 then x0 else x1
      end

end