X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=dd8b00ae327aeb0248acc88a92024046320b7051;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ca0e36550908bad1b826891b03c8ed538280e9e4;hpb=cab4eba3c7da115ecc1973d989b321b46835e1eb;p=helm.git diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index ca0e36550..dd8b00ae3 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -23,483 +23,167 @@ * http://cs.unibo.it/helm/. *) -(* Query issuing functions **************************************************) - -type uri = string -type position = string -type depth = int option -type sort = string - -type r_obj = (uri * position * depth) -type r_rel = (position* depth) -type r_sort = (position* depth * sort) - -type must_restrictions = (r_obj list * r_rel list * r_sort list) -type only_restrictions = - (r_obj list option * r_rel list option * r_sort list option) -type universe = position list option - -let builtin s = - let ns = "h:" in - match s with - | "MH" -> ns ^ "MainHypothesis" - | "IH" -> ns ^ "InHypothesis" - | "MC" -> ns ^ "MainConclusion" - | "IC" -> ns ^ "InConclusion" - | "IB" -> ns ^ "InBody" - | "SET" -> ns ^ "Set" - | "PROP" -> ns ^ "Prop" - | "TYPE" -> ns ^ "Type" - | _ -> raise (Failure "MQueryGenerator.builtin") - -(* Query building functions ************************************************) +(* AUTOR: Ferruccio Guidi + *) module M = MathQL +module T = MQGTypes +module U = MQGUtil -let locate s = - M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s])) - -let query_of_constraints univ must_use can_use = -(* FG : The (univ : universe) is not used in this implementation *) - let in_path s = (s, []) in - let assign v p = (in_path v, in_path p) in - -(* can restrictions *) - - let (cr_o,cr_r,cr_s) = can_use in - - let uri_of_entry (r, p, d) = r in - - let universe = - match cr_o with - None -> [] - | Some cr_o -> List.map uri_of_entry cr_o - in - - let tfst (a,b,c) = a in - let tsnd (a,b,c) = b in - let trd (a,b,c) = c in - - let to_int_list l d = - match d with - None -> l - | Some d -> l@[d] - in +(* low level functions *****************************************************) - let opos = - match cr_o with - None -> [] - | Some cr_o -> (List.map tsnd cr_o) in - - let odep = - match cr_o with - None -> [] - | Some cr_o -> List.map trd cr_o - (* let odep_option_list = List.map trd cr_o in - let lo_dep_int = List.fold_left to_int_list [] odep_option_list in - List.map string_of_int lo_dep_int*) - in - print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout; - print_endline""; - let rpos = - match cr_r with - None -> [] - | Some cr_r -> (List.map fst cr_r) in - - let rdep = - match cr_r with - None -> [] - | Some cr_r -> List.map snd cr_r - (* let rdep_option_list = List.map snd cr_r in - let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in - List.map string_of_int lr_dep_int *) - in - - - let spos = - match cr_s with - None -> [] - | Some cr_s -> (List.map tfst cr_s) in - +let locate s = + let query = + M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) + in query + +let unreferred target_pattern source_pattern = + let query = + M.Bin (M.BinFDiff, + ( + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern)) + ), ( + M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) - let sdep = - match cr_s with - None -> [] - | Some cr_s -> List.map tsnd cr_s - (* let sdep_option_list = List.map tsnd cr_s in - let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in - List.map string_of_int ls_dep_int*) - in - - - let sor = - match cr_s with - None -> [] - | Some cr_s -> List.map trd cr_s in - - (* let q_where_obj = function - Some l -> - if odep = [] then - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]), - M.Ex ["uri"] - (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))), - M.VVar "universe") - else - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (M.And - ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))), - (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d"))))) - ) - ), - M.VVar "universe" - ) - - | None -> M.True - in*) - - - - let q_where_obj n = function - Some l -> - let rec q_ex n = function - [] -> M.True - | [(u,p,None)] -> - M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")) - - | [(u,p,d)] -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.And - (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")), - M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))) - | (u,p,None)::tl -> - M.Or - (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")), - q_ex (n+1) tl) - | (u,p,d)::tl -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.Or - ((M.And - ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))), - (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))), - q_ex (n+1) tl) - in - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (q_ex 1 l))), - M.VVar "universe") - | None -> M.True - in - - - - - let rec q_where_rel n cr_r= (*function*) - (* Some l ->*) - let q0 = - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["position"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_position" ^ string_of_int n)) - in - match cr_r with - Some [] -> M.True - | Some [(p,None)] -> q0 - | Some [(p,d)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))) - | Some ((p,None)::tl) -> - M.Or - (q0, - q_where_rel (n+1) (Some tl)) - | Some ((p,d)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))), - q_where_rel (n+1) (Some tl)) - | None -> M.True - in - - let rec q_where_sort n cr_s = (*function *) - (* Some l ->*) - let q0 = - M.And - (M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["position"]), - M.RefOf(M.RVar "uri0") - ), - M.VVar ("sort_position" ^ string_of_int n)), - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["sort"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort" ^ string_of_int n))) - in - match cr_s with - Some [] -> M.True - | Some [(p,None,s)] -> q0 - - | Some [(p,d,s)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))) - - | Some ((p,None,s)::tl) -> - M.Or - (q0, - q_where_sort (n+1) (Some tl)) - - | Some((p,d,s)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))), - q_where_sort (n+1) (Some tl)) - | None -> M.True + )) + in query + +let compose cl = + let letin = ref [] in + let must = ref [] in + let onlyobj = ref [] in + let onlysort = ref [] in + let onlyrel = ref [] in + let only = ref true in + let univ = ref [] in + let set_val = function + | [s] -> M.Const s + | l -> + let msval = M.Set (List.map (fun s -> M.Const s) l) in + if ! only then begin + let vvar = "val" ^ string_of_int (List.length ! letin) in + letin := (vvar, msval) :: ! letin; + M.VVar vvar + end else msval in - - - - - let q_where cr = - let (cr_o,cr_r,cr_s) = cr in - M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s)) - - in - -(* must restrictions *) - - let build_select_obj (r, pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position"]), - M.Ex ["uri"] - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_rel (pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_sort (pos, dep, sor) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - in - - let rec build_intersect_obj = function - [] -> M.Pattern (M.Const ["[.]*"]) - | [hd] -> build_select_obj hd - | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl) - in - - let rec build_intersect_rel = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_rel hd - | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl) - in - - let rec build_intersect_sort = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_sort hd - | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl) + let cons o (r, s, p, d) = + let con p = function + | [] -> [] + | l -> [(false, [p], set_val l)] + in + only := o; + con "h:occurrence" r @ + con "h:sort" (List.map U.string_of_sort s) @ + con "h:position" (List.map U.string_of_position p) @ + con "h:depth" (List.map U.string_of_depth d) in - - let build_intersect = function -(* let tostring_sort (a,b,c) = - let b1 = string_of_int b in - (a,b1,c) + let property_must n c = + M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) + in + let property_only n cl = + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl in - let tostring_rel (a,b) = - let b1 = string_of_int b in - (a,b1) - in*) - -(* let (l1,l2,l3) = must in - match (l1,l2,l3) with *) - l1,[],[] -> build_intersect_obj l1 - | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - build_intersect_rel l2 - | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*) - build_intersect_sort l3 - | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - M.Intersect (build_intersect_obj l1, build_intersect_rel l2) - | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *) - M.Intersect (build_intersect_obj l1, build_intersect_sort l3) - | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in*) - M.Intersect (build_intersect_rel l2, build_intersect_sort l3) - | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in *) - M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3) - in - - let q_in = build_intersect must_use in - let q_select = M.Select ("uri0", q_in, q_where can_use) in - -(* variables for can restrictions *) - - let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in - - let rec q_let_s sor n = - match sor with - [] -> q_let_u - | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u) - | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1)) + let cll = build cl in + M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) in - -(* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *) - - let rec q_let_ds sdep n = - match sdep with - [] - | [None] -> q_let_s sor 1 - | (None)::tl -> q_let_ds tl (n+1) - | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1) - | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1)) - in - -(* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *) - - let rec q_let_dr rdep n = - match rdep with - [] - | [None] -> q_let_ds sdep 1 - | (None)::tl -> q_let_dr tl (n+1) - | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1) - | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1)) + let rec aux = function + | [] -> () + | T.Universe l :: tail -> + only := true; + let l = List.map U.string_of_position l in + univ := [(false, ["h:position"], set_val l)]; aux tail + | T.MustObj(r,p,d) :: tail -> + must := property_must "refObj" (r, [], p, d) :: ! must; aux tail + | T.MustSort(s,p,d) :: tail -> + must := property_must "refSort" ([], s, p, d) :: ! must; aux tail + | T.MustRel(p,d) :: tail -> + must := property_must "refRel" ([], [], p, d) :: ! must; aux tail + | T.OnlyObj(r,p,d) :: tail -> + onlyobj := (r, [], p, d) :: ! onlyobj; aux tail + | T.OnlySort(s,p,d) :: tail -> + onlysort := ([], s, p, d) :: ! onlysort; aux tail + | T.OnlyRel(p,d) :: tail -> + onlyrel := ([], [], p, d) :: ! onlyrel; aux tail in - - - (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*) - - let rec q_let_do odep n = - match odep with - [] - | [None] -> q_let_dr rdep 1 - | (None)::tl -> q_let_do tl (n+1) - | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1) - | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1)) + let rec iter f g = function + | [] -> raise (Failure "MQueryGenerator.iter") + | [head] -> (f head) + | head :: tail -> let t = (iter f g tail) in g (f head) t in - - -(* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *) - - - let rec q_let_ps spos n = - match spos with - [] -> q_let_do odep 1 - | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1) - | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1)) + (* prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; *) + aux cl; + let must_query = + if ! must = [] then + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) + else + iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must + in + let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in + let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in + let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in + let select_query x = + match ! onlyobj, ! onlysort, ! onlyrel with + | [], [], [] -> x + | _, [], [] -> M.Select("obj",x,onlyobj_val) + | [], _, [] -> M.Select("obj",x,onlysort_val) + | [], [], _ -> M.Select("obj",x,onlyrel_val) + | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val))) + | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val))) + | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val))) + | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val))) + in + let letin_query = + if ! letin = [] then fun x -> x + else + let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in + iter f (fun x y z -> x (y z)) ! letin + in + letin_query (select_query must_query) + +(* high-level functions ****************************************************) + +let query_of_constraints u (musts_obj, musts_rel, musts_sort) + (onlys_obj, onlys_rel, onlys_sort) = + let conv = function + | `MainHypothesis None -> [T.MainHypothesis], [] + | `MainHypothesis (Some d) -> [T.MainHypothesis], [d] + | `MainConclusion None -> [T.MainConclusion], [] + | `MainConclusion (Some d) -> [T.MainConclusion], [d] + | `InHypothesis -> [T.InHypothesis], [] + | `InConclusion -> [T.InConclusion], [] + | `InBody -> [T.InBody], [] in - - -(* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *) - - - let rec q_let_pr rpos n = - match rpos with - [] -> q_let_ps spos 1 - | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1) - | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1)) + let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in + let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in + let must_rel p = let p, d = conv p in T.MustRel (p, d) in + let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in + let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in + let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in + let must = List.map must_obj musts_obj @ + List.map must_rel musts_rel @ + List.map must_sort musts_sort in - - - -(* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *) - - let rec q_let_po opos n = - match opos with - [] -> q_let_pr rpos 1 - | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1) - | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1)) + let only = + (match onlys_obj with + | None -> [] + | Some [] -> [T.OnlyObj ([], [], [])] + | Some l -> List.map only_obj l + ) @ + (match onlys_rel with + | None -> [] + | Some [] -> [T.OnlyRel ([], [])] + | Some l -> List.map only_rel l + ) @ + (match onlys_sort with + | None -> [] + | Some [] -> [T.OnlySort ([], [], [])] + | Some l -> List.map only_sort l + ) in - - (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*) - - let query = (M.Ref (M.RefOf (q_let_po opos 1))) in - -print_endline "### "; MQueryUtil.text_of_query print_string query "\n"; flush stdout; - query + let univ = match u with None -> [] | Some l -> [T.Universe l] in + compose (must @ only @ univ)