(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-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
+module M = MathQL
+module T = MQGTypes
+module U = MQGUtil
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
+(* helpers *****************************************************************)
-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 stat x = M.Fun (["stat"], [], [x])
+let diff x y = M.Fun (["diff"], [], [x; y])
+let union xl = M.Fun (["union"], [], xl)
+let const s = M.Const [(s, [])]
+let intersect xl = M.Fun (["intersect"], [], xl)
+let lnot x = M.Fun (["not"], [], [x])
+let lamp xl = M.Fun (["and"], [], xl)
-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
+(* low level functions *****************************************************)
let locate s =
let query =
M.Property true M.RefineExact ["objectName"] [] [] [] []
- false (M.Const s)
- in M.StatQuery query
+ false (const s)
+ in stat query
+
+let unreferred target_pattern source_pattern =
+ let query =
+ diff
+ (
+ M.Property false M.RefineExact [] [] [] [] []
+ true (const target_pattern)
+ ) (
+ M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
+ true (const source_pattern)
+
+ )
+ in stat query
let compose cl =
let letin = ref [] in
let only = ref true in
let univ = ref [] in
let set_val = function
- | [s] -> M.Const s
+ | [s] -> const s
| l ->
- let msval = M.Set (List.map (fun s -> M.Const s) l) in
+ let msval = union (List.map (fun s -> 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
+ M.SVar vvar
end else msval
in
let cons o (r, s, p, d) =
| 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 "")
+ (cons false c) [] [] false (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"))
+ ! univ cll [] false (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 (const ".*")
else
- iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must
+ intersect ! 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 = lnot (property_only "refObj" ! onlyobj) in
+ let onlysort_val = lnot (property_only "refSort" ! onlysort) in
+ let onlyrel_val = lnot (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, lamp [onlyobj_val; onlysort_val])
+ | _, [], _ -> M.Select ("obj", x, lamp [onlyobj_val; onlyrel_val])
+ | [], _, _ -> M.Select ("obj", x, lamp [onlysort_val; onlyrel_val])
+ | _, _, _ -> M.Select ("obj", x, lamp [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.Let (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 ***************************)
+ stat (letin_query (select_query must_query))
-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
-
-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)
+
projects / helm.git / blobdiff