From c88c60d45e1502d07ebb56275c12255e7cecc290 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Feb 2003 17:32:03 +0000 Subject: [PATCH] added TacticChaser module to emebed functions which search set of tactics which can be applied --- helm/ocaml/tactics/.depend | 3 + helm/ocaml/tactics/Makefile | 10 +-- helm/ocaml/tactics/tacticChaser.ml | 102 ++++++++++++++++++++++++++++ helm/ocaml/tactics/tacticChaser.mli | 33 +++++++++ 4 files changed, 143 insertions(+), 5 deletions(-) create mode 100644 helm/ocaml/tactics/tacticChaser.ml create mode 100644 helm/ocaml/tactics/tacticChaser.mli diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index e6dc05be5..8d0d98338 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -11,6 +11,7 @@ equalityTactics.cmi: proofEngineTypes.cmo discriminationTactics.cmi: proofEngineTypes.cmo ring.cmi: proofEngineTypes.cmo fourierR.cmi: proofEngineTypes.cmo +tacticChaser.cmi: proofEngineTypes.cmo proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi @@ -75,3 +76,5 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ tacticals.cmx fourierR.cmi +tacticChaser.cmo: tacticChaser.cmi +tacticChaser.cmx: tacticChaser.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index f82a7d48f..35cd53517 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -1,20 +1,20 @@ PACKAGE = tactics -REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification +REQUIRES = \ + helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification \ + helm-mquery_generator INTERFACE_FILES = \ proofEngineReduction.mli proofEngineHelpers.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli variousTactics.mli introductionTactics.mli \ eliminationTactics.mli negationTactics.mli equalityTactics.mli \ - discriminationTactics.mli ring.mli \ - fourierR.mli + discriminationTactics.mli ring.mli fourierR.mli tacticChaser.mli IMPLEMENTATION_FILES = \ proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \ fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \ primitiveTactics.ml variousTactics.ml introductionTactics.ml \ eliminationTactics.ml negationTactics.ml equalityTactics.ml \ - discriminationTactics.ml ring.ml \ - fourierR.ml + discriminationTactics.ml ring.ml fourierR.ml tacticChaser.ml include ../Makefile.common diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml new file mode 100644 index 000000000..054ad98bd --- /dev/null +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -0,0 +1,102 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/02/2003 *) +(* *) +(* *) +(******************************************************************************) + + (* search arguments on which Apply tactic doesn't fail *) +let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status = + let ((_, metasenv, _, _), metano) = status in + let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in + let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in + let must = choose_must list_of_must only in + let torigth_restriction (u,b) = + let p = + if b then + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else + "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u,p,None) + in + let rigth_must = List.map torigth_restriction must in + let rigth_only = Some (List.map torigth_restriction only) in + let result = + MQueryGenerator.searchPattern + (rigth_must,[],[]) (rigth_only,None,None) in + let uris = + List.map + (function uri,_ -> + MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + let uris',exc = + let rec filter_out = + function + [] -> [],"" + | uri::tl -> + let tl',exc = filter_out tl in + try + if + (try + ignore + (PrimitiveTactics.apply_tac + ~term:(MQueryMisc.term_of_cic_textual_parser_uri + (MQueryMisc.cic_textual_parser_uri_of_string uri)) + ~status); + true + with ProofEngineTypes.Fail _ -> false) + then + uri::tl',exc + else + tl',exc + with + e -> + let exc' = + "

^ Exception raised trying to apply " ^ + uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc + in + tl',exc' + in + filter_out uris + in + let html' = + "

Objects that can actually be applied:

" ^ + String.concat "
" uris' ^ exc ^ + "

Number of false matches: " ^ + string_of_int (List.length uris - List.length uris') ^ "

" ^ + "

Number of good matches: " ^ + string_of_int (List.length uris') ^ "

" + in + output_html html' ; + uris' +;; + diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli new file mode 100644 index 000000000..b5acbf7cb --- /dev/null +++ b/helm/ocaml/tactics/tacticChaser.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val searchPattern : + ?output_html:(string -> unit) -> + (* boolean value: true = in main position *) + choose_must:((MQueryGenerator.uri * bool) list list -> + (MQueryGenerator.uri * bool) list -> + (MQueryGenerator.uri * bool) list) -> + unit -> status: ProofEngineTypes.status -> string list + -- 2.39.2