CompletedNatWitness.ml 2.26 KB
Newer Older
1
(* This is an enriched version of [CompletedNat], where we compute not just
2
   numbers, but also sequences of matching length. *)
3 4

(* A property is either [Finite (n, xs)], where [n] is a natural number and
5
   [xs] is a sequence of length [n]; or [Infinity]. *)
6 7

type 'a t =
8
| Finite of int * 'a Seq.seq
9 10 11 12 13 14 15 16 17 18 19
| Infinity

let equal p1 p2 =
  match p1, p2 with
  | Finite (i1, _), Finite (i2, _) ->
      i1 = i2
  | Infinity, Infinity ->
      true
  | _, _ ->
      false

20 21 22 23 24 25 26 27 28 29 30
let compare p1 p2 =
  match p1, p2 with
  | Finite (i1, _), Finite (i2, _) ->
      if i1 < i2 then -1 else if i1 = i2 then 0 else 1
  | Infinity, Infinity ->
      0
  | Finite _, Infinity ->
      -1
  | Infinity, Finite _ ->
      1

31 32 33
let bottom =
  Infinity

POTTIER Francois's avatar
POTTIER Francois committed
34
let epsilon =
35
  Finite (0, Seq.empty)
POTTIER Francois's avatar
POTTIER Francois committed
36 37

let singleton x =
38
  Finite (1, Seq.singleton x)
POTTIER Francois's avatar
POTTIER Francois committed
39

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
let is_maximal p =
  match p with
  | Finite (0, _) ->
      true
  | _ ->
      false

let min p1 p2 =
  match p1, p2 with
  | Finite (i1, _), Finite (i2, _) ->
      if i1 <= i2 then p1 else p2
  | p, Infinity
  | Infinity, p ->
      p

let min_lazy p1 p2 =
  match p1 with
  | Finite (0, _) ->
      p1
  | _ ->
60
      min p1 (p2())
61

POTTIER Francois's avatar
POTTIER Francois committed
62 63 64 65 66 67 68 69 70 71 72
let min_cutoff p1 p2 =
  match p1 with
  | Finite (0, _) ->
      p1
  | Finite (i1, _) ->
      (* Pass [i1] as a cutoff value to [p2]. *)
      min p1 (p2 i1)
  | Infinity ->
      (* Pass [max_int] to indicate no cutoff. *)
      p2 max_int

73 74 75
let add p1 p2 =
  match p1, p2 with
  | Finite (i1, xs1), Finite (i2, xs2) ->
76
      Finite (i1 + i2, Seq.append xs1 xs2)
77 78 79 80 81 82 83 84
  | _, _ ->
      Infinity

let add_lazy p1 p2 =
  match p1 with
  | Infinity ->
      Infinity
  | _ ->
85
      add p1 (p2())
86

POTTIER Francois's avatar
POTTIER Francois committed
87 88 89 90 91 92 93 94 95 96 97 98
let add_cutoff cutoff p1 p2 =
  match p1 with
  | Infinity ->
      Infinity
  | Finite (i1, _) ->
      if cutoff <= i1 then
        (* Cut. No need to evaluate [p2]. *)
        Infinity
      else
        (* Evaluate [p2], with an adjusted cutoff value. *)
        add p1 (p2 (cutoff - i1))

99 100 101 102
let print conv p =
  match p with
  | Finite (i, xs) ->
      string_of_int i ^ " " ^
103
      String.concat " " (List.map conv (Seq.elements xs))
104 105
  | Infinity ->
      "infinity"
106 107 108 109 110 111 112 113

let to_int p =
  match p with
  | Finite (i, _) ->
      i
  | Infinity ->
      max_int

114 115 116 117 118 119
let extract p =
  match p with
  | Finite (_, xs) ->
      Seq.elements xs
  | Infinity ->
      assert false