]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mqint.ml
Whithout List.hd error
[helm.git] / helm / ocaml / mathql_interpreter / mqint.ml
index 0de53503ec72edc48f11c0190b9a5ab80a8ac635..ba7d0713a592a3fd7b7a034d44ff833e45d465be 100644 (file)
 (*
  * implementazione del'interprete MathQL
  *)
+
+(*
+(* FG: ROBA VECCHIA DA BUTTARE (tranne apertura e chiusura database *)
+
 open MathQL;;
 open Eval;;
 open Utility;;
 open Dbconn;;
-open Pattern;;
+open Pattern;;*)
 open Union;;
 open Intersect;;
+open Meet;;
+open Sub;;
+open Context;;
 open Diff;;
-open Sortedby;;
+open Relation;;
+(*open Sortedby;;
 open Use;;
 open Select;;
 open Letin;;
 open Mathql_semantics;;
 
+
+
 let prop_pool = ref None;;
 
 let fi_to_string fi =
@@ -92,13 +102,6 @@ let get_prop_id prop =
  else List.assoc prop (match !prop_pool with Some l -> l | _ -> assert false)
 ;;
 
-(* automatically performes the union of a given list of patterns *)
-let rec pattern_list_ex = function
-   | [] -> []
-   | [(apreamble, apattern, afragid)] -> pattern_ex (apreamble, apattern, afragid)
-   | (apreamble, apattern, afragid) :: tail -> 
-      union_ex (pattern_ex (apreamble, apattern, afragid)) (pattern_list_ex tail)
-
 (* execute_ex env q                                                   *)
 (*  [env] is the attributed uri environment in which the query [q]    *)
 (*        must be evaluated                                           *)
@@ -112,8 +115,8 @@ let rec execute_ex env =
      use_ex (execute_ex env alist) asvar (get_prop_id "refObj")      (* "F" (*"refObj"*) *)
  |  MQUse (alist, asvar) ->
      use_ex (execute_ex env alist) asvar (get_prop_id "backPointer") (* "B" (*"backPointer"*) *)
- |  MQPattern l ->
-     pattern_list_ex l
+ |  MQPattern (apreamble, apattern, afragid) ->
+     pattern_ex (apreamble, apattern, afragid)
  |  MQUnion (l1, l2) ->
      union_ex (execute_ex env l1) (execute_ex env l2)
  |  MQDiff (l1, l2) ->
@@ -138,14 +141,12 @@ let rec execute_ex env =
        res
  |  MQListLVar lvar ->
      letref_ex lvar
- |  MQReference l -> (* FG: *)
+ |  MQReference l ->
      let rec build_result = function
        | [] -> []
        | s :: tail -> 
         {uri = s ; attributes = [] ; extra = ""} :: build_result tail
-     in build_result l
- | MQMinimize l ->     (* FG: sostituire con l'implementazione vera *)
-     execute_ex env l 
+     in build_result (List.sort compare l)
 ;;
 
 (* Let's initialize the execute in Select, creating a cyclical recursion *)
@@ -253,3 +254,99 @@ let execute q =
  *)
 let close () = Dbconn.close ();;
 
+*****************************************************************************)
+
+let init () = () (* FG: implementare l'apertura del database *)
+
+let close () = () (* FG: implementare la chiusura del database *)
+
+
+
+exception BooleExpTrue
+
+(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *)
+
+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 -> let c1 = upd_rvars c ((rvar,r)::c.rvars) in                      
+                                              if (exec_boole_exp c1 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 c = function
+   | MathQL.False      -> false
+   | MathQL.True       -> true
+   | 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 -> let c1 = upd_groups c ((uri,att)::c.groups) in             
+                                                      prod c1 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 c = function
+   | MathQL.Const x -> let ol = List.sort compare x in 
+                       let rec edup = function
+                       
+                          [] -> [] 
+                        | s::tl -> if tl <> [] then  
+                                                if s = (List.hd tl) then edup tl
+                                                else s::(edup tl)
+                                   else s::[]
+                       in
+                        edup ol
+   | 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 *)
+
+and execute x =
+   exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x 
+