From 7efaa8f1772264f104346c88784eb714b0cb9c8a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 25 Jun 2003 12:28:59 +0000 Subject: [PATCH] It should have already been moved to ocaml/mathql_generator --- helm/gTopLevel/mQueryGenerator.ml | 228 ------------------------------ 1 file changed, 228 deletions(-) delete mode 100644 helm/gTopLevel/mQueryGenerator.ml diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml deleted file mode 100644 index 78ce04e6c..000000000 --- a/helm/gTopLevel/mQueryGenerator.ml +++ /dev/null @@ -1,228 +0,0 @@ -(* 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 *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -(* 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 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.Attribute true M.RefineExact ("objectName", []) (M.Const [s])) in - execute_query q - -let backward e c t level = - 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 (false, M.RefineExact, ("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 - in - let build_select (r, b, v) = - let pos = if b then "MainConclusion" else "InConclusion" in - M.Select ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), M.Ref (M.Const [r]), ["pos"]), - M.Ex ["uri"] (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 -- 2.39.2