From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 18 Dec 2009 08:53:10 +0000 (+0000)
Subject: Final subst returned by superposition and passed around.
X-Git-Tag: make_still_working~3162
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;p=helm.git

Final subst returned by superposition and passed around.
---

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 7b57e5bb3..1dfdbc57c 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -28,7 +28,7 @@ module Utils (B : Orderings.Blob) = struct
   let rec eq_foterm x y =
     x == y ||
     match x, y with
-    | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+    | 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
diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 78a57faa2..fb60d3142 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -17,7 +17,7 @@ NCicProof.set_default_sig()
 ;;
 
 let debug _ = ();;
-(* let debug s = prerr_endline (Lazy.force s);; *)
+let print s = prerr_endline (Lazy.force s);; 
 
 module B(C : NCicBlob.NCicContext): Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
@@ -25,15 +25,15 @@ module B(C : NCicBlob.NCicContext): Orderings.Blob
 
 module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
 
-let readback rdb metasenv subst context (bag,i,l) =
+let readback rdb metasenv subst context (bag,i,fo_subst,l) =
 (*
   List.iter (fun x ->
      print_endline (Pp.pp_unit_clause ~margin:max_int
      (fst(Terms.M.find x bag)))) l; 
 *)
   let stamp = Unix.gettimeofday () in
-  let proofterm = NCicProof.mk_proof bag i l in
-    debug (lazy (Printf.sprintf "Got proof term in %fs"
+  let proofterm = NCicProof.mk_proof bag i fo_subst l in
+    print (lazy (Printf.sprintf "Got proof term in %fs"
 		     (Unix.gettimeofday() -. stamp)));
   let metasenv, proofterm = 
     let rec aux k metasenv = function
@@ -48,13 +48,15 @@ let readback rdb metasenv subst context (bag,i,l) =
     in
       aux 0 metasenv proofterm
   in
-  debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+  print (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+  let stamp = Unix.gettimeofday () in
   let metasenv, subst, proofterm, _prooftype = 
     NCicRefiner.typeof 
       (rdb#set_coerc_db NCicCoercion.empty_db) 
       metasenv subst context proofterm None
   in
-    debug (lazy "refined!");
+    print (lazy (Printf.sprintf "Refined in %fs"
+		     (Unix.gettimeofday() -. stamp)));
     proofterm, metasenv, subst
 
 let nparamod rdb metasenv subst context t table =
@@ -113,9 +115,12 @@ let index_obj s uri =
 ;;
 
 let fast_eq_check rdb metasenv subst context s goal =
+  let stamp = Unix.gettimeofday () in
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
   | P.Unsatisfiable solutions -> 
+      print (lazy (Printf.sprintf "Got solutions in %fs"
+		     (Unix.gettimeofday() -. stamp)));
       List.map (readback rdb metasenv subst context) solutions
 ;;
 
diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 59d7e95ff..65c0b1613 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -14,9 +14,8 @@
 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
 
 let eqsig = ref (fun _ -> assert false);;
-let set_sig f = eqsig:= 
-f;;
-
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
@@ -66,12 +65,13 @@ let set_reference_of_oxuri reference_of_oxuri =
   in eqsig:= nsig
   ;;
 
-let debug c r = prerr_endline r; c 
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
 
-  let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp"  ;;
-  let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;;
-  let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";; 
-  let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";;
+  let eqP() = debug (!eqsig Eq) "eqp"  ;;
+  let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
+  let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; 
+  let eq_refl() = debug (!eqsig Refl) "refl";;
 
 
   let extract lift vl t =
@@ -122,7 +122,7 @@ let debug c r = prerr_endline r; c
       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
     ;;
 
-  let mk_proof (bag : NCic.term Terms.bag) mp steps =
+  let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
     let module Subst = FoSubst in
     let position i l = 
       let rec aux = function
@@ -155,16 +155,22 @@ let debug c r = prerr_endline r; c
       in
 	lit, vl, proof
     in
+    let mk_refl = function
+      | NCic.Appl [_; ty; l; _]
+	  -> NCic.Appl [eq_refl();ty;l]
+      | _ -> assert false
+    in  
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
+	    let lit = Subst.apply_subst subst lit in
+            let eq_ty = extract amount [] lit in
+	    let refl = mk_refl eq_ty in
             ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
-             NCic.LetIn ("clause_" ^ string_of_int id, 
-                extract amount [] lit, 
-                (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
+             NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
                 aux true ((id,([],lit))::seen) (id::tl)))
           else
           match proof with
diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli
index 0c65b5793..4383b2928 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.mli
+++ b/helm/software/components/ng_paramodulation/nCicProof.mli
@@ -11,7 +11,15 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
+
 val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
 val set_default_sig: unit -> unit
+val get_sig: eq_sig_type -> NCic.term
 
-val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term
+val mk_proof:
+  NCic.term Terms.bag 
+  -> Terms.M.key 
+  -> NCic.term Terms.substitution
+  -> Terms.M.key list 
+  -> NCic.term
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b06d8a654..a3fd41e21 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline (Lazy.force s) ;; *) 
+(* let debug s = prerr_endline (Lazy.force s) ;; *)
 let debug _ = ();; 
 
 let monster = 100;;
@@ -21,7 +21,8 @@ module type Paramod =
     type t
     type input
     type szsontology = 
-      | Unsatisfiable of (t Terms.bag * int * int list) list
+      | Unsatisfiable of 
+	  (t Terms.bag * int * t Terms.substitution * int list) list
       | GaveUp 
       | Error of string 
       | Timeout of int * t Terms.bag
@@ -80,7 +81,8 @@ module Paramod (B : Orderings.Blob) = struct
   type input = B.input
   type bag = B.t Terms.bag * int 
   type szsontology = 
-    | Unsatisfiable of (B.t Terms.bag * int * int list) list
+    | Unsatisfiable of 
+	(B.t Terms.bag * int * B.t Terms.substitution * int list) list
     | GaveUp 
     | Error of string 
     | Timeout of int * B.t Terms.bag
@@ -460,7 +462,7 @@ module Paramod (B : Orderings.Blob) = struct
     in
       goal_narrowing iterno max_steps timeout newstatus
 
-    let compute_result bag i =
+    let compute_result bag i subst =
       let l =
         let rec traverse ongoal (accg,acce) i =
           match Terms.get_from_bag i bag with
@@ -503,7 +505,7 @@ module Paramod (B : Orderings.Blob) = struct
 		(fun x ->
 		   let cl,_,_ = Terms.get_from_bag x bag in
 		     Pp.pp_unit_clause cl) l))));
