CompletedNatWitness.ml 2.21 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14
type 'a t =
15
| Finite of int * 'a Seq.seq
16 17 18 19 20 21 22 23 24 25 26 27 28 29
| Infinity

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

let bottom =
  Infinity

POTTIER Francois's avatar
POTTIER Francois committed
30
let epsilon =
31
  Finite (0, Seq.empty)
POTTIER Francois's avatar
POTTIER Francois committed
32 33

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

36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
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
  | _ ->
56
      min p1 (p2())
57 58 59 60

let add p1 p2 =
  match p1, p2 with
  | Finite (i1, xs1), Finite (i2, xs2) ->
61
      Finite (i1 + i2, Seq.append xs1 xs2)
62 63 64 65 66 67 68 69
  | _, _ ->
      Infinity

let add_lazy p1 p2 =
  match p1 with
  | Infinity ->
      Infinity
  | _ ->
70
      add p1 (p2())
71 72 73 74

let print conv p =
  match p with
  | Finite (i, xs) ->
75
      Printf.sprintf "(* %d *) " i ^
76
      String.concat " " (List.map conv (Seq.elements xs))
77 78
  | Infinity ->
      "infinity"
79 80 81 82 83 84 85 86

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

87 88 89 90 91 92
let extract p =
  match p with
  | Finite (_, xs) ->
      Seq.elements xs
  | Infinity ->
      assert false