X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=dd8b00ae327aeb0248acc88a92024046320b7051;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2d529c9e8aa32f9f23659bebafcc418706bc5378;hpb=931f10c61b4e3914474955a94a05cf43b5fa2bc0;p=helm.git diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 2d529c9e8..dd8b00ae3 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -26,64 +26,27 @@ (* AUTOR: Ferruccio Guidi *) -type uri = string -type position = string -type depth = string -type sort = string - -type spec = MustObj of uri list * position list * depth list - | MustSort of sort list * position list * depth list - | MustRel of position list * depth list - | OnlyObj of uri list * position list * depth list - | OnlySort of sort list * position list * depth list - | OnlyRel of position list * depth list - | Universe of position list - -type builtin_t = MainHypothesis - | InHypothesis - | MainConclusion - | InConclusion - | InBody - | Set - | Prop - | Type - -let text_of_builtin s = - let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in - if s = ns ^ "MainHypothesis" then "$MH" else - if s = ns ^ "InHypothesis" then "$IH" else - if s = ns ^ "MainConclusion" then "$MC" else - if s = ns ^ "InConclusion" then "$IC" else - if s = ns ^ "InBody" then "$IB" else - if s = "Set" then "$SET" else - if s = "Prop" then "$PROP" else - if s = "Type" then "$TYPE" else s - -let text_of_spec out l = - let rec iter = function - | [] -> () - | [s] -> out "\""; out (text_of_builtin s); out "\"" - | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail - in - let txt_list l = out "{"; iter l; out "} " in - let txt_spec = function - | MustObj (u, p, d) -> out "mustobj "; txt_list u; txt_list p; txt_list d; out "\n" - | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n" - | MustRel ( p, d) -> out "mustrel "; txt_list p; txt_list d; out "\n" - | OnlyObj (u, p, d) -> out "onlyobj "; txt_list u; txt_list p; txt_list d; out "\n" - | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n" - | OnlyRel ( p, d) -> out "onlyrel "; txt_list p; txt_list d; out "\n" - | Universe ( p ) -> out "universe "; txt_list p; out "\n" - in - List.iter txt_spec l - module M = MathQL +module T = MQGTypes +module U = MQGUtil + +(* low level functions *****************************************************) let locate s = let query = - M.Property true M.RefineExact ["objectName"] [] [] [] [] - false (M.Const s) - in M.StatQuery 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)) + + )) + in query let compose cl = let letin = ref [] in @@ -109,33 +72,41 @@ let compose cl = | l -> [(false, [p], set_val l)] in only := o; - con "h:occurrence" r @ con "h:sort" s @ - con "h:position" p @ con "h:depth" d + 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 property_must n c = - M.Property true M.RefineExact [n] [] - (cons false c) [] [] false (M.Const "") + M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) in let property_only n cl = - let cll = List.map (cons true) cl in - M.Property false M.RefineExact [n] [] - ! univ cll [] false (M.Proj None (M.AVar "obj")) + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl + in + let cll = build cl in + M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) in let rec aux = function | [] -> () - | Universe l :: tail -> - only := true; univ := [(false, ["h:position"], set_val l)]; aux tail - | MustObj r p d :: tail -> + | 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 - | MustSort s p d :: tail -> + | T.MustSort(s,p,d) :: tail -> must := property_must "refSort" ([], s, p, d) :: ! must; aux tail - | MustRel p d :: tail -> + | T.MustRel(p,d) :: tail -> must := property_must "refRel" ([], [], p, d) :: ! must; aux tail - | OnlyObj r p d :: tail -> + | T.OnlyObj(r,p,d) :: tail -> onlyobj := (r, [], p, d) :: ! onlyobj; aux tail - | OnlySort s p d :: tail -> + | T.OnlySort(s,p,d) :: tail -> onlysort := ([], s, p, d) :: ! onlysort; aux tail - | OnlyRel p d :: tail -> + | T.OnlyRel(p,d) :: tail -> onlyrel := ([], [], p, d) :: ! onlyrel; aux tail in let rec iter f g = function @@ -143,74 +114,56 @@ let compose cl = | [head] -> (f head) | head :: tail -> let t = (iter f g tail) in g (f head) t in - text_of_spec prerr_string cl; + (* 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 ".*") + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) else - iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must + 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 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) + | _, [], [] -> 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 + let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in iter f (fun x y z -> x (y z)) ! letin in - M.StatQuery (letin_query (select_query must_query)) - -let builtin s = - let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in - match s with - | MainHypothesis -> ns ^ "MainHypothesis" - | InHypothesis -> ns ^ "InHypothesis" - | MainConclusion -> ns ^ "MainConclusion" - | InConclusion -> ns ^ "InConclusion" - | InBody -> ns ^ "InBody" - | Set -> "Set" - | Prop -> "Prop" - | Type -> "Type" - -(* conversion functions from the old constraints ***************************) - -type old_depth = int option - -type r_obj = uri * position * old_depth -type r_rel = position * old_depth -type r_sort = position * old_depth * sort - -type universe = position list option + letin_query (select_query must_query) -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 +(* high-level functions ****************************************************) let query_of_constraints u (musts_obj, musts_rel, musts_sort) (onlys_obj, onlys_rel, onlys_sort) = let conv = function - | None -> [] - | Some i -> [string_of_int i] + | `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 must_obj (r, p, d) = MustObj ([r], [p], conv d) in - let must_sort (p, d, s) = MustSort ([s], [p], conv d) in - let must_rel (p, d) = MustRel ([p], conv d) in - let only_obj (r, p, d) = OnlyObj ([r], [p], conv d) in - let only_sort (p, d, s) = OnlySort ([s], [p], conv d) in - let only_rel (p, d) = OnlyRel ([p], conv d) in + 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 @@ -218,19 +171,19 @@ let query_of_constraints u (musts_obj, musts_rel, musts_sort) let only = (match onlys_obj with | None -> [] - | Some [] -> [OnlyObj ([], [], [])] + | Some [] -> [T.OnlyObj ([], [], [])] | Some l -> List.map only_obj l ) @ (match onlys_rel with | None -> [] - | Some [] -> [OnlyRel ([], [])] + | Some [] -> [T.OnlyRel ([], [])] | Some l -> List.map only_rel l ) @ (match onlys_sort with | None -> [] - | Some [] -> [OnlySort ([], [], [])] + | Some [] -> [T.OnlySort ([], [], [])] | Some l -> List.map only_sort l ) in - let univ = match u with None -> [] | Some l -> [Universe l] in + let univ = match u with None -> [] | Some l -> [T.Universe l] in compose (must @ only @ univ)