]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryIO.ml
patched and new Gen constructor added
[helm.git] / helm / ocaml / mathql_interpreter / mQueryIO.ml
index a7d30dd0910ade259a1a2f549c1a562384b63738..a8fe2006eeb4faaccc08ac8c86d3eb340379c2f2 100644 (file)
@@ -32,7 +32,22 @@ module L = MQILib
 
 (* text linearization and parsing *******************************************)
 
-let txt_str out s = out ("\"" ^ s ^ "\"")
+let txt_quote s =
+   let rec aux r i l s = 
+      let commit c =
+         let l = pred (l - i) in
+         aux (r ^ String.sub s 0 i ^ c) 0 l (String.sub s (succ i) l) 
+      in
+      if i = l then r ^ s else
+      match s.[i] with
+         | '\\' -> commit "\\\\^"
+         | '^'  -> commit "\\^^"
+         | '\"' -> commit "\\\"^"
+         | _    -> aux r (succ i) l s
+   in
+   aux "" 0 (String.length s) s
+
+let txt_str out s = out ("\"" ^ txt_quote s ^ "\"")
 
 let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p 
 
@@ -51,7 +66,7 @@ let text_of_result out sep x =
    let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in
    txt_set x
 
-let text_of_query out sep x = 
+let rec text_of_query out sep x = 
    let txt_svar sv = out ("$" ^ sv) in 
    let txt_avar av = out ("@" ^ av) in
    let txt_inv i = if i then out "inverse " in
@@ -96,10 +111,11 @@ let text_of_query out sep x =
       | M.From av -> txt_avar av
    and txt_set = function
       | M.Fun p pl xl      -> 
-         let o = {L.out = out; L.path = txt_path out; L.query = txt_set;
-           L.result = text_of_result out sep} 
+         let o = {L.out = out; L.path = txt_path; 
+                 L.query = text_of_query; L.result = text_of_result
+                } 
         in
-        L.txt_out o p pl xl 
+        L.fun_txt_out o p pl xl 
       | M.Const [s, []] -> txt_str out s
       | M.Const r       -> text_of_result out " " r
       | M.Dot av p      -> txt_avar av; out "."; txt_path out p
@@ -120,15 +136,21 @@ let text_of_query out sep x =
                            txt_set x; txt_gen k; txt_set y
       | M.Add d g x     -> out "add "; txt_distr d; txt_grp g; 
                            out " in "; txt_set x
+      | M.Gen p [x]     -> out "gen "; txt_path out p; out " in "; txt_set x
+      | M.Gen p l       -> out "gen "; txt_path out p; out " {";
+                           P.flat_list out txt_set ", " l; out "}"
    in 
    txt_set x; out sep
 
 let text_out_spec out sep =
-   {L.out = out; L.path = txt_path out; L.query = text_of_query out sep;
-    L.result = text_of_result out sep}
+   {L.out = out; L.path = txt_path; 
+    L.query = text_of_query; L.result = text_of_result
+   }
 
 let query_of_text lexbuf =
    MQueryTParser.query MQueryTLexer.query_token lexbuf 
 
 let result_of_text lexbuf =
    MQueryTParser.result MQueryTLexer.result_token lexbuf 
+
+let text_in_spec = {L.result_in = result_of_text}