CompletedNatWitness.ml 2.26 KB
 POTTIER Francois committed Jul 02, 2015 1 ``````(* This is an enriched version of [CompletedNat], where we compute not just `````` POTTIER Francois committed Jul 03, 2015 2 `````` numbers, but also sequences of matching length. *) `````` POTTIER Francois committed Jul 02, 2015 3 4 `````` (* A property is either [Finite (n, xs)], where [n] is a natural number and `````` POTTIER Francois committed Jul 03, 2015 5 `````` [xs] is a sequence of length [n]; or [Infinity]. *) `````` POTTIER Francois committed Jul 02, 2015 6 7 `````` type 'a t = `````` POTTIER Francois committed Jul 03, 2015 8 ``````| Finite of int * 'a Seq.seq `````` POTTIER Francois committed Jul 02, 2015 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 `````` POTTIER Francois committed Jul 07, 2015 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 `````` POTTIER Francois committed Jul 02, 2015 31 32 33 ``````let bottom = Infinity `````` POTTIER Francois committed Jul 02, 2015 34 ``````let epsilon = `````` POTTIER Francois committed Jul 03, 2015 35 `````` Finite (0, Seq.empty) `````` POTTIER Francois committed Jul 02, 2015 36 37 `````` let singleton x = `````` POTTIER Francois committed Jul 03, 2015 38 `````` Finite (1, Seq.singleton x) `````` POTTIER Francois committed Jul 02, 2015 39 `````` `````` POTTIER Francois committed Jul 02, 2015 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 | _ -> `````` POTTIER Francois committed Jul 03, 2015 60 `````` min p1 (p2()) `````` POTTIER Francois committed Jul 02, 2015 61 `````` `````` POTTIER Francois committed Jul 03, 2015 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 `````` POTTIER Francois committed Jul 02, 2015 73 74 75 ``````let add p1 p2 = match p1, p2 with | Finite (i1, xs1), Finite (i2, xs2) -> `````` POTTIER Francois committed Jul 03, 2015 76 `````` Finite (i1 + i2, Seq.append xs1 xs2) `````` POTTIER Francois committed Jul 02, 2015 77 78 79 80 81 82 83 84 `````` | _, _ -> Infinity let add_lazy p1 p2 = match p1 with | Infinity -> Infinity | _ -> `````` POTTIER Francois committed Jul 03, 2015 85 `````` add p1 (p2()) `````` POTTIER Francois committed Jul 02, 2015 86 `````` `````` POTTIER Francois committed Jul 03, 2015 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)) `````` POTTIER Francois committed Jul 02, 2015 99 100 101 102 ``````let print conv p = match p with | Finite (i, xs) -> string_of_int i ^ " " ^ `````` POTTIER Francois committed Jul 03, 2015 103 `````` String.concat " " (List.map conv (Seq.elements xs)) `````` POTTIER Francois committed Jul 02, 2015 104 105 `````` | Infinity -> "infinity" `````` POTTIER Francois committed Jul 03, 2015 106 107 108 109 110 111 112 113 `````` let to_int p = match p with | Finite (i, _) -> i | Infinity -> max_int `````` POTTIER Francois committed Jul 07, 2015 114 115 116 117 118 119 ``````let extract p = match p with | Finite (_, xs) -> Seq.elements xs | Infinity -> assert false``````