more controled API for Res

src/backend/Coq.ml

@@ -170,7 +170,7 @@ module Simple(S : Res.S)
     let lit = S.Atom.lit
 
     let get_assumption c =
-      match S.to_list c with
+      match S.Clause.atoms_l c with
       | [ x ] -> x
       | _ -> assert false
 
@@ -180,7 +180,7 @@ module Simple(S : Res.S)
       | _ -> assert false
 
     let prove_hyp fmt name c =
-      A.prove_hyp fmt name (List.map lit (S.to_list c))
+      A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c))
 
     let prove_lemma fmt name c =
       A.prove_lemma fmt name (get_lemma c)

src/backend/Dedukti.ml

@@ -40,7 +40,7 @@ module Make(S : Res.S)(A : Arg with type formula := S.formula
         fprintf fmt "%s _b %a ->@ %a"
           (if pos then "_pos" else "_neg") A.print f aux r
     in
-    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.to_list c)
+    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
 
   let context fmt p =
     fprintf fmt "(; Embedding ;)";

src/backend/Dot.ml

@@ -160,7 +160,7 @@ module Simple(S : Res.S)
     let lit = Atom.lit
 
     let get_assumption c =
-      match S.to_list c with
+      match S.Clause.atoms_l c with
       | [ x ] -> x
       | _ -> assert false
 
@@ -174,7 +174,7 @@ module Simple(S : Res.S)
       A.print_atom fmt (Atom.lit a)
 
     let hyp_info c =
-      A.hyp_info (List.map lit (S.to_list c))
+      A.hyp_info (List.map lit (S.Clause.atoms_l c))
 
     let lemma_info c =
       A.lemma_info (get_lemma c)

src/core/Res_intf.ml

@@ -31,6 +31,8 @@ module type S = sig
     step : step;          (** The reasoning step used to prove the conclusion *)
   }
   (** A proof can be expanded into a proof node, which show the first step of the proof. *)
+
+  (** The type of reasoning steps allowed in a proof. *)
   and step =
     | Hypothesis
     (** The conclusion is a user-provided hypothesis *)
@@ -44,21 +46,6 @@ module type S = sig
     | Resolution of proof * proof * atom
     (** The conclusion can be deduced by performing a resolution between the conclusions
         of the two given proofs. The atom on which to perform the resolution is also given. *)
-  (** The type of reasoning steps allowed in a proof. *)
-
-  (** {3 Resolution helpers} *)
-
-  val to_list : clause -> atom list
-  (** Returns the sorted list of atoms of a clause. *)
-
-  val merge : atom list -> atom list -> atom list
-  (** Merge two sorted atom list using a suitable comparison function. *)
-
-  val resolve : atom list -> atom list * atom list
-  (** Performs a "resolution step" on a sorted list of atoms.
-      [resolve (List.merge l1 l2)] where [l1] and [l2] are sorted atom lists should return the pair
-      [\[a\], l'], where [l'] is the result of the resolution of [l1] and [l2] over [a]. *)
-
 
   (** {3 Proof building functions} *)
 
@@ -71,7 +58,7 @@ module type S = sig
       @raise Insuficient_hyps if it does not succeed. *)
 
   val prove_atom : atom -> proof option
-  (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *)
+  (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
 
   (** {3 Proof Nodes} *)
 
@@ -95,6 +82,7 @@ module type S = sig
   (** Return the proof step at the root of a given proof. *)
 
   val conclusion : proof -> clause
+  (** What is proved at the root of the clause *)
 
   val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
   (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
@@ -116,6 +104,7 @@ module type S = sig
     type t = clause
     val name : t -> string
     val atoms : t -> atom array
+    val atoms_l : t -> atom list
     val pp : t printer
     (** A nice looking printer for clauses, which sort the atoms before printing. *)
 

src/core/Solver.ml

@@ -142,6 +142,7 @@ module Make
     include St.Clause
 
     let atoms c = St.Clause.atoms c |> Array.map (fun a -> a.St.lit)
+    let atoms_l c = St.Clause.atoms_l c |> List.map (fun a -> a.St.lit)
 
     let make st ?tag l =
       let l = List.map (S.mk_atom st) l in

src/core/Solver_intf.ml

@@ -142,6 +142,7 @@ module type S = sig
     type t = clause
 
     val atoms : t -> atom array
+    val atoms_l : t -> atom list
     val tag : t -> int option
     val equal : t -> t -> bool
 

src/core/Solver_types.ml

@@ -402,6 +402,7 @@ module McMake (E : Expr_intf.S) = struct
     let name = name_of_clause
     let[@inline] equal c1 c2 = c1==c2
     let[@inline] atoms c = c.atoms
+    let[@inline] atoms_l c = Array.to_list c.atoms
     let[@inline] tag c = c.tag
     let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms
 

src/core/Solver_types_intf.ml

@@ -245,6 +245,7 @@ module type S = sig
     val equal : t -> t -> bool
     val hash : t -> int
     val atoms : t -> Atom.t array
+    val atoms_l : t -> Atom.t list
     val tag : t -> int option
     val premise : t -> premise