From: natile Date: Tue, 1 Oct 2002 15:25:25 +0000 (+0000) Subject: After Union and Relation X-Git-Tag: new_mathql_before_first_merge~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ac188650f64fb947c5d87dcf3c932a4d013d842;p=helm.git After Union and Relation --- diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index 722043c03..1440e28c7 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,4 +1,20 @@ +dbconn.cmo: dbconn.cmi +dbconn.cmx: dbconn.cmi +utility.cmo: dbconn.cmi utility.cmi +utility.cmx: dbconn.cmx utility.cmi +relation.cmo: dbconn.cmi utility.cmi relation.cmi +relation.cmx: dbconn.cmx utility.cmx relation.cmi +diff.cmo: diff.cmi +diff.cmx: diff.cmi +meet.cmo: meet.cmi +meet.cmx: meet.cmi +sub.cmo: sub.cmi +sub.cmx: sub.cmi +union.cmo: union.cmi +union.cmx: union.cmi intersect.cmo: intersect.cmi intersect.cmx: intersect.cmi -mqint.cmo: intersect.cmi mqint.cmi -mqint.cmx: intersect.cmx mqint.cmi +mqint.cmo: context.cmo diff.cmi intersect.cmi meet.cmi relation.cmi sub.cmi \ + union.cmi mqint.cmi +mqint.cmx: context.cmx diff.cmx intersect.cmx meet.cmx relation.cmx sub.cmx \ + union.cmx mqint.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile index 1ef0ab3fc..a8aea2b32 100644 --- a/helm/ocaml/mathql_interpreter/Makefile +++ b/helm/ocaml/mathql_interpreter/Makefile @@ -2,9 +2,9 @@ PACKAGE = mathql_interpreter REQUIRES = helm-urimanager postgres unix helm-mathql PREDICATES = -INTERFACE_FILES = intersect.mli mqint.mli +INTERFACE_FILES = dbconn.mli utility.mli relation.mli diff.mli meet.mli sub.mli union.mli intersect.mli mqint.mli -IMPLEMENTATION_FILES = intersect.ml mqint.ml +IMPLEMENTATION_FILES = dbconn.ml utility.ml relation.ml diff.ml meet.ml sub.ml union.ml intersect.ml context.ml mqint.ml # $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_interpreter/dbconn.ml b/helm/ocaml/mathql_interpreter/dbconn.ml index db4b8fb9c..a6b1b2cce 100644 --- a/helm/ocaml/mathql_interpreter/dbconn.ml +++ b/helm/ocaml/mathql_interpreter/dbconn.ml @@ -33,6 +33,12 @@ *) open MathQL;; +exception MQInvalidURI of string +exception MQConnectionFailed of string +exception MQInvalidConnection of string + + + (* * paramentri della connessione * diff --git a/helm/ocaml/mathql_interpreter/diff.ml b/helm/ocaml/mathql_interpreter/diff.ml index e2eea1bc1..28e874c86 100644 --- a/helm/ocaml/mathql_interpreter/diff.ml +++ b/helm/ocaml/mathql_interpreter/diff.ml @@ -24,8 +24,8 @@ *) (* - * implementazione del comando DIFF - *) + * vecchia implementazione del comando DIFF + exception NotCompatible;; @@ -45,9 +45,7 @@ let rec intersect_attributes (attr1, attr2) = | _, _ -> raise NotCompatible (* same keys, different values *) ;; -(* - * implementazione del comando DIFF - *) + let rec diff_ex l1 l2 = let module S = Mathql_semantics in match (l1, l2) with @@ -67,6 +65,22 @@ let rec diff_ex l1 l2 = NotCompatible -> {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 tl2) ;; +*) + +(* + * implementazione del comando DIFF + *) +let rec diff_ex rs1 rs2 = + match (rs1, rs2) with + [],_ -> [] + | l,[] -> l + | (uri1,l)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l)::(diff_ex tl1 rs2) + | (uri1,_)::_,(uri2,_)::tl2 when uri2 < uri1 -> (diff_ex rs1 tl2) + | (uri1,_)::tl1, (uri2,_)::tl2 -> (diff_ex tl1 tl2) +;; + + + let diff_ex l1 l2 = let before = Unix.time () in diff --git a/helm/ocaml/mathql_interpreter/diff.mli b/helm/ocaml/mathql_interpreter/diff.mli index 8c247687f..1cd9cf4de 100644 --- a/helm/ocaml/mathql_interpreter/diff.mli +++ b/helm/ocaml/mathql_interpreter/diff.mli @@ -24,4 +24,4 @@ *) val diff_ex : - Mathql_semantics.result -> Mathql_semantics.result -> Mathql_semantics.result + MathQL.resource_set -> MathQL.resource_set -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/intersect.ml b/helm/ocaml/mathql_interpreter/intersect.ml index e56d1d1f3..8a2f55ff2 100644 --- a/helm/ocaml/mathql_interpreter/intersect.ml +++ b/helm/ocaml/mathql_interpreter/intersect.ml @@ -23,7 +23,6 @@ * http://cs.unibo.it/helm/. *) -exception NotCompatible;; (* Catenates two lists preserving order and getting rid of duplicates *) let rec append (l1,l2) = @@ -48,7 +47,7 @@ let rec sum_groups(gr1, gr2) = ;; -(* Product between an attribute set and a gropu of attributes *) +(* Product between an attribute set and a group of attributes *) let rec sub_prod (aset, gr) = (*prende un aset e un gr e fa la somma tra tutti i gruppi di aset e gr *) match aset with [] -> [] @@ -70,10 +69,10 @@ let intersect_ex rs1 rs2 = match (rs1, rs2) with [],_ | _,[] -> [] - | (uri1,as1)::tl1, - (uri2,as2)::_ when uri1 < uri2 -> intersect_aux tl1 rs2 - | (uri1,as1)::_, - (uri2,as2)::tl2 when uri2 < uri1 -> intersect_aux rs1 tl2 + | (uri1,_)::tl1, + (uri2,_)::_ when uri1 < uri2 -> intersect_aux tl1 rs2 + | (uri1,_)::_, + (uri2,_)::tl2 when uri2 < uri1 -> intersect_aux rs1 tl2 | (uri1,as1)::tl1, (uri2,as2)::tl2 -> (uri1, prod(as1,as2))::intersect_aux tl1 tl2 in diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index a0c56e384..95d3c8f2e 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -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 c = 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 diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index c25ea2625..960a0a2ba 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -26,7 +26,7 @@ (* * implementazione del comando SELECT *) - +(* open MathQL;; open Func;; open Utility;; @@ -147,4 +147,7 @@ let select_ex env avar alist abool = print_endline (string_of_float (Unix.time () -. t) ^ "s") ; flush stdout ; result -;; +;; *) + +let select_ex rvar rset bexp + diff --git a/helm/ocaml/mathql_interpreter/union.ml b/helm/ocaml/mathql_interpreter/union.ml index c8e46cd0b..a02fbd0f5 100644 --- a/helm/ocaml/mathql_interpreter/union.ml +++ b/helm/ocaml/mathql_interpreter/union.ml @@ -106,24 +106,25 @@ let union_ex alist1 alist2 = ) ;; *) +(* Merges two attribute group lists preserves order and gets rid of duplicates*) +let rec merge l1 l2 = + match (l1,l2) with + [],l + | l,[] -> l + | g1::tl1,g2::_ when g1 < g2 -> g1::(merge tl1 l2) + | g1::_,g2::tl2 when g2 < g1 -> g2::(merge l1 tl2) + | g1::tl1,g2::tl2 -> g1::(merge tl1 tl2) +;; (* preserves order and gets rid of duplicates *) -let rec union_ex l1 l2 = - let module S = Mathql_semantics in - match (l1, l2) with +let rec union_ex rs1 rs2 = + match (rs1, rs2) with [],l | l,[] -> l - | ({S.uri = uri1} as entry1)::tl1, - ({S.uri = uri2} as entry2)::_ when uri1 < uri2 -> - entry1::(union_ex tl1 l2) - | ({S.uri = uri1} as entry1)::_, - ({S.uri = uri2} as entry2)::tl2 when uri2 < uri1 -> - entry2::(union_ex l1 tl2) - | entry1::tl1,entry2::tl2 -> (* same entry *) - if entry1 = entry2 then (* same attributes *) - entry1::(union_ex tl1 tl2) - else - assert false + | (uri1,l1)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l1)::(union_ex tl1 rs2) + | (uri1,_)::_,(uri2,l2)::tl2 when uri2 < uri1 -> (uri2,l2)::(union_ex rs1 tl2) + | (uri1,l1)::tl1,(uri2,l2)::tl2 -> if l1 = l2 then (uri1,l1)::(union_ex tl1 tl2) + else (uri1,merge l1 l2)::(union_ex tl1 tl2) ;; let union_ex l1 l2 = diff --git a/helm/ocaml/mathql_interpreter/union.mli b/helm/ocaml/mathql_interpreter/union.mli index 6b6ba6d27..6890bdb0c 100644 --- a/helm/ocaml/mathql_interpreter/union.mli +++ b/helm/ocaml/mathql_interpreter/union.mli @@ -24,4 +24,4 @@ *) val union_ex : - Mathql_semantics.result -> Mathql_semantics.result -> Mathql_semantics.result +MathQL.result -> MathQL.result -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/use.ml b/helm/ocaml/mathql_interpreter/use.ml index 93ed9a8a4..654c3e69b 100644 --- a/helm/ocaml/mathql_interpreter/use.ml +++ b/helm/ocaml/mathql_interpreter/use.ml @@ -44,66 +44,25 @@ open Dbconn;; * output: string list list; lista su cui e' stato eseguito il * comando USE/USED BY *) -let use_ex alist asvar usek = - (*(*let _ = print_string ("USE ") - and t = Unix.time () in*) - let result = - let c = pgc () - in - [ (List.hd alist) @ [asvar] ] - @ - Sort.list - (fun l m -> List.hd l < List.hd m) - (List.fold_left - (fun parziale xres -> - (*let r1 = helm_property_id usek - and r2 = helm_property_id "position" - and r3 = helm_property_id "occurrence" - in - let qq = "select distinct t" ^ r3 ^ ".att1, t" ^ r2 ^ ".att1 " ^ - "from t" ^ r3 ^ ", t" ^ r2 ^ ", t" ^ r1 ^ " " ^ - "where " ^ "t" ^ r1 ^ ".att0 = '" ^ (List.hd xres) ^ "' and t" ^ r1 ^ - ".att1 = t" ^ r2 ^ ".att0 and t" ^ r1 ^ ".att1 = t" ^ r3 ^ - ".att0 order by t" ^ r3 ^ ".att1 asc"*) - let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ (List.hd xres) ^ "'")) in - let _ = print_endline ("DEBUG (use.ml): " ^ tv) in - let qq = "select uri, context from t" ^ tv ^ " where back_for='" ^ usek ^ "'" in - let res = c#exec qq in - (List.map - (fun l -> [List.hd l] @ List.tl xres @ List.tl l) - res#get_list - ) - @ - parziale - ) - [] - (List.tl alist) - ) - in - (*let _ = print_endline (string_of_float (Unix.time () -. t)); flush stdout in*) +let get_prop_id prop = + if prop="refObj" then "F" + else if prop="backPointer" then "B" + else assert false + ;; + + +let relation_ex rop path rset attl = + let usek = get_prop_id (List.hd path) in - *) -let module S = Mathql_semantics in -let _ = print_string ("USE ") +let _ = print_string ("RELATION "^usek) and t = Unix.time () in let result = let c = pgc () in Sort.list - (fun {S.uri = uri1} {S.uri = uri2} -> uri1 < uri2) + (fun (uri1-> uri1 < uri2) (List.fold_left - (fun parziale {S.uri = uri ; S.attributes = attributes} -> + (fun parziale (uri,aset)-> print_string uri ; - (* RSSDB - let r1 = helm_property_id usek - and r2 = helm_property_id "position" - and r3 = helm_property_id "occurrence" - in - let qq = "select distinct t" ^ r3 ^ ".att1, t" ^ r2 ^ ".att1 " ^ - "from t" ^ r3 ^ ", t" ^ r2 ^ ", t" ^ r1 ^ " " ^ - "where " ^ "t" ^ r1 ^ ".att0 = '" ^ (List.hd xres) ^ "' and t" ^ r1 ^ - ".att1 = t" ^ r2 ^ ".att0 and t" ^ r1 ^ ".att1 = t" ^ r3 ^ - ".att0 order by t" ^ r3 ^ ".att1 asc" - *) let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ uri ^ "'")) @@ -120,7 +79,7 @@ let result = ) res#get_list ) @ parziale - ) [] alist + ) [] rset ) in print_string (" = " ^ string_of_int (List.length result) ^ ": ") ;