(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (* AUTOR: Ferruccio Guidi *) module M = MathQL module I = M.I module P = MQueryUtil module L = MQILib (* text linearization and parsing *******************************************) 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 let text_of_result out sep x = let txt_attr _ p l b = txt_path out p; if l <> [] then begin out " = "; P.flat_list out (txt_str out) ", " l end; if b then out ("; " ^ sep) in let txt_group l = out "{"; I.x_grp_iter txt_attr () l; out "}" in let txt_res _ s l b = txt_str out s; if l <> [] then begin out " = "; P.flat_list out txt_group ", " l end; if b then out "; " in I.x_iter txt_res () x; out sep let rec xtext_of_groups out l = let txt_attr (p, x) = txt_path out p; out " = "; text_of_query out "" x in let txt_group l = out "{"; P.flat_list out txt_attr "; " l; out "}" in P.flat_list out txt_group ", " l and xtext_of_result out x = let txt_res = function | (s, []) -> txt_str out s | (s, l) -> txt_str out s; out " attr "; xtext_of_groups out l in P.flat_list out txt_res "; " x and 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 let txt_ref = function | M.RefineExact -> () | M.RefineSub -> out "sub " | M.RefineSuper -> out "super " in let txt_qualif i r p = txt_inv i; txt_ref r; txt_path out p in let main = function | [] -> () | p -> out " main "; txt_path out p in let txt_exp = function | (pl, None) -> txt_path out pl | (pl, Some pr) -> txt_path out pl; out " as "; txt_path out pr in let txt_exp_list = function | [] -> () | l -> out " attr "; P.flat_list out txt_exp ", " l in let pattern b = if b then out "pattern " in let txt_distr d = if d then out "distr " in let txt_gen = function | M.GenFJoin -> out " sup " | M.GenFMeet -> out " inf " in let rec txt_con (pat, p, x) = txt_path out p; if pat then out " match " else out " in "; txt_set x and txt_con_list s = function | [] -> () | l -> out s; P.flat_list out txt_con ", " l and txt_istrue lt = txt_con_list " istrue " lt and txt_isfalse lf = txt_con_list " isfalse " lf and txt_grp = function | M.Attr g -> xtext_of_groups out g | M.From av -> txt_avar av and txt_set = function | M.Fun (p, pl, xl) -> let o = {L.out = out; L.path = txt_path; L.query = text_of_query; L.result = text_of_result } in L.fun_txt_out o p pl xl | M.Const [s, []] -> txt_str out s | M.Const r -> xtext_of_result out r | M.Dot (av, p) -> txt_avar av; out "."; txt_path out p | M.Ex (b, x) -> out "ex "; txt_set x (* | M.Ex b x -> out "ex ["; P.flat_list out txt_avar "," b; out "] "; txt_set x *) | M.SVar sv -> txt_svar sv | M.AVar av -> txt_avar av | M.Property (q0, q1, q2, mc, ct, cfl, xl, b, x) -> out "property "; txt_qualif q0 q1 q2; main mc; txt_istrue ct; P.flat_list out txt_isfalse "" cfl; txt_exp_list xl; out " of "; pattern b; txt_set x | M.Let (Some sv, x, y) -> out "let "; txt_svar sv; out " = "; txt_set x; out " in "; txt_set y | M.Let (None, x, y) -> txt_set x; out " ;; "; txt_set y | M.Select (av, x, y) -> out "select "; txt_avar av; out " from "; txt_set x; out " where "; txt_set y | M.For (k, av, x, y) -> out "for "; txt_avar av; out " in "; txt_set x; txt_gen k; txt_set y | M.While (k, x, y) -> out "while "; 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; 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}