(* *)
(******************************************************************************)
-(* level managing functions *************************************************)
+(* Query issuing functions **************************************************)
+
+
+
+type uri = string
+type position = string
+type depth = int
+type sort = string
+
+type r_obj = (uri * position * depth option)
+type r_rel = (position* depth)
+type r_sort = (position* depth * sort)
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type can_restrictions = (r_obj list option * r_rel list option * r_sort list option)
+
+
+
+
-type levels_spec = (string * bool * int) list
-let levels_of_term metasenv context term =
- let module TC = CicTypeChecker in
- let module Red = CicReduction in
- let module Util = MQueryUtil in
- let degree t =
- let rec degree_aux = function
- | Cic.Sort _ -> 1
- | Cic.Cast (u, _) -> degree_aux u
- | Cic.Prod (_, _, t) -> degree_aux t
- | _ -> 2
- in
- let u = TC.type_of_aux' metasenv context t in
- degree_aux (Red.whd context u)
- in
- let entry_eq (s1, b1, v1) (s2, b2, v2) =
- s1 = s2 && b1 = b2
- in
- let rec entry_in e = function
- | [] -> [e]
- | head :: tail ->
- head :: if entry_eq head e then tail else entry_in e tail
- in
- let inspect_uri main l uri tc v term =
- let d = degree term in
- entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
- in
- let rec inspect_term main l v term = match term with
- Cic.Rel _ -> l
- | Cic.Meta _ -> l
- | Cic.Sort _ -> l
- | Cic.Implicit -> l
- | Cic.Var (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.Const (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.MutInd (u, t, exp_named_subst) ->
- let l' = inspect_uri main l u [t] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.MutConstruct (u, t, c, exp_named_subst) ->
- let l' = inspect_uri main l u [t; c] v term in
- inspect_exp_named_subst l' (v+1) exp_named_subst
- | Cic.Cast (uu, _) ->
- inspect_term main l v uu
- | Cic.Prod (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term main luu (v + 1) tt
- | Cic.Lambda (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Cic.LetIn (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Cic.Appl m -> inspect_list main l true v m
- | Cic.MutCase (u, t, tt, uu, m) ->
- let lu = inspect_uri main l u [t] (v + 1) term in
- let ltt = inspect_term false lu (v + 1) tt in
- let luu = inspect_term false ltt (v + 1) uu in
- inspect_list main luu false (v + 1) m
- | Cic.Fix (_, m) -> inspect_ind l (v + 1) m
- | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m
- and inspect_list main l head v = function
- | [] -> l
- | tt :: m ->
- let ltt = inspect_term main l (if head then v else v + 1) tt in
- inspect_list false ltt false v m
- and inspect_exp_named_subst l v = function
- [] -> l
- | (_,t) :: tl ->
- let l' = inspect_term false l v t in
- inspect_exp_named_subst l' v tl
- and inspect_ind l v = function
- | [] -> l
- | (_, _, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_ind luu v m
- and inspect_coind l v = function
- | [] -> l
- | (_, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_coind luu v m
- in
- let rec inspect_backbone = function
- | Cic.Cast (uu, _) -> inspect_backbone uu
- | Cic.Prod (_, _, tt) -> inspect_backbone tt
- | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
- | t -> inspect_term true [] 0 t
- in
- inspect_backbone term
-let string_of_levels l sep =
- let entry_out (s, b, v) =
- let pos = if b then " HEAD: " else " TAIL: " in
- string_of_int v ^ pos ^ s ^ sep
- in
- let rec levels_out = function
- | [] -> ""
- | head :: tail -> entry_out head ^ levels_out tail
- in
- levels_out l
-(* Query issuing functions **************************************************)
exception Discard
let locate s =
let module M = MathQL in
- let q = M.Ref (M.Fun "nameObject" (M.Const [s])) in
- execute_query q
+ let q =
+ M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
+ in
+ execute_query q
-let searchPattern e c t level =
+let searchPattern must_use can_use =
let module M = MathQL in
- let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
- let q_where = M.Sub (M.RefOf (
- M.Select ("uri",
- M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
- M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos")))
- )), M.VVar "universe"
- )
- in
- let uri_of_entry (r, b, v) = r in
- let rec restrict level = function
- | [] -> []
- | (u, b, v) :: tail ->
- if v <= level then (u, b, v) :: restrict level tail
- else restrict level tail
+ let in_path s = (s, []) in
+ let assign v p = (in_path v, in_path p) in
+
+ let q_where_obj = function
+ Some l ->
+ 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"
+ )
+ | None -> M.True
+ in
+
+ let q_where_rel = function
+ Some l ->
+ M.And
+ (M.Sub(M.VVar "rel_positions", M.Property(false, M.RefineExact, ("refRel", ["position"]), M.RefOf(M.RVar "uri0"))),
+ M.Sub(M.VVar "rel_depths", M.Property(false, M.RefineExact, ("refRel", ["depth"]), M.RefOf(M.RVar "uri0"))))
+ | None -> M.True
+ in
+
+ let q_where_sort = function
+ Some l ->
+ M.And
+ (M.And
+ (M.Sub(M.VVar "sort_positions", M.Property(false, M.RefineExact, ("refSort", ["position"]), M.RefOf(M.RVar "uri0"))),
+ M.Sub(M.VVar "sort_depths", M.Property(false, M.RefineExact, ("refSort", ["depth"]), M.RefOf(M.RVar "uri0")))),
+ M.Sub(M.VVar "sorts", M.Property(false, M.RefineExact, ("refSort", ["sort"]), M.RefOf(M.RVar "uri0"))))
+ | None -> M.True
in
- let build_select (r, b, v) =
- let pos = if b then "MainConclusion" else "InConclusion" in
- M.Select
+
+ let q_where cr =
+ let (cr_o,cr_r,cr_s) = cr in
+ M.And(M.And(q_where_obj cr_o, q_where_rel cr_r), q_where_sort cr_s)
+
+ in
+
+ let uri_of_entry (r, p, d) = r in
+
+ 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 "pos" "position"]),
+ M.Ex ["uri"]
+ ((M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))))
+ | 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) =
+ M.Select
("uri",
- M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
- M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
- )
+ 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 [dep], M.Record ("uri", in_path "d"))))))
in
- let rec build_intersect = function
- | [] -> M.Pattern (M.Const [".*"])
- | [hd] -> build_select hd
- | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
+
+ let build_select_sort (pos, dep, sor) =
+ 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 [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 levels = levels_of_term e c t in
- let rest = restrict level levels in
- info := [string_of_int (List.length rest)];
- let q_in = build_intersect rest in
- let q_select = M.Select ("uri0", q_in, q_where) in
- let universe = M.Const (List.map uri_of_entry levels) 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 must =
+ 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 lrel
+ | [],[],l3 -> let lsort = List.map tostring_sort l3 in
+ build_intersect_sort lsort
+ | l1,l2,[] -> let lrel = List.map tostring_rel l2 in
+ M.Intersect (build_intersect_obj l1, build_intersect_rel lrel)
+ | l1,[],l3 -> let lsort = List.map tostring_sort l3 in
+ M.Intersect (build_intersect_obj l1, build_intersect_sort lsort)
+ | [],l2,l3 -> let lrel = List.map tostring_rel l2 in
+ let lsort = List.map tostring_sort l3 in
+ M.Intersect (build_intersect_rel lrel, build_intersect_sort lsort)
+ | _ -> 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 lrel), build_intersect_sort lsort)
+ in
+
+ let q_in = build_intersect must_use in
+ let q_select = M.Select ("uri0", q_in, q_where can_use) in
+
+ let (cr_o,cr_r,cr_s) = can_use in
+
+ let universe =
+ match cr_o with
+ None -> M.Const []
+ | Some cr_o -> M.Const (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 opos =
+ match cr_o with
+ None -> M.Const []
+ | Some cr_o -> M.Const (List.map tsnd cr_o) in
+
+ let odep =
+ match cr_o with
+ None -> M.Const []
+ | Some cr_o -> let lofc = List.map trd cr_o in
+ let f l c =
+ match c with
+ None -> l
+ | Some c -> l@[c]
+ in
+ let lof_dep_int = List.fold_left f [] lofc in
+ M.Const(List.map string_of_int lof_dep_int)
+ in
+
+ let rpos =
+ match cr_r with
+ None -> M.Const []
+ | Some cr_r -> M.Const (List.map fst cr_r) in
+
+ let rdep =
+ match cr_r with
+ None -> M.Const []
+ | Some cr_r -> let rdep_int = List.map snd cr_r in
+ M.Const (List.map string_of_int rdep_int)
+ in
+
+
+ let spos =
+ match cr_s with
+ None -> M.Const []
+ | Some cr_s -> M.Const (List.map tfst cr_s) in
+
+
+ let sdep =
+ match cr_s with
+ None -> M.Const []
+ | Some cr_s -> let sdep_int = List.map tsnd cr_s in
+ M.Const (List.map string_of_int sdep_int)
+ in
+
+
+ let sor =
+ match cr_s with
+ None -> M.Const[]
+ | Some cr_s -> M.Const (List.map trd cr_s) in
+
let q_let_u = M.LetVVar ("universe", universe, q_select) in
- let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
- execute_query q_let_p
+
+ let q_let_s = M.LetVVar ("sorts", sor, q_let_u) in
+
+ let q_let_ds = M.LetVVar ("sort_depths", sdep, q_let_s) in
+
+ let q_let_dr = M.LetVVar ("rel_depths", rdep, q_let_ds) in
+
+ let q_let_do = M.LetVVar ("obj_depths", odep, q_let_dr) in
+
+ let q_let_ps = M.LetVVar ("sort_positions", spos, q_let_do) in
+
+ let q_let_pr = M.LetVVar ("rel_positions", rpos, q_let_ps) in
+
+ let q_let_po = M.LetVVar ("obj_positions", opos, q_let_pr) in
+print_endline ("### " ^ MQueryUtil.text_of_query q_let_po) ; flush stdout;
+ execute_query q_let_po
projects / helm.git / blobdiff