* 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 =
false (M.Const s)
in M.StatQuery 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 M.StatQuery query
+
let compose cl =
let letin = ref [] in
let must = 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] []
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
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
-
-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