From f24441c88f3ba0c7870646fc2cfd1cbdf6517178 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Sep 2008 12:07:45 +0000 Subject: [PATCH] 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. --- .../components/cic/discrimination_tree.ml | 4 ++++ .../components/cic/discrimination_tree.mli | 1 + .../components/grafite_engine/grafiteEngine.ml | 8 +++++++- .../tactics/paramodulation/equality_indexing.ml | 1 + .../paramodulation/equality_indexing.mli | 1 + .../tactics/paramodulation/indexing.ml | 10 ++++++++++ .../components/tactics/paramodulation/utils.ml | 17 +++++++++++++---- 7 files changed, 37 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index 546f4a34f..f5d614630 100644 --- 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 63464e2cc..94c51ec57 100644 --- 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 679f4246f..fd1eb3484 100644 --- 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 85ec40f8a..01fecc0ed 100644 --- 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 f9b51a589..9fd06f3ff 100644 --- 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 4e14964ff..6942a6884 100644 --- 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 affd4897f..8a2722bb6 100644 --- 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)); *) -- 2.39.2