]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
test branch
[helm.git] / helm / ocaml / mathql_interpreter / mQueryInterpreter.ml
diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
new file mode 100644 (file)
index 0000000..9280a2c
--- /dev/null
@@ -0,0 +1,247 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* $Id$ *)
+
+(* contexts *****************************************************************)
+
+type svar_context = (MathQL.svar * MathQL.resource_set) list
+
+type avar_context = (MathQL.avar * MathQL.resource) list
+
+type group_context = (MathQL.avar * MathQL.attribute_group) list
+
+type vvar_context = (MathQL.vvar * MathQL.value) list
+
+type context = {svars: svar_context;   
+                avars: avar_context;   
+                groups: group_context; (* auxiliary context *)
+                vvars: vvar_context  
+               }
+
+(* execute  *****************************************************************)
+
+exception Found
+
+module M = MathQL
+module P = MQueryUtil 
+module C = MQIConn
+module U = MQIUtil
+
+let execute h x =
+   let warn q = 
+     if C.set h C.Warn then 
+     begin
+        C.log h "MQIExecute: waring: reference to undefined variables: ";
+       P.text_of_query (C.log h) "\n" q
+     end
+   in
+   let rec eval_val c = function
+      | M.False -> U.mql_false
+      | M.True -> U.mql_true
+      | M.Const s -> [s]
+      | M.Set l -> U.iter (eval_val c) l
+      | M.Test (k,y1,y2) ->
+         let cand y1 y2 =
+           if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2
+        in
+        let cor y1 y2 =
+            let v1 = eval_val c y1 in
+           if v1 = U.mql_false then eval_val c y2 else v1
+        in
+        let h f y1 y2 = f (eval_val c y1) (eval_val c y2) in
+         let f = match k with
+           | M.And  -> cand
+           | M.Or   -> cor
+           | M.Xor  -> h U.xor
+           | M.Sub  -> h U.set_sub
+           | M.Meet -> h U.set_meet
+           | M.Eq   -> h U.set_eq
+           | M.Le   -> h U.le
+           | M.Lt   -> h U.lt
+        in
+         f y1 y2 
+      | M.Not y -> 
+         if eval_val c y = U.mql_false then U.mql_true else U.mql_false
+      | M.VVar i -> begin
+         try List.assoc i c.vvars 
+         with Not_found -> warn (M.Subj (M.VVar i)); [] end
+      | M.Dot (i,p) -> begin
+         try List.assoc p (List.assoc i c.groups) 
+        with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end
+      | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x)
+      | M.Proj ((Some p),x) -> 
+         let proj_group_aux (q, v) = if q = p then v else [] in 
+         let proj_group a = U.iter proj_group_aux a in
+         let proj_set (_, g) = U.iter proj_group g in
+         U.iter proj_set (eval_query c x)
+      | M.Ex (l,y) -> 
+         let rec ex_aux h = function
+           | []        -> 
+              let d = {c with groups = h} in
+               if eval_val d y = U.mql_false then () else raise Found 
+           | i :: tail -> 
+               begin
+                 try 
+                    let (_, a) = List.assoc i c.avars in 
+                    let rec add_group = function
+                       | []     -> ()
+                       | g :: t -> ex_aux ((i, g) :: h) tail; add_group t 
+                    in
+                    add_group a
+                 with Not_found -> ()
+              end
+         in
+        (try ex_aux [] l; U.mql_false with Found -> U.mql_true)
+      | M.StatVal y ->
+         let t = P.start_time () in
+        let r = (eval_val c y) in
+        let s = P.stop_time t in
+         C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+        r
+      | M.Count y -> [string_of_int (List.length (eval_val c y))]
+      | M.Align (s,y) -> U.iter (U.align s) (eval_val c y)
+   and eval_query c = function
+      | M.Empty -> [] 
+      | M.Subj x ->
+         List.map (fun s -> (s, [])) (eval_val c x)
+      | M.Log (_,b,x) ->
+         if b then begin
+           let t = P.start_time () in
+           P.text_of_query (C.log h) "\n" x;
+           let s = P.stop_time t in
+           if C.set h C.Times then 
+              C.log h (Printf.sprintf "Log source: %s\n" s);
+           eval_query c x
+        end else begin
+            let s = (eval_query c x) in
+           let t = P.start_time () in
+           P.text_of_result (C.log h) "\n" s; 
+           let r = P.stop_time t in
+           if C.set h C.Times then 
+              C.log h (Printf.sprintf "Log: %s\n" r);
+           s
+        end
+      | M.If (y,x1,x2) ->
+         if (eval_val c y) = U.mql_false 
+           then (eval_query c x2) else (eval_query c x1)
+      | M.Bin (k,x1,x2) ->
+         let f = match k with
+           | M.BinFJoin -> U.mql_union
+           | M.BinFMeet -> U.mql_intersect
+           | M.BinFDiff -> U.mql_diff
+        in
+        f (eval_query c x1) (eval_query c x2) 
+      | M.SVar i -> begin
+         try List.assoc i c.svars 
+        with Not_found -> warn (M.SVar i); [] end  
+      | M.AVar i -> begin
+         try [List.assoc i c.avars] 
+        with Not_found -> warn (M.AVar i); [] end
+      | M.LetSVar (i,x1,x2) ->
+        let d = {c with svars = U.set (i, eval_query c x1) c.svars} in
+         eval_query d x2
+      | M.LetVVar (i,y,x) ->
+        let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in
+         eval_query d x
+      | M.For (k,i,x1,x2) ->
+         let f = match k with
+           | M.GenFJoin -> U.mql_union
+           | M.GenFMeet -> U.mql_intersect
+        in
+         let rec for_aux = function
+           | []     -> []
+           | h :: t ->
+              let d = {c with avars = U.set (i, h) c.avars} in
+              f (eval_query d x2) (for_aux t)
+        in
+        for_aux (eval_query c x1)
+      | M.Add (b,z,x) ->
+         let f = if b then U.mql_prod else U.set_union in
+        let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
+        List.fold_right g (eval_query c x) []
+      | M.Property (q0,q1,q2,mc,ct,cfl,el,pat,y) ->
+        let subj, mct = 
+           if q0 then [], (pat, q2 @ mc, eval_val c y)
+                 else (q2 @ mc), (pat, [], eval_val c y)  
+        in
+         let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in
+        let cons_true = mct :: List.map eval_cons ct in
+        let cons_false = List.map (List.map eval_cons) cfl in
+        let eval_exp (p, po) = (q2 @ p, po) in
+        let exp = List.map eval_exp el in
+        let t = P.start_time () in
+        let r = MQIProperty.exec h q1 subj cons_true cons_false exp in 
+        let s = P.stop_time t in
+         if C.set h C.Times then 
+           C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
+        r 
+      | M.StatQuery x ->
+         let t = P.start_time () in
+        let r = (eval_query c x) in
+        let s = P.stop_time t in
+         C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+        r
+      | M.Select (i,x,y) ->
+         let rec select_aux = function
+           | []     -> []
+           | h :: t ->
+              let d = {c with avars = U.set (i, h) c.avars} in
+              if eval_val d y = U.mql_false 
+                 then select_aux t else h :: select_aux t
+        in
+        select_aux (eval_query c x)
+      | M.Keep (b,l,x) -> 
+         let keep_path (p, v) t = 
+           if List.mem p l = b then t else (p, v) :: t in
+        let keep_grp a = List.fold_right keep_path a [] in
+         let keep_set a g = 
+           let kg = keep_grp a in
+           if kg = [] then g else kg :: g
+        in
+        let keep_av (s, g) = (s, List.fold_right keep_set g []) in
+        List.map keep_av (eval_query c x) 
+   and eval_grp c = function
+      | M.Attr gs ->
+         let attr_aux g (p, y) = U.mql_union g [(p, eval_val c y)] in
+        let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
+        List.fold_left attr_auxs [] gs
+      | M.From i ->
+         try snd (List.assoc i c.avars) 
+        with Not_found -> warn (M.AVar i); []
+   in
+   let c = {svars = []; avars = []; groups = []; vvars = []} in
+   let t = P.start_time () in   
+   if C.set h C.Source then P.text_of_query (C.log h) "\n" x;
+   let r = eval_query c x in
+   if C.set h C.Result then P.text_of_result (C.log h) "\n" r;
+   let s = P.stop_time t in
+   if C.set h C.Times then 
+      C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s 
+         (C.string_of_flags (C.flags h)));
+   r