helm/ocaml/mathql_interpreter/mQueryStandard.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 U = AvsUtil
  30 module M = MathQL
  31 module I = M.I
  32 module P = MQueryUtil
  33 module C = MQIConn
  34 module L = MQILib
  35
  36 let init = ()
  37
  38 let test f v1 v2 = U.avs_of_bool (f v1 v2)
  39
  40 let num_test f v1 v2 = U.avs_of_bool (f (U.int_of_avs v1) (U.int_of_avs v2))
  41
  42 (* FALSE / EMPTY ************************************************************)
  43
  44 let false_fun b =
  45    let s = if b then "false" else "empty" in
  46    L.fun_arity0 [] s U.val_false
  47
  48 let _ = L.fun_register ["empty"] (false_fun false)
  49
  50 let _ = L.fun_register ["false"] (false_fun true)
  51
  52 (* TRUE *********************************************************************)
  53
  54 let true_fun = L.fun_arity0 [] "true" U.val_true
  55
  56 let _ = L.fun_register ["true"] true_fun
  57
  58 (* NOT **********************************************************************)
  59
  60 let not_fun =
  61    let aux r = if r = U.val_false then U.val_true else U.val_false in
  62    L.fun_arity1 [] "!" aux
  63
  64 let _ = L.fun_register ["not"] not_fun
  65
  66 (* COUNT ********************************************************************)
  67
  68 let count_fun =
  69    let aux r = U.avs_of_int (U.count r) in
  70    L.fun_arity1 [] "#" aux
  71
  72 let _ = L.fun_register ["count"] count_fun
  73
  74 (* PEEK *********************************************************************)
  75
  76 let peek_fun =
  77    let aux r =
  78       match (I.peek r) with
  79          | I.Empty
  80          | I.Single _     -> r
  81          | I.Many (s, gl) -> U.make_x s gl
  82    in
  83    L.fun_arity1 [] "peek" aux
  84
  85 let _ = L.fun_register ["peek"] peek_fun
  86
  87 (* DIFF *********************************************************************)
  88
  89 let diff_fun = L.fun_arity2 [] "diff" I.diff
  90
  91 let _ = L.fun_register ["diff"] diff_fun
  92
  93 (* XOR **********************************************************************)
  94
  95 let xor_fun =
  96    let aux v1 v2 =
  97       let b = v1 <> U.val_false in
  98       if b && v2 <> U.val_false then U.val_false else
  99       if b then v1 else v2
 100    in
 101    L.fun_arity2 [] "xor" aux
 102
 103 let _ = L.fun_register ["xor"] xor_fun
 104
 105 (* SUB **********************************************************************)
 106
 107 let sub_fun = L.fun_arity2 [] "sub" (test I.sub)
 108
 109 let _ = L.fun_register ["sub"] sub_fun
 110
 111 (* MEET *********************************************************************)
 112
 113 let meet_fun = L.fun_arity2 [] "meet" (test I.meet)
 114
 115 let _ = L.fun_register ["meet"] meet_fun
 116
 117 (* EQ ***********************************************************************)
 118
 119 let eq_fun = L.fun_arity2 [] "==" (test I.eq)
 120
 121 let _ = L.fun_register ["eq"] eq_fun
 122
 123 (* LE ***********************************************************************)
 124
 125 let le_fun = L.fun_arity2 [] "<=" (num_test (<=))
 126
 127 let _ = L.fun_register ["le"] le_fun
 128
 129 (* LT ***********************************************************************)
 130
 131 let lt_fun = L.fun_arity2 [] "<" (num_test (<))
 132
 133 let _ = L.fun_register ["lt"] lt_fun
 134
 135 (* STAT *********************************************************************)
 136
 137 let stat_fun =
 138    let arity_p = L.Const 0 in
 139    let arity_s = L.Const 1 in
 140    let body e o _ _ = function
 141       | [x] ->
 142          let t = P.start_time () in
 143          let r = (e.L.eval x) in
 144          let s = P.stop_time t in
 145          o.L.out (Printf.sprintf "Stat: %s,%i\n" s (U.count r));
 146          r
 147       | _   -> assert false
 148    in
 149    let txt_out o _ = function
 150       | [x] -> let o = L.std o in o.L.s_out "stat "; o.L.s_query x
 151       | _   -> assert false
 152    in
 153    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 154
 155 let _ = L.fun_register ["stat"] stat_fun
 156
 157 (* LOG **********************************************************************)
 158
 159 let log_fun xml src =
 160    let log_src e o x =
 161       let t = P.start_time () in o.L.s_query x;
 162       let s = P.stop_time t in
 163       if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log source: %s\n" s);
 164       e.L.eval x
 165    in
 166    let log_res e o x =
 167       let s = e.L.eval x in
 168       let t = P.start_time () in o.L.s_result s;
 169       let r = P.stop_time t in
 170       if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log: %s\n" r); s
 171    in
 172    let txt_log o =
 173       if xml then o.L.s_out "xml ";
 174       if src then o.L.s_out "source "
 175    in
 176    let arity_p = L.Const 0 in
 177    let arity_s = L.Const 1 in
 178    let body e o _ _ = function
 179       | [x] -> let o = L.std o in if src then log_src e o x else log_res e o x
 180       | _   -> assert false
 181    in
 182    let txt_out o _ = function
 183       | [x] -> let o = L.std o in o.L.s_out "log "; txt_log o; o.L.s_query x
 184       | _   -> assert false
 185    in
 186    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 187
 188 let _ = L.fun_register ["log"; "text"; "result"] (log_fun false false)
 189
 190 let _ = L.fun_register ["log"; "text"; "source"] (log_fun false true)
 191
 192 (* RENDER *******************************************************************)
 193
 194 let render_fun =
 195    let arity_p = L.Const 0 in
 196    let arity_s = L.Const 1 in
 197    let body e o _ _ = function
 198       | [x] ->
 199          let rs = ref "" in
 200          let out s = rs := ! rs ^ s in
 201          o.L.result out " " (e.L.eval x);
 202          I.make ! rs I.grp_empty
 203       | _   -> assert false
 204    in
 205    let txt_out o _ = function
 206       | [x] -> let o = L.std o in o.L.s_out "render "; o.L.s_query x
 207       | _   -> assert false
 208    in
 209    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 210
 211 let _ = L.fun_register ["render"] render_fun
 212
 213 (* READ *********************************************************************)
 214
 215 let read_fun =
 216    let arity_p = L.Const 0 in
 217    let arity_s = L.Const 1 in
 218    let body e o i _ = function
 219       | [x] ->
 220          let aux avs s _ =
 221             let ich = open_in s in
 222             let r = i.L.result_in (Lexing.from_channel ich) in
 223             close_in ich; I.union avs r
 224          in
 225          I.iter aux I.empty (e.L.eval x)
 226       | _   -> assert false
 227    in
 228    let txt_out o _ = function
 229       | [x] -> let o = L.std o in o.L.s_out "read "; o.L.s_query x
 230       | _   -> assert false
 231    in
 232    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 233
 234 let _ = L.fun_register ["read"] read_fun
 235
 236 (* ALIGN ********************************************************************)
 237
 238 let align_fun =
 239    let aux2 l v =
 240       let c = String.length v in
 241       if c < l then String.make (l - c) ' ' ^ v else v
 242    in
 243    let aux l r s gl _ = I.append r (U.make_x (aux2 l s) gl) in
 244    let arity_p = L.Const 0 in
 245    let arity_s = L.Const 2 in
 246    let body e _ _ _ = function
 247       | [y; x] ->
 248          let l = U.int_of_avs (e.L.eval y) in
 249          I.x_iter (aux l) I.empty (e.L.eval x)
 250       | _      -> assert false
 251    in
 252    let txt_out o _ = function
 253       | [y; x] ->
 254          let o = L.std o in
 255          o.L.s_out "align "; o.L.s_query y; o.L.s_out " in "; o.L.s_query x
 256       | _      -> assert false
 257    in
 258    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 259
 260 let _ = L.fun_register ["align"] align_fun
 261
 262 (* IF ***********************************************************************)
 263
 264 let if_fun =
 265    let arity_p = L.Const 0 in
 266    let arity_s = L.Const 3 in
 267    let body e _ _ _ = function
 268       | [y; x1; x2] ->
 269          if U.bool_of_avs (e.L.eval y) then (e.L.eval x1) else (e.L.eval x2)
 270       | _           -> assert false
 271    in
 272    let txt_out o _ = function
 273       | [y; x1; x2] ->
 274          let o = L.std o in
 275          o.L.s_out "if "; o.L.s_query y; o.L.s_out " then "; o.L.s_query x1;
 276          o.L.s_out " else "; o.L.s_query x2
 277       | _           -> assert false
 278    in
 279    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 280
 281 let _ = L.fun_register["if"] if_fun
 282
 283 (* INTERSECT ****************************************************************)
 284
 285 let intersect_fun =
 286    let rec iter f = function
 287       | []           -> assert false
 288       | [head]       -> f head
 289       | head :: tail -> I.intersect (f head) (iter f tail)
 290    in
 291    let arity_p = L.Const 0 in
 292    let arity_s = L.Positive in
 293    let body e _ _ _ xl = iter e.L.eval xl in
 294    let txt_out o _ = function
 295       | []           -> assert false
 296       | [x1; x2]     -> let o = L.std o in L.out_txt2 o "/\\" x1 x2
 297       | xl           -> let o = L.std o in L.out_txt_ o ["intersect"] xl
 298    in
 299    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 300
 301 let _ = L.fun_register ["intersect"] intersect_fun
 302
 303 (* UNION ********************************************************************)
 304
 305 let union_fun =
 306    let arity_p = L.Const 0 in
 307    let arity_s = L.Any in
 308    let body e _ _ _ xl = U.iter e.L.eval xl in
 309    let txt_out o _ xl = let o = L.std o in L.out_txt_ o [] xl
 310    in
 311    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 312
 313 let _ = L.fun_register ["union"] union_fun
 314
 315 (* OR ***********************************************************************)
 316
 317 let or_fun =
 318    let rec iter f = function
 319       | []           -> U.val_false
 320       | head :: tail ->
 321          let r1 = f head in
 322          if U.bool_of_avs r1 then r1 else (iter f tail)
 323    in
 324    let arity_p = L.Const 0 in
 325    let arity_s = L.Any in
 326    let body e _ _ _ xl = iter e.L.eval xl in
 327    let txt_out o _ = function
 328       | [x1; x2]     -> let o = L.std o in L.out_txt2 o "||" x1 x2
 329       | xl           -> let o = L.std o in L.out_txt_ o ["or"] xl
 330    in
 331    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 332
 333 let _ = L.fun_register ["or"] or_fun
 334
 335 (* AND **********************************************************************)
 336
 337 let and_fun =
 338    let rec iter f = function
 339       | []           -> U.val_true
 340       | [head]       -> f head
 341       | head :: tail ->
 342          if U.bool_of_avs (f head) then iter f tail else U.val_false
 343    in
 344    let arity_p = L.Const 0 in
 345    let arity_s = L.Any in
 346    let body e _ _ _ xl = iter e.L.eval xl in
 347    let txt_out o _ = function
 348       | [x1; x2]  -> let o = L.std o in L.out_txt2 o "&&" x1 x2
 349       | xl        -> let o = L.std o in L.out_txt_ o ["and"] xl
 350    in
 351    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 352
 353 let _ = L.fun_register ["and"] and_fun
 354
 355 (* PROJ *********************************************************************)
 356
 357 let proj_fun =
 358    let aux2 p a q v _ = if p = q then I.union a (U.subj v) else a in
 359    let aux p a _ gl _ =
 360       I.union a (U.iter (I.x_grp_iter (aux2 p) I.empty) gl)
 361    in
 362    let arity_p = L.Const 1 in
 363    let arity_s = L.Const 1 in
 364    let body e _ _ pl xl =
 365       match pl, xl with
 366          | [p], [x] -> I.x_iter (aux p) I.empty (e.L.eval x)
 367          | _        -> assert false
 368    in
 369    let txt_out o pl xl =
 370       match pl, xl with
 371          | [p], [x] ->
 372             let o = L.std o in
 373             o.L.s_out "proj "; o.L.s_path p; o.L.s_out " of "; o.L.s_query x
 374          | _        -> assert false
 375    in
 376    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 377
 378 let _ = L.fun_register ["proj"] proj_fun
 379
 380 (* KEEP *********************************************************************)
 381
 382 let keep_fun b =
 383    let aux2 s l a q v _ =
 384       if List.mem q l = b then a else I.union a (I.make s (U.grp_make_x q v))
 385    in
 386    let aux l a s gl _ =
 387       I.append a (
 388          if l = [] then I.make s I.grp_empty else
 389          U.iter (I.x_grp_iter (aux2 s l) I.empty) gl)
 390    in
 391    let txt_allbut o = if b then o.L.s_out "allbut " in
 392    let txt_path_list o l = P.flat_list o.L.s_out o.L.s_path ", " l in
 393    let arity_p = L.Any in
 394    let arity_s = L.Const 1 in
 395    let body e _ _ pl xl =
 396       match b, pl, xl with
 397          | true, [], [x]  -> e.L.eval x
 398          | _, l, [x]      -> I.x_iter (aux l) I.empty (e.L.eval x)
 399          | _              -> assert false
 400   in
 401   let txt_out o pl xl =
 402       match pl, xl with
 403          | [], [x] ->
 404             let o = L.std o in
 405             o.L.s_out "keep "; txt_allbut o; o.L.s_query x
 406          | l, [x]  ->
 407             let o = L.std o in
 408             o.L.s_out "keep "; txt_allbut o; txt_path_list o l;
 409             o.L.s_out " in "; o.L.s_query x
 410          | _      -> assert false
 411    in
 412    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
 413
 414 let _ = L.fun_register ["keep"; "these"] (keep_fun false)
 415
 416 let _ = L.fun_register ["keep"; "allbut"] (keep_fun true)