Commit ba303c67 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added [BooleanWitness], unused.

Added a comment in [Coverage] about the use of
  [CompletedNatWitness] versus [BooleanWitness].
parent d9c1a521
type 'a t =
| Reachable of 'a list Lazy.t
| Unreachable
let equal p1 p2 =
match p1, p2 with
| Reachable _, Reachable _
| Unreachable, Unreachable ->
true
| _, _ ->
false
let bottom =
Unreachable
let epsilon =
Reachable (lazy [])
let singleton x =
Reachable (lazy [x])
let is_maximal p =
match p with
| Reachable _ ->
true
| _ ->
false
let min p1 p2 =
match p1, p2 with
| Reachable _, _ ->
p1
| Unreachable, p ->
p
let min_lazy p1 p2 =
match p1 with
| Reachable _ ->
p1
| Unreachable ->
Lazy.force p2
let add p1 p2 =
match p1, p2 with
| Reachable xs1, Reachable xs2 ->
Reachable (
(* The only list operation in the code! *)
lazy (Lazy.force xs1 @ Lazy.force xs2)
)
| _, _ ->
Unreachable
let add_lazy p1 p2 =
match p1 with
| Unreachable ->
Unreachable
| Reachable _ ->
add p1 (Lazy.force p2)
let print conv p =
match p with
| Reachable xs ->
String.concat " " (List.map conv (Lazy.force xs))
| Unreachable ->
"unreachable"
(* This is an enriched version of [Boolean], where we compute not just a
Boolean property, [Unreachable] or [Reachable], but also (in the latter
case) a path (a list). During the fixed point computation, instead of
manipulating actual lists, we manipulate only recipes for constructing
lists. These recipes can be evaluated by the user after the fixed point has
been reached. *)
(* A property is either [Reachable xs], where [xs] is a (recipe for
constructing a) path; or [Unreachable]. *)
type 'a t =
| Reachable of 'a list Lazy.t
| Unreachable
val bottom: 'a t
val equal: 'a t -> 'b t -> bool
val is_maximal: 'a t -> bool
val epsilon: 'a t
val singleton: 'a -> 'a t
val min: 'a t -> 'a t -> 'a t
val add: 'a t -> 'a t -> 'a t
val min_lazy: 'a t -> 'a t Lazy.t -> 'a t
val add_lazy: 'a t -> 'a t Lazy.t -> 'a t
val print: ('a -> string) -> 'a t -> string
module P = CompletedNatWitness
open Grammar
(* Using [CompletedNatWitness] means that we wish to compute shortest paths.
An alternative would be to use [BooleanWitness], which offers the same
interface. That would mean we wish to compute an arbitrary path. That
would be faster, but the paths thus obtained are (according to a quick
experiment) really far from optimal. *)
module P =
CompletedNatWitness
(* TEMPORARY check no symbol produces the empty language *)
type property =
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment