]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
standard library and while construction inserted
[helm.git] / helm / ocaml / mathql_interpreter / mQueryInterpreter.ml
index 58fb7b87e734545491f893046333a50a85265bf0..b66228581c9a66ab56a6c47e08c51782cd836d0a 100644 (file)
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
-(* contexts *****************************************************************)
+exception Found
 
-type svar_context = (MathQL.svar * MathQL.resource_set) list
+module M = MathQL
+module P = MQueryUtil 
+module C = MQIConn
+module U = MQIUtil
+module L = MQILib
+module F = MQueryIO
+
+(* contexts *****************************************************************)
 
-type avar_context = (MathQL.avar * MathQL.resource) list
+type svar_context = (M.svar * M.resource_set) list
 
-type group_context = (MathQL.avar * MathQL.attribute_group) list
+type avar_context = (M.avar * M.resource) list
 
-type vvar_context = (MathQL.vvar * MathQL.value) list
+type group_context = (M.avar * M.attribute_group) list
 
 type context = {svars: svar_context;   
                 avars: avar_context;   
-                groups: group_context; (* auxiliary context *)
-                vvars: vvar_context  
+                groups: group_context (* auxiliary context *)  
                }
-
-(* execute  *****************************************************************)
-
-exception Found
-
-module M = MathQL
-module P = MQueryUtil 
-module C = MQIConn
-module U = MQIUtil
+              
+(* execute ******************************************************************)
 
 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) q "\n"
+       F.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)
+   let proj v = List.map fst v in
+   let rec eval_query c = function
+      | M.Const r -> c, r
+      | M.Dot i p -> 
+         begin
+            try c, U.mql_subj (List.assoc p (List.assoc i c.groups)) 
+           with Not_found -> warn (M.Dot i p); c, [] 
+        end
       | 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 
+               if snd (eval_query d y) = U.mql_false then () else raise Found 
            | i :: tail -> 
                begin
                  try 
@@ -115,80 +83,62 @@ let execute h x =
                  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) x "\n";
-           let s = P.stop_time t in
-           if C.set h C.Stat 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) s "\n"; 
-           let r = P.stop_time t in
-           if C.set h C.Stat then 
-              C.log h (Printf.sprintf "Log: %s\n" r);
-           s
+        begin try ex_aux [] l; c, U.mql_false with Found -> c, U.mql_true end
+      | M.SVar i -> 
+         begin
+            try c, List.assoc i c.svars 
+           with Not_found -> warn (M.SVar i); c, []
+        end  
+      | M.AVar i -> 
+         begin
+            try c, [List.assoc i c.avars] 
+           with Not_found -> warn (M.AVar i); c, []
         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
+      | M.Let (Some i) x1 x2 ->
+        let d, r = eval_query c x1 in
+        let d = {d with svars = P.add_assoc (i, r) d.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.Let None x1 x2 ->
+        let d, r = eval_query c x1 in eval_query d x2
       | 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
-           | []     -> []
+         let rec for_aux (d, r) = match r with
+           | []     -> d, []
            | h :: t ->
-              let d = {c with avars = U.set (i, h) c.avars} in
-              f (eval_query d x2) (for_aux t)
+              let d = {d with avars = P.add_assoc (i, h) d.avars} in
+              let d, r = eval_query d x2 in
+              let d, s = for_aux (d, t) in
+              d, f r s
         in
         for_aux (eval_query c x1)
+      | M.While k x1 x2 ->
+         let f = match k with
+           | M.GenFJoin -> U.mql_union
+           | M.GenFMeet -> U.mql_intersect
+        in
+         let rec while_aux (d, r) = 
+           let d, b = eval_query d x1 in
+           if b = U.mql_false then d, r else 
+           let d, s = eval_query d x2 in
+           while_aux (d, f r s)
+        in
+        while_aux (c, U.mql_false)
       | 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) []
+        let _, r = eval_query c x in
+        c, List.fold_right g r []
       | M.Property q0 q1 q2 mc ct cfl el pat y ->
+        let _, r = eval_query c y in
         let subj, mct = 
-           if q0 then [], (pat, q2 @ mc, eval_val c y)
-                 else (q2 @ mc), (pat, [], eval_val c y)  
+           if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)  
+        in
+         let eval_cons (pat, p, y) = 
+           let _, r = eval_query c y in (pat, q2 @ p, r)
         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
@@ -198,44 +148,39 @@ let execute h x =
         let s = P.stop_time t in
          if C.set h C.Stat 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
+        c, r 
       | M.Select i x y ->
-         let rec select_aux = function
-           | []     -> []
+         let rec select_aux (d, r) = match r with
+           | []     -> d, []
            | 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
+              let d = {d with avars = P.add_assoc (i, h) d.avars} in
+              let d, r = eval_query d y in
+              let d, s = select_aux (d, t) in
+              if r = U.mql_false then d, s else d, (h :: s)
         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) 
+      | M.Fun p pl xl ->        
+        let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
+         c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec 
+            p pl xl
+      | M.Gen p xl -> 
+         let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
+        eval_query c (L.gen_eval e p xl)
    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_aux g (p, y) = 
+           let _, r = eval_query c y in
+           U.mql_union g [p, proj r]
+        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 c = {svars = []; avars = []; groups = []} in
    let t = P.start_time () in
-   let r = eval_query c x in
+   let _, r = eval_query c x in
    let s = P.stop_time t in
    if C.set h C.Stat then 
       C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s