From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 2 Dec 2009 10:05:30 +0000 (+0000)
Subject: New ways for initialising the signature required for paramodultion
X-Git-Tag: make_still_working~3185
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5587716849ea45d539c26b6aaeeba00bf16f00be;p=helm.git

New ways for initialising the signature required for paramodultion
---

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 9a7285062..28c6f9e03 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -11,46 +11,69 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
+type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
 
+let eqsig = ref (fun _ -> assert false);;
+let set_sig f = eqsig:= 
+f;;
 
-  let eqP () = 
-    let r = 
-      !reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
-    in
-    NCic.Const r
-  ;;
 
-  let eq_ind () = 
-    let r = 
-      !reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq_ind.con")
-    in
-    NCic.Const r
-  ;;
+let default_sig = function
+  | Eq -> 
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.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(2)) in
+	NCic.Const ref
+  | Refl ->
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
+	NCic.Const ref
 
-  let eq_ind_r () = 
-    let r = 
-      !reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq_elim_r.con")
-    in
-    NCic.Const r
-  ;;
+let set_default_sig () =
+  prerr_endline "setting default sig";
+  eqsig := default_sig
 
-  let eq_refl () = 
-    let r = 
-      !reference_of_oxuri 
-       (UriManager.uri_of_string 
-         "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
-    in
-    NCic.Const r
+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 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 extract lift vl t =
     let rec pos i = function 
       | [] -> raise Not_found 
diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli
index 337752edc..0c65b5793 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.mli
+++ b/helm/software/components/ng_paramodulation/nCicProof.mli
@@ -12,5 +12,6 @@
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
 val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
+val set_default_sig: unit -> unit
 
 val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term