From: Ferruccio Guidi Date: Sat, 22 Jun 2002 17:01:41 +0000 (+0000) Subject: untested version of mQueryGenerator (was mquery part 2) X-Git-Tag: V_0_3_0_debian_8~24 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b2b968e27508993b1716810c2c27ff532e284742 untested version of mQueryGenerator (was mquery part 2) --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 4ffdddf54..13d6f74d5 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -10,9 +10,9 @@ logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx -mquery.cmo: mquery.cmi -mquery.cmx: mquery.cmi -gTopLevel.cmo: cic2Xml.cmo cic2acic.cmi logicalOperations.cmo mquery.cmi \ - proofEngine.cmo sequentPp.cmo xml2Gdome.cmo -gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx mquery.cmx \ - proofEngine.cmx sequentPp.cmx xml2Gdome.cmx +mQueryGenerator.cmo: mQueryGenerator.cmi +mQueryGenerator.cmx: mQueryGenerator.cmi +gTopLevel.cmo: cic2Xml.cmo cic2acic.cmi logicalOperations.cmo \ + mQueryGenerator.cmi proofEngine.cmo sequentPp.cmo xml2Gdome.cmo +gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \ + mQueryGenerator.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 0fc38eac9..121d94f50 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -17,11 +17,12 @@ opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ cic2Xml.ml cic2acic.mli logicalOperations.ml sequentPp.ml \ - mquery.mli mquery.ml gTopLevel.ml + mQueryGenerator.mli mQueryGenerator.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo + logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ + gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4a8b0a382..d052040c5 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1072,7 +1072,7 @@ let locate rendering_window () = | [] -> "" | head :: tail -> inputt#delete_text 0 inputlen; - Mquery.locate head + MQueryGenerator.locate head with e -> "

" ^ Printexc.to_string e ^ "

" ) @@ -1096,7 +1096,7 @@ let backward rendering_window () = let (_,_,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - Mquery.backward ty level + MQueryGenerator.backward ty level in output_html outputhtml result @@ -1471,8 +1471,8 @@ let initialize_everything () = let _ = CicCooking.init () ; - Mquery.init () ; + MQueryGenerator.init () ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - Mquery.close () + MQueryGenerator.close () ;; diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml deleted file mode 100644 index 3e5548c68..000000000 --- a/helm/gTopLevel/mquery.ml +++ /dev/null @@ -1,324 +0,0 @@ -open MathQL -open Cic - -(* string linearization of a reference *) - -let str_uptoken = function - | MQBC s -> s - | MQBD -> "/" - | MQBQ -> "?" - | MQBS -> "*" - | MQBSS -> "**" - -let rec str_up = function - | [] -> "" - | head :: tail -> str_uptoken head ^ str_up tail - -let str_fi fi = - "#1/" ^ - String.concat "/" - (List.map - (function - MQFC n -> string_of_int n - | MQFS -> "*" - | MQFSS -> "**" - ) fi) - - function - | (None, _) -> "" - | (Some t, None) -> "#1/" ^ string_of_int t - | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c - -let str_tref (p, u, i) = - let p = - match p with - None -> "*" - | Some s -> s - in - p ^ ":/" ^ str_up u ^ str_fi i - -let str_uref (u, i) = - UriManager.string_of_uri u ^ str_fi i - -(* raw HTML representation *) - -let key s = "" ^ s ^ " " - -let sym s = s ^ " " - -let sep s = s - -let con s = "\"" ^ s ^ "\" " - -let res s = "\"" ^ s ^ "\" " - -let nl () = "
" - -let par () = "

" - -(* HTML representation of a query *) - -let out_rvar s = sym s - -let out_svar s = sep "$" ^ sym s - -let out_tref r = con (str_tref r) - -let out_pat p = out_tref p - -let out_func = function - | MQName -> key "name" - | _ -> assert false - -let out_str = function - | MQCons s -> con s - | MQStringRVar s -> out_rvar s - | MQStringSVar s -> out_svar s - | MQFunc (f, r) -> out_func f ^ out_rvar r - | MQMConclusion -> key "mainconclusion" - | MQConclusion -> key "conclusion" - -let rec out_bool = function - | MQTrue -> key "true" - | MQFalse -> key "false" - | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t - | MQNot b -> key "not" ^ out_bool b - | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")" - | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")" - | MQSetEqual (l1, l2) -> - sep "(" ^ out_list l1 ^ key "setequal" ^ out_list l2 ^ sep ")" - | MQSubset (l1, l2) -> - sep "(" ^ out_list l1 ^ key "subset" ^ out_list l2 ^ sep ")" - -and out_list = function - | MQSelect (r, l, b) -> - key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b - | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v - | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v - | MQPattern p -> key "pattern" ^ out_pat p - | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")" - | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")" - | MQListRVar v -> key "rvaroccur" ^ v - | MQLetIn (v, l1, l2) -> - key "let " ^ out_rvar v ^ " = " ^ out_list l1 ^ key " in " ^ out_list l2 - | MQListLVar v -> out_rvar v - -let out_query = function - | MQList l -> out_list l - -(* HTML representation of a query result *) - -let rec out_list = function - | [] -> "" - | u :: l -> res u ^ nl () ^ out_list l - -let out_result qr = - par () ^ "Result:" ^ nl () ^ - match qr with - | MQRefs l -> out_list l - -(* Converting functions *) - -let split s = - try - let i = Str.search_forward (Str.regexp_string ":/") s 0 in - let p = Str.string_before s i in - let q = Str.string_after s (i + 2) in - (p, q) - with - Not_found -> (s, "") - -let encode = function - | Str.Text s -> MQBC s - | Str.Delim s -> - if s = "?" then MQBQ else - if s = "*" then MQBS else - if s = "**" then MQBSS else - if s = "/" then MQBD else MQBC s - -let tref_uref (u, i) = - let s = UriManager.string_of_uri u in - match split s with - | (p, q) -> - let rx = Str.regexp "\?\|\*\*\|\*\|/" in - let l = Str.full_split rx q in - (Some p, List.map encode l, i) - -(* CIC term inspecting functions *) - -let out_ie (r, b, v) = - let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in - res (pos ^ str_uref r) ^ nl () ^ - con (pos ^ str_tref (tref_uref r)) ^ nl () - -let rec out_il = function - | [] -> "" - | head :: tail -> out_ie head ^ out_il tail - -let tie_uie (r, b, v) = (tref_uref r, b, v) - -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 level = ref 0 - -(*CSC: che brutto il codice imperativo!!!*) -let universe = ref [];; - -let inspect_uri main l uri t c v = - let fi = - match (t, c) with - | (None, _) -> [] - | (Some t0, Some c0) -> [MQFC (t0 + 1); MQFC c0] - | (Some t0, None) -> [MQFC (t0 + 1)] - in -(*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *) - universe := (tref_uref (uri,fi))::!universe ; - if v > !level then - l - else - 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 None None v - | Const (u, i) -> inspect_uri main l u None None v - | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v - | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some 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 (Some t) None (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) "mquery.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 (MQPattern r, svar), - MQIs (MQStringSVar svar, mqs) - ) - -let rec build_inter n = function - | [] -> MQPattern (Some "cic", [MQBSS; MQBC ".con"], []) - | [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 = - (*CSC: Usare tante Union e Pattern per fare un insieme di uri mi *) - (*CSC: sembra un poco penoso. Inoltre creo un albero completamente *) - (*CSC: sbilanciato, aumentando il costo della risoluzione della *) - (*CSC: query. *) - let rec compose_universe = - function - [] -> assert false - | [uri] -> MQPattern uri - | uri::tl -> MQUnion(MQPattern uri, compose_universe tl) - in - compose_universe !universe - 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 (Some "cic", [MQBSS ; MQBC ".con"], []), - MQIs (MQFunc (MQName, "ref"), - MQCons s - ) - ) - ) - in - build_result query - -let backward t n = - level := n ; - universe := [] ; - let uil = inspect t in - let til = List.map tie_uie uil in - let query = build_inter 0 til in - let query' = restrict_universe query til in - let query'' = MQList query' in - par () ^ out_il uil ^ build_result query'' -;; diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli deleted file mode 100644 index 2d07f4ec4..000000000 --- a/helm/gTopLevel/mquery.mli +++ /dev/null @@ -1,42 +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 *) -(* *) -(* *) -(******************************************************************************) - -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 *)