stdlib/tree.mlw

   1
   2 (** {1 Polymorphic n-ary trees} *)
   3
   4 (** {2 Basic theory with polymorphic lists of children} *)
   5
   6 module Tree
   7
   8   use list.List
   9
  10   type forest 'a = list (tree 'a)
  11   with tree 'a   = Node 'a (forest 'a)
  12
  13 end
  14
  15 (** {2 Tree size} *)
  16
  17 module Size
  18
  19   use Tree
  20   use list.List
  21   use int.Int
  22
  23   let rec function size_forest (f: forest 'a) : int
  24     ensures { result >= 0 }
  25   = match f with
  26     | Nil      -> 0
  27     | Cons t f -> size_tree t + size_forest f
  28     end
  29   with function size_tree (t: tree 'a) : int
  30     ensures { result > 0 }
  31   = match t with
  32     | Node _ f -> 1 + size_forest f
  33     end
  34
  35 end
  36
  37 (** {2 Forests} *)
  38
  39 module Forest
  40
  41   use int.Int
  42
  43   type forest 'a =
  44     | E
  45     | N 'a (forest 'a) (forest 'a)
  46
  47 end
  48
  49 (** {2 Forest size} *)
  50
  51 module SizeForest
  52
  53   use Forest
  54   use int.Int
  55
  56   let rec function size_forest (f: forest 'a) : int
  57     ensures { result >= 0 }
  58   = match f with
  59     | E -> 0
  60     | N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
  61     end
  62
  63 end
  64
  65 (** {2 Membership in a forest} *)
  66
  67 module MemForest
  68
  69   use Forest
  70
  71   predicate mem_forest (n: 'a) (f: forest 'a) = match f with
  72     | E -> false
  73     | N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
  74     end
  75
  76 end