From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jan 2010 08:08:44 +0000 (+0000)
Subject: new reloc_subst (to avoid cyclic substitutions).
X-Git-Tag: make_still_working~3145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa01419bafd483b5a043a93a2f812a98cf178e22;p=helm.git

new reloc_subst (to avoid cyclic substitutions).
Changed default sig.
---

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index 5cb84e1c9..2d63d34af 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -36,6 +36,17 @@
       varlist
   ;;
 
+  let rec reloc_subst subst = function
+    | (Terms.Leaf _) as t -> t
+    | Terms.Var i -> 
+        (try
+           List.assoc i subst
+         with
+             Not_found -> assert false)
+    | (Terms.Node l) ->
+	Terms.Node (List.map (fun t -> reloc_subst subst t) l)
+;;
+
   let rec apply_subst subst = function
     | (Terms.Leaf _) as t -> t
     | Terms.Var i -> 
diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli
index 1ed311433..29516c57f 100644
--- a/helm/software/components/ng_paramodulation/foSubst.mli
+++ b/helm/software/components/ng_paramodulation/foSubst.mli
@@ -22,6 +22,8 @@ module Subst (B : Terms.Blob) :
     val lookup : 
           int -> 'a Terms.substitution -> 'a Terms.foterm
     val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist
+    val reloc_subst : 
+          'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm
     val apply_subst : 
           'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm
     val concat: 
diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 1dfdbc57c..e42f1b5b9 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -80,21 +80,23 @@ module Utils (B : Orderings.Blob) = struct
   ;;
 
   let fresh_unit_clause maxvar (id, lit, varlist, proof) =
+    (* prerr_endline 
+      ("varlist = " ^ (String.concat "," (List.map string_of_int varlist)));*)
     let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst 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
+          let l = Subst.reloc_subst subst l in
+          let r = Subst.reloc_subst subst r in
+          let ty = Subst.reloc_subst subst ty in
           Terms.Equation (l,r,ty,o)
       | Terms.Predicate p ->
-          let p = Subst.apply_subst subst p in
+          let p = Subst.reloc_subst subst p in
           Terms.Predicate p
     in
     let proof =
       match proof with
-      | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
+      | Terms.Exact t -> Terms.Exact (Subst.reloc_subst subst t)
       | Terms.Step (rule,c1,c2,dir,pos,s) ->
           Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s)
     in
diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 7a67aa9ad..36c9dd75e 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -44,10 +44,10 @@ module Index(B : Orderings.Blob) = struct
       let path_string_of =
         let rec aux arity = function
           | Terms.Leaf a -> [Constant (a, arity)]
-          | Terms.Var i -> assert (arity = 0); [Variable]
+          | Terms.Var i -> (* assert (arity = 0); *) [Variable]
+	  (* FIXME : should this be allowed or not ? 
           | Terms.Node (Terms.Var _::_) ->
-	      (* FIXME : should this be allowed or not ? *)
-	      assert false
+	      assert false *)
           | Terms.Node ([] | [ _ ] ) -> assert false
           | Terms.Node (Terms.Node _::_) -> assert false	      
           | Terms.Node (hd::tl) ->
diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 4c3c13205..39bc9523a 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -15,7 +15,7 @@ let eqPref = ref (fun _ -> assert false);;
 let set_eqP t = eqPref := fun _ -> t;;
 
 let default_eqP() = 
-  let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+  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
 
@@ -60,7 +60,9 @@ with type t = NCic.term and type input = NCic.term = struct
     | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
     | NCic.Appl _, NCic.Meta _ -> ~-1
     | NCic.Meta _, NCic.Appl _ -> 1
-    | _ -> assert false
+    | _ -> Pervasives.compare x y
+	(* was assert false, but why? *)
+	
   ;;
   
   let compare x y = 
diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 3b9bfce04..c680e8417 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -77,7 +77,7 @@ let nparamod rdb metasenv subst context t table =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
   let (bag,maxvar), passives = 
-    HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
+    HExtlib.list_mapi_acc (fun x _ a -> prerr_endline "there"; P.mk_passive a x) (bag,maxvar) table
   in
   match 
     P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
@@ -101,7 +101,8 @@ type state = P.state
 let empty_state = P.empty_state
 
 let forward_infer_step s t ty =
-  let bag = P.bag_of_state s in 
+  let bag = P.bag_of_state s in
+  prerr_endline "here"; 
   let bag,clause = P.mk_passive bag (t,ty) in
     if Terms.is_eq_clause clause then
       P.forward_infer_step (P.replace_bag s bag) clause 0
diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index f13f35fbf..1c74ac9e5 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -19,7 +19,7 @@ let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      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 -> 
@@ -31,7 +31,7 @@ let default_sig = function
       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/peq.ind" in
+      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
 
@@ -68,7 +68,7 @@ let set_reference_of_oxuri reference_of_oxuri =
 (* let debug c r = prerr_endline r; c *)
 let debug c _ = c;;
 
-  let eqP() = debug (!eqsig Eq) "eqp"  ;;
+  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";;