"
-
-(* CIC term inspecting functions *)
-
-let ie_out (r, b, v) =
- let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
- res (pos ^ str_uref r) ^ nl ()
-
-let rec il_out = function
- | [] -> ""
- | head :: tail -> ie_out head ^ il_out tail
-
-let ie_struri (u, b, v) = str_uref u
-
-let rec il_restrict level = function
- | [] -> []
- | (u, b, v) :: tail ->
- if v <= level then (u, b, v) :: il_restrict level tail
- else il_restrict level tail
-
-let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
- UriManager.eq u1 u2 && f1 = f2 && b1 = b2
-
-let rec ie_insert ie = function
- | [] -> [ie]
- | head :: tail ->
- head :: if ie_eq head ie then tail else ie_insert ie tail
-
-let inspect_uri main l uri tc v =
- let fi = match tc with
- | t0 :: c0 :: _ -> [t0 + 1; c0]
- | t0 :: _ -> [t0 + 1]
- | [] -> []
- in ie_insert ((uri, fi), main, v) l
-
-let rec inspect_term main l v = function
- | Rel i -> l
- | Meta (i, _) -> l
- | Sort s -> l
- | Implicit -> l
- | Var u -> inspect_uri main l u [] v
- | Const (u, i) -> inspect_uri main l u [] v
- | MutInd (u, i, t) -> inspect_uri main l u [t] v
- | MutConstruct (u, i, t, c) -> inspect_uri main l u [t; c] v
- | Cast (uu, _) ->
- (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
- inspect_term main l v uu
- | Prod (n, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Lambda (n, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | LetIn (n, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Appl m -> inspect_list main l true v m
- | MutCase (u, i, t, tt, uu, m) ->
- let lu = inspect_uri main l u [t] (v + 1) 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
- | Fix (i, m) -> inspect_ind l (v + 1) m
- | CoFix (i, 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_ind l v = function
- | [] -> l
- | (n, i, 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
- | (n, 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
-
-let inspect t = inspect_term true [] 0 t
-
-(* query building functions *)
-
-let save s =
- let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
- (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
- output_string och s; flush och; s
-
-let build_select (r, b, v) n =
- let rvar = "ref" ^ string_of_int n in
- let svar = "str" ^ string_of_int n in
- let mqs = if b then MQMConclusion else MQConclusion in
- MQSelect (rvar,
- MQUse (MQReference [str_uref r], svar),
- MQIs (MQStringSVar svar, mqs)
- )
-
-let rec build_inter n = function
- | [] -> MQPattern [(None, [MQBSS], [MQFSS])]
- | [ie] -> build_select ie n
- | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
-
-let restrict_universe query =
- function
- [] -> query (* no constraints ===> the universe is the library *)
- | l ->
- let universe =
- MQReference (List.map ie_struri l)
- in
- MQLetIn (
- "universe", universe,
- MQSelect (
- "uri", query,
- MQSubset (
- MQSelect (
- "uri2",
- MQUsedBy (MQListRVar "uri", "pos"),
- MQOr (
- MQIs (MQStringSVar "pos", MQConclusion),
- MQIs (MQStringSVar "pos", MQMConclusion)
- )
- ),
- MQListLVar "universe"
- )
- )
- )
-
-let build_result query =
- let html = par () ^ out_query query ^ nl () in
- let result = Mqint.execute query in
- save (html ^ out_result result)
-
-let init = Mqint.init
-
-let close = Mqint.close
-
-let locate s =
- let query =
-(*CSC: next query to be fixed
- 1) I am exploiting the bug that does not quote '|'
- 2) I am searching only constants and mutual inductive definition blocks
- (i.e. no fragment identifier at all)
-*)
- MQList (MQSelect ("ref",
- MQPattern [(Some "cic", [MQBSS ; MQBC ".con|.ind"],[])],
- MQIs (MQFunc (MQName, "ref"),
- MQCons s
- )
- )
- )
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Ferruccio Guidi \n"
+
+let query_num = ref 1
+
+let log_file = ref ""
+
+let confirm_query = ref (fun _ -> true)
+
+let info = ref []
+
+let set_log_file f =
+ log_file := f
+
+let set_confirm_query f =
+ confirm_query := f
+
+let get_query_info () = ! info
+
+let execute_query query =
+ let module Util = MQueryUtil in
+ let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
+ let perm = 64 * 6 + 8 * 6 + 4 in
+ let time () =
+ let lt = Unix.localtime (Unix.time ()) in
+ "NEW LOG: " ^
+ string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
+ string_of_int (lt.Unix.tm_hour) ^ ":" ^
+ string_of_int (lt.Unix.tm_min) ^ ":" ^
+ string_of_int (lt.Unix.tm_sec)
+ in
+ let log q r =
+ let och = open_out_gen mode perm ! log_file in
+ if ! query_num = 1 then output_string och (time () ^ nl);
+ let str =
+ "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
+ "Result:" ^ nl ^ Util.text_of_result r nl in
+ output_string och str;
+ flush och
+ in
+ let execute q =
+ let r = Mqint.execute q in
+ if ! log_file <> "" then log q r;
+ info := string_of_int ! query_num :: ! info;
+ incr query_num;
+ r
+ in
+ if ! confirm_query query then execute query else raise Discard
+
+(* Query building functions ************************************************)
+
+let locate s =
+ let module M = MathQL in
+ let q =
+ M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
in
- build_result query
+ execute_query q
+
+let searchPattern must_use can_use =
+ let module M = MathQL in
+ 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 -> 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
+
+ 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 -> 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 -> 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_rel = function
+ Some l ->
+ let q0 =
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refRel", ["position"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar "rel_positions")
+ in
+ if rdep = [] then q0
+ else
+ M.And
+ (q0,
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refRel", ["depth"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar "rel_depths"))
+ | None -> M.True
+ in
+
+ let q_where_sort = function
+ Some l ->
+ let q0 =
+ M.And
+ (M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["position"]),
+ M.RefOf(M.RVar "uri0")
+ ),
+ M.VVar "sort_positions"),
+ M.Sub
+ (M.Property
+ (false, M.RefineExact, ("refSort", ["sort"]),
+ M.RefOf(M.RVar "uri0")),
+ M.VVar "sorts"))
+ in
+ if sdep = [] then
+ q0
+ else
+ M.And
+ (q0,
+ M.Sub
+ (M.VVar "sort_depths",
+ M.Property
+ (false, M.RefineExact, ("refSort", ["depth"]),
+ M.RefOf(M.RVar "uri0"))))
+ | None -> M.True
+ in
+
+ 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
+
+(* 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 "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) =
+ 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 q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in
+
+ let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in
+
+ let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in
-let backward t level =
- let il = inspect t in
- let query = build_inter 0 (il_restrict level il) in
- let query' = restrict_universe query il in
- let query'' = MQList query' in
- par () ^ il_out il ^ build_result query''
+ let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in
+
+ let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in
+
+ let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in
+ let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in
+print_endline ("### " ^ MQueryUtil.text_of_query q_let_po) ; flush stdout;
+ execute_query q_let_po