X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fmqint.ml;h=b275de355372b898404fe49d85f668acb5fff179;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=01fbc1de1b102005a876ecfb62501a56854d8e6d;hpb=cef7b3b104313195d378890cd79656e5640eebec;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 01fbc1de1..b275de355 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -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 =