X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=801e56b2623ed802a8f0eb71ce93c733d72f59a8;hb=076439def28e649ec384fae038ed021dadd5f75c;hp=50b31317a614f74336d11c933096961658f73080;hpb=b78de5584633b864248519d9f7cd9f86a0005c24;p=helm.git diff --git a/matita/components/ng_paramodulation/superposition.ml b/matita/components/ng_paramodulation/superposition.ml index 50b31317a..801e56b26 100644 --- a/matita/components/ng_paramodulation/superposition.ml +++ b/matita/components/ng_paramodulation/superposition.ml @@ -111,7 +111,7 @@ module Superposition (B : Orderings.Blob) = | Terms.Leaf _ as t -> let bag,subst,t,id = f bag t pos ctx id in assert (subst=[]); bag,t,id - | Terms.Var i as t -> + | Terms.Var _ as t -> let t= Subst.apply_subst subst t in bag,t,id | Terms.Node (hd::l) -> @@ -145,11 +145,13 @@ module Superposition (B : Orderings.Blob) = (* CSC: to avoid equations of the form ? -> T that can always be applied and that lead to type-checking errors *) (match l,r,o with - Terms.Var _,_,Terms.Gt - | _,Terms.Var _,Terms.Lt -> assert false - | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) -> +(* + (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt + | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false +*) + | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) -> Terms.Equation (l, r, ty, Terms.Lt) - | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> + | _, (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),(Terms.Incomparable | Terms.Invertible) -> Terms.Equation (l, r, ty, Terms.Gt) | _ -> Terms.Equation (l, r, ty, o)) | t -> Terms.Predicate t @@ -179,7 +181,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, (id,lit,vl,_)) -> + (fun (dir, (id,lit,_vl,_)) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> @@ -225,7 +227,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, ((id,lit,vl,_) as c)) -> + (fun (dir, ((id,lit,_vl,_) as c)) -> debug (lazy("candidate: " ^ Pp.pp_unit_clause c)); match lit with @@ -278,7 +280,7 @@ module Superposition (B : Orderings.Blob) = (bag,subst,newside,id) ;; - let rec demodulate bag (id, literal, vl, pr) table = + let demodulate bag (id, literal, vl, _pr) table = debug (lazy ("demodulate " ^ (string_of_int id))); match literal with | Terms.Predicate t -> (* assert false *) @@ -339,7 +341,7 @@ module Superposition (B : Orderings.Blob) = let is_identity_goal = function | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some [] - | _, Terms.Equation (l,r,_,_), vl, proof -> + | _, Terms.Equation (l,r,_,_), _vl, _proof -> (try Some (Unif.unification (* vl *) [] l r) with FoUnif.UnificationFailure _ -> None) | _, Terms.Predicate _, _, _ -> assert false @@ -387,7 +389,7 @@ module Superposition (B : Orderings.Blob) = let f b c = let id, dir, l, r, vl = match c with - | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl + | (d, (id,Terms.Equation (l,r,_ty,_),vl,_))-> id, d, l, r, vl |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -506,7 +508,7 @@ module Superposition (B : Orderings.Blob) = let rec orphan_murder bag acc i = match Terms.get_from_bag i bag with | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) + | (_,_,_,Terms.Step (_,_i1,_i2,_,_,_)),true,_ -> (true,acc) | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> if (List.mem i acc) then (false,acc) else match orphan_murder bag acc i1 with @@ -568,7 +570,7 @@ module Superposition (B : Orderings.Blob) = match simplify ctable maxvar bag c with |bag,None -> (bag,alist,atable) (* an active clause as been discarded *) - |bag,Some c1 -> + |bag,Some _c1 -> bag, c :: alist, IDX.index_unit_clause atable c) (bag,[],IDX.DT.empty) alist in @@ -669,7 +671,7 @@ module Superposition (B : Orderings.Blob) = else match (is_identity_goal clause) with | Some subst -> raise (Success (bag,maxvar,clause,subst)) | None -> - let (id,lit,vl,_) = clause in + let (_id,lit,vl,_) = clause in (* this optimization makes sense only if we demodulated, since in that case the clause should have been turned into an identity *) if (vl = [] && not(no_demod)) @@ -704,10 +706,10 @@ module Superposition (B : Orderings.Blob) = (* =================== inference ===================== *) (* this is OK for both the sup_left and sup_right inference steps *) - let superposition table varlist subterm pos context = + let superposition table _varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map - (fun (dir, (id,lit,vl,_ (*as uc*))) -> + (fun (dir, (id,lit,_vl,_ (*as uc*))) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) ->