From 92835bcddaec9bcc3906101710f6c918b11a91fe Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 12 Apr 2017 20:48:08 +0200
Subject: [PATCH] Add useful function on proof steps

These new functions are designed to help people if (or when) the proof
API will break next time (i.e. adding a new variant case in step).
---
 src/core/res.ml      | 22 ++++++++++++++++++++++
 src/core/res_intf.ml | 16 ++++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/src/core/res.ml b/src/core/res.ml
index fdf391da..d0fa44e4 100644
--- a/src/core/res.ml
+++ b/src/core/res.ml
@@ -212,6 +212,28 @@ module Make(St : Solver_types.S) = struct
       assert (cmp_cl l (to_list conclusion) = 0);
       { conclusion; step = Resolution (c', d', a); }
 
+  (* Proof nodes manipulation *)
+  let is_leaf = function
+    | Hypothesis
+    | Assumption
+    | Lemma _ -> true
+    | Duplicate _
+    | Resolution _ -> false
+
+  let parents = function
+    | Hypothesis
+    | Assumption
+    | Lemma _ -> []
+    | Duplicate (p, _) -> [p]
+    | Resolution (p, p', _) -> [p; p']
+
+  let expl = function
+    | Hypothesis -> "hypothesis"
+    | Assumption -> "assumption"
+    | Lemma _ -> "lemma"
+    | Duplicate _ -> "duplicate"
+    | Resolution _ -> "resolution"
+
   (* Compute unsat-core
      TODO: replace visited bool by a int unique to each call
      of unsat_core, so that the cleanup can be removed ? *)
diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml
index 3260baec..6cc2297e 100644
--- a/src/core/res_intf.ml
+++ b/src/core/res_intf.ml
@@ -74,6 +74,22 @@ module type S = sig
   (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *)
 
 
+  (** {3 Proof Nodes} *)
+
+  val is_leaf : step -> bool
+  (** Returns wether the the proof node is a leaf, i.e. an hypothesis,
+      an assumption, or a lemma.
+      [true] if and only if {parents} returns the empty list. *)
+
+  val expl : step -> string
+  (** Returns a short string description for the proof step; for instance
+      ["hypothesis"] for a [Hypothesis] (generally, it currently is the
+      variant name in lowercase). *)
+
+  val parents : step -> proof list
+  (** Returns the parents of a proof node. *)
+
+
   (** {3 Proof Manipulation} *)
 
   val expand : proof -> proof_node