helm/ocaml/mathql_interpreter/mQueryInterpreter.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 exception Found
  30
  31 module U = AvsUtil
  32 module M = MathQL
  33 module I = M.I
  34 module P = MQueryUtil
  35 module C = MQIConn
  36 module L = MQILib
  37 module F = MQueryIO
  38
  39 (* contexts *****************************************************************)
  40
  41 type svar_context = (M.svar * M.result) list
  42
  43 type avar_context = (M.avar * (string * M.group list)) list
  44
  45 type group_context = (M.avar * M.group) list
  46
  47 type context = {svars: svar_context;
  48                 avars: avar_context;
  49                 groups: group_context (* auxiliary context *)
  50                }
  51
  52 (* execute ******************************************************************)
  53
  54 let execute h x =
  55    let warn q =
  56      if C.set h C.Warn then
  57      begin
  58         C.log h "MQIExecute: waring: reference to undefined variables: ";
  59         F.text_of_query (C.log h) "\n" q
  60      end
  61    in
  62    let rec eval_query c = function
  63       | M.Const r ->
  64          let aux2 s g = I.make s (eval_list c g) in
  65          let aux (s, gl) =
  66             if gl = [] then U.avs_of_string s else U.iter (aux2 s) gl
  67          in
  68          c, U.iter aux r
  69       | M.Dot (i, p) ->
  70          begin
  71             try c, I.grp_read (List.assoc i c.groups) p
  72             with Not_found -> warn (M.Dot (i, p)); c, I.empty
  73          end
  74       | M.Ex (l, y) ->
  75          let rec ex_aux h = function
  76             | []        ->
  77                let d = {c with groups = h} in
  78                if snd (eval_query d y) = U.val_false then () else raise Found
  79             | i :: tail ->
  80                begin
  81                   try
  82                      let (_, a) = List.assoc i c.avars in
  83                      let rec add_group = function
  84                         | []     -> ()
  85                         | g :: t -> ex_aux ((i, g) :: h) tail; add_group t
  86                      in
  87                      add_group a
  88                   with Not_found -> ()
  89                end
  90          in
  91          begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end
  92       | M.SVar i ->
  93          begin
  94             try c, List.assoc i c.svars
  95             with Not_found -> warn (M.SVar i); c, I.empty
  96          end
  97       | M.AVar i ->
  98          begin
  99             try
 100                let s, gl = List.assoc i c.avars in
 101                c, U.make_x s gl
 102             with Not_found -> warn (M.AVar i); c, I.empty
 103          end
 104       | M.Let (Some i, x1, x2) ->
 105          let d, r = eval_query c x1 in
 106          let d = {d with svars = P.add_assoc (i, r) d.svars} in
 107          eval_query d x2
 108       | M.Let (None, x1, x2) ->
 109          let d, r = eval_query c x1 in eval_query d x2
 110       | M.For (k, i, x1, x2) ->
 111          let f = match k with
 112             | M.GenFJoin -> I.union
 113             | M.GenFMeet -> I.intersect
 114          in
 115          let for_aux (d, r) s gl _ =
 116             let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in
 117             let d, s = eval_query d x2 in
 118             d, f r s
 119          in
 120          let d, r = eval_query c x1 in
 121          I.x_iter for_aux (d, I.empty) (I.optimize r)
 122       | M.While (k, x1, x2) ->
 123          let f = match k with
 124             | M.GenFJoin -> I.union
 125             | M.GenFMeet -> I.intersect
 126          in
 127          let rec while_aux (d, r) =
 128             let d, b = eval_query d x1 in
 129             if b = U.val_false then d, r else
 130             let d, s = eval_query d x2 in
 131             while_aux (d, f r s)
 132          in
 133          while_aux (c, U.val_false)
 134       | M.Add (b, z, x) ->
 135          let f = if b then I.d_union else I.union in
 136          let agl = eval_grp c z in
 137          let aux r sj gl _ =
 138             I.union r (f (U.make_x sj gl) (U.make_x sj agl))
 139          in
 140          let _, r = eval_query c x in
 141          c, I.x_iter aux I.empty (I.optimize r)
 142       | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) ->
 143          let _, r = eval_query c y in
 144          let subj, mct =
 145             if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)
 146          in
 147          let eval_cons (pat, p, y) =
 148             let _, r = eval_query c y in (pat, q2 @ p, r)
 149          in
 150          let cons_true = mct :: List.map eval_cons ct in
 151          let cons_false = List.map (List.map eval_cons) cfl in
 152          let eval_exp (p, po) = (q2 @ p, po) in
 153          let exp = List.map eval_exp el in
 154          let t = P.start_time () in
 155          let r = MQIProperty.exec h q1 subj cons_true cons_false exp in
 156          let s = P.stop_time t in
 157          if C.set h C.Stat then
 158             C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r));
 159          c, r
 160       | M.Select (i, x, y) ->
 161          let aux (d, r) sj gl _ =
 162             let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in
 163             let d, s = eval_query d y in
 164             if s = U.val_false then d, r else d, (I.union r (U.make_x sj gl))
 165          in
 166          let d, r = eval_query c x in
 167          I.x_iter aux (d, I.empty) (I.optimize r)
 168       | M.Fun (p, pl, xl) ->
 169          let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
 170          c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec
 171             p pl xl
 172       | M.Gen (p, xl) ->
 173          let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
 174          eval_query c (L.gen_eval e p xl)
 175    and eval_list c l =
 176       let aux (p, y) =
 177          let _, r = eval_query c y in
 178          U.x_grp_make_x p r
 179       in
 180       U.grp_iter aux l
 181    and eval_grp c = function
 182       | M.Attr gs ->
 183          let attr_auxs s l = I.grps_make s (eval_list c l) in
 184          List.fold_left attr_auxs [] gs
 185       | M.From i ->
 186          try snd (List.assoc i c.avars)
 187          with Not_found -> warn (M.AVar i); []
 188    in
 189    let c = {svars = []; avars = []; groups = []} in
 190    let t = P.start_time () in
 191    let _, r = eval_query c x in
 192    let s = P.stop_time t in
 193    if C.set h C.Stat then
 194       C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s
 195          (C.string_of_flags (C.flags h)));
 196    r