1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
29 (* text linearization and parsing *******************************************)
31 let rec txt_list out f s = function
34 | a :: tail -> f a; out s; txt_list out f s tail
36 let txt_str out s = out ("\"" ^ s ^ "\"")
38 let txt_path out p = out "/"; txt_list out (txt_str out) "/" p
40 let text_of_query out sep x =
41 let module M = MathQL in
42 let txt_path_list l = txt_list out (txt_path out) ", " l in
43 let txt_svar sv = out ("%" ^ sv) in
44 let txt_avar av = out ("@" ^ av) in
45 let txt_vvar vv = out ("$" ^ vv) in
46 let txt_inv i = if i then out "inverse " in
47 let txt_ref = function
49 | M.RefineSub -> out "sub "
50 | M.RefineSuper -> out "super "
52 let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in
55 | p -> out " main "; txt_path out p
57 let txt_exp = function
58 | (pl, None) -> txt_path out pl
59 | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr
61 let txt_exp_list = function
63 | l -> out " attr "; txt_list out txt_exp ", " l
65 let pattern b = if b then out "pattern " in
66 let txt_opt_path = function
68 | Some p -> txt_path out p; out " "
70 let txt_distr d = if d then out "distr " in
71 let txt_bin = function
72 | M.BinFJoin -> out " union "
73 | M.BinFMeet -> out " intersect "
74 | M.BinFDiff -> out " diff "
76 let txt_gen = function
77 | M.GenFJoin -> out " sup "
78 | M.GenFMeet -> out " inf "
80 let txt_test = function
81 | M.Xor -> out " xor "
83 | M.And -> out " and "
84 | M.Sub -> out " sub "
85 | M.Meet -> out " meet "
92 if b then out "source "
94 let txt_allbut b = if b then out "allbut " in
95 let rec txt_con (pat, p, x) =
97 if pat then out " match " else out " in ";
99 and txt_con_list s = function
101 | l -> out s; txt_list out txt_con ", " l
102 and txt_istrue lt = txt_con_list " istrue " lt
103 and txt_isfalse lf = txt_con_list " isfalse " lf
104 and txt_ass (p, x) = txt_val x; out " as "; txt_path out p
105 and txt_ass_list l = txt_list out txt_ass ", " l
106 and txt_assg_list g = txt_list out txt_ass_list "; " g
107 and txt_val_list = function
109 | l -> out "{"; txt_list out txt_val ", " l; out "}"
110 and txt_grp = function
111 | M.Attr g -> txt_assg_list g
112 | M.From av -> txt_avar av
113 and txt_val = function
114 | M.True -> out "true"
115 | M.False -> out "false"
116 | M.Const s -> txt_str out s
117 | M.Set l -> txt_val_list l
118 | M.VVar vv -> txt_vvar vv
119 | M.Dot (av,p) -> txt_avar av; out "."; txt_path out p
120 | M.Proj (op,x) -> out "proj "; txt_opt_path op; txt_set x
121 | M.Ex (b,x) -> out "ex "; txt_val x
122 (* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x
123 *) | M.Not x -> out "not "; txt_val x
124 | M.Test (k,x,y) -> out "("; txt_val x; txt_test k; txt_val y; out ")"
125 | M.StatVal x -> out "stat "; txt_val x
126 | M.Count x -> out "count "; txt_val x
127 | M.Align (s,x) -> out "align "; txt_str out s; out " in "; txt_val x
128 and txt_set = function
129 | M.Empty -> out "empty"
130 | M.SVar sv -> txt_svar sv
131 | M.AVar av -> txt_avar av
132 | M.Property (q0,q1,q2,mc,ct,cfl,xl,b,x) ->
133 out "property "; txt_qualif q0 q1 q2; main mc;
134 txt_istrue ct; txt_list out txt_isfalse "" cfl; txt_exp_list xl;
135 out " of "; pattern b; txt_val x
136 | M.Bin (k,x,y) -> out "("; txt_set x; txt_bin k; txt_set y;
138 | M.LetSVar (sv,x,y) -> out "let "; txt_svar sv; out " be ";
139 txt_set x; out " in "; txt_set y
140 | M.LetVVar (vv,x,y) -> out "let "; txt_vvar vv; out " be ";
141 txt_val x; out " in "; txt_set y
142 | M.Select (av,x,y) -> out "select "; txt_avar av; out " from ";
143 txt_set x; out " where "; txt_val y
144 | M.Subj x -> out "subj "; txt_val x
145 | M.For (k,av,x,y) -> out "for "; txt_avar av; out " in ";
146 txt_set x; txt_gen k; txt_set y
147 | M.If (x,y,z) -> out "if "; txt_val x; out " then ";
148 txt_set y; out " else "; txt_set z
149 | M.Add (d,g,x) -> out "add "; txt_distr d; txt_grp g;
150 out " in "; txt_set x
151 | M.Log (a,b,x) -> out "log "; txt_log a b; txt_set x
152 | M.StatQuery x -> out "stat "; txt_set x
153 | M.Keep (b,l,x) -> out "keep "; txt_allbut b; txt_path_list l;
158 let text_of_result out sep x =
159 let txt_attr = function
160 | (p, []) -> txt_path out p
161 | (p, l) -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l
163 let txt_group l = out "{"; txt_list out txt_attr "; " l; out "}" in
164 let txt_res = function
165 | (s, []) -> txt_str out s
166 | (s, l) -> txt_str out s; out " attr "; txt_list out txt_group ", " l
168 let txt_set l = txt_list out txt_res ("; " ^ sep) l; out sep in
171 let query_of_text lexbuf =
172 MQueryTParser.query MQueryTLexer.query_token lexbuf
174 let result_of_text lexbuf =
175 MQueryTParser.result MQueryTLexer.result_token lexbuf
177 (* time handling ***********************************************************)
179 type time = float * float
182 (Sys.time (), Unix.time ())
184 let stop_time (s0, u0) =
185 let s1 = Sys.time () in
186 let u1 = Unix.time () in
187 Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0)
189 (* operations on lists *****************************************************)
191 type 'a comparison = Lt
195 let list_join f l1 l2 =
196 let rec aux = function
199 | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
201 | Lt -> h1 :: aux (t1, v2)
202 | Gt -> h2 :: aux (v1, t2)
203 | Eq h -> h :: aux (t1, t2)
207 let list_meet f l1 l2 =
208 let rec aux = function
211 | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
215 | Eq h -> h :: aux (t1, t2)