X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fmqint.ml;h=b275de355372b898404fe49d85f668acb5fff179;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=611fdf388fd3b2b6969cb4fede53ab4c4bf3da49;hpb=9a5fcfd85222669ba70aae8c73433afc047f8f8a;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 611fdf388..b275de355 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -23,186 +23,232 @@ * http://cs.unibo.it/helm/. *) + + + (* * implementazione del'interprete MathQL *) -open MathQL;; -open Eval;; -open Utility;; + + + + open Dbconn;; -open Pattern;; open Union;; open Intersect;; +open Meet;; +open Property;; +open Sub;; +open Context;; open Diff;; -open Sortedby;; -open Use;; -open Select;; -open Letin;; - -let fi_to_string fi = - match fi with - (None, _) -> - "" - | (Some i, y) -> - "#xpointer(1/" ^ - string_of_int i ^ - ( - match y with - None -> - "" - | Some j -> - "/" ^ (string_of_int j) - ) ^ - ")" -;; +open Relation;; +open Func;; +open Pattern;; -(* - * inizializzazione della connessione al database - *) -let init () = Dbconn.init ();; - -(* execute_ex env q *) -(* [env] is the attributed uri environment in which the query [q] *) -(* must be evaluated *) -(* [q] is the query to evaluate *) -(* It returns a [Mathql_semantics.result] *) -let rec execute_ex env = - function - MQSelect (apvar, alist, abool) -> - select_ex env apvar (execute_ex env alist) abool - | MQUsedBy (alist, asvar) -> - use_ex (execute_ex env alist) asvar "F" (*"refObj"*) - | MQUse (alist, asvar) -> - use_ex (execute_ex env alist) asvar "B" (*"backPointer"*) - | 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) -> - diff_ex (execute_ex env l1) (execute_ex env l2) - | MQSortedBy (l, o, f) -> - sortedby_ex (execute_ex env l) o f - | MQIntersect (l1, l2) -> - intersect_ex (execute_ex env l1) (execute_ex env l2) - | MQLRVar rvar -> [List.assoc rvar env] - | MQLetIn (lvar, l1, l2) -> - let t = Unix.time () in - let res = - (*CSC: The interesting code *) - let _ = letin_ex lvar (execute_ex env l1) in - execute_ex env l2 - (*CSC: end of the interesting code *) - in - print_string ("LETIN = " ^ string_of_int (List.length res) ^ ": ") ; - print_endline (string_of_float (Unix.time () -. t) ^ "s") ; - flush stdout ; - res - | MQLetRef rvar -> - letref_ex rvar -;; - -(* Let's initialize the execute in Select, creating a cyclical recursion *) -Select.execute := execute_ex;; +exception SVarUnbound of string;; +exception RVarUnbound of string;; +exception VVarUnbound of string;; +exception PathUnbound of (string * string list);; -(* - * converte il risultato interno di una query (uri + contesto) - * in un risultato di sole uri - * - * parametri: - * l: string list list; - * - * output: mqresult; - * - * note: - * il tipo del risultato mantenuto internamente e' diverso dal tipo di risultato - * restituito in output poiche', mentre chi effettua le query vuole come risultato - * solo le eventuali uri che soddisfano le query stesse, internamente ad una uri - * sono associati anche i valori delle variabili che ancora non sono state valutate - * perche', ad esempio, si trovano in altri rami dell'albero. - * - * Esempio: - * SELECT x IN USE PATTERN "cic:/**.con" POSITION $a WHERE $a IS MainConclusion - * L'albero corrispondente a questa query e': - * - * SELECT - * / | \ - * x USE IS - * / \ /\ - * PATTERN $a $a MainConclusion - * - * Nel momento in cui si esegue il ramo USE non sono noti i vincoli sullla variabile $a - * percui e' necessario considerare, oltre alle uri, i valori della variabile per i quali - * la uri puo' far parte del risultato. - *) -let xres_to_res l = - MQRefs (List.map (function {Mathql_semantics.uri = uri} -> uri) l) -(* - let tmp = List.map (function {Mathql_semantics.uri = uri} -> uri) l in - MQRefs - (List.map - (function l -> - (*let _ = print_endline ("DEBUG: (mqint.ml: xres_to_res)" ^ l) in*) - match Str.split (Str.regexp ":\|#\|/\|(\|)") l with - hd::""::tl -> ( - match List.rev tl with - n::"1"::"xpointer"::tail -> - ( - Some hd, - List.fold_left - (fun par t -> - match par with - [] -> [MQBC t] - | _ -> (MQBC t) :: MQBD :: par - ) - [] - tail, - [MQFC (int_of_string n)] - ) - | n::m::"1"::"xpointer"::tail -> - ( - Some hd, - List.fold_left - (fun par t -> - match par with - [] -> [MQBC t] - | _ -> (MQBC t) :: MQBD :: par - ) - [] - tail, - [MQFC (int_of_string m); MQFC (int_of_string n)] - ) - | tail -> - ( - Some hd, - List.fold_left - (fun par t -> - match par with - [] -> [MQBC t] - | _ -> (MQBC t) :: MQBD :: par - ) - [] - tail, - [] - ) - ) - | _ -> assert false - ) - tmp - ) -*) -;; +exception BooleExpTrue +let init connection_param = Dbconn.init connection_param -(* - * - *) -let execute q = - match q with - MQList qq -> xres_to_res (execute_ex [] qq) -;; +let close () = Dbconn.close () -(* - * chiusura della connessione al database - *) -let close () = Dbconn.close ();; +let check () = + let status = Dbconn.pgc () + in () + +let stat = ref true + +let set_stat b = stat := b + +let get_stat () = ! stat + +let postgres_db = "postgres" + +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 -> + (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 + let rs2 = exec_set_exp c sexp2 in + let res = intersect_ex rs1 rs2 in + let after = Sys.time() in + let ll1 = string_of_int (List.length rs1) in + let ll2 = string_of_int (List.length rs2) in + let diff = string_of_float (after -. before) in + if !stat then + (print_endline("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ + ": " ^ diff ^ "s"); + flush stdout); + res + | MathQL.Union (sexp1, sexp2) -> + let before = Sys.time () in + let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in + let after = Sys.time() in + let diff = string_of_float (after -. before) in + if !stat then + (print_endline ("UNION: " ^ diff ^ "s"); + flush stdout); + res + | MathQL.LetSVar (svar, sexp1, sexp2) -> + 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 + (print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res + | MathQL.LetVVar (vvar, vexp, sexp) -> + 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 + (print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res + | MathQL.Relation (inv, rop, path, sexp, assl) -> + let before = Sys.time() in + 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 inv rop path (exec_set_exp c sexp) assl in + if !stat then + (print_string ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": "); + print_endline (string_of_float (Sys.time() -. before) ^ "s"); + flush stdout); + res) + + + | MathQL.Select (rvar, sexp, bexp) -> + let before = Sys.time() in + 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 + let res = select_ex rset in + 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) + +(* 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) = + (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 -> + (*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 *) + +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, 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.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 = + exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x