-        Unsatisfiable [ bag, i, l ]
+        Unsatisfiable [ bag, i, subst, l ]
 
   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let _initial_timestamp = Unix.gettimeofday () in
@@ -519,8 +521,8 @@ module Paramod (B : Orderings.Blob) = struct
      given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
-    | Sup.Success (bag, _, (i,_,_,_)) ->
-	compute_result bag i
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+	compute_result bag i subst
     | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;
@@ -532,8 +534,8 @@ let fast_eq_check s goal =
   try 
     goal_narrowing 0 2 None s
   with
-    | Sup.Success (bag, _, (i,_,_,_)) ->
-	compute_result bag i
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+	compute_result bag i subst
     | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;
diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index b161ae459..321d0f897 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -17,7 +17,8 @@ module type Paramod =
     type input
     type state
     type szsontology = 
-      | Unsatisfiable of (t Terms.bag * int * int list) list
+      | Unsatisfiable of 
+	  (t Terms.bag * int * t Terms.substitution * int list) list
       | GaveUp 
       | Error of string 
       | Timeout of int * t Terms.bag
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 585fbe237..6f1fb0f7f 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -20,7 +20,11 @@ module Superposition (B : Orderings.Blob) =
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
     
-    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
 
     (* let debug s = prerr_endline (Lazy.force s);; *)
     let debug _ = ();; 
@@ -311,15 +315,21 @@ module Superposition (B : Orderings.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause ~unify = function
+    let is_identity_clause = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
-          (try ignore(Unif.unification (* vl *) [] l r); true
-          with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false          
     ;;
 
+    let is_identity_goal = function
+      | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
+      | _, Terms.Equation (l,r,_,_), vl, proof ->
+          (try Some (Unif.unification (* vl *) [] l r)
+           with FoUnif.UnificationFailure _ -> None)
+      | _, Terms.Equation (_,_,_,_), _, _ -> None
+      | _, Terms.Predicate _, _, _ -> assert false          
+    ;;
+
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
       let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
       (Subst.apply_subst subst t)) subst in
@@ -475,10 +485,10 @@ module Superposition (B : Orderings.Blob) =
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause =
       debug (lazy "simplify...");
-      if is_identity_clause ~unify:false clause then bag,None
+      if is_identity_clause clause then bag,None
       (* else if orphan_murder bag actives clause then bag,None *)
       else let bag, clause = demodulate bag clause table in
-      if is_identity_clause ~unify:false clause then bag,None
+      if is_identity_clause clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
           | None -> bag, Some clause
@@ -608,9 +618,9 @@ module Superposition (B : Orderings.Blob) =
         if no_demod then bag, clause else demodulate bag clause table 
       in
       if List.exists (are_alpha_eq clause) g_actives then None
-      else if (is_identity_clause ~unify:true clause)
-      then raise (Success (bag, maxvar, clause))
-      else   
+      else match (is_identity_goal clause) with
+	| Some subst -> raise (Success (bag,maxvar,clause,subst))
+	| None ->
         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 *)
@@ -627,7 +637,7 @@ module Superposition (B : Orderings.Blob) =
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
              debug (lazy "Goal subsumed");
-             raise (Success (bag,maxvar,cl))
+             raise (Success (bag,maxvar,cl,subst))
 (*
         match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 9bd662b19..c67dbfb07 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,7 +15,11 @@ module Superposition (B : Orderings.Blob) :
   sig
 
                         (* bag, maxvar, meeting point *)
-    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
 
     (* The returned active set is the input one + the selected clause *)
     val infer_right :