(* 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 *) (* text linearization and parsing *******************************************) let rec txt_list out f s = function | [] -> () | [a] -> f a | a :: tail -> f a; out s; txt_list out f s tail let txt_str out s = out ("\"" ^ s ^ "\"") let txt_path out p = out "/"; txt_list out (txt_str out) "/" p let text_of_query out sep x = let module M = MathQL in let txt_path_list l = txt_list out (txt_path out) ", " l in let txt_svar sv = out ("%" ^ sv) in let txt_avar av = out ("@" ^ av) in let txt_vvar vv = out ("$" ^ vv) 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 "; txt_list out txt_exp ", " l in let pattern b = if b then out "pattern " in let txt_opt_path = function | None -> () | Some p -> txt_path out p; out " " in let txt_distr d = if d then out "distr " in let txt_bin = function | M.BinFJoin -> out " union " | M.BinFMeet -> out " intersect " | M.BinFDiff -> out " diff " in let txt_gen = function | M.GenFJoin -> out " sup " | M.GenFMeet -> out " inf " in let txt_test = function | M.Xor -> out " xor " | M.Or -> out " or " | M.And -> out " and " | M.Sub -> out " sub " | M.Meet -> out " meet " | M.Eq -> out " eq " | M.Le -> out " le " | M.Lt -> out " lt " in let txt_log a b = if a then out "xml "; if b then out "source " in let txt_allbut b = if b then out "allbut " in let rec txt_con (pat, p, x) = txt_path out p; if pat then out " match " else out " in "; txt_val x and txt_con_list s = function | [] -> () | l -> out s; txt_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_ass (p, x) = txt_val x; out " as "; txt_path out p and txt_ass_list l = txt_list out txt_ass ", " l and txt_assg_list g = txt_list out txt_ass_list "; " g and txt_val_list = function | [v] -> txt_val v | l -> out "{"; txt_list out txt_val ", " l; out "}" and txt_grp = function | M.Attr g -> txt_assg_list g | M.From av -> txt_avar av and txt_val = function | M.True -> out "true" | M.False -> out "false" | M.Const s -> txt_str out s | M.Set l -> txt_val_list l | M.VVar vv -> txt_vvar vv | M.Dot (av,p) -> txt_avar av; out "."; txt_path out p | M.Proj (op,x) -> out "proj "; txt_opt_path op; txt_set x | M.Ex (b,x) -> out "ex "; txt_val x (* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x *) | M.Not x -> out "not "; txt_val x | M.Test (k,x,y) -> out "("; txt_val x; txt_test k; txt_val y; out ")" | M.StatVal x -> out "stat "; txt_val x | M.Count x -> out "count "; txt_val x | M.Align (s,x) -> out "align "; txt_str out s; out " in "; txt_val x and txt_set = function | M.Empty -> out "empty" | 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; txt_list out txt_isfalse "" cfl; txt_exp_list xl; out " of "; pattern b; txt_val x | M.Bin (k,x,y) -> out "("; txt_set x; txt_bin k; txt_set y; out ")" | M.LetSVar (sv,x,y) -> out "let "; txt_svar sv; out " be "; txt_set x; out " in "; txt_set y | M.LetVVar (vv,x,y) -> out "let "; txt_vvar vv; out " be "; txt_val x; out " in "; txt_set y | M.Select (av,x,y) -> out "select "; txt_avar av; out " from "; txt_set x; out " where "; txt_val y | M.Subj x -> out "subj "; txt_val x | M.For (k,av,x,y) -> out "for "; txt_avar av; out " in "; txt_set x; txt_gen k; txt_set y | M.If (x,y,z) -> out "if "; txt_val x; out " then "; txt_set y; out " else "; txt_set z | M.Add (d,g,x) -> out "add "; txt_distr d; txt_grp g; out " in "; txt_set x | M.Log (a,b,x) -> out "log "; txt_log a b; txt_set x | M.StatQuery x -> out "stat "; txt_set x | M.Keep (b,l,x) -> out "keep "; txt_allbut b; txt_path_list l; txt_set x in txt_set x; out sep let text_of_result out sep x = let txt_attr = function | (p, []) -> txt_path out p | (p, l) -> txt_path out p; out " = "; txt_list out (txt_str out) ", " l in let txt_group l = out "{"; txt_list out txt_attr "; " l; out "}" in let txt_res = function | (s, []) -> txt_str out s | (s, l) -> txt_str out s; out " attr "; txt_list out txt_group ", " l in let txt_set l = txt_list out txt_res ("; " ^ sep) l; out sep in txt_set x let query_of_text lexbuf = MQueryTParser.query MQueryTLexer.query_token lexbuf let result_of_text lexbuf = MQueryTParser.result MQueryTLexer.result_token lexbuf (* time handling ***********************************************************) type time = float * float let start_time () = (Sys.time (), Unix.time ()) let stop_time (s0, u0) = let s1 = Sys.time () in let u1 = Unix.time () in Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) (* operations on lists *****************************************************) type 'a comparison = Lt | Gt | Eq of 'a let list_join f l1 l2 = let rec aux = function | [], v | v, [] -> v | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin match f h1 h2 with | Lt -> h1 :: aux (t1, v2) | Gt -> h2 :: aux (v1, t2) | Eq h -> h :: aux (t1, t2) end in aux (l1, l2) let list_meet f l1 l2 = let rec aux = function | [], v | v, [] -> [] | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin match f h1 h2 with | Lt -> aux (t1, v2) | Gt -> aux (v1, t2) | Eq h -> h :: aux (t1, t2) end in aux (l1, l2)