From 53cc8b35a0d713483cd83e19ff29564e3ac1baaa Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 3 Jan 2018 22:07:40 +0100 Subject: [PATCH] more controled API for Res --- src/backend/Coq.ml | 4 ++-- src/backend/Dedukti.ml | 2 +- src/backend/Dot.ml | 4 ++-- src/core/Res_intf.ml | 21 +++++---------------- src/core/Solver.ml | 1 + src/core/Solver_intf.ml | 1 + src/core/Solver_types.ml | 1 + src/core/Solver_types_intf.ml | 1 + 8 files changed, 14 insertions(+), 21 deletions(-) diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index adde1c05..bba56ac7 100644 --- a/src/backend/Coq.ml +++ b/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) diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index 1a13cb08..76c9db7f 100644 --- a/src/backend/Dedukti.ml +++ b/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 ;)"; diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 067046e7..d25f1a09 100644 --- a/src/backend/Dot.ml +++ b/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) diff --git a/src/core/Res_intf.ml b/src/core/Res_intf.ml index cdebd00b..fd4afff6 100644 --- a/src/core/Res_intf.ml +++ b/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. *) diff --git a/src/core/Solver.ml b/src/core/Solver.ml index a8099c38..883636f0 100644 --- a/src/core/Solver.ml +++ b/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 diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 7c56168f..aebfe2b2 100644 --- a/src/core/Solver_intf.ml +++ b/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 diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index 8b399a31..5e2686ab 100644 --- a/src/core/Solver_types.ml +++ b/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 diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml index f073456c..f5076d30 100644 --- a/src/core/Solver_types_intf.ml +++ b/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