examples/relabel.mlw

   1
   2 (* Tree relabelling.
   3
   4    Given a tree t, with values at the leaves, build a new tree with the
   5    same structure and leaves labelled with distinct integers.
   6  *)
   7
   8 module Relabel
   9
  10   use list.List
  11   use list.Mem
  12   use list.Append
  13   use list.Distinct
  14
  15   type tree 'a =
  16     | Leaf 'a
  17     | Node (tree 'a) (tree 'a)
  18
  19   function labels (t : tree 'a) : list 'a = match t with
  20     | Leaf x -> Cons x Nil
  21     | Node l r -> labels l ++ labels r
  22   end
  23
  24   lemma labels_Leaf :
  25     forall x y : 'a. mem x (labels (Leaf y)) <-> x=y
  26
  27   lemma labels_Node :
  28     forall x : 'a, l r : tree 'a.
  29       mem x (labels (Node l r)) <-> (mem x (labels l) \/ mem x (labels r))
  30
  31   inductive same_shape (t1 : tree 'a) (t2 : tree 'b) =
  32     | same_shape_Leaf :
  33         forall x1 : 'a, x2 : 'b.
  34         same_shape (Leaf x1) (Leaf x2)
  35     | same_shape_Node :
  36         forall l1 r1 : tree 'a, l2 r2 : tree 'b.
  37         same_shape l1 l2 -> same_shape r1 r2 ->
  38         same_shape (Node l1 r1) (Node l2 r2)
  39
  40   use int.Int
  41   use ref.Ref
  42
  43   val r : ref int
  44
  45   let fresh () ensures { !r = old !r + 1 /\ result = !r } =
  46     r := !r + 1; !r
  47
  48   let rec relabel (t : tree 'a) : tree int
  49     variant { t }
  50     ensures { same_shape t result /\ distinct (labels result) /\
  51       old !r <= !r /\
  52       (forall x:int. mem x (labels result) -> old !r < x <= !r) }
  53   = match t with
  54     | Leaf _   -> Leaf (fresh ())
  55     | Node l r -> Node (relabel l) (relabel r)
  56     end
  57
  58 end