From: Ferruccio Guidi Date: Sat, 22 Jun 2002 17:03:34 +0000 (+0000) Subject: ted version of mQueryGenerator (was mquery part 2) X-Git-Tag: V_0_3_0_debian_8~23 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec899ba2461af8c3f0ef253a8879fc1882b8b46f;p=helm.git ted version of mQueryGenerator (was mquery part 2) --- diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml new file mode 100644 index 000000000..b1c84ce10 --- /dev/null +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -0,0 +1,168 @@ +open MQueryUtil +open MathQL +open Cic + +(* raw HTML representation *) + +let res s = "\"" ^ s ^ "\" " + +let nl () = "
" + +let par () = "

" + +(* 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 = + MQList (MQSelect ("ref", + MQPattern [(None, [MQBSS], [MQFSS])], + MQIs (MQFunc (MQName, "ref"), + MQCons s + ) + ) + ) + in + build_result query + +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'' + diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli new file mode 100644 index 000000000..2d07f4ec4 --- /dev/null +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -0,0 +1,42 @@ +(* 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 *) +(* *) +(* *) +(******************************************************************************) + +val init : unit -> unit (* INIT database function *) + +val close : unit -> unit (* CLOSE database function *) + +val locate : string -> string (* LOCATE query building function *) + +val backward : Cic.term -> int -> string (* BACKWARD query building function *)