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   : (string -> unit) -> M.path -> unit;
  46                       query  : (string -> unit) -> string -> M.query -> unit;
  47                       result : (string -> unit) -> string -> M.result -> unit
  48                      }
  49
  50 type text_in_spec = {result_in : Lexing.lexbuf -> M.result}
  51
  52 type fun_spec = {arity_p : arity_t;
  53                  arity_s : arity_t;
  54                  body    : eval_spec -> text_out_spec -> text_in_spec ->
  55                            M.path list -> M.query list -> M.result;
  56                  txt_out : text_out_spec ->
  57                            M.path list -> M.query list -> unit
  58                 }
  59
  60 type gen_spec = {arity : arity_t;
  61                  code  : eval_spec -> M.query list -> M.query
  62                 }
  63
  64 exception ArityError of M.path * arity_t * int
  65
  66 exception NameError of M.path
  67
  68 exception NumberError of M.result
  69
  70 type std_text_out_spec = {s_out    : string -> unit;
  71                           s_path   : M.path -> unit;
  72                           s_query  : M.query -> unit;
  73                           s_result : M.result -> unit
  74 }
  75
  76 let check_arity p i = function
  77    | Const k when i = k  -> ()
  78    | Positive when i > 0 -> ()
  79    | Any                 -> ()
  80    | a                   -> raise (ArityError (p, a, i))
  81
  82 (* external functions implementation ****************************************)
  83
  84 let std o =
  85    {s_out = o.out; s_path = o.path o.out;
  86     s_query = o.query o.out ""; s_result = o.result o.out "\n"
  87    }
  88
  89 type t = End
  90        | Space
  91        | Figure of int
  92        | Error
  93
  94 let my_int_of_string s =
  95    let l = String.length s in
  96    let get_t i =
  97       if i = l then End else
  98       match s.[i] with
  99          | ' ' | '\t' | '\r' | 'n' -> Space
 100          | '0' .. '9'              -> Figure (Char.code s.[i] - Char.code '0')
 101          | _                       -> Error
 102    in
 103    let rec aux i xv = match get_t i, xv with
 104       | Error, _
 105       | End, None        -> raise (Failure "int_of_string")
 106       | End, Some v      -> v
 107       | Space, xv        -> aux (succ i) xv
 108       | Figure f, None   -> aux (succ i) (Some f)
 109       | Figure f, Some v -> aux (succ i) (Some (10 * v + f))
 110    in
 111    aux 0 None
 112
 113 let int_of_set r =
 114    try match r with
 115       | [s, _] -> my_int_of_string s
 116       | _      -> raise (Failure "int_of_string")
 117    with Failure "int_of_string" -> raise (NumberError r)
 118
 119 let out_txt2 o n x1 x2 =
 120    o.s_out "(" ; o.s_query x1; o.s_out (" " ^ n ^ " "); o.s_query x2; o.s_out ")"
 121
 122 let out_txt_ o p xl =
 123    if p <> [] then begin o.s_path p; o.s_out " " end;
 124    o.s_out "{"; P.flat_list o.s_out o.s_query ", " xl; o.s_out "}"
 125
 126 let out_txt_full o p pl xl =
 127    o.s_path p; o.s_out " {"; P.flat_list o.s_out o.s_path ", " pl; o.s_out "} {";
 128    P.flat_list o.s_out o.s_query ", " xl; o.s_out "}"
 129
 130 let arity0 n r =
 131    let arity_p = Const 0 in
 132    let arity_s = Const 0 in
 133    let body _ _ _ _ _ = r in
 134    let txt_out o _ _ = (std o).s_out n in
 135    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 136
 137 let arity1 n f =
 138    let arity_p = Const 0 in
 139    let arity_s = Const 1 in
 140    let body e _ _ _ = function
 141       | [x] -> f (e.eval x)
 142       | _   -> assert false
 143    in
 144    let txt_out o _ = function
 145       | [x] -> let o = std o in o.s_out (n ^ " "); o.s_query x
 146       | _   -> assert false
 147    in
 148    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 149
 150 let arity2 n f =
 151    let arity_p = Const 0 in
 152    let arity_s = Const 2 in
 153    let body e _ _ _ = function
 154       | [x1; x2] -> f (e.eval x1) (e.eval x2)
 155       | _        -> assert false
 156    in
 157    let txt_out o _ = function
 158       | [x1; x2] -> let o = std o in out_txt2 o n x1 x2
 159       | _        -> assert false
 160    in
 161    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 162
 163 let false_fun b =
 164    let s = if b then "false" else "empty" in
 165    arity0 s U.mql_false
 166
 167 let true_fun = arity0 "true" U.mql_true
 168
 169 let not_fun =
 170    let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
 171    arity1 "!" aux
 172
 173 let count_fun =
 174    let aux r = [string_of_int (List.length r), []] in
 175    arity1 "#" aux
 176
 177 let peek_fun =
 178    let aux = function [] -> [] | hd :: _ -> [hd] in
 179    arity1 "peek" aux
 180
 181 let diff_fun = arity2 "diff" U.mql_diff
 182
 183 let xor_fun = arity2 "xor" U.xor
 184
 185 let sub_fun = arity2 "sub" U.set_sub
 186
 187 let meet_fun = arity2 "meet" U.set_meet
 188
 189 let eq_fun = arity2 "==" U.set_eq
 190
 191 let le_fun =
 192    let le v1 v2 =
 193       if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false
 194    in
 195    arity2 "<=" le
 196
 197 let lt_fun =
 198    let lt v1 v2 =
 199       if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false
 200    in
 201    arity2 "<" lt
 202
 203 let stat_fun =
 204    let arity_p = Const 0 in
 205    let arity_s = Const 1 in
 206    let body e o _ _ = function
 207       | [x] ->
 208          let t = P.start_time () in
 209          let r = (e.eval x) in
 210          let s = P.stop_time t in
 211          o.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
 212          r
 213       | _   -> assert false
 214    in
 215    let txt_out o _ = function
 216       | [x] -> let o = std o in o.s_out "stat "; o.s_query x
 217       | _   -> assert false
 218    in
 219    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 220
 221 let log_fun xml src =
 222    let log_src e o x =
 223       let t = P.start_time () in o.s_query x;
 224       let s = P.stop_time t in
 225       if C.set e.conn C.Stat then o.s_out (Printf.sprintf "Log source: %s\n" s);
 226       e.eval x
 227    in
 228    let log_res e o x =
 229       let s = e.eval x in
 230       let t = P.start_time () in o.s_result s;
 231       let r = P.stop_time t in
 232       if C.set e.conn C.Stat then o.s_out (Printf.sprintf "Log: %s\n" r); s
 233    in
 234    let txt_log o =
 235       if xml then o.s_out "xml ";
 236       if src then o.s_out "source "
 237    in
 238    let arity_p = Const 0 in
 239    let arity_s = Const 1 in
 240    let body e o _ _ = function
 241       | [x] -> let o = std o in if src then log_src e o x else log_res e o x
 242       | _   -> assert false
 243    in
 244    let txt_out o _ = function
 245       | [x] -> let o = std o in o.s_out "log "; txt_log o; o.s_query x
 246       | _   -> assert false
 247    in
 248    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 249
 250 let render_fun =
 251    let arity_p = Const 0 in
 252    let arity_s = Const 1 in
 253    let body e o _ _ = function
 254       | [x] ->
 255          let rs = ref "" in
 256          let out s = rs := ! rs ^ s in
 257          o.result out " " (e.eval x);
 258          [! rs, []]
 259       | _   -> assert false
 260    in
 261    let txt_out o _ = function
 262       | [x] -> let o = std o in o.s_out "render "; o.s_query x
 263       | _   -> assert false
 264    in
 265    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 266
 267 let read_fun =
 268    let arity_p = Const 0 in
 269    let arity_s = Const 1 in
 270    let body e o i _ = function
 271       | [x] ->
 272          let aux av =
 273             let ich = open_in (fst av) in
 274             let r = i.result_in (Lexing.from_channel ich) in
 275             close_in ich; r
 276          in
 277          U.mql_iter aux (e.eval x)
 278       | _   -> assert false
 279    in
 280    let txt_out o _ = function
 281       | [x] -> let o = std o in o.s_out "read "; o.s_query x
 282       | _   -> assert false
 283    in
 284    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 285
 286 let align_fun =
 287    let aux l (v, g) =
 288       let c = String.length v in
 289       if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
 290    in
 291    let arity_p = Const 0 in
 292    let arity_s = Const 2 in
 293    let body e _ _ _ = function
 294       | [y; x] ->
 295          let l = int_of_set (e.eval y) in
 296          U.mql_iter (aux l) (e.eval x)
 297       | _      -> assert false
 298    in
 299    let txt_out o _ = function
 300       | [y; x] ->
 301          let o = std o in
 302          o.s_out "align "; o.s_query y; o.s_out " in "; o.s_query x
 303       | _      -> assert false
 304    in
 305    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 306
 307 let if_fun =
 308    let arity_p = Const 0 in
 309    let arity_s = Const 3 in
 310    let body e _ _ _ = function
 311       | [y; x1; x2] ->
 312          if (e.eval y) = U.mql_false then (e.eval x2) else (e.eval x1)
 313       | _           -> assert false
 314    in
 315    let txt_out o _ = function
 316       | [y; x1; x2] ->
 317          let o = std o in
 318          o.s_out "if "; o.s_query y; o.s_out " then "; o.s_query x1;
 319          o.s_out " else "; o.s_query x2
 320       | _           -> assert false
 321    in
 322    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 323
 324 let intersect_fun =
 325    let rec iter f = function
 326       | []           -> assert false
 327       | [head]       -> f head
 328       | head :: tail -> U.mql_intersect (f head) (iter f tail)
 329    in
 330    let arity_p = Const 0 in
 331    let arity_s = Positive in
 332    let body e _ _ _ xl = iter e.eval xl in
 333    let txt_out o _ = function
 334       | []           -> assert false
 335       | [x1; x2]     -> let o = std o in out_txt2 o "/\\" x1 x2
 336       | xl           -> let o = std o in out_txt_ o ["intersect"] xl
 337    in
 338    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 339
 340 let union_fun =
 341    let arity_p = Const 0 in
 342    let arity_s = Any in
 343    let body e _ _ _ xl = U.mql_iter e.eval xl in
 344    let txt_out o _ xl = let o = std o in out_txt_ o [] xl
 345    in
 346    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 347
 348 let or_fun =
 349    let rec iter f = function
 350       | []           -> U.mql_false
 351       | head :: tail ->
 352          let r1 = f head in
 353          if r1 = U.mql_false then (iter f tail) else r1
 354    in
 355    let arity_p = Const 0 in
 356    let arity_s = Any in
 357    let body e _ _ _ xl = iter e.eval xl in
 358    let txt_out o _ = function
 359       | [x1; x2]     -> let o = std o in out_txt2 o "||" x1 x2
 360       | xl           -> let o = std o in out_txt_ o ["or"] xl
 361    in
 362    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 363
 364 let and_fun =
 365    let rec iter f = function
 366       | []           -> U.mql_true
 367       | [head]       -> f head
 368       | head :: tail ->
 369          if f head = U.mql_false then U.mql_false else iter f tail
 370    in
 371    let arity_p = Const 0 in
 372    let arity_s = Any in
 373    let body e _ _ _ xl = iter e.eval xl in
 374    let txt_out o _ = function
 375       | [x1; x2]  -> let o = std o in out_txt2 o "&&" x1 x2
 376       | xl        -> let o = std o in out_txt_ o ["and"] xl
 377    in
 378    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 379
 380 let seq_fun =
 381    let rec iter f = function
 382       | []           -> U.mql_true
 383       | [head]       -> f head
 384       | head :: tail -> ignore (f head); iter f tail
 385    in
 386    let arity_p = Const 0 in
 387    let arity_s = Any in
 388    let body e _ _ _ xl = iter e.eval xl in
 389    let txt_out o _ = function
 390       | [x1; x2]  ->
 391          let o = std o in o.s_query x1; o.s_out " ;; "; o.s_query x2
 392       | xl        -> let o = std o in out_txt_ o ["seq"] xl
 393    in
 394    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 395
 396 let proj_fun =
 397    let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in
 398    let proj_group p a = U.mql_iter (proj_group_aux p) a in
 399    let proj_set p (_, g) = U.mql_iter (proj_group p) g in
 400    let arity_p = Const 1 in
 401    let arity_s = Const 1 in
 402    let body e _ _ pl xl =
 403       match pl, xl with
 404          | [p], [x] -> U.mql_iter (proj_set p) (e.eval x)
 405          | _        -> assert false
 406    in
 407    let txt_out o pl xl =
 408       match pl, xl with
 409          | [p], [x] ->
 410             let o = std o in
 411             o.s_out "proj "; o.s_path p; o.s_out " of "; o.s_query x
 412          | _        -> assert false
 413    in
 414    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 415
 416 let keep_fun b =
 417    let proj (r, _) = (r, []) in
 418    let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in
 419    let keep_grp l a = List.fold_right (keep_path l) a [] in
 420    let keep_set l a g =
 421       let kg = keep_grp l a in
 422       if kg = [] then g else kg :: g
 423    in
 424    let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
 425    let txt_allbut o = if b then o.s_out "allbut " in
 426    let txt_path_list o l = P.flat_list o.s_out o.s_path ", " l in
 427    let arity_p = Any in
 428    let arity_s = Const 1 in
 429    let body e _ _ pl xl =
 430       match b, pl, xl with
 431          | true, [], [x]  -> e.eval x
 432          | false, [], [x] -> List.map proj (e.eval x)
 433          | _, l, [x]      -> List.map (keep_av l) (e.eval x)
 434          | _              -> assert false
 435   in
 436   let txt_out o pl xl =
 437       match pl, xl with
 438          | [], [x] ->
 439             let o = std o in
 440             o.s_out "keep "; txt_allbut o; o.s_query x
 441          | l, [x]  ->
 442             let o = std o in
 443             o.s_out "keep "; txt_allbut o; txt_path_list o l;
 444             o.s_out " in "; o.s_query x
 445          | _      -> assert false
 446    in
 447    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 448
 449 (* external functions interface *********************************************)
 450
 451 let fun_get_spec = function
 452    | ["empty"]                 -> false_fun false
 453    | ["false"]                 -> false_fun true
 454    | ["true"]                  -> true_fun
 455    | ["not"]                   -> not_fun
 456    | ["count"]                 -> count_fun
 457    | ["stat"]                  -> stat_fun
 458    | ["log"; "text"; "result"] -> log_fun false false
 459    | ["log"; "text"; "source"] -> log_fun false true
 460    | ["render"]                -> render_fun
 461    | ["read"]                  -> read_fun
 462    | ["peek"]                  -> peek_fun
 463    | ["diff"]                  -> diff_fun
 464    | ["xor"]                   -> xor_fun
 465    | ["sub"]                   -> sub_fun
 466    | ["meet"]                  -> meet_fun
 467    | ["eq"]                    -> eq_fun
 468    | ["le"]                    -> le_fun
 469    | ["lt"]                    -> lt_fun
 470    | ["align"]                 -> align_fun
 471    | ["if"]                    -> if_fun
 472    | ["intersect"]             -> intersect_fun
 473    | ["union"]                 -> union_fun
 474    | ["or"]                    -> or_fun
 475    | ["and"]                   -> and_fun
 476    | ["seq"]                   -> seq_fun
 477    | ["proj"]                  -> proj_fun
 478    | ["keep"; "these"]         -> keep_fun false
 479    | ["keep"; "allbut"]        -> keep_fun true
 480    | p                         -> raise (NameError p)
 481
 482 let fun_arity p m n =
 483    check_arity p m (fun_get_spec p).arity_p;
 484    check_arity p n (fun_get_spec p).arity_s
 485
 486 let fun_eval e o i p pl xl = (fun_get_spec p).body e o i pl xl
 487
 488 let fun_txt_out o p pl xl =
 489    try (fun_get_spec p).txt_out o pl xl
 490    with NameError q when q = p -> out_txt_full (std o) p pl xl
 491
 492 (* generator functions implementation ***************************************)
 493
 494 let helm_vars_gen =
 495    let mk_let v s x = M.Let (v, M.Const [(s, [])], x) in
 496    let arity = Const 1 in
 497    let code _ = function
 498       | [x] -> mk_let "SET" "Set" x
 499       | _   -> assert false
 500    in
 501    {arity = arity; code = code}
 502
 503 (* generator functions interface ********************************************)
 504
 505 let gen_get_spec = function
 506    | ["helm"; "vars"] -> helm_vars_gen
 507    | p                -> raise (NameError p)
 508
 509 let gen_arity p n = check_arity p n (gen_get_spec p).arity
 510
 511 let gen_eval e p xl = (gen_get_spec p).code e xl