diff --git a/src/backend/dot.ml b/src/backend/dot.ml index 8b452202..fd1b79d1 100644 --- a/src/backend/dot.ml +++ b/src/backend/dot.ml @@ -11,17 +11,46 @@ module type S = Backend_intf.S module type Arg = sig type atom + (* Type of atoms *) + + type hyp type lemma - (** Types *) + type assumption + (** Types for hypotheses, lemmas, and assumptions. *) val print_atom : Format.formatter -> atom -> unit + (** Printing function for atoms *) + + val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - (** Printing functions for atoms and lemmas. *) + val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list + (** Functions to return information about hypotheses and lemmas *) + +end + +module Default(S : Res.S) = struct + + let print_atom = S.St.print_atom + + let hyp_info c = + "hypothesis", Some "LIGHTBLUE", + [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] + + let lemma_info c = + "lemma", Some "BLUE", + [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] + + let assumption_info c = + "assumption", Some "PURPLE", + [ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] end (** Functor to provide dot printing *) -module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) = struct +module Make(S : Res.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) = struct let node_id n = n.S.conclusion.S.St.name @@ -75,16 +104,21 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm let print_contents fmt n = match S.(n.step) with + (* Leafs of the proof tree *) | S.Hypothesis -> - print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" - [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; + let rule, color, l = A.hyp_info S.(n.conclusion) in + let color = match color with None -> "LIGHTBLUE" | Some c -> c in + print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l | S.Assumption -> - print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Assumption" "LIGHTBLUE" - [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; + let rule, color, l = A.assumption_info S.(n.conclusion) in + let color = match color with None -> "LIGHTBLUE" | Some c -> c in + print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l | S.Lemma lemma -> - let rule, color, l = A.lemma_info lemma in + let rule, color, l = A.lemma_info S.(n.conclusion) in let color = match color with None -> "YELLOW" | Some c -> c in print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l + + (* Tree nodes *) | S.Duplicate (p, l) -> print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY" ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: @@ -107,9 +141,38 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm end -module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) = +module Simple(S : Res.S) + (A : Arg with type atom := S.St.formula + and type hyp = S.St.formula list + and type lemma := S.lemma + and type assumption = S.St.formula) = Make(S)(struct - let lemma_info = A.lemma_info - let print_atom fmt a = A.print_atom fmt a.S.St.lit + + (* Some helpers *) + let lit a = a.S.St.lit + + let get_assumption c = + match S.to_list c with + | [ x ] -> x + | _ -> assert false + + let get_lemma c = + match c.S.St.cpremise with + | S.St.Lemma p -> p + | _ -> assert false + + (* Actual functions *) + let print_atom fmt a = + A.print_atom fmt a.S.St.lit + + let hyp_info c = + A.hyp_info (List.map lit (S.to_list c)) + + let lemma_info c = + A.lemma_info (get_lemma c) + + let assumption_info c = + A.assumption_info (lit (get_assumption c)) + end) diff --git a/src/backend/dot.mli b/src/backend/dot.mli index c5ccfd6f..59412b47 100644 --- a/src/backend/dot.mli +++ b/src/backend/dot.mli @@ -23,7 +23,9 @@ module type Arg = sig type atom (** The type of atomic formuals *) + type hyp type lemma + type assumption (** The type of theory-specifi proofs (also called lemmas). *) val print_atom : Format.formatter -> atom -> unit @@ -31,11 +33,12 @@ module type Arg = sig WARNING: this function should take care to escape and/or not output special reserved characters for the dot format (such as quotes and so on). *) + val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - (** Generate some information about a theory specific lemmas. This backend does not - support printing of proper proofs in DOT format, so all proofs are printed as leafs - of the resolution tree. This function should return a triplet [(rule, color, l)], - such that: + val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list + (** Generate some information about the leafs of the proof tree. Currently this backend + print each lemma/assumption/hypothesis as a single leaf of the proof tree. + These function should return a triplet [(rule, color, l)], such that: - [rule] is a name for the proof (arbitrary, does not need to be unique, but should rather be descriptive) - [color] is a color name (optional) understood by DOT @@ -44,11 +47,24 @@ module type Arg = sig end -module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) : - S with type t := S.proof +module Default(S : Res.S) : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause +(** Provides a reasonnable default to instantiate the [Make] functor, assuming + the original printing functions are compatible with DOT html labels. *) + +module Make(S : Res.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. *) -module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) : - S with type t := S.proof -(** Functor for making a module to export proofs to the DOT format. *) +module Simple(S : Res.S)(A : Arg with type atom := S.St.formula + and type hyp = S.St.formula list + and type lemma := S.lemma + and type assumption = S.St.formula) : S with type t := S.proof +(** Functor for making a module to export proofs to the DOT format. + The substitution of the hyp type is non-destructive due to a restriction + of destructive substitutions on earlier versions of ocaml. *) diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml index 6cc2297e..a9d02b6c 100644 --- a/src/core/res_intf.ml +++ b/src/core/res_intf.ml @@ -18,8 +18,8 @@ module type S = sig (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) type atom = St.atom - type clause = St.clause type lemma = St.proof + type clause = St.clause (** Abstract types for atoms, clauses and theory-specific lemmas *) type proof diff --git a/src/main.ml b/src/main.ml index 2c7abeec..07381946 100644 --- a/src/main.ml +++ b/src/main.ml @@ -31,10 +31,7 @@ module Make val do_task : Dolmen.Statement.t -> unit end = struct - module D = Dot.Make(S.Proof)(struct - let print_atom = S.St.print_atom - let lemma_info _ = "<>", None, [] - end) + module D = Dot.Make(S.Proof)(Dot.Default(S.Proof)) let hyps = ref []