]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
a459fe82954e9eaa02ca09e9c3d07bac31712dad
[helm.git] / 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 M = MathQL
32 module P = MQueryUtil 
33 module C = MQIConn
34 module U = MQIUtil
35 module L = MQILib
36 module F = MQueryIO
37
38 (* contexts *****************************************************************)
39
40 type svar_context = (M.svar * M.resource_set) list
41
42 type avar_context = (M.avar * M.resource) list
43
44 type group_context = (M.avar * M.attribute_group) list
45
46 type context = {svars: svar_context;   
47                 avars: avar_context;   
48                 groups: group_context (* auxiliary context *)  
49                }
50                
51 (* execute ******************************************************************)
52
53 let execute h x =
54    let warn q = 
55      if C.set h C.Warn then 
56      begin
57         C.log h "MQIExecute: waring: reference to undefined variables: ";
58         F.text_of_query (C.log h) "\n" q
59      end
60    in
61    let proj v = List.map fst v in
62    let rec eval_query c = function
63       | M.Const r -> r
64       | M.Dot i p -> begin
65          try U.mql_subj (List.assoc p (List.assoc i c.groups)) 
66          with Not_found -> warn (M.Dot i p); [] end
67       | M.Ex l y -> 
68          let rec ex_aux h = function
69             | []        -> 
70                let d = {c with groups = h} in
71                if eval_query d y = U.mql_false then () else raise Found 
72             | i :: tail -> 
73                begin
74                   try 
75                      let (_, a) = List.assoc i c.avars in 
76                      let rec add_group = function
77                         | []     -> ()
78                         | g :: t -> ex_aux ((i, g) :: h) tail; add_group t 
79                      in
80                      add_group a
81                   with Not_found -> ()
82                end
83          in
84          (try ex_aux [] l; U.mql_false with Found -> U.mql_true)
85       | M.SVar i -> begin
86          try List.assoc i c.svars 
87          with Not_found -> warn (M.SVar i); [] end  
88       | M.AVar i -> begin
89          try [List.assoc i c.avars] 
90          with Not_found -> warn (M.AVar i); [] end
91       | M.Let i x1 x2 ->
92          let d = {c with svars = P.add_assoc (i, eval_query c x1) c.svars} in
93          eval_query d x2
94       | M.For k i x1 x2 ->
95          let f = match k with
96             | M.GenFJoin -> U.mql_union
97             | M.GenFMeet -> U.mql_intersect
98          in
99          let rec for_aux = function
100             | []     -> []
101             | h :: t ->
102                let d = {c with avars = P.add_assoc (i, h) c.avars} in
103                f (eval_query d x2) (for_aux t)
104          in
105          for_aux (eval_query c x1)
106       | M.Add b z x ->
107          let f = if b then U.mql_prod else U.set_union in
108          let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
109          List.fold_right g (eval_query c x) []
110       | M.Property q0 q1 q2 mc ct cfl el pat y ->
111          let subj, mct = 
112             if q0 then [], (pat, q2 @ mc, eval_query c y)
113                   else (q2 @ mc), (pat, [], eval_query c y)  
114          in
115          let eval_cons (pat, p, y) = (pat, q2 @ p, eval_query c y) in
116          let cons_true = mct :: List.map eval_cons ct in
117          let cons_false = List.map (List.map eval_cons) cfl in
118          let eval_exp (p, po) = (q2 @ p, po) in
119          let exp = List.map eval_exp el in
120          let t = P.start_time () in
121          let r = MQIProperty.exec h q1 subj cons_true cons_false exp in 
122          let s = P.stop_time t in
123          if C.set h C.Stat then 
124             C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
125          r 
126       | M.Select i x y ->
127          let rec select_aux = function
128             | []     -> []
129             | h :: t ->
130                let d = {c with avars = P.add_assoc (i, h) c.avars} in
131                if eval_query d y = U.mql_false 
132                   then select_aux t else h :: select_aux t
133          in
134          select_aux (eval_query c x)
135       | M.Fun p pl xl -> 
136          let e = {L.eval = eval_query c; L.conn = h} in
137          L.eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec 
138             p pl xl
139    and eval_grp c = function
140       | M.Attr gs ->
141          let attr_aux g (p, y) = U.mql_union g [p, proj (eval_query c y)] in
142          let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
143          List.fold_left attr_auxs [] gs
144       | M.From i ->
145          try snd (List.assoc i c.avars) 
146          with Not_found -> warn (M.AVar i); []
147    in
148    let c = {svars = []; avars = []; groups = []} in
149    let t = P.start_time () in
150    let r = eval_query c x in
151    let s = P.stop_time t in
152    if C.set h C.Stat then 
153       C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s 
154          (C.string_of_flags (C.flags h)));
155    r