(* This is an enriched version of [CompletedNat], where we compute not just numbers, but also sequences of matching length. *) (* A property is either [Finite (n, xs)], where [n] is a natural number and [xs] is a sequence of length [n]; or [Infinity]. *) type 'a t = | Finite of int * 'a Seq.seq | Infinity let equal p1 p2 = match p1, p2 with | Finite (i1, _), Finite (i2, _) -> i1 = i2 | Infinity, Infinity -> true | _, _ -> false 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 let bottom = Infinity let epsilon = Finite (0, Seq.empty) let singleton x = Finite (1, Seq.singleton x) 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 | _ -> min p1 (p2()) 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 let add p1 p2 = match p1, p2 with | Finite (i1, xs1), Finite (i2, xs2) -> Finite (i1 + i2, Seq.append xs1 xs2) | _, _ -> Infinity let add_lazy p1 p2 = match p1 with | Infinity -> Infinity | _ -> add p1 (p2()) 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)) let print conv p = match p with | Finite (i, xs) -> string_of_int i ^ " " ^ String.concat " " (List.map conv (Seq.elements xs)) | Infinity -> "infinity" let to_int p = match p with | Finite (i, _) -> i | Infinity -> max_int let extract p = match p with | Finite (_, xs) -> Seq.elements xs | Infinity -> assert false