From 27602e8f9a442b1effd75cd8f3e8b1f8a8a9d90d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 17 Sep 2002 13:28:50 +0000 Subject: [PATCH] new query generator --- helm/gTopLevel/mQueryGenerator.ml | 385 +++++++++++++---------------- helm/gTopLevel/mQueryGenerator.mli | 23 +- 2 files changed, 189 insertions(+), 219 deletions(-) diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index bb27633bb..7ffe6e208 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -33,215 +33,180 @@ (* *) (******************************************************************************) -open Cic -open MathQL -open MQueryHTML -open MQueryUtil - -(* CIC term inspecting functions ********************************************) - -let env = ref [] (* metasemv *) -let cont = ref [] (* context *) - -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 () - (* FG: si puo' usare xp_str_uref se si vuole xpointer *) - -let rec il_out = function - | [] -> "" - | head :: tail -> ie_out head ^ il_out tail - -let rec il_max = function - | [] -> 0 - | (_, _, v) :: tail -> - let v0 = il_max tail in - if v > v0 then v else v0 - -let ie_str_uri (u, b, v) = xp_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 degree t = - let u0 = CicTypeChecker.type_of_aux' !env !cont t in - let u = CicReduction.whd !cont u0 in - let rec deg = function - | Sort _ -> 1 - | Cast (uu, _) -> deg uu - | Prod (_, _, tt) -> deg tt - | _ -> 2 - in deg u - -let inspect_uri main l uri tc v term = - let d = degree term in - let fi = match tc with - | t0 :: c0 :: _ -> [t0 + 1; c0] - | t0 :: _ -> [t0 + 1] - | [] -> [] - in ie_insert ((uri, fi), main, 2 * v + d - 1) l - -let rec inspect_term main l v term = - match term with - | Rel _ -> l - | Meta (_, _) -> l - | Sort _ -> l - | Implicit -> l - | Var u -> inspect_uri main l u [] v term - | Const (u, _) -> inspect_uri main l u [] v term - | MutInd (u, _, t) -> inspect_uri main l u [t] v term - | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term - | Cast (uu, _) -> - inspect_term main l v uu - | Prod (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term main luu (v + 1) tt - | Lambda (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | LetIn (_, 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, _, 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 - | Fix (_, m) -> inspect_ind l (v + 1) m - | 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_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 - -let rec inspect_backbone = function - | Cast (uu, _) -> inspect_backbone uu - | Prod (_, _, tt) -> inspect_backbone tt - | LetIn (_, uu, tt) -> inspect_backbone tt - | t -> inspect_term true [] 0 t - -let inspect t = inspect_backbone t - -(* query building functions *************************************************) - -let issue = ref (fun _ -> true) - -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_result query = - if ! issue query then - let html = par () ^ out_query query ^ nl () in - let result = Mqint.execute query in - save (html ^ out_result result) - else "" - -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 [xp_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_str_uri 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 init = Mqint.init - -let close = Mqint.close - -let locate_query s = -(*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 - ) - ) - ) - -let locate s = Mqint.execute (locate_query s) -let locate_html s = build_result (locate_query s) - -let levels e c t = - env := e; cont := c; - let il = inspect t in - par () ^ il_out il ^ nl () - -let call_back f = - issue := f +(* level managing functions *************************************************) + +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 -> inspect_uri main l u [] v term + | Cic.Const (u, _) -> inspect_uri main l u [] v term + | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term + | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term + | 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_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 nl = "

\n" + +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 log q r = + let och = open_out_gen mode perm ! log_file in + let str = "Query:" ^ 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; 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.Fun "uri_of_alias" (M.Const [s])) in + execute_query q let backward e c t level = - let t0 = Sys.time () in - env := e; cont := c; - 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 - let r = build_result query'' in - if r <> "" then - begin - print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^ - string_of_float (Sys.time () -. t0) ^ "s"); - par () ^ il_out il ^ r - end else "" + 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 (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 + in + let build_select (r, b, v) = + let pos = if b then "MainConclusion" else "InConclusion" in + M.Select ("uri", + M.Relation (M.ExactOp, "backPointer", M.Ref (M.Const [r]), ["pos"]), + M.Ex (M.Sub (M.Const [pos], M.Record ("uri", "pos"))) + ) + in + let rec build_intersect = function + | [] -> M.Pattern (M.Const [".*"]) + | [hd] -> build_select hd + | hd :: tl -> M.Intersect (build_select hd, build_intersect 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 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 diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli index 69cbfeba5..21202a2e9 100644 --- a/helm/gTopLevel/mQueryGenerator.mli +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -33,17 +33,22 @@ (* *) (******************************************************************************) -val levels : Cic.metasenv -> Cic.context -> Cic.term -> string - (* level assignment testing function *) +exception Discard -val call_back : (MathQL.mquery -> bool) -> unit +type levels_spec = (string * bool * int) list -val init : unit -> unit (* INIT database function *) +val levels_of_term : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec -val close : unit -> unit (* CLOSE database function *) +val string_of_levels : levels_spec -> string -> string -val locate : string -> MathQL.mqresult (* LOCATE query building function *) -val locate_html : string -> string (* LOCATE query building function *) +val set_log_file : string -> unit -val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> string - (* BACKWARD query building function *) +val set_confirm_query : (MathQL.query -> bool) -> unit + +val execute_query : MathQL.query -> MathQL.result + +val locate : string -> MathQL.result + +val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result + +val get_query_info : unit -> string list -- 2.39.2