From: Enrico Tassi Date: Mon, 8 Jun 2009 16:34:39 +0000 (+0000) Subject: some more functors and a nice higher-order all_positions iterator X-Git-Tag: make_still_working~3907 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b0a195b180e3526af7b55771b2df7b10acd7c30;p=helm.git some more functors and a nice higher-order all_positions iterator --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 8181c02de..c8985f260 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,9 +1,11 @@ terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi +foUtils.cmi: terms.cmi foUnif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi +superposition.cmi: terms.cmi index.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi paramod.cmi: @@ -13,15 +15,21 @@ pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi -foUnif.cmo: terms.cmi foUnif.cmi -foUnif.cmx: terms.cmx foUnif.cmi -index.cmo: terms.cmi index.cmi -index.cmx: terms.cmx index.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi foUtils.cmi index.cmi +index.cmx: terms.cmx foUtils.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi +superposition.cmo: terms.cmi index.cmi superposition.cmi +superposition.cmx: terms.cmx index.cmx superposition.cmi nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi -paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi -paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi +paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \ + foUnif.cmi paramod.cmi +paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \ + foUnif.cmx paramod.cmi diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 8181c02de..c8985f260 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -1,9 +1,11 @@ terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi +foUtils.cmi: terms.cmi foUnif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi +superposition.cmi: terms.cmi index.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi paramod.cmi: @@ -13,15 +15,21 @@ pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi -foUnif.cmo: terms.cmi foUnif.cmi -foUnif.cmx: terms.cmx foUnif.cmi -index.cmo: terms.cmi index.cmi -index.cmx: terms.cmx index.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi foUtils.cmi index.cmi +index.cmx: terms.cmx foUtils.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi +superposition.cmo: terms.cmi index.cmi superposition.cmi +superposition.cmx: terms.cmx index.cmx superposition.cmi nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi -paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi paramod.cmi -paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx paramod.cmi +paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \ + foUnif.cmi paramod.cmi +paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \ + foUnif.cmx paramod.cmi diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index a48753c4a..ceda25692 100644 --- a/helm/software/components/ng_paramodulation/Makefile +++ b/helm/software/components/ng_paramodulation/Makefile @@ -1,7 +1,8 @@ PACKAGE = ng_paramodulation INTERFACE_FILES = \ - terms.mli pp.mli foSubst.mli foUnif.mli index.mli orderings.mli \ + terms.mli pp.mli foSubst.mli foUtils.mli \ + foUnif.mli index.mli orderings.mli superposition.mli \ nCicBlob.mli cicBlob.mli paramod.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml index 195f53df7..c6cb31cfc 100644 --- a/helm/software/components/ng_paramodulation/cicBlob.ml +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -33,5 +33,8 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct let pp t = CicPp.pp t names;; let embed t = assert false;; + + let is_eq_predicate = assert false + let saturate = assert false end diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml index 1b9f2624c..92d6aba25 100644 --- a/helm/software/components/ng_paramodulation/foSubst.ml +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -35,5 +35,8 @@ module Subst (B : Terms.Blob) = struct not (is_in_subst m subst)) varlist ;; + + let apply_subst = assert false;; + let concat = assert false end diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli index dd7e0c2ec..74845d28a 100644 --- a/helm/software/components/ng_paramodulation/foSubst.mli +++ b/helm/software/components/ng_paramodulation/foSubst.mli @@ -20,4 +20,9 @@ module Subst (B : Terms.Blob) : val lookup_subst : int -> B.t Terms.substitution -> B.t Terms.foterm val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist + val apply_subst : + B.t Terms.substitution -> B.t Terms.foterm -> B.t Terms.foterm + val concat: + B.t Terms.substitution -> B.t Terms.substitution -> + B.t Terms.substitution end diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml index e4ea77c99..fae6e0840 100644 --- a/helm/software/components/ng_paramodulation/foUnif.ml +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -15,7 +15,7 @@ exception UnificationFailure of string Lazy.t;; module Founif (B : Terms.Blob) = struct module Subst = FoSubst.Subst(B) - module U = Terms.Utils(B) + module U = FoUtils.Utils(B) let unification vars locked_vars t1 t2 = let lookup = Subst.lookup_subst in diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml new file mode 100644 index 000000000..69e451e2e --- /dev/null +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -0,0 +1,130 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) + + +module Utils (B : Terms.Blob) = struct + module Subst = FoSubst.Subst(B) ;; + module Order = Orderings.Orderings(B) ;; + + let rec eq_foterm x y = + x == y || + match x, y with + | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2 + | Terms.Var i, Terms.Var j -> i = j + | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2 + | _ -> false + ;; + + let rec lexicograph f l1 l2 = + match l1, l2 with + | [], [] -> 0 + | x::xs, y::ys -> + let c = f x y in + if c <> 0 then c else lexicograph f xs ys + | [],_ -> ~-1 + | _,[] -> 1 + ;; + + let rec compare_foterm x y = + match x, y with + | Terms.Leaf t1, Terms.Leaf t2 -> B.compare t1 t2 + | Terms.Var i, Terms.Var j -> i - j + | Terms.Node l1, Terms.Node l2 -> lexicograph compare_foterm l1 l2 + | Terms.Leaf _, ( Terms.Node _ | Terms.Var _ ) -> ~-1 + | Terms.Node _, Terms.Leaf _ -> 1 + | Terms.Node _, Terms.Var _ -> ~-1 + | Terms.Var _, _ -> 1 + ;; + + let eq_literal l1 l2 = + match l1, l2 with + | Terms.Predicate p1, Terms.Predicate p2 -> eq_foterm p1 p2 + | Terms.Equation (l1,r1,ty1,o1), Terms.Equation (l2,r2,ty2,o2) -> + o1 = o2 && eq_foterm l1 l2 && eq_foterm r1 r2 && eq_foterm ty1 ty2 + | _ -> false + ;; + + let compare_literal l1 l2 = + match l1, l2 with + | Terms.Predicate p1, Terms.Predicate p2 -> compare_foterm p1 p2 + | Terms.Equation (l1,r1,ty1,o1), Terms.Equation (l2,r2,ty2,o2) -> + let c = Pervasives.compare o1 o2 in + if c <> 0 then c else + let c = compare_foterm l1 l2 in + if c <> 0 then c else + let c = compare_foterm r1 r2 in + if c <> 0 then c else + compare_foterm ty1 ty2 + | Terms.Predicate _, Terms.Equation _ -> ~-1 + | Terms.Equation _, Terms.Predicate _ -> 1 + ;; + + let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2 + let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2 + + let relocate maxvar varlist = + List.fold_right + (fun i (maxvar, varlist, s) -> + maxvar+1, maxvar::varlist, Subst.build_subst i (Terms.Var maxvar) s) + varlist (maxvar+1, [], Subst.id_subst) + ;; + + let fresh_unit_clause maxvar (id, lit, varlist, proof) = + let maxvar, varlist, subst = relocate maxvar varlist in + let lit = + match lit with + | Terms.Equation (l,r,ty,o) -> + let l = Subst.apply_subst subst l in + let r = Subst.apply_subst subst r in + let ty = Subst.apply_subst subst ty in + Terms.Equation (l,r,ty,o) + | Terms.Predicate p -> + let p = Subst.apply_subst subst p in + Terms.Predicate p + in + let proof = + match proof with + | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t) + | Terms.Step (rule,c1,c2,dir,pos,s) -> + Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s) + in + (id, lit, varlist, proof), maxvar + ;; + + (* may be moved inside the bag *) + let mk_id = + let id = ref 0 in + fun () -> incr id; !id + ;; + + let mk_unit_clause maxvar ty proofterm = + let varlist = + let rec aux acc = function + | Terms.Leaf _ -> acc + | Terms.Var i -> if List.mem i acc then acc else i::acc + | Terms.Node l -> List.fold_left aux acc l + in + aux (aux [] ty) proofterm + in + let lit = + match ty with + | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.is_eq_predicate eq -> + let o = Order.compare_terms l r in + Terms.Equation (l, r, ty, o) + | t -> Terms.Predicate t + in + let proof = Terms.Exact proofterm in + fresh_unit_clause maxvar (mk_id (), lit, varlist, proof) + ;; + +end diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli new file mode 100644 index 000000000..5d83a987d --- /dev/null +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -0,0 +1,32 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) + +module Utils (B : Terms.Blob) : + sig + val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool + val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int + + val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool + val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int + + (* mk_unit_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *) + val mk_unit_clause : + int -> B.t Terms.foterm -> B.t Terms.foterm -> + B.t Terms.unit_clause * int + + val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool + val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int + + val fresh_unit_clause : + int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int + end diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 9ec7fa4cb..ca30c9b50 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -12,7 +12,7 @@ (* $Id$ *) module Index(B : Terms.Blob) = struct - module U = Terms.Utils(B) + module U = FoUtils.Utils(B) module ClauseOT = struct diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index e01edfae3..a0fa80ada 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -46,6 +46,24 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l in (Terms.Node (List.rev res)), vars | t -> Terms.Leaf t, [] -;; + ;; + + let embed t = fst (embed t) ;; + + let saturate t ty = + let sty, _, args = + NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context + ty 0 + in + let proof = + if args = [] then Terms.Leaf t + else Terms.Node (Terms.Leaf t :: List.map embed args) + in + let sty = embed sty in + proof, sty + ;; + + let is_eq_predicate t = assert false;; + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 0414de7e3..b1fc1c704 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -7,17 +7,19 @@ let nparamod metasenv subst context t = in let module B = NCicBlob.NCicBlob(C) in let module Pp = Pp.Pp (B) in - let res,vars = B.embed t in + let res = B.embed t in let module FU = FoUnif.Founif(B) in - let test_unification vars = function + let module IDX = Index.Index(B) in + let module Sup = Superposition.Superposition(B) in + let test_unification _ = function | Terms.Node [_; _; lhs; rhs] -> prerr_endline "Unification test :"; prerr_endline (Pp.pp_foterm lhs); prerr_endline (Pp.pp_foterm rhs); - FU.unification vars [] lhs rhs + FU.unification [] [] lhs rhs | _ -> assert false in - let subst,vars = test_unification vars res in + let subst,vars = test_unification [] res in prerr_endline "Result :"; prerr_endline (Pp.pp_foterm res); prerr_endline "Substitution :"; diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index 9dac9001b..609ca47a7 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -59,7 +59,9 @@ let pp_substitution ~formatter:f subst = let pp_proof bag ~formatter:f p = let rec aux eq = function | Terms.Exact t -> - Format.fprintf f "%d: Exact (%s)@;" eq (B.pp t) + Format.fprintf f "%d: Exact (" eq; + pp_foterm f t; + Format.fprintf f ")@;"; | Terms.Step (rule,eq1,eq2,dir,pos,subst) -> Format.fprintf f "%d: %s(" eq (string_of_rule rule); diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml new file mode 100644 index 000000000..67185a88a --- /dev/null +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -0,0 +1,59 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) + +module Superposition (B : Terms.Blob) = + struct + module IDX = Index.Index(B) + + let all_positions t f = + let rec aux pos ctx = function + | Terms.Leaf a as t -> f t pos ctx + | Terms.Var i -> [] + | Terms.Node l as t-> + let acc, _, _ = + List.fold_left + (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *) + let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in + let acc = aux (List.length pre :: pos) newctx t @ acc in + if post = [] then acc, l, [] + else acc, pre @ [t], List.tl post) + (f t pos ctx, [], List.tl l) l + in + acc + in + aux [] (fun x -> x) t + ;; + + let superposition_right table subterm pos context = + let _cands = IDX.DT.retrieve_unifiables table subterm in + assert false;; +(* + for every cand in cands + let subst = FoUnif.unify l_can t + (apply_subst subst (c r_cand)), pos, id_cand, subst +*) + + let superposition_right_step bag (_,selected,_,_) table = + match selected with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,_,Terms.Lt) -> + let _r's = all_positions r (superposition_right table) in + assert false + | Terms.Equation (l,r,_,Terms.Gt) -> assert false + | _ -> assert false + ;; + + end + + + diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli new file mode 100644 index 000000000..c2c0ef43d --- /dev/null +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -0,0 +1,27 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) + + +module Superposition (B : Terms.Blob) : + sig + + val superposition_right_step : + B.t Terms.bag -> + B.t Terms.unit_clause -> + Index.Index(B).DT.t -> + B.t Terms.bag * B.t Terms.unit_clause list + + end + + + diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 38e1723c2..9b374a8a5 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -25,7 +25,7 @@ type direction = Left2Right | Right2Left | Nodir type position = int list type 'a proof = - | Exact of 'a + | Exact of 'a foterm | Step of rule * int * int * direction * position * 'a substitution (* rule, eq1, eq2, direction of eq2, position, substitution *) @@ -63,65 +63,9 @@ module type Blob = type t val eq : t -> t -> bool val compare : t -> t -> int + val is_eq_predicate : t -> bool val pp : t -> string - val embed : t -> t foterm * int list + val embed : t -> t foterm + val saturate : t -> t -> t foterm * t foterm end -module Utils (B : Blob) = struct - let rec eq_foterm x y = - x == y || - match x, y with - | Leaf t1, Leaf t2 -> B.eq t1 t2 - | Var i, Var j -> i = j - | Node l1, Node l2 -> List.for_all2 eq_foterm l1 l2 - | _ -> false - ;; - - let rec lexicograph f l1 l2 = - match l1, l2 with - | [], [] -> 0 - | x::xs, y::ys -> - let c = f x y in - if c <> 0 then c else lexicograph f xs ys - | [],_ -> ~-1 - | _,[] -> 1 - ;; - - let rec compare_foterm x y = - match x, y with - | Leaf t1, Leaf t2 -> B.compare t1 t2 - | Var i, Var j -> i - j - | Node l1, Node l2 -> lexicograph compare_foterm l1 l2 - | Leaf _, ( Node _ | Var _ ) -> ~-1 - | Node _, Leaf _ -> 1 - | Node _, Var _ -> ~-1 - | Var _, _ -> 1 - ;; - - let eq_literal l1 l2 = - match l1, l2 with - | Predicate p1, Predicate p2 -> eq_foterm p1 p2 - | Equation (l1,r1,ty1,o1), Equation (l2,r2,ty2,o2) -> - o1 = o2 && eq_foterm l1 l2 && eq_foterm r1 r2 && eq_foterm ty1 ty2 - | _ -> false - ;; - - let compare_literal l1 l2 = - match l1, l2 with - | Predicate p1, Predicate p2 -> compare_foterm p1 p2 - | Equation (l1,r1,ty1,o1), Equation (l2,r2,ty2,o2) -> - let c = Pervasives.compare o1 o2 in - if c <> 0 then c else - let c = compare_foterm l1 l2 in - if c <> 0 then c else - let c = compare_foterm r1 r2 in - if c <> 0 then c else - compare_foterm ty1 ty2 - | Predicate _, Equation _ -> ~-1 - | Equation _, Predicate _ -> 1 - ;; - - let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2 - let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2 - -end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 47c2c6e40..c16b6f9b7 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -25,7 +25,10 @@ type direction = Left2Right | Right2Left | Nodir type position = int list type 'a proof = - | Exact of 'a + | Exact of 'a foterm + (* for theorems like T : \forall x. C[x] = D[x] the proof is + * a foterm like (Node [ Leaf T ; Var i ]), while for the Goal + * it is just (Var g), i.e. the identity proof *) | Step of rule * int * int * direction * position * 'a substitution (* rule, eq1, eq2, direction of eq2, position, substitution *) @@ -59,22 +62,14 @@ module type Blob = type t val eq : t -> t -> bool val compare : t -> t -> int + val is_eq_predicate : t -> bool (* TODO: consider taking in input an imperative buffer for Format * val pp : Format.formatter -> t -> unit * *) val pp : t -> string - val embed : t -> t foterm * int list + val embed : t -> t foterm + (* saturate [proof] [type] -> [proof] * [type] *) + val saturate : t -> t -> t foterm * t foterm end -module Utils (B : Blob) : - sig - val eq_foterm : B.t foterm -> B.t foterm -> bool - val compare_foterm : B.t foterm -> B.t foterm -> int - - val eq_literal : B.t literal -> B.t literal -> bool - val compare_literal : B.t literal -> B.t literal -> int - - val eq_unit_clause : B.t unit_clause -> B.t unit_clause -> bool - val compare_unit_clause : B.t unit_clause -> B.t unit_clause -> int - end