* http://cs.unibo.it/helm/.
*)
-(* Query issuing functions **************************************************)
-
type uri = string
type position = string
-type depth = int option
+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
-type r_obj = (uri * position * depth)
-type r_rel = (position* depth)
-type r_sort = (position* depth * sort)
+module M = MathQL
-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 locate s =
+ let query =
+ M.Property true M.RefineExact ["objectName"] [] [] [] []
+ false (M.Const s)
+ in M.StatQuery 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 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" s @
+ con "h:position" p @ con "h:depth" d
+ in
+ let property_must n c =
+ 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"))
+ in
+ let rec aux = function
+ | [] -> ()
+ | Universe l :: tail ->
+ only := true; univ := [(false, ["h:position"], set_val l)]; aux tail
+ | MustObj r p d :: tail ->
+ must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
+ | MustSort s p d :: tail ->
+ must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
+ | MustRel p d :: tail ->
+ must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
+ | OnlyObj r p d :: tail ->
+ onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
+ | OnlySort s p d :: tail ->
+ onlysort := ([], s, p, d) :: ! onlysort; aux tail
+ | OnlyRel p d :: tail ->
+ onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
+ in
+ 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
+ text_of_spec prerr_string cl;
+ 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
+ M.StatQuery (letin_query (select_query must_query))
let builtin s =
- let ns = "h:" in
+ let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
match s with
| "MH" -> ns ^ "MainHypothesis"
| "IH" -> ns ^ "InHypothesis"
| "TYPE" -> ns ^ "Type"
| _ -> raise (Failure "MQueryGenerator.builtin")
-(* Query building functions ************************************************)
-
-module M = MathQL
-
-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
-
- 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 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
+(* 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
-
- 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
-
-
-
-
- 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)
- in
-
- let build_intersect = function
-(* let tostring_sort (a,b,c) =
- let b1 = string_of_int b in
- (a,b1,c)
- 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))
- 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))
- 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))
- in
-
+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
-(* 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))
+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]
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 (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 = 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 [] -> [OnlyObj ([], [], [])]
+ | Some l -> List.map only_obj l
+ ) @
+ (match onlys_rel with
+ | None -> []
+ | Some [] -> [OnlyRel ([], [])]
+ | Some l -> List.map only_rel l
+ ) @
+ (match onlys_sort with
+ | None -> []
+ | Some [] -> [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 -> [Universe l] in
+ compose (must @ only @ univ)