* http://cs.unibo.it/helm/.
*)
-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
-
-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 = ns ^ "Set" then "$SET" else
- if s = ns ^ "Prop" then "$PROP" else
- if s = ns ^ "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
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
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
| 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
| [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
- | "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")
-
-(* 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
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)