New module helm-mathql.

[helm.git] / helm / gTopLevel / mquery.ml

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index 73118c962e743ae70b13799d273106875d78525b..0cf33c83cc155bff55f1abd37db3146422b35e07 100644 (file)
--- 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
                              )