ted version of mQueryGenerator (was mquery part 2)

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
new file mode 100644 (file)
index 0000000..b1c84ce
--- /dev/null
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -0,0 +1,168 @@
+open MQueryUtil
+open MathQL
+open Cic
+
+(* raw HTML representation *)
+
+let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
+
+let nl () = "<br>"
+
+let par () = "<p>"
+
+(* CIC term inspecting functions *)
+
+let ie_out (r, b, v) =
+   let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
+   res (pos ^ str_uref r) ^ nl ()
+
+let rec il_out = function
+   | []           -> ""
+   | head :: tail -> ie_out head ^ il_out tail
+
+let ie_struri (u, b, v) = str_uref u
+
+let rec il_restrict level = function
+   | []                -> []
+   | (u, b, v) :: tail ->
+      if v <= level then (u, b, v) :: il_restrict level tail
+      else il_restrict level tail 
+
+let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) = 
+   UriManager.eq u1 u2 && f1 = f2 && b1 = b2 
+
+let rec ie_insert ie = function
+   | []           -> [ie]
+   | head :: tail -> 
+      head :: if ie_eq head ie then tail else ie_insert ie tail
+
+let inspect_uri main l uri tc v = 
+   let fi = match tc with
+      | t0 :: c0 :: _ -> [t0 + 1; c0]
+      | t0 :: _       -> [t0 + 1]
+      | []            -> []
+   in ie_insert ((uri, fi), main, v) l
+
+let rec inspect_term main l v = function
+   | Rel i                        -> l 
+   | Meta (i, _)                  -> l
+   | Sort s                       -> l 
+   | Implicit                     -> l 
+   | Var u                        -> inspect_uri main l u [] v
+   | Const (u, i)                 -> inspect_uri main l u [] v
+   | MutInd (u, i, t)             -> inspect_uri main l u [t] v
+   | MutConstruct (u, i, t, c)    -> inspect_uri main l u [t; c] v
+   | Cast (uu, _)                 -> 
+      (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
+      inspect_term main l v uu
+   | Prod (n, uu, tt)             ->
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt
+   | Lambda (n, uu, tt)           ->
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt 
+   | LetIn (n, uu, tt)            ->
+      let luu = inspect_term false l (v + 1) uu in
+      inspect_term false luu (v + 1) tt
+   | Appl m                       -> inspect_list main l true v m 
+   | MutCase (u, i, t, tt, uu, m) -> 
+      let lu = inspect_uri main l u [t] (v + 1) in
+      let ltt = inspect_term false lu (v + 1) tt in
+      let luu = inspect_term false ltt (v + 1) uu in
+      inspect_list main luu false (v + 1) m
+   | Fix (i, m)                   -> inspect_ind l (v + 1) m 
+   | CoFix (i, m)                 -> inspect_coind l (v + 1) m 
+and inspect_list main l head v = function
+   | []      -> l
+   | tt :: m -> 
+      let ltt = inspect_term main l (if head then v else v+1) tt in
+      inspect_list false ltt false v m
+and inspect_ind l v = function
+   | []                  -> l
+   | (n, i, tt, uu) :: m ->  
+      let ltt = inspect_term false l v tt in
+      let luu = inspect_term false ltt v uu in
+      inspect_ind luu v m
+and inspect_coind l v = function
+   | []               -> l
+   | (n, tt, uu) :: m ->
+      let ltt = inspect_term false l v tt in
+      let luu = inspect_term false ltt v uu in
+      inspect_coind luu v m
+
+let inspect t = inspect_term true [] 0 t  
+
+(* query building functions *)
+
+let save s = 
+   let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
+                          (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
+   output_string och s; flush och; s
+
+let build_select (r, b, v) n  =
+   let rvar = "ref" ^ string_of_int n in
+   let svar = "str" ^ string_of_int n in
+   let mqs = if b then MQMConclusion else MQConclusion in
+   MQSelect (rvar, 
+             MQUse (MQReference [str_uref r], svar),
+             MQIs (MQStringSVar svar, mqs)
+            )
+
+let rec build_inter n = function
+   | []       -> MQPattern [(None, [MQBSS], [MQFSS])]
+   | [ie]     -> build_select ie n
+   | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
+
+let restrict_universe query = 
+ function
+    [] -> query   (* no constraints ===> the universe is the library *)
+  | l ->
+     let universe = 
+       MQReference (List.map ie_struri l)
+     in
+      MQLetIn (
+       "universe", universe,
+        MQSelect (
+         "uri", query,
+          MQSubset (
+           MQSelect (
+            "uri2",
+            MQUsedBy (MQListRVar "uri", "pos"),
+            MQOr (
+             MQIs (MQStringSVar "pos", MQConclusion),
+             MQIs (MQStringSVar "pos", MQMConclusion)
+            )
+           ),
+           MQListLVar "universe"
+          )
+        )
+      )
+
+let build_result query =
+   let html = par () ^ out_query query ^ nl () in
+   let result = Mqint.execute query in
+   save (html ^ out_result result)
+
+let init = Mqint.init
+
+let close = Mqint.close
+
+let locate s = 
+   let query = 
+      MQList (MQSelect ("ref", 
+                        MQPattern [(None, [MQBSS], [MQFSS])],
+                        MQIs (MQFunc (MQName, "ref"),
+                              MQCons s
+                             )
+                       )
+             )
+   in
+   build_result query
+
+let backward t level =
+   let il = inspect t in
+   let query = build_inter 0 (il_restrict level il) in
+   let query' = restrict_universe query il in
+   let query'' = MQList query' in 
+   par () ^ il_out il ^ build_result query''
+

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
new file mode 100644 (file)
index 0000000..2d07f4e
--- /dev/null
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -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/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
+(*                                 30/04/2002                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+val init      : unit -> unit                   (* INIT database function *)
+
+val close     : unit -> unit                   (* CLOSE database function *)
+
+val locate    : string -> string               (* LOCATE query building function *)
+
+val backward  : Cic.term -> int -> string      (* BACKWARD query building function *)