From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 4 Sep 2003 11:04:15 +0000 (+0000)
Subject: added the support for the "Locate Inductive Principles" query
X-Git-Tag: v0_0_1~54
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

added the support for the "Locate Inductive Principles" query
---

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 <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 
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 <fguidi@cs.unibo.it>
+ *)
+
+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 <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) =
@@ -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
 ;;