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
module P = MQGTopParser
module TL = CicTextualLexer
module TP = CicTextualParser
+module C3 = CGLocateInductive
module C2 = CGSearchPattern
module C1 = CGMatchConclusion
module GU = MQGUtil
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
| [] -> ()
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
| [] -> ()
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
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";
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";
| ("-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 _ =
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
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)
--- /dev/null
+(* 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 <fguidi@cs.unibo.it>
+ *)
+
+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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it>
+ *)
+
+val get_constraints : Cic.term -> MQGTypes.must_restrictions
+
+val universe : MQGTypes.universe
+
+exception NotAnInductiveDefinition
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+module T = MQGTypes
+
let text_of_entries out entries =
out "(** MatchConclusion: results of the term inspection **)\n";
let text_of_entry (u, b, v) =
mk_musts (prev @ [acc]) acc next
in
mk_musts [] [] can
+
+let universe = [T.MainConclusion; T.InConclusion]
val get_constraints: Cic.metasenv -> Cic.context -> Cic.term ->
MQGTypes.r_obj list list *
MQGTypes.r_obj list
+
+val universe : MQGTypes.universe
) sorts ;
res
;;
+
+let universe =
+ [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]
(* *)
(******************************************************************************)
-val get_constraints: Cic.term -> MQGTypes.must_restrictions
+val get_constraints : Cic.term -> MQGTypes.must_restrictions
+
+val universe : MQGTypes.universe
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]
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
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
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)
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
;;
projects / helm.git / commitdiff