X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=1c74ac9e5b259d74fef23108a89aee864f88fb41;hb=94bd7b4d027e4152bd08cb984a66fae7077d9da6;hp=9223d1bcb12ae0b106bcd5260c5349e0473726f1;hpb=772def9075b7b62870ebf4cecec6bcd37a549b1d;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 9223d1bcb..1c74ac9e5 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -11,42 +11,69 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-  let eqP () = 
-    let r = 
-      OCic2NCic.reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
-    in
-    NCic.Const r
-  ;;
+type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
 
-  let eq_ind () = 
-    let r = 
-      OCic2NCic.reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq_ind.con")
-    in
-    NCic.Const r
-  ;;
+let eqsig = ref (fun _ -> assert false);;
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
 
-  let eq_ind_r () = 
-    let r = 
-      OCic2NCic.reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq_elim_r.con")
-    in
-    NCic.Const r
-  ;;
+let default_sig = function
+  | Eq -> 
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+      let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
+	NCic.Const ref
+  | EqInd_l -> 
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
+      let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
+	NCic.Const ref
+  | EqInd_r -> 
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
+      let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
+	NCic.Const ref
+  | Refl ->
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+      let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
+	NCic.Const ref
 
-  let eq_refl () = 
-    let r = 
-      OCic2NCic.reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
-    in
-    NCic.Const r
+let set_default_sig () =
+  prerr_endline "setting default sig";
+  eqsig := default_sig
+
+let set_reference_of_oxuri reference_of_oxuri = 
+  prerr_endline "setting oxuri in nCicProof";
+  let nsig = function
+    | Eq -> 
+	NCic.Const
+	  (reference_of_oxuri 
+	     (UriManager.uri_of_string 
+		"cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))  
+    | EqInd_l -> 
+	NCic.Const
+	  (reference_of_oxuri 
+	     (UriManager.uri_of_string 
+		"cic:/matita/logic/equality/eq_ind.con"))
+    | EqInd_r -> 
+	NCic.Const
+	  (reference_of_oxuri 
+	     (UriManager.uri_of_string 
+		"cic:/matita/logic/equality/eq_elim_r.con"))
+    | Refl ->
+	NCic.Const
+	  (reference_of_oxuri 
+	     (UriManager.uri_of_string 
+		"cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
+  in eqsig:= nsig
   ;;
 
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
+
+  let eqP() = debug (!eqsig Eq) "eq"  ;;
+  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 =
     let rec pos i = function 
       | [] -> raise Not_found 
@@ -95,7 +122,7 @@
       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
@@ -128,16 +155,26 @@
       in
 	lit, vl, proof
     in
+    let mk_refl = function
+      | NCic.Appl [_; ty; l; _]
+	  -> NCic.Appl [eq_refl();ty;l]
+      | _ -> assert false
+    in  
+    let proof_type =
+      let lit,_,_ = get_literal mp in
+      let lit = Subst.apply_subst subst lit in
+	extract 0 [] lit 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
@@ -206,6 +243,6 @@
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
     in 
-      aux false [] steps
+      aux false [] steps, proof_type
   ;;