From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Jun 2009 15:09:42 +0000 (+0000)
Subject: snapshot
X-Git-Tag: make_still_working~3894
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01b628fc79155f545b283c1d095d8a2ffe00e0a1;p=helm.git

snapshot
---

diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml
index bfef2f2b1..9053ec223 100644
--- a/helm/software/components/ng_paramodulation/foSubst.ml
+++ b/helm/software/components/ng_paramodulation/foSubst.ml
@@ -38,7 +38,10 @@ module Subst (B : Terms.Blob) = struct
 
   let rec apply_subst subst = function
     | (Terms.Leaf _) as t -> t
-    | Terms.Var i -> lookup_subst i subst
+    | Terms.Var i -> 
+        (match lookup_subst i subst with
+        | Terms.Node _ as t -> apply_subst subst t
+        | t -> t)
     | (Terms.Node l) ->
 	Terms.Node (List.map (fun t -> apply_subst subst t) l)
 ;;
diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index d53b19c82..624b6c99c 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -11,6 +11,15 @@
 
 (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
 
+let rec lexicograph f l1 l2 =
+  match l1, l2 with
+  | [], [] -> 0
+  | x::xs, y::ys ->
+     let c = f x y in
+     if c <> 0 then c else lexicograph f xs ys
+  | [],_ -> ~-1
+  | _,[] -> 1
+;;
 
 module Utils (B : Terms.Blob) = struct
   module Subst = FoSubst.Subst(B) ;;
@@ -25,15 +34,6 @@ module Utils (B : Terms.Blob) = struct
     | _ -> false
   ;;
 
-  let rec lexicograph f l1 l2 =
-    match l1, l2 with
-    | [], [] -> 0
-    | x::xs, y::ys ->
-       let c = f x y in
-       if c <> 0 then c else lexicograph f xs ys
-    | [],_ -> ~-1
-    | _,[] -> 1
-  ;;
 
   let rec compare_foterm x y =
     match x, y with
@@ -127,12 +127,10 @@ module Utils (B : Terms.Blob) = struct
     fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
   ;;
 
-  let add_to_bag =
-  let id = ref 0 in
-  fun bag  (_,lit,vl,proof) ->
-    incr id;
-    let clause = (!id, lit, vl, proof) in
-    let bag = Terms.M.add !id clause bag in
+  let add_to_bag bag  (_,lit,vl,proof) =
+    let id = mk_id () in
+    let clause = (id, lit, vl, proof) in
+    let bag = Terms.M.add id clause bag in
     bag, clause 
    ;;
     
diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli
index 4cddee8c1..d78ce32f2 100644
--- a/helm/software/components/ng_paramodulation/foUtils.mli
+++ b/helm/software/components/ng_paramodulation/foUtils.mli
@@ -11,6 +11,8 @@
 
 (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
 
+val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int
+
 module Utils (B : Terms.Blob) :
   sig
     val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool
diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 7cd4e5762..09399b326 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -27,10 +27,22 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
   let rec compare x y = 
     match x,y with
     | NCic.Rel i, NCic.Rel j -> i-j
+    | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
     | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
-    | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
+    | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+    | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+    | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+    | NCic.Appl _, NCic.Meta _ -> ~-1
+    | NCic.Meta _, NCic.Appl _ -> 1
     | _ -> assert false
   ;;
+  
+  let compare x y = 
+    if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 
+    else compare x y
+  ;;
 
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1bd9bcf4f..fb93ec7f8 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,4 +1,5 @@
 let nparamod metasenv subst context t table =
+  prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -45,9 +46,12 @@ let nparamod metasenv subst context t table =
   let table =  
     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
   in
+  prerr_endline "Active table:";
+  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
   let bag, maxvar, newclauses = 
     Sup.superposition_right_with_table bag maxvar clause table
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+  prerr_endline "========================================";
 ;;
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 64cc35bd4..fe4b578b6 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -18,6 +18,7 @@ module Superposition (B : Terms.Blob) =
     module Subst = FoSubst.Subst(B)
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
+    module Pp = Pp.Pp(B)
 
     let all_positions pos ctx t f =
       let rec aux pos ctx = function
@@ -41,7 +42,7 @@ module Superposition (B : Terms.Blob) =
     let superposition_right table varlist subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
       HExtlib.filter_map
-        (fun (dir, (id,lit,vl,_)) ->
+        (fun (dir, (id,lit,vl,_ (*as uc*))) ->
            match lit with
            | Terms.Predicate _ -> assert false
            | Terms.Equation (l,r,_,o) ->
@@ -59,7 +60,10 @@ module Superposition (B : Terms.Blob) =
                    if o <> Terms.Lt && o <> Terms.Eq then  
                      Some (context newside, subst, varlist, id, pos, dir)
                    else 
-                     None
+                     ((*prerr_endline ("Filtering: " ^ 
+                        Pp.pp_foterm side ^ " =(< || =)" ^ 
+                        Pp.pp_foterm newside ^ " coming from " ^ 
+                        Pp.pp_unit_clause uc );*)None)
                  else
                    Some (context newside, subst, varlist, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
@@ -84,7 +88,7 @@ module Superposition (B : Terms.Blob) =
         in
         Some (bag, maxvar, uc)
       else
-        None
+        ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
     ;;
 
     let fold_build_new_clause bag maxvar id filter res =
diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma
index 4e8747297..de4c42048 100644
--- a/helm/software/matita/tests/paratest.ma
+++ b/helm/software/matita/tests/paratest.ma
@@ -14,5 +14,9 @@
 
 include "nat/plus.ma".
 
-ntheorem foo: \forall x, y. ((λz. x + x = z + z) ?).
-##[ #x; #y; nnormalize; nauto.
\ No newline at end of file
+ntheorem foo:  
+   ((λx.x + 0 = x) ?) → 
+   ((λx,y.x + S y = S (x + y)) ? ?) →
+   ((λx,y.y + x = x + y) ? ?) →
+   ∀x. ((λz. x + x = z + S z) ?). 
+##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file