helm/ocaml/mathql_interpreter/mQILib.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  27  *)
  28
  29 module M = MathQL
  30 module P = MQueryUtil
  31 module C = MQIConn
  32 module U = MQIUtil
  33
  34 (* external function specification ******************************************)
  35
  36 type arity_t = Const of int
  37              | Positive
  38              | Any
  39
  40 type eval_spec = {eval : M.query -> M.result;
  41                   conn : C.handle
  42                  }
  43
  44 type text_out_spec = {out    : string -> unit;
  45                       path   : M.path -> unit;
  46                       query  : M.query -> unit;
  47                       result : M.result -> unit
  48                      }
  49
  50 type fun_spec = {arity_p : arity_t;
  51                  arity_s : arity_t;
  52                  body    : eval_spec -> text_out_spec ->
  53                            M.path list -> M.query list -> M.result;
  54                  txt_out : text_out_spec ->
  55                            M.path list -> M.query list -> unit
  56                 }
  57
  58 exception ArityError of M.path * arity_t * int
  59
  60 exception NameError of M.path
  61
  62 exception NumberError of M.result
  63
  64 (* external functions implementation ****************************************)
  65
  66 let int_of_set s =
  67    try match s with
  68       | [s, _] -> int_of_string s
  69       | _      -> raise (Failure "int_of_string")
  70    with Failure "int_of_string" -> raise (NumberError s)
  71
  72 let out_txt2 o n x1 x2 =
  73    o.out "(" ; o.query x1; o.out (" " ^ n ^ " "); o.query x2; o.out ")"
  74
  75 let out_txt_ o p xl =
  76    if p <> [] then begin o.path p; o.out " " end;
  77    o.out "{"; P.flat_list o.out o.query ", " xl; o.out "}"
  78
  79 let out_txt_full o p pl xl =
  80    o.path p; o.out " {"; P.flat_list o.out o.path ", " pl; o.out "} {";
  81    P.flat_list o.out o.query ", " xl; o.out "}"
  82
  83 let arity0 n r =
  84    let arity_p = Const 0 in
  85    let arity_s = Const 0 in
  86    let body _ _ _ _ = U.mql_true in
  87    let txt_out o _ _ = o.out n in
  88    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
  89
  90 let arity1 n f =
  91    let arity_p = Const 0 in
  92    let arity_s = Const 1 in
  93    let body e _ _ = function
  94       | [x] -> f (e.eval x)
  95       | _   -> assert false
  96    in
  97    let txt_out o _ = function
  98       | [x] -> o.out (n ^ " "); o.query x
  99       | _   -> assert false
 100    in
 101    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 102
 103 let arity2 n f =
 104    let arity_p = Const 0 in
 105    let arity_s = Const 2 in
 106    let body e _ _ = function
 107       | [x1; x2] -> f (e.eval x1) (e.eval x2)
 108       | _        -> assert false
 109    in
 110    let txt_out o _ = function
 111       | [x1; x2] -> out_txt2 o n x1 x2
 112       | _        -> assert false
 113    in
 114    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 115
 116 let false_fun b =
 117    let s = if b then "false" else "empty" in
 118    arity0 s U.mql_false
 119
 120 let true_fun = arity0 "true" U.mql_true
 121
 122 let not_fun =
 123    let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
 124    arity1 "!" aux
 125
 126 let count_fun =
 127    let aux r = [string_of_int (List.length r), []] in
 128    arity1 "#" aux
 129
 130 let diff_fun = arity2 "diff" U.mql_diff
 131
 132 let xor_fun = arity2 "xor" U.xor
 133
 134 let sub_fun = arity2 "sub" U.set_sub
 135
 136 let meet_fun = arity2 "meet" U.set_meet
 137
 138 let eq_fun = arity2 "==" U.set_eq
 139
 140 let le_fun =
 141    let le v1 v2 =
 142       if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false
 143    in
 144    arity2 "<=" le
 145
 146 let lt_fun =
 147    let lt v1 v2 =
 148       if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false
 149    in
 150    arity2 "<" lt
 151
 152 let stat_fun =
 153    let arity_p = Const 0 in
 154    let arity_s = Const 1 in
 155    let body e o _ = function
 156       | [x] ->
 157          let t = P.start_time () in
 158          let r = (e.eval x) in
 159          let s = P.stop_time t in
 160          o.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
 161          r
 162       | _   -> assert false
 163    in
 164    let txt_out o _ = function
 165       | [x] -> o.out "stat "; o.query x
 166       | _   -> assert false
 167    in
 168    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 169
 170 let log_fun xml src =
 171    let log_src e o x =
 172       let t = P.start_time () in o.query x;
 173       let s = P.stop_time t in
 174       if C.set e.conn C.Stat then o.out (Printf.sprintf "Log source: %s\n" s);
 175       e.eval x
 176    in
 177    let log_res e o x =
 178       let s = e.eval x in
 179       let t = P.start_time () in o.result s;
 180       let r = P.stop_time t in
 181       if C.set e.conn C.Stat then o.out (Printf.sprintf "Log: %s\n" r); s
 182    in
 183    let txt_log o =
 184       if xml then o.out "xml ";
 185       if src then o.out "source "
 186    in
 187    let arity_p = Const 0 in
 188    let arity_s = Const 1 in
 189    let body e o _ = function
 190       | [x] -> if src then log_src e o x else log_res e o x
 191       | _   -> assert false
 192    in
 193    let txt_out o _ = function
 194       | [x] -> o.out "log "; txt_log o; o.query x
 195       | _   -> assert false
 196    in
 197    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 198
 199 let align_fun =
 200    let aux l (v, g) =
 201       let c = String.length v in
 202       if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
 203    in
 204    let arity_p = Const 0 in
 205    let arity_s = Const 2 in
 206    let body e _ _ = function
 207       | [y; x] ->
 208          let l = int_of_set (e.eval y) in
 209          U.mql_iter (aux l) (e.eval x)
 210       | _      -> assert false
 211    in
 212    let txt_out o _ = function
 213       | [y; x] -> o.out "align "; o.query y; o.out " in "; o.query x
 214       | _      -> assert false
 215    in
 216    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 217
 218 let if_fun =
 219    let arity_p = Const 0 in
 220    let arity_s = Const 3 in
 221    let body e _ _ = function
 222       | [y; x1; x2] ->
 223          if (e.eval y) = U.mql_false then (e.eval x2) else (e.eval x1)
 224       | _           -> assert false
 225    in
 226    let txt_out o _ = function
 227       | [y; x1; x2] ->
 228          o.out "if "; o.query y; o.out " then "; o.query x1;
 229          o.out " else "; o.query x2
 230       | _           -> assert false
 231    in
 232    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 233
 234 let intersect_fun =
 235    let rec iter f = function
 236       | []           -> assert false
 237       | [head]       -> f head
 238       | head :: tail -> U.mql_intersect (f head) (iter f tail)
 239    in
 240    let arity_p = Const 0 in
 241    let arity_s = Positive in
 242    let body e _ _ xl = iter e.eval xl in
 243    let txt_out o _ = function
 244       | []           -> assert false
 245       | [x1; x2]     -> out_txt2 o "/\\" x1 x2
 246       | xl           -> out_txt_ o ["intersect"] xl
 247    in
 248    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 249
 250 let union_fun =
 251    let arity_p = Const 0 in
 252    let arity_s = Any in
 253    let body e _ _ xl = U.mql_iter e.eval xl in
 254    let txt_out o _ xl = out_txt_ o [] xl
 255    in
 256    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 257
 258 let or_fun =
 259    let rec iter f = function
 260       | []           -> U.mql_false
 261       | head :: tail ->
 262          let r1 = f head in
 263          if r1 = U.mql_false then (iter f tail) else r1
 264    in
 265    let arity_p = Const 0 in
 266    let arity_s = Any in
 267    let body e _ _ xl = iter e.eval xl in
 268    let txt_out o _ = function
 269       | [x1; x2]     -> out_txt2 o "||" x1 x2
 270       | xl           -> out_txt_ o ["or"] xl
 271    in
 272    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 273
 274 let and_fun =
 275    let rec iter f = function
 276       | []           -> U.mql_true
 277       | head :: tail ->
 278          if f head = U.mql_false then U.mql_false else iter f tail
 279    in
 280    let arity_p = Const 0 in
 281    let arity_s = Any in
 282    let body e _ _ xl = iter e.eval xl in
 283    let txt_out o _ = function
 284       | [x1; x2]  -> out_txt2 o "&&" x1 x2
 285       | xl        -> out_txt_ o ["and"] xl
 286    in
 287    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 288
 289 let seq_fun =
 290    let rec iter f = function
 291       | []           -> U.mql_true
 292       | head :: tail -> ignore (f head); iter f tail
 293    in
 294    let arity_p = Const 0 in
 295    let arity_s = Any in
 296    let body e _ _ xl = iter e.eval xl in
 297    let txt_out o _ = function
 298       | [x1; x2]  -> o.query x1; o.out " ;; "; o.query x2
 299       | xl        -> out_txt_ o ["seq"] xl
 300    in
 301    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 302
 303 let proj_fun =
 304    let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in
 305    let proj_group p a = U.mql_iter (proj_group_aux p) a in
 306    let proj_set p (_, g) = U.mql_iter (proj_group p) g in
 307    let arity_p = Const 1 in
 308    let arity_s = Const 1 in
 309    let body e _ pl xl =
 310       match pl, xl with
 311          | [p], [x] -> U.mql_iter (proj_set p) (e.eval x)
 312          | _        -> assert false
 313    in
 314    let txt_out o pl xl =
 315       match pl, xl with
 316          | [p], [x] -> o.out "proj "; o.path p; o.out " of "; o.query x
 317          | _        -> assert false
 318    in
 319    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 320
 321 let keep_fun b =
 322    let proj (r, _) = (r, []) in
 323    let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in
 324    let keep_grp l a = List.fold_right (keep_path l) a [] in
 325    let keep_set l a g =
 326       let kg = keep_grp l a in
 327       if kg = [] then g else kg :: g
 328    in
 329    let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
 330    let txt_allbut o = if b then o.out "allbut " in
 331    let txt_path_list o l = P.flat_list o.out o.path ", " l in
 332    let arity_p = Any in
 333    let arity_s = Const 1 in
 334    let body e _ pl xl =
 335       match b, pl, xl with
 336          | true, [], [x]  -> e.eval x
 337          | false, [], [x] -> List.map proj (e.eval x)
 338          | _, l, [x]      -> List.map (keep_av l) (e.eval x)
 339          | _              -> assert false
 340   in
 341   let txt_out o pl xl =
 342       match pl, xl with
 343          | [], [x] -> o.out "keep "; txt_allbut o; o.query x
 344          | l, [x]  ->
 345             o.out "keep "; txt_allbut o; txt_path_list o l;
 346             o.out " in "; o.query x
 347          | _      -> assert false
 348    in
 349    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 350
 351 (* external functions interface *********************************************)
 352
 353 let get_spec = function
 354    | ["empty"]                 -> false_fun false
 355    | ["false"]                 -> false_fun true
 356    | ["true"]                  -> true_fun
 357    | ["not"]                   -> not_fun
 358    | ["count"]                 -> count_fun
 359    | ["stat"]                  -> stat_fun
 360    | ["log"; "text"; "result"] -> log_fun false false
 361    | ["log"; "text"; "source"] -> log_fun false true
 362    | ["diff"]                  -> diff_fun
 363    | ["xor"]                   -> xor_fun
 364    | ["sub"]                   -> sub_fun
 365    | ["meet"]                  -> meet_fun
 366    | ["eq"]                    -> eq_fun
 367    | ["le"]                    -> le_fun
 368    | ["lt"]                    -> lt_fun
 369    | ["align"]                 -> align_fun
 370    | ["if"]                    -> if_fun
 371    | ["intersect"]             -> intersect_fun
 372    | ["union"]                 -> union_fun
 373    | ["or"]                    -> or_fun
 374    | ["and"]                   -> and_fun
 375    | ["seq"]                   -> seq_fun
 376    | ["proj"]                  -> proj_fun
 377    | ["keep"; "these"]         -> keep_fun false
 378    | ["keep"; "allbut"]        -> keep_fun true
 379    | p                         -> raise (NameError p)
 380
 381 let check_arity p m n =
 382    let aux i = function
 383       | Const k when i = k  -> ()
 384       | Positive when i > 0 -> ()
 385       | Any                 -> ()
 386       | a                     -> raise (ArityError (p, a, i))
 387    in
 388    aux m (get_spec p).arity_p; aux n (get_spec p).arity_s
 389
 390 let eval e o p pl xl = (get_spec p).body e o pl xl
 391
 392 let txt_out o p pl xl =
 393    try (get_spec p).txt_out o pl xl
 394    with NameError q when q = p -> out_txt_full o p pl xl