]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mqint.ml
Initial revision
[helm.git] / helm / ocaml / mathql_interpreter / mqint.ml
index 01fbc1de1b102005a876ecfb62501a56854d8e6d..b275de355372b898404fe49d85f668acb5fff179 100644 (file)
@@ -37,12 +37,18 @@ open Dbconn;;
 open Union;;
 open Intersect;;
 open Meet;;
+open Property;;
 open Sub;;
 open Context;;
 open Diff;;
 open Relation;;
 open Func;;
+open Pattern;;
 
+exception SVarUnbound of string;;
+exception RVarUnbound of string;;
+exception VVarUnbound of string;;
+exception PathUnbound of (string * string list);;
 
 exception BooleExpTrue
 
@@ -54,22 +60,39 @@ let check () =
    let status = Dbconn.pgc () 
    in ()
 
-let stat = ref false
+let stat = ref true
 
 let set_stat b = stat := b
 
 let get_stat () = ! stat
 
-let dbname = ref "db-postgres"
+let postgres_db = "postgres"
 
-let set_database db = dbname := db  
+let galax_db = "galax"
+
+let dbname = ref galax_db
+
+let set_database s = 
+    if s = postgres_db || s = galax_db then dbname := s
+    else raise (Invalid_argument s)
+
+let get_database () = ! dbname
 
 (* 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.SVar svar ->
+      (try
+        List.assoc svar c.svars
+       with Not_found ->
+        raise (SVarUnbound svar))
+   | MathQL.RVar rvar ->
+      (try
+        [List.assoc rvar c.rvars]  
+       with Not_found ->
+        raise (RVarUnbound rvar))
    | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp)
+   | MathQL.Pattern vexp -> pattern_ex (exec_val_exp c vexp)
    | MathQL.Intersect (sexp1, sexp2) ->    
         let before = Sys.time() in
        let rs1 = exec_set_exp c sexp1 in
@@ -97,7 +120,7 @@ let rec exec_set_exp c = function
         let before = Sys.time() in
         let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in 
        let res = exec_set_exp c1 sexp2 in
-       if !stat then
+       if ! stat then
        (print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": ");
         print_endline (string_of_float (Sys.time() -. before) ^ "s");
          flush stdout); 
@@ -106,24 +129,25 @@ let rec exec_set_exp c = function
         let before = Sys.time() in
        let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in
        let res = exec_set_exp c1 sexp in
-       if !stat then
+       if ! stat then
        (print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": ");
          print_endline (string_of_float (Sys.time() -. before) ^ "s");
          flush stdout); 
        res
-   | MathQL.Relation (rop, path, sexp, attl) -> 
+   | MathQL.Relation (inv, rop, path, sexp, assl) -> 
         let before = Sys.time() in
-       if !dbname = "db-postgres" then
-        (let res = relation_ex rop path (exec_set_exp c sexp) attl in
-        if !stat then 
-        (print_string ("RELATION " ^ (List.hd path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
+       if ! dbname = postgres_db then
+        (let res = relation_ex inv rop path (exec_set_exp c sexp) assl in
+        if ! stat then 
+        (print_string ("RELATION " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
           print_endline (string_of_float (Sys.time() -. before) ^ "s");
           flush stdout);
          res)
+       
        else
-        (let res = relation_galax_ex rop path (exec_set_exp c sexp) attl in
+        (let res = relation_galax_ex inv rop path (exec_set_exp c sexp) assl in
          if !stat then
-         (print_string ("RELATION-GALAX " ^ (List.hd path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
+         (print_string ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
           print_endline (string_of_float (Sys.time() -. before) ^ "s");
           flush stdout);
          res) 
@@ -140,44 +164,58 @@ let rec exec_set_exp c = function
                   else select_ex tl
         in 
        let res = select_ex rset in
-       if !stat then
+       if ! stat then
        (print_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": ");
         print_endline (string_of_float (Sys.time() -. before) ^ "s");
          flush stdout); 
        res
    | 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*)
+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) =
+              (try
+                List.assoc uri c.rvars
+               with Not_found -> assert false)
+             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
+         try
+          let rec prod c =
+            function
+              [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue 
+            | (uri,attl)::tail1 ->
+                 (*per ogni el. di attl devo andare in ric. su tail1*)
+                 let rec sub_prod attl =
+                  match attl with
+                     [] -> () 
+                   | 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
 
 (* valuta una MathQL.val_exp e ritorna un MathQL.value *)
 
@@ -193,12 +231,23 @@ and exec_val_exp c = function
                                    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.Record (rvar, path) ->
+      (try
+        List.assoc path
+         (try
+           List.assoc rvar c.groups
+          with Not_found ->
+           raise (RVarUnbound rvar))
+       with Not_found ->
+        raise (PathUnbound path))
+   | MathQL.VVar s ->
+      (try
+        List.assoc s c.vvars
+       with Not_found ->
+        raise (VVarUnbound s))
    | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp)
    | MathQL.Fun (s, vexp) -> fun_ex s (exec_val_exp c vexp)
-   | MathQL.Attribute (rop, path, vexp) -> [] 
+   | MathQL.Property (inv, rop, path, vexp) -> property_ex rop path inv (exec_val_exp c vexp) 
 
 (* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *)
 and execute x =