some work to make tries "printable", fixed comparison of constants in

paramodulation, added (but commented) a call to auto after every tactic
invocation to test it on the whole library.

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 546f4a34fce9f01b2fcca86ff0148af5ee6ee045..f5d61463024e3efe957406e6621cbb869de4816a 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/components/cic/discrimination_tree.ml
@@ -101,6 +101,10 @@ module DiscriminationTreeIndexing =
       type t = A.t DiscriminationTree.t * (path_string_elem*int) list
       let empty = DiscriminationTree.empty, [] ;;
 
+      let iter (dt, _ ) f =
+        DiscriminationTree.iter (fun _ x -> f x) dt
+      ;;
+
       let index (tree,arity) term info =
         let arity,ps = path_string_of_term arity term in
         let ps_set =

diff --git a/helm/software/components/cic/discrimination_tree.mli b/helm/software/components/cic/discrimination_tree.mli
index 63464e2ccf77b01b10bf11b3ff00debd098fd308..94c51ec576ee4b1184da5889d8d926683ad90866 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.mli
+++ b/helm/software/components/cic/discrimination_tree.mli
@@ -28,6 +28,7 @@ module DiscriminationTreeIndexing :
     sig
 
       type t 
+      val iter : t -> (A.t -> unit) -> unit
 
       val empty : t
       val index : t -> Cic.term -> A.elt -> t

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 679f4246f82fad9fcb905fa246fa0c361d0a71d8..fd1eb34849b8a066796d3e81396d1fe756caf3e5 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -794,9 +794,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
 ~disambiguate_macro opts status (text,prefix_len,ex) ->
   match ex with
-  | GrafiteAst.Tactic (_, Some tac, punct) ->
+  | GrafiteAst.Tactic (_(*loc*), Some tac, punct) ->
      let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
      let status = eval_tactical status (tactic_of_ast' tac) in
+     (* CALL auto on every goal, easy way of testing it 
+     let auto = GrafiteAst.AutoBatch (loc, ([],["depth","1";"timeout","1"])) in
+     (try
+       let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in
+       let _ = eval_tactical status (tactic_of_ast' auto) in ()
+     with _ -> ()); *)
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
   | GrafiteAst.Tactic (_, None, punct) ->

diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.ml b/helm/software/components/tactics/paramodulation/equality_indexing.ml
index 85ec40f8ab0ed4f5f23979b3bae832bbc34b95d4..01fecc0ed27f746100e019e962a1078fe835e9cb 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality_indexing.ml
+++ b/helm/software/components/tactics/paramodulation/equality_indexing.ml
@@ -36,6 +36,7 @@ module type EqualityIndex =
     val remove_index : t -> Equality.equality -> t
     val index : t -> Equality.equality -> t
     val in_index : t -> Equality.equality -> bool
+    val iter : t -> (PosEqSet.t -> unit) -> unit
   end
 
 module DT = 

diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.mli b/helm/software/components/tactics/paramodulation/equality_indexing.mli
index f9b51a5893e575fd9d4f3594297a8bb9efa584e7..9fd06f3ff96e1a3f89bec485470c995f0d9a4932 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality_indexing.mli
+++ b/helm/software/components/tactics/paramodulation/equality_indexing.mli
@@ -34,6 +34,7 @@ module type EqualityIndex =
     val remove_index : t -> Equality.equality -> t
     val index : t -> Equality.equality -> t
     val in_index : t -> Equality.equality -> bool
+    val iter : t -> (PosEqSet.t -> unit) -> unit
   end
 
 module DT : EqualityIndex

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 4e14964ff3dc26016818fecd566e83ced817214c..6942a6884a2dfbecdc71ec18a8e87f37c80786a6 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -587,6 +587,16 @@ exception Foo
 
 (** demodulation, when target is an equality *)
 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
+        (*
+          prerr_endline ("demodulation_eq:\n");
+        Index.iter table (fun l -> 
+          let l = Index.PosEqSet.elements l in
+          let l = 
+            List.map (fun (p,e) -> 
+              Utils.string_of_pos p ^ Equality.string_of_equality e) l in
+          prerr_endline (String.concat "\n" l)
+          );
+          *)
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index affd4897f5b7a351906554746b4debc93accb3c3..8a2722bb6820a1bf3d06652c8d9101be147dabad 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -506,12 +506,21 @@ let rec aux_ordering ?(recursion=true) t1 t2 =
   | C.Const _, _ -> Lt
   | _, C.Const _ -> Gt
 
-  | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2
+  | C.MutInd (u1, tno1, _), C.MutInd (u2, tno2, _) -> 
+       let res =  compare_uris u1 u2 in
+       if res <> Eq then res 
+       else 
+          let res = compare tno1 tno2 in
+          if res = 0 then Eq else if res < 0 then Lt else Gt
   | C.MutInd _, _ -> Lt
   | _, C.MutInd _ -> Gt
 
-  | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) ->
-      compare_uris u1 u2
+  | C.MutConstruct (u1, tno1, cno1, _), C.MutConstruct (u2, tno2, cno2, _) ->
+       let res =  compare_uris u1 u2 in
+       if res <> Eq then res 
+       else 
+          let res = compare (tno1,cno1) (tno2,cno2) in
+          if res = 0 then Eq else if res < 0 then Lt else Gt
   | C.MutConstruct _, _ -> Lt
   | _, C.MutConstruct _ -> Gt
 
@@ -552,7 +561,7 @@ let nonrec_kbo_w (t1, w1) (t2, w2) =
 let nonrec_kbo t1 t2 =
   let w1 = weight_of_term t1 in
   let w2 = weight_of_term t2 in
-  (* 
+  (*
   prerr_endline ("weight1 :"^(string_of_weight w1));
   prerr_endline ("weight2 :"^(string_of_weight w2)); 
   *)