]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mqint.ml
After Union and Relation
[helm.git] / helm / ocaml / mathql_interpreter / mqint.ml
index a0c56e3848835e0cc8a65212d8227ae87e28008c..95d3c8f2e47f9b5aa37e17e000a87b49ab508630 100644 (file)
@@ -34,11 +34,15 @@ open MathQL;;
 open Eval;;
 open Utility;;
 open Dbconn;;
-open Pattern;;
-open Union;;*)
+open Pattern;;*)
+open Union;;
 open Intersect;;
-(*open Diff;;
-open Sortedby;;
+open Meet;;
+open Sub;;
+open Context;;
+open Diff;;
+open Relation;;
+(*open Sortedby;;
 open Use;;
 open Select;;
 open Letin;;
@@ -257,51 +261,83 @@ let init () = () (* FG: implementare l'apertura del database *)
 let close () = () (* FG: implementare la chiusura del database *)
 
 
-(* contexts *****************************************************************)
 
-type svar_context = (MathQL.svar * MathQL.resource_set) list
-
-type rvar_context = (MathQL.rvar * MathQL.resource) list
-
-type group_context = (MathQL.rvar * MathQL.attribute_group) list
-
-type vvar_context = (MathQL.vvar * MathQL.value) list
-
-
-let svars = ref [] (* contesto delle svar *)
-
-let rvars = ref [] (* contesto delle rvar *)
-
-let groups = ref [] (* contesto dei gruppi *)
-
-let vvars = ref [] (* contesto delle vvar introdotte con let-in *)
+exception BooleExpTrue
 
+(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *)
 
-let rec exec_set_exp = function 
-   | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp vexp)
-   | MathQL.Intersect sexp1 sexp2 -> intersect_ex (exec_set_exp sexp1) (exec_set_exp sexp2)    
+let rec exec_set_exp c = function
+   |MathQL.SVar svar -> List.assoc svar c.svars
+   |MathQL.RVar rvar -> [List.assoc rvar c.rvars]  
+   | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp)
+   | MathQL.Intersect (sexp1, sexp2) -> intersect_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)    
+   | MathQL.Union (sexp1, sexp2) -> union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)
+   | MathQL.LetSVar (svar, sexp1, sexp2) -> let _ = (svar, (exec_set_exp c sexp1)):: (List.remove_assoc svar c.svars) 
+                                       in (exec_set_exp c sexp2)
+   | MathQL.LetVVar (vvar, vexp, sexp) -> let _ = (vvar, (exec_val_exp c vexp)):: (List.remove_assoc vvar c.vvars)
+                                       in (exec_set_exp c sexp)
+   | MathQL.Relation (rop, path, sexp, attl) -> relation_ex rop path (exec_set_exp c sexp) attl
+   | MathQL.Select (rvar, sexp, bexp) -> let rset = (exec_set_exp c sexp) in
+                                          let rec select_ex rset =
+                                           match rset with 
+                                                     [] -> []
+                                           | r::tl -> upd_rvars c ((rvar,r)::c.rvars);                     
+                                              if (exec_boole_exp c bexp) then r::(select_ex tl)
+                                              else select_ex tl
+                                          in select_ex rset
+                                                      
+                                                                                  
+   
+   | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)
    | _ -> assert false
    
 (* valuta una MathQL.boole_exp e ritorna un boole *)
 
-and exec_boole_exp = function
+and exec_boole_exp = function
    | MathQL.False      -> false
    | MathQL.True       -> true
-   | MathQL.Not x      -> not (exec_boole_exp x)
-   | MathQL.And (x, y) -> (exec_boole_exp x) && (exec_boole_exp y)
-   | MathQL.Or (x, y)  -> (exec_boole_exp x) || (exec_boole_exp y)   
-   | _ -> assert false
+   | MathQL.Not x      -> not (exec_boole_exp c x)
+   | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y)
+   | MathQL.Or (x, y)  -> (exec_boole_exp c x) || (exec_boole_exp c y)
+   | MathQL.Sub (vexp1, vexp2) -> sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
+   | MathQL.Meet (vexp1, vexp2) -> meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
+   | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2)
+   | MathQL.Ex l bexp -> 
+       if l = [] then (exec_boole_exp c bexp)
+       else
+         let latt = List.map (fun uri -> 
+                                       let (r,attl) = List.assoc uri c.rvars 
+                                      in (uri,attl)) l (*latt = l + attributi*)
+         in
+          try
+            let rec prod c = function
+               [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue 
+             | (uri,attl)::tail1 -> let rec sub_prod attl =
+                                     match attl with
+(*per ogni el. di attl  *)             [] -> () 
+(*devo andare in ric. su tail1*)      | att::tail2 -> upd_groups c ((uri,att)::c.groups);             
+                                                      prod c tail1; sub_prod tail2 
+                                    in       
+                                     sub_prod attl 
+            in
+             prod c latt; false
+          with BooleExpTrue -> true  
+   | _ -> assert false    
 
 (* valuta una MathQL.val_exp e ritorna un MathQL.value *)
 
-and exec_val_exp = function
-   | MathQL.Const x -> x
+and exec_val_exp c = function
+   | MathQL.Const x -> List.sort compare x
+   | MathQL.Record (rvar, vvar) -> List.assoc vvar (List.assoc rvar c.groups) 
+                                 
+   | MathQL.VVar s -> List.assoc s c.vvars                               
+   | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp)
+   
    | _ -> assert false
 
+
 (* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *)
 
-(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *)
-let execute x =
-   svars := []; rvars := []; groups := []; vvars := [];
-   exec_set_exp x
+and execute x =
+   exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x