From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 May 2002 15:07:52 +0000 (+0000)
Subject: New module helm-mathql.
X-Git-Tag: V_0_3_0_debian_8~65
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e755543523fd1dc050e062b277996b0c9f4752e;p=helm.git

New module helm-mathql.
---

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index cd800f906..44c9887f7 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -1,6 +1,7 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
-           helm-xml gdome2-xslt helm-cic_unification helm-mathql_interpreter
+           helm-xml gdome2-xslt helm-cic_unification helm-mathql \
+           helm-mathql_interpreter
 PREDICATES =
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 73118c962..0cf33c83c 100644
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -1,26 +1,41 @@
-open Mathql
+open MathQL
 open Cic
 
 (* string linearization of a reference *)
 
 let str_uptoken = function
-   | MQString s -> s
-   | MQSlash    -> "/"
-   | MQAnyChr   -> "?"
-   | MQAst      -> "*"
-   | MQAstAst   -> "**"
+   | MQBC s -> s
+   | MQBD -> "/"
+   | MQBQ -> "?"
+   | MQBS -> "*"
+   | MQBSS -> "**"
 
 let rec str_up = function
    | [] -> ""
    | head :: tail -> str_uptoken head ^ str_up tail 
 
-let str_fi = function 
-   | (None, _)        -> ""
-   | (Some t, None)   -> "#1/" ^ string_of_int t
-   | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
+let str_fi fi =
+ "#1/" ^
+  String.concat "/" 
+   (List.map
+     (function
+         MQFC n -> string_of_int n
+       | MQFS -> "*"
+       | MQFSS -> "**"
+     ) fi)
+
+ function 
+  | (None, _)        -> ""
+  | (Some t, None)   -> "#1/" ^ string_of_int t
+  | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
 
 let str_tref (p, u, i) = 
-   p ^ ":/" ^ str_up u ^ str_fi i
+ let p =
+  match p with
+     None -> "*"
+   | Some s -> s
+ in
+  p ^ ":/" ^ str_up u ^ str_fi i
 
 let str_uref (u, i) = 
    UriManager.string_of_uri u ^ str_fi i
@@ -92,7 +107,7 @@ let out_query = function
 
 let rec out_list = function 
    | []     -> ""
-   | u :: l -> res (str_tref u) ^ nl () ^ out_list l 
+   | u :: l -> res u ^ nl () ^ out_list l 
 
 let out_result qr =
    par () ^ "Result:" ^ nl () ^
@@ -111,12 +126,12 @@ let split s =
       Not_found -> (s, "")
 
 let encode = function
-   | Str.Text s  -> MQString s
+   | Str.Text s  -> MQBC s
    | Str.Delim s ->  
-      if s = "?"  then MQAnyChr else
-      if s = "*"  then MQAst    else
-      if s = "**" then MQAstAst else
-      if s = "/"  then MQSlash  else MQString s
+      if s = "?"  then MQBQ else
+      if s = "*"  then MQBS else
+      if s = "**" then MQBSS else
+      if s = "/"  then MQBD  else MQBC s
 
 let tref_uref (u, i) =
    let s = UriManager.string_of_uri u in
@@ -124,7 +139,7 @@ let tref_uref (u, i) =
       | (p, q) -> 
          let rx = Str.regexp "\?\|\*\*\|\*\|/" in
          let l = Str.full_split rx q in
-         (p, List.map encode l, i) 
+         (Some p, List.map encode l, i) 
 
 (* CIC term inspecting functions *)
 
@@ -155,8 +170,9 @@ let universe = ref [];;
 let inspect_uri main l uri t c v =
  let fi =
   match (t, c) with
-     | (None, _) -> (None, None)
-     | (Some t0, c0) -> (Some (t0 + 1), c0) 
+     | (None, _) -> []
+     | (Some t0, Some c0) -> [MQFC (t0 + 1); MQFC c0]
+     | (Some t0, None) -> [MQFC (t0 + 1)]
  in
 (*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *)
   universe := (tref_uref (uri,fi))::!universe ;
@@ -233,7 +249,7 @@ let build_select (r, b, v) n =
             )
 
 let rec build_inter n = function
-   | []       -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None))
+   | []       -> MQPattern (Some "cic", [MQBSS; MQBC ".con"], [])
    | [ie]     -> build_select ie n
    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 
@@ -282,7 +298,7 @@ let close = Mqint.close
 let locate s = 
    let query = 
       MQList (MQSelect ("ref", 
-                        MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)),
+                        MQPattern (Some "cic", [MQBSS ; MQBC ".con"], []),
                         MQIs (MQFunc (MQName, "ref"),
                               MQCons s
                              )
diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli
index 3ea31b8d2..2d07f4ec4 100644
--- a/helm/gTopLevel/mquery.mli
+++ b/helm/gTopLevel/mquery.mli
@@ -33,12 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val str_tref  : Mathql.mqtref -> string        (* string linearization of a tokenized reference *)
-
-val out_query : Mathql.mquery -> string        (* HTML representation of a query *)
-
-val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *)
-
 val init      : unit -> unit                   (* INIT database function *)
 
 val close     : unit -> unit                   (* CLOSE database function *)