]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mQueryIO.ml
f220a270de5694cb1f4f0a33fe3b24f022bf2484
[helm.git] / helm / ocaml / mathql_interpreter / mQueryIO.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
27  *)
28
29 module M = MathQL
30 module P = MQueryUtil
31 module L = MQILib
32
33 (* text linearization and parsing *******************************************)
34
35 let txt_quote s =
36    let rec aux r i l s = 
37       let commit c =
38          let l = pred (l - i) in
39          aux (r ^ String.sub s 0 i ^ c) 0 l (String.sub s (succ i) l) 
40       in
41       if i = l then r ^ s else
42       match s.[i] with
43          | '\\' -> commit "\\\\^"
44          | '^'  -> commit "\\^^"
45          | '\"' -> commit "\\\"^"
46          | _    -> aux r (succ i) l s
47    in
48    aux "" 0 (String.length s) s
49
50 let txt_str out s = out ("\"" ^ txt_quote s ^ "\"")
51
52 let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p 
53
54 let text_of_result out sep x = 
55    let txt_attr = function
56       | (p, []) -> txt_path out p
57       | (p, l)  -> txt_path out p; out " = "; 
58                    P.flat_list out (txt_str out) ", " l
59    in
60    let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in
61    let txt_res = function
62       | (s, []) -> txt_str out s 
63       | (s, l)  -> txt_str out s; out " attr "; 
64                    P.flat_list out txt_group ", " l
65    in   
66    let txt_set l = P.flat_list out txt_res ("; " ^ sep) l; out sep in
67    txt_set x
68
69 let rec text_of_query out sep x = 
70    let txt_svar sv = out ("$" ^ sv) in 
71    let txt_avar av = out ("@" ^ av) in
72    let txt_inv i = if i then out "inverse " in
73    let txt_ref = function
74       | M.RefineExact -> ()
75       | M.RefineSub   -> out "sub "
76       | M.RefineSuper -> out "super "
77    in
78    let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in
79    let main = function
80       | [] -> ()
81       | p  -> out " main "; txt_path out p
82    in
83    let txt_exp = function
84       | (pl, None)    -> txt_path out pl 
85       | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr
86    in
87    let txt_exp_list = function
88       | [] -> ()
89       | l  -> out " attr "; P.flat_list out txt_exp ", " l 
90    in
91    let pattern b = if b then out "pattern " in
92    let txt_distr d = if d then out "distr " in
93    let txt_gen = function
94       | M.GenFJoin -> out " sup "
95       | M.GenFMeet -> out " inf "
96    in
97    let rec txt_con (pat, p, x) = 
98       txt_path out p; 
99       if pat then out " match " else out " in ";
100       txt_set x
101    and txt_con_list s = function
102       | [] -> ()
103       | l  -> out s; P.flat_list out txt_con ", " l 
104    and txt_istrue lt = txt_con_list " istrue " lt 
105    and txt_isfalse lf = txt_con_list " isfalse " lf
106    and txt_ass (p, x) = txt_set x; out " as "; txt_path out p
107    and txt_ass_list l = P.flat_list out txt_ass ", " l
108    and txt_assg_list g = P.flat_list out txt_ass_list "; " g
109    and txt_grp = function
110       | M.Attr g  -> txt_assg_list g
111       | M.From av -> txt_avar av
112    and txt_set = function
113       | M.Fun p pl xl      -> 
114          let o = {L.out = out; L.path = txt_path; 
115                   L.query = text_of_query; L.result = text_of_result
116                  } 
117          in
118          L.txt_out o p pl xl 
119       | M.Const [s, []] -> txt_str out s
120       | M.Const r       -> text_of_result out " " r
121       | M.Dot av p      -> txt_avar av; out "."; txt_path out p
122       | M.Ex b x        -> out "ex "; txt_set x
123 (*    | M.Ex b x        -> out "ex ["; P.flat_list out txt_avar "," b; 
124                            out "] "; txt_set x
125 *)    | M.SVar sv       -> txt_svar sv
126       | M.AVar av       -> txt_avar av
127       | M.Property q0 q1 q2 mc ct cfl xl b x -> 
128          out "property "; txt_qualif q0 q1 q2; main mc;
129          txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl;
130          out " of "; pattern b; txt_set x
131       | M.Let sv x y    -> out "let "; txt_svar sv; out " = "; 
132                            txt_set x; out " in "; txt_set y
133       | M.Select av x y -> out "select "; txt_avar av; out " from ";
134                            txt_set x; out " where "; txt_set y
135       | M.For k av x y  -> out "for "; txt_avar av; out " in ";
136                            txt_set x; txt_gen k; txt_set y
137       | M.Add d g x     -> out "add "; txt_distr d; txt_grp g; 
138                            out " in "; txt_set x
139    in 
140    txt_set x; out sep
141
142 let text_out_spec out sep =
143    {L.out = out; L.path = txt_path; 
144     L.query = text_of_query; L.result = text_of_result
145    }
146
147 let query_of_text lexbuf =
148    MQueryTParser.query MQueryTLexer.query_token lexbuf 
149
150 let result_of_text lexbuf =
151    MQueryTParser.result MQueryTLexer.result_token lexbuf 
152
153 let text_in_spec = {L.result_in = result_of_text}