From 506b4b7597021c98e34fb65cf9d0bb7879f06e92 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 4 Sep 2003 11:04:15 +0000 Subject: [PATCH] added the support for the "Locate Inductive Principles" query --- helm/gTopLevel/gTopLevel.ml | 2 +- helm/mathql_test/mqgtop.ml | 37 ++++++++++++++-- helm/ocaml/mathql_generator/.depend | 7 +++- helm/ocaml/mathql_generator/Makefile | 3 +- .../mathql_generator/cGLocateInductive.ml | 42 +++++++++++++++++++ .../mathql_generator/cGLocateInductive.mli | 33 +++++++++++++++ .../mathql_generator/cGMatchConclusion.ml | 4 ++ .../mathql_generator/cGMatchConclusion.mli | 2 + .../ocaml/mathql_generator/cGSearchPattern.ml | 3 ++ .../mathql_generator/cGSearchPattern.mli | 4 +- helm/ocaml/mathql_generator/mQGUtil.ml | 5 --- helm/ocaml/mathql_generator/mQGUtil.mli | 5 --- helm/ocaml/tactics/tacticChaser.ml | 2 +- helm/searchEngine/searchEngine.ml | 21 +++------- 14 files changed, 135 insertions(+), 35 deletions(-) create mode 100644 helm/ocaml/mathql_generator/cGLocateInductive.ml create mode 100644 helm/ocaml/mathql_generator/cGLocateInductive.mli diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ec19107dd..65f381859 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1916,7 +1916,7 @@ let completeSearchPattern () = let must = CGSearchPattern.get_constraints expr in let must',only = refine_constraints must in let query = - MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only + MQG.query_of_constraints (Some CGSearchPattern.universe) must' only in let results = MQI.execute mqi_handle query in show_query_results results diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index 2bf4e5f82..aba3bb3d4 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -46,6 +46,7 @@ module L = MQGTopLexer module P = MQGTopParser module TL = CicTextualLexer module TP = CicTextualParser +module C3 = CGLocateInductive module C2 = CGSearchPattern module C1 = CGMatchConclusion module GU = MQGUtil @@ -163,7 +164,7 @@ let unreferred target source = let mpattern n m l = let queries = ref [] in - let univ = Some GU.universe_for_search_pattern in + let univ = Some C2.universe in let handle = get_handle () in let rec pattern level = function | [] -> () @@ -198,7 +199,7 @@ let mpattern n m l = let mbackward n m l = let queries = ref [] in - let univ = Some GU.universe_for_match_conclusion in + let univ = Some C1.universe in let handle = get_handle () in let rec backward level = function | [] -> () @@ -229,6 +230,33 @@ let mbackward n m l = flush stderr; C.close handle +let inductive l = + let queries = ref [] in + let univ = Some C3.universe in + let handle = get_handle () in + let rec aux = function + | [] -> () + | term :: tail -> + aux tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t = U.start_time () in + let m = C3.get_constraints term in + let q = G.query_of_constraints univ m (None, None, None) in + if not (List.mem q ! queries) then + begin + issue handle q; + Printf.eprintf "[%i] " (pred ! query_num); flush stderr; + Printf.printf "%i GEN: %s" + (pred ! query_num) (U.stop_time t ^ nl); + flush stdout; queries := q :: ! queries + end + in + aux l; + Printf.eprintf "\nmqgtop: inductive: %i queries issued\n" + (List.length ! queries); + flush stderr; + C.close handle + let check () = let handle = get_handle () in Printf.eprintf @@ -252,6 +280,7 @@ let prerr_help () = prerr_endline "-i -interp FILE sets the CIC short names interpretation file"; prerr_endline "-d -disply outputs the CIC terms given in the input file"; prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns"; prerr_endline "-C -compose issues the \"Compose\" query reading its specifications"; prerr_endline " from the input file"; prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all"; @@ -262,7 +291,8 @@ let prerr_help () = prerr_endline " CIC terms in the input file"; prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0"; prerr_endline " on all CIC terms in the input file"; - prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns\n"; + prerr_endline "-I issues the \"Inductive\" query on all CIC terms in the"; + prerr_endline " input file\n"; prerr_endline "NOTES: * current interpreter options are:"; prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)"; prerr_endline " * CIC terms are read with the HELM CIC Textual Parser"; @@ -290,6 +320,7 @@ let rec parse = function | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem -> unreferred arg1 arg2; parse rem + | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem | _ :: rem -> parse rem let _ = diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index b3e8556fb..ef727f7b9 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -2,11 +2,14 @@ mQGUtil.cmi: mQGTypes.cmo mQueryGenerator.cmi: mQGTypes.cmo cGMatchConclusion.cmi: mQGTypes.cmo cGSearchPattern.cmi: mQGTypes.cmo +cGLocateInductive.cmi: mQGTypes.cmo mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi mQueryGenerator.cmo: mQGTypes.cmo mQGUtil.cmi mQueryGenerator.cmi mQueryGenerator.cmx: mQGTypes.cmx mQGUtil.cmx mQueryGenerator.cmi -cGMatchConclusion.cmo: cGMatchConclusion.cmi -cGMatchConclusion.cmx: cGMatchConclusion.cmi +cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi +cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi +cGLocateInductive.cmo: cGSearchPattern.cmi mQGTypes.cmo cGLocateInductive.cmi +cGLocateInductive.cmx: cGSearchPattern.cmx mQGTypes.cmx cGLocateInductive.cmi diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index 5b0135a3d..3079a6643 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -5,7 +5,8 @@ REQUIRES = helm-cic helm-cic_proof_checking helm-mathql PREDICATES = INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ - cGMatchConclusion.mli cGSearchPattern.mli + cGMatchConclusion.mli cGSearchPattern.mli \ + cGLocateInductive.mli IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml new file mode 100644 index 000000000..04a2f2ad4 --- /dev/null +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -0,0 +1,42 @@ +(* Copyright (C) 2000, 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/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +exception NotAnInductiveDefinition + +let get_constraints = function + | Cic.MutInd (uri, t, _) -> + let uri = MQueryUtil.string_of_uriref (uri, [t]) in + let constr_obj = + [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] + in + let constr_rel = [`MainConclusion None] in + let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in + (constr_obj, constr_rel, constr_sort) + | _ -> raise NotAnInductiveDefinition + +let universe = CGSearchPattern.universe diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.mli b/helm/ocaml/mathql_generator/cGLocateInductive.mli new file mode 100644 index 000000000..e4c6c1fa9 --- /dev/null +++ b/helm/ocaml/mathql_generator/cGLocateInductive.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2000, 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/. + *) + +(* AUTOR: Ferruccio Guidi + *) + +val get_constraints : Cic.term -> MQGTypes.must_restrictions + +val universe : MQGTypes.universe + +exception NotAnInductiveDefinition diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index 4f739763a..28639c8f7 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +module T = MQGTypes + let text_of_entries out entries = out "(** MatchConclusion: results of the term inspection **)\n"; let text_of_entry (u, b, v) = @@ -151,3 +153,5 @@ let get_constraints e c t = mk_musts (prev @ [acc]) acc next in mk_musts [] [] can + +let universe = [T.MainConclusion; T.InConclusion] diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.mli b/helm/ocaml/mathql_generator/cGMatchConclusion.mli index a8340312f..a9fbef47f 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.mli +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.mli @@ -29,3 +29,5 @@ val get_constraints: Cic.metasenv -> Cic.context -> Cic.term -> MQGTypes.r_obj list list * MQGTypes.r_obj list + +val universe : MQGTypes.universe diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 60633f897..77f3b488c 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -187,3 +187,6 @@ let get_constraints term = ) sorts ; res ;; + +let universe = + [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion] diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.mli b/helm/ocaml/mathql_generator/cGSearchPattern.mli index 83f681414..528283387 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.mli +++ b/helm/ocaml/mathql_generator/cGSearchPattern.mli @@ -34,4 +34,6 @@ (* *) (******************************************************************************) -val get_constraints: Cic.term -> MQGTypes.must_restrictions +val get_constraints : Cic.term -> MQGTypes.must_restrictions + +val universe : MQGTypes.universe diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml index a7a6bc6a4..36dd0653c 100644 --- a/helm/ocaml/mathql_generator/mQGUtil.ml +++ b/helm/ocaml/mathql_generator/mQGUtil.ml @@ -142,8 +142,3 @@ let set_full_position pos depth = match pos with let set_main_position pos depth = match pos with | `MainHypothesis _ -> `MainHypothesis depth | `MainConclusion _ -> `MainConclusion depth - -let universe_for_search_pattern = - [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion] - -let universe_for_match_conclusion = [T.MainConclusion; T.InConclusion] diff --git a/helm/ocaml/mathql_generator/mQGUtil.mli b/helm/ocaml/mathql_generator/mQGUtil.mli index bb623cc86..065abb157 100644 --- a/helm/ocaml/mathql_generator/mQGUtil.mli +++ b/helm/ocaml/mathql_generator/mQGUtil.mli @@ -67,8 +67,3 @@ val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth -> MQGTypes.full_position val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth -> MQGTypes.main_position - -(* these functions give some universes for "query_of_constraints" ---------*) - -val universe_for_search_pattern : MQGTypes.universe -val universe_for_match_conclusion : MQGTypes.universe diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index f248735df..06333d231 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -46,7 +46,7 @@ let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~s let result = I.execute mqi_handle (G.query_of_constraints - (Some U.universe_for_match_conclusion) + (Some CGMatchConclusion.universe) (must,[],[]) (Some only,None,None)) in let uris = List.map diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index e4e33c629..622f10bd5 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -155,8 +155,6 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, Pcre.regexp "@VARIABLES_INITIALIZATION@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" -exception NotAnInductiveDefinition - let port = try int_of_string (Sys.getenv port_env_var) @@ -180,29 +178,20 @@ let contype = "Content-Type", "text/html";; let get_constraints term = function | "/locateInductivePrinciple" -> - let uri = - match term with - Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t]) - | _ -> raise NotAnInductiveDefinition - in - let constr_obj = - [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] - in - let constr_rel = [`MainConclusion None] in - let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in - U.universe_for_search_pattern, - (constr_obj, constr_rel, constr_sort), (None,None,None) + CGLocateInductive.universe, + (CGLocateInductive.get_constraints term), + (None,None,None) | "/searchPattern" -> let constr_obj, constr_rel, constr_sort = CGSearchPattern.get_constraints term in - U.universe_for_search_pattern, + CGSearchPattern.universe, (constr_obj, constr_rel, constr_sort), (Some constr_obj, Some constr_rel, Some constr_sort) | "/matchConclusion" -> let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in (* FG: there is no way to choose the block number ***************************) let block = pred (List.length list_of_must) in - U.universe_for_match_conclusion, + CGMatchConclusion.universe, (List.nth list_of_must block, [], []), (Some only, None, None) | _ -> assert false ;; -- 2.39.2