From: Enrico Tassi Date: Mon, 26 Jun 2006 08:21:43 +0000 (+0000) Subject: more work for the generic auto parameters X-Git-Tag: 0.4.95@7852~1282 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=41e76668e9389ce17e41747026e533f907a0311c;p=helm.git more work for the generic auto parameters --- diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml index 871ff7b56..786ff7e75 100644 --- a/components/binaries/tptp2grafite/main.ml +++ b/components/binaries/tptp2grafite/main.ml @@ -201,7 +201,7 @@ let convert_ast statements context = function fv)) else [])@ [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Auto (floc,None,None,Some "paramodulation",None)), + GA.Auto (floc,["paramodulation",""])), Some (GA.Dot(floc))))]@ (if fv <> [] then (List.flatten diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 1ba1dd912..63dc8631d 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -328,10 +328,10 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = let paramodulation = bool "paramodulation" params in let full = bool "full" params in let superposition = bool "superposition" params in - let what = string "what" params in - let other = string "other" params in + let target = string "target" params in + let table = string "table" params in let subterms_only = bool "subterms_only" params in - let demodulate = bool "demodulate" params in + let demod_table = string "demod_table" params in (* the real tactic *) let auto_tac dbd (proof, goal) = let normal_auto () = @@ -378,7 +378,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = match superposition with | true -> ProofEngineTypes.mk_tactic - (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate) + (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table) | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) ;; diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index f81556c8f..bb1b3a853 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1888,8 +1888,19 @@ let rec position_of i x = function | _ -> i ;; -let superposition_tac ~what ~other ~subterms_only ~demodulate status = +(* Syntax: + * auto superposition target = NAME + * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] + * + * - if table is omitted no superposition will be performed + * - if demod_table is omitted no demodulation will be prformed + * - subterms_only is passed to Indexing.superposition_right + * + * lists are coded using _ (example: H_H1_H2) + *) +let superposition_tac ~target ~table ~subterms_only ~demod_table status = reset_refs(); + Indexing.init_index (); let proof,goalno = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goalno metasenv in @@ -1897,18 +1908,32 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status = let env = (metasenv, context, CicUniv.empty_ugraph) in let names = names_of_context context in let eq_index, equalities, maxm = find_equalities context proof in - let what = find_in_ctx 1 what context in - let other = find_in_ctx 1 other context in - let eq_what = List.nth equalities (position_of 0 what eq_index) in - let eq_other = List.nth equalities (position_of 0 other eq_index) in - let index = Indexing.index Indexing.empty eq_other in + let eq_what = + let what = find_in_ctx 1 target context in + List.nth equalities (position_of 0 what eq_index) + in + let eq_other = + if table <> "" then + let other = + let others = Str.split (Str.regexp "_") table in + List.map (fun other -> find_in_ctx 1 other context) others + in + List.map + (fun other -> List.nth equalities (position_of 0 other eq_index)) + other + else + [] + in + let index = List.fold_left Indexing.index Indexing.empty eq_other in let maxm, eql = + if table = "" then maxm,[eq_what] else Indexing.superposition_right ~subterms_only eq_uri maxm env index eq_what in prerr_endline ("Superposition right:"); prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); - prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env); + prerr_endline ("\n table: "); + List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other; prerr_endline ("\n result: "); List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; prerr_endline ("\n result (cut&paste): "); @@ -1917,9 +1942,18 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status = let t = Equality.term_of_equality eq_uri e in prerr_endline (CicPp.pp t names)) eql; - if demodulate then + if demod_table <> "" then begin - let table = List.fold_left Indexing.index Indexing.empty equalities in + let demod = + let demod = Str.split (Str.regexp "_") demod_table in + List.map (fun other -> find_in_ctx 1 other context) demod + in + let eq_demod = + List.map + (fun demod -> List.nth equalities (position_of 0 demod eq_index)) + demod + in + let table = List.fold_left Indexing.index Indexing.empty eq_demod in let maxm,eql = List.fold_left (fun (maxm,acc) e -> @@ -1946,5 +1980,6 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status = let get_stats () = <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ - Equality.get_stats ();; + Equality.get_stats () +;; diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 6a4688711..9f1ad293d 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -52,9 +52,8 @@ val demodulate_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val superposition_tac: - what:string -> other:string -> subterms_only:bool -> - demodulate:bool -> - ProofEngineTypes.proof * ProofEngineTypes.goal -> + target:string -> table:string -> subterms_only:bool -> + demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal -> ProofEngineTypes.proof * ProofEngineTypes.goal list val get_stats: unit -> string