examples/finger_trees.mlw

   1
   2 module FingerTrees
   3
   4   use int.Int
   5   use list.List
   6   use list.Length
   7   use list.Append
   8
   9   type digit 'a =
  10    | One 'a
  11    | Two 'a 'a
  12    | Three 'a 'a 'a
  13    | Four 'a 'a 'a 'a
  14
  15   function d_m (b:digit 'a) : list 'a = match b with
  16     | One x -> Cons x Nil
  17     | Two y x -> Cons y (Cons x Nil)
  18     | Three z y x -> Cons z (Cons y (Cons x Nil))
  19     | Four u z y x -> Cons u (Cons z (Cons y (Cons x Nil)))
  20     end
  21
  22   type node 'a =
  23     | Node2 'a 'a
  24     | Node3 'a 'a 'a
  25
  26   function node_cons (nd:node 'a) (l:list 'a) : list 'a = match nd with
  27     | Node2 x y -> Cons x (Cons y l)
  28     | Node3 x y z -> Cons x (Cons y (Cons z l))
  29     end
  30
  31   let lemma node_cons_app (nd:node 'a) (p q:list 'a)
  32     ensures { node_cons nd (p++q) = node_cons nd p ++ q }
  33   = match nd with Node2 _ _ -> [@keep_on_simp] () | _ -> () end
  34
  35   function flatten (l:list (node 'a)) : list 'a = match l with
  36     | Nil -> Nil
  37     | Cons nd q -> node_cons nd (flatten q)
  38     end
  39
  40   type t 'a =
  41     | Empty
  42     | Single (digit 'a)
  43     | Deep (digit 'a) (t (node 'a)) (digit 'a)
  44
  45   function t_m (t:t 'a) : list 'a = match t with
  46     | Empty -> Nil
  47     | Single x -> d_m x
  48     | Deep l m r -> d_m l ++ flatten (t_m m) ++ d_m r
  49     end
  50
  51   let d_cons (x:'a) (d:digit 'a) : (b: digit 'a, o: list (node 'a))
  52     ensures { Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 }
  53   = match d with
  54     | One y -> Two x y , Nil
  55     | Two y z -> Three x y z , Nil
  56     | Three y z t -> Four x y z t , Nil
  57     | Four y z t u -> Two x y , Cons (Node3 z t u) Nil
  58     end
  59
  60   let rec cons (x:'a) (t:t 'a) : t 'a
  61     ensures { t_m result = Cons x (t_m t) }
  62     variant { t }
  63   = match t with
  64     | Empty -> Single (One x)
  65     | Single d -> Deep (One x) Empty d
  66     | Deep lf md rg -> let lf2 , rem = d_cons x lf in
  67       match rem with
  68       | Nil -> Deep lf2 md rg
  69       | Cons x q -> assert { q = Nil };
  70         Deep lf2 (cons x md) rg
  71       end
  72     end
  73
  74 end
  75