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 5cb84e1c938d1ff20b359bc738f7f0b713cfe87f..2d63d34afca2372e1c49f9dcea9c1f44959b17b7 100644 (file)
--- 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 1ed311433697d180aa65d1c1bda41fe8c234b7b8..29516c57f8fb9d6095802baf869141d41889a06f 100644 (file)
--- 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 1dfdbc57cca156506059754d598c391878d50079..e42f1b5b9745993ef7202dd631a3bc0784c29ebf 100644 (file)
--- 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 7a67aa9ad3cf8256c68d8455f0e83287ef78c1d8..36c9dd75e693ec51cf5e168995563113c2b92f66 100644 (file)
--- 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 4c3c1320558f39f424a0c510d21404608ae675cb..39bc9523a12791f82b85c121ec8dd3aea5f0db51 100644 (file)
--- 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 3b9bfce045a4ca2496f9fa1c6b74b030a5d36100..c680e8417346885453b2e70852d814065c6e0ed8 100644 (file)
--- 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 f13f35fbfb9c6552a621aada1db5aee60e40b1a9..1c74ac9e5b259d74fef23108a89aee864f88fb41 100644 (file)
--- 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";;