(* 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 P = MQueryUtil module C = MQIConn module U = MQIUtil (* external function specification ******************************************) type arity_t = Const of int | Positive | Any type eval_spec = {eval : M.query -> M.result; conn : C.handle } type text_out_spec = {out : string -> unit; path : M.path -> unit; query : M.query -> unit; result : M.result -> unit } type fun_spec = {arity_p : arity_t; arity_s : arity_t; body : eval_spec -> text_out_spec -> M.path list -> M.query list -> M.result; txt_out : text_out_spec -> M.path list -> M.query list -> unit } exception ArityError of M.path * arity_t * int exception NameError of M.path exception NumberError of M.result (* external functions implementation ****************************************) let int_of_set s = try match s with | [s, _] -> int_of_string s | _ -> raise (Failure "int_of_string") with Failure "int_of_string" -> raise (NumberError s) let out_txt2 o n x1 x2 = o.out "(" ; o.query x1; o.out (" " ^ n ^ " "); o.query x2; o.out ")" let out_txt_ o p xl = if p <> [] then begin o.path p; o.out " " end; o.out "{"; P.flat_list o.out o.query ", " xl; o.out "}" let out_txt_full o p pl xl = o.path p; o.out " {"; P.flat_list o.out o.path ", " pl; o.out "} {"; P.flat_list o.out o.query ", " xl; o.out "}" let arity0 n r = let arity_p = Const 0 in let arity_s = Const 0 in let body _ _ _ _ = U.mql_true in let txt_out o _ _ = o.out n in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let arity1 n f = let arity_p = Const 0 in let arity_s = Const 1 in let body e _ _ = function | [x] -> f (e.eval x) | _ -> assert false in let txt_out o _ = function | [x] -> o.out (n ^ " "); o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let arity2 n f = let arity_p = Const 0 in let arity_s = Const 2 in let body e _ _ = function | [x1; x2] -> f (e.eval x1) (e.eval x2) | _ -> assert false in let txt_out o _ = function | [x1; x2] -> out_txt2 o n x1 x2 | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let false_fun b = let s = if b then "false" else "empty" in arity0 s U.mql_false let true_fun = arity0 "true" U.mql_true let not_fun = let aux r = if r = U.mql_false then U.mql_true else U.mql_false in arity1 "!" aux let count_fun = let aux r = [string_of_int (List.length r), []] in arity1 "#" aux let diff_fun = arity2 "diff" U.mql_diff let xor_fun = arity2 "xor" U.xor let sub_fun = arity2 "sub" U.set_sub let meet_fun = arity2 "meet" U.set_meet let eq_fun = arity2 "==" U.set_eq let le_fun = let le v1 v2 = if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false in arity2 "<=" le let lt_fun = let lt v1 v2 = if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false in arity2 "<" lt let stat_fun = let arity_p = Const 0 in let arity_s = Const 1 in let body e o _ = function | [x] -> let t = P.start_time () in let r = (e.eval x) in let s = P.stop_time t in o.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); r | _ -> assert false in let txt_out o _ = function | [x] -> o.out "stat "; o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let log_fun xml src = let log_src e o x = let t = P.start_time () in o.query x; let s = P.stop_time t in if C.set e.conn C.Stat then o.out (Printf.sprintf "Log source: %s\n" s); e.eval x in let log_res e o x = let s = e.eval x in let t = P.start_time () in o.result s; let r = P.stop_time t in if C.set e.conn C.Stat then o.out (Printf.sprintf "Log: %s\n" r); s in let txt_log o = if xml then o.out "xml "; if src then o.out "source " in let arity_p = Const 0 in let arity_s = Const 1 in let body e o _ = function | [x] -> if src then log_src e o x else log_res e o x | _ -> assert false in let txt_out o _ = function | [x] -> o.out "log "; txt_log o; o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let align_fun = let aux l (v, g) = let c = String.length v in if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g] in let arity_p = Const 0 in let arity_s = Const 2 in let body e _ _ = function | [y; x] -> let l = int_of_set (e.eval y) in U.mql_iter (aux l) (e.eval x) | _ -> assert false in let txt_out o _ = function | [y; x] -> o.out "align "; o.query y; o.out " in "; o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let if_fun = let arity_p = Const 0 in let arity_s = Const 3 in let body e _ _ = function | [y; x1; x2] -> if (e.eval y) = U.mql_false then (e.eval x2) else (e.eval x1) | _ -> assert false in let txt_out o _ = function | [y; x1; x2] -> o.out "if "; o.query y; o.out " then "; o.query x1; o.out " else "; o.query x2 | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let intersect_fun = let rec iter f = function | [] -> assert false | [head] -> f head | head :: tail -> U.mql_intersect (f head) (iter f tail) in let arity_p = Const 0 in let arity_s = Positive in let body e _ _ xl = iter e.eval xl in let txt_out o _ = function | [] -> assert false | [x1; x2] -> out_txt2 o "/\\" x1 x2 | xl -> out_txt_ o ["intersect"] xl in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let union_fun = let arity_p = Const 0 in let arity_s = Any in let body e _ _ xl = U.mql_iter e.eval xl in let txt_out o _ xl = out_txt_ o [] xl in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let or_fun = let rec iter f = function | [] -> U.mql_false | head :: tail -> let r1 = f head in if r1 = U.mql_false then (iter f tail) else r1 in let arity_p = Const 0 in let arity_s = Any in let body e _ _ xl = iter e.eval xl in let txt_out o _ = function | [x1; x2] -> out_txt2 o "||" x1 x2 | xl -> out_txt_ o ["or"] xl in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let and_fun = let rec iter f = function | [] -> U.mql_true | head :: tail -> if f head = U.mql_false then U.mql_false else iter f tail in let arity_p = Const 0 in let arity_s = Any in let body e _ _ xl = iter e.eval xl in let txt_out o _ = function | [x1; x2] -> out_txt2 o "&&" x1 x2 | xl -> out_txt_ o ["and"] xl in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let seq_fun = let rec iter f = function | [] -> U.mql_true | head :: tail -> ignore (f head); iter f tail in let arity_p = Const 0 in let arity_s = Any in let body e _ _ xl = iter e.eval xl in let txt_out o _ = function | [x1; x2] -> o.query x1; o.out " ;; "; o.query x2 | xl -> out_txt_ o ["seq"] xl in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let proj_fun = let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in let proj_group p a = U.mql_iter (proj_group_aux p) a in let proj_set p (_, g) = U.mql_iter (proj_group p) g in let arity_p = Const 1 in let arity_s = Const 1 in let body e _ pl xl = match pl, xl with | [p], [x] -> U.mql_iter (proj_set p) (e.eval x) | _ -> assert false in let txt_out o pl xl = match pl, xl with | [p], [x] -> o.out "proj "; o.path p; o.out " of "; o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} let keep_fun b = let proj (r, _) = (r, []) in let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in let keep_grp l a = List.fold_right (keep_path l) a [] in let keep_set l a g = let kg = keep_grp l a in if kg = [] then g else kg :: g in let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in let txt_allbut o = if b then o.out "allbut " in let txt_path_list o l = P.flat_list o.out o.path ", " l in let arity_p = Any in let arity_s = Const 1 in let body e _ pl xl = match b, pl, xl with | true, [], [x] -> e.eval x | false, [], [x] -> List.map proj (e.eval x) | _, l, [x] -> List.map (keep_av l) (e.eval x) | _ -> assert false in let txt_out o pl xl = match pl, xl with | [], [x] -> o.out "keep "; txt_allbut o; o.query x | l, [x] -> o.out "keep "; txt_allbut o; txt_path_list o l; o.out " in "; o.query x | _ -> assert false in {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out} (* external functions interface *********************************************) let get_spec = function | ["empty"] -> false_fun false | ["false"] -> false_fun true | ["true"] -> true_fun | ["not"] -> not_fun | ["count"] -> count_fun | ["stat"] -> stat_fun | ["log"; "text"; "result"] -> log_fun false false | ["log"; "text"; "source"] -> log_fun false true | ["diff"] -> diff_fun | ["xor"] -> xor_fun | ["sub"] -> sub_fun | ["meet"] -> meet_fun | ["eq"] -> eq_fun | ["le"] -> le_fun | ["lt"] -> lt_fun | ["align"] -> align_fun | ["if"] -> if_fun | ["intersect"] -> intersect_fun | ["union"] -> union_fun | ["or"] -> or_fun | ["and"] -> and_fun | ["seq"] -> seq_fun | ["proj"] -> proj_fun | ["keep"; "these"] -> keep_fun false | ["keep"; "allbut"] -> keep_fun true | p -> raise (NameError p) let check_arity p m n = let aux i = function | Const k when i = k -> () | Positive when i > 0 -> () | Any -> () | a -> raise (ArityError (p, a, i)) in aux m (get_spec p).arity_p; aux n (get_spec p).arity_s let eval e o p pl xl = (get_spec p).body e o pl xl let txt_out o p pl xl = try (get_spec p).txt_out o pl xl with NameError q when q = p -> out_txt_full o p pl xl