tree.mlw 983 Bytes
Newer Older
1
module Tree
2

3
  use list.List
4 5 6 7 8 9

  type forest 'a = list (tree 'a)
  with tree 'a   = Node 'a (forest 'a)

end

10
module Size
11

12 13 14
  use Tree
  use list.List
  use int.Int
15 16 17 18 19 20 21 22 23 24 25 26 27

  let rec function size_forest (f: forest 'a) : int
    ensures { result >= 0 }
  = match f with
    | Nil      -> 0
    | Cons t f -> size_tree t + size_forest f
    end
  with function size_tree (t: tree 'a) : int
    ensures { result > 0 }
  = match t with
    | Node _ f -> 1 + size_forest f
    end

Mario Pereira's avatar
Mario Pereira committed
28 29
end

30
module Forest
Mario Pereira's avatar
Mario Pereira committed
31

32
  use int.Int
Mario Pereira's avatar
Mario Pereira committed
33 34 35 36 37 38 39

  type forest 'a =
    | E
    | N 'a (forest 'a) (forest 'a)

end

40
module SizeForest
Mario Pereira's avatar
Mario Pereira committed
41

42 43
  use Forest
  use int.Int
Mario Pereira's avatar
Mario Pereira committed
44 45 46 47 48 49 50 51 52 53

  let rec function size_forest (f: forest 'a) : int
    ensures { result >= 0 }
  = match f with
    | E -> 0
    | N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
    end

end

54
module MemForest
Mario Pereira's avatar
Mario Pereira committed
55

56
  use Forest
Mario Pereira's avatar
Mario Pereira committed
57 58 59 60 61 62

  predicate mem_forest (n: 'a) (f: forest 'a) = match f with
    | E -> false
    | N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
    end

63
end