X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryUtil.ml;fp=helm%2Focaml%2Fmathql_interpreter%2FmQueryUtil.ml;h=0000000000000000000000000000000000000000;hp=e8344b0d60daa3fdb3c94bc833c1d220ba4a2296;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml deleted file mode 100644 index e8344b0d6..000000000 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.ml +++ /dev/null @@ -1,218 +0,0 @@ -(* 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) -