From: Ferruccio Guidi Date: Tue, 30 Apr 2002 16:52:08 +0000 (+0000) Subject: basic MathQL support X-Git-Tag: V_0_3_0_debian_8~115 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=185fc93ada03ee7e736c90adf165a4f396fb2eba;p=helm.git basic MathQL support --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 5540d5d1a..e2b5d7730 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -4,7 +4,9 @@ logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx -gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo proofEngine.cmo \ - sequentPp.cmo xml2Gdome.cmo -gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx proofEngine.cmx \ - sequentPp.cmx xml2Gdome.cmx +mquery.cmo: mathql.cmo mquery.cmi +mquery.cmx: mathql.cmx mquery.cmi +gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo 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 diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 0b936260c..781704b65 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -14,11 +14,11 @@ all: gTopLevel opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ - cic2acic.ml logicalOperations.ml sequentPp.ml gTopLevel.ml + cic2acic.ml logicalOperations.ml sequentPp.ml mathql.ml mquery.mli mquery.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ - gTopLevel.cmo + mathql.cmo mquery.cmo gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 905de7410..49510a9dd 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -151,7 +151,7 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = (*CSC: We save the innertypes to disk so that we can retrieve them in the *) (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) (*CSC: local. *) - Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ; + Xml.pp xmlinnertypes (Some "/public/fguidi/innertypes") ; let output = applyStylesheets input mml_styles mml_args in output ;; @@ -780,6 +780,29 @@ let check rendering_window scratch_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let locate rendering_window () = + let inputt = (rendering_window#inputt : GEdit.text) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen in + try + output_html outputhtml (Mquery.locate input) ; + inputt#delete_text 0 inputlen + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +let backward rendering_window () = + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let result = + match !ProofEngine.goal with + | None -> "" + | Some (_, (_, t)) -> (Mquery.backward t) + in + output_html outputhtml result + let choose_selection (mmlwidget : GMathView.math_view) (element : Gdome.element option) = @@ -1007,6 +1030,12 @@ class rendering_window output proofw (label : GMisc.label) = let checkb = GButton.button ~label:"Check" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let locateb = + GButton.button ~label:"Locate" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let backwardb = + GButton.button ~label:"Backward" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in let vbox1 = @@ -1082,6 +1111,8 @@ object(self) ignore(stateb#connect#clicked (state self)) ; ignore(openb#connect#clicked (open_ self)) ; ignore(checkb#connect#clicked (check self scratch_window)) ; + ignore(locateb#connect#clicked (locate self)) ; + ignore(backwardb#connect#clicked (backward self)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; ignore(elimintrosb#connect#clicked (elimintros self)) ; diff --git a/helm/gTopLevel/mathql.ml b/helm/gTopLevel/mathql.ml new file mode 100644 index 000000000..2279551c6 --- /dev/null +++ b/helm/gTopLevel/mathql.ml @@ -0,0 +1,104 @@ +(* 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 *) +(* Domenico Lordi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + +exception MQInvalidURI of string +exception MQConnectionFailed of string +exception MQInvalidConnection of string + +(* Input types **************************************************************) +(* main type is mquery *) + +type mqrvar = string (* name *) + +type mqsvar = string (* name *) + +type mquptoken = + | MQString of string (* a constant string *) + | MQSlash (* a slash: '/' *) + | MQAnyChr (* Any single character: '?' *) + | MQAst (* single asterisk: '*' *) + | MQAstAst (* double asterisk: '**' *) + +type mqup = mquptoken list (* uri pattern (helper) *) + +type mqfi = int option * int option + +type mqtref = string * mqup * string * mqfi (* HELM preamble, + uri pattern, + extension, + fragment identifier *) + +type mqpattern = mqtref (* constant pattern *) + +type mqfunc = + | MQName (* NAME *) + +type mqstring = + | MQCons of string (* constant *) + | MQFunc of mqfunc * mqrvar (* function, rvar *) + | MQRVar of mqrvar (* rvar *) + | MQSVar of mqsvar (* svar *) + | MQMConclusion (* main conclusion *) + | MQConclusion (* inner conclusion *) + +type mqbool = + | MQTrue + | MQFalse + | MQAnd of mqbool * mqbool + | MQOr of mqbool * mqbool + | MQNot of mqbool + | MQIs of mqstring * mqstring (* operands *) + +type mqlist = + | MQSelect of mqrvar * mqlist * mqbool (* rvar, list, boolean *) + | MQUse of mqlist * mqsvar (* list, Position attribute *) + | MQPattern of mqpattern (* pattern *) + | MQUnion of mqlist * mqlist (* *) + | MQIntersect of mqlist * mqlist (* *) + +type mquery = + | MQList of mqlist + +(* Output types *************************************************************) +(* main type is mqresult *) + +(* TODO: usare le uri in questo formato *) +type mquref = UriManager.uri * mqfi (* uri, fragment identifier *) + +type mqrefs = mqtref list (* list of references (helper) *) + +type mqresult = + | MQRefs of mqrefs diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml new file mode 100644 index 000000000..e9c50bd08 --- /dev/null +++ b/helm/gTopLevel/mquery.ml @@ -0,0 +1,266 @@ +(* 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 *) +(* *) +(* *) +(******************************************************************************) + +open Mathql +open Cic + +(* string linearization of a reference *) + +let str_uptoken = function + | MQString s -> s + | MQSlash -> "/" + | MQAnyChr -> "?" + | MQAst -> "*" + | MQAstAst -> "**" + +let rec str_up = function + | [] -> "" + | head :: tail -> str_uptoken head ^ str_up tail + +let str_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, x, i) = + p ^ ":/" ^ str_up u ^ "." ^ x ^ 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" + +let out_str = function + | MQCons s -> con s + | MQRVar s -> out_rvar s + | MQSVar 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 ")" + +let rec 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 + | 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 ")" + +let out_query = function + | MQList 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 + try + let j = String.rindex q '.' in + (p, Str.string_before q j, Str.string_after q (j + 1)) + with + Not_found -> (p, q, "") + with + Not_found -> (s, "", "") + +let encode = function + | Str.Text s -> MQString s + | Str.Delim s -> + if s = "?" then MQAnyChr else + if s = "*" then MQAst else + if s = "**" then MQAstAst else + if s = "/" then MQSlash else MQString s + +let tref_uref (u, i) = + let s = UriManager.string_of_uri u in + match split s with + | (p, q, r) -> + let rx = Str.regexp "\?\|\*\*\|\*\|/" in + let l = Str.full_split rx q in + (p, List.map encode l, r, i) + +(* CIC term inspecting functions *) + +let out_ie (r, b) = + let pos = 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) = (tref_uref r, b) + +let ie_eq ((u1, f1), b1) ((u2, f2), b2) = + 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 t c = + let fi = + match (t, c) with + | (None, _) -> (None, None) + | (Some t0, c0) -> (Some (t0 + 1), c0) + in + ie_insert ((uri, fi), main) l + +let rec inspect_term main l = function + | Rel i -> l + | Meta i -> l + | Sort s -> l + | Implicit -> l + | Abst u -> l + | Var u -> inspect_uri main l u None None + | Const (u, i) -> inspect_uri main l u None None + | MutInd (u, i, t) -> inspect_uri main l u (Some t) None + | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) + | Cast (uu, tt) -> + let luu = inspect_term main l uu in + inspect_term false luu tt + | Prod (n, uu, tt) -> + let luu = inspect_term false l uu in + inspect_term false luu tt + | Lambda (n, uu, tt) -> + let luu = inspect_term false l uu in + inspect_term false luu tt + | LetIn (n, uu, tt) -> + let luu = inspect_term false l uu in + inspect_term false luu tt + | Appl m -> inspect_list main l m + | MutCase (u, i, t, tt, uu, m) -> + let lu = inspect_uri main l u (Some t) None in + let ltt = inspect_term false lu tt in + let luu = inspect_term false ltt uu in + inspect_list main luu m + | Fix (i, m) -> inspect_ind l m + | CoFix (i, m) -> inspect_coind l m +and inspect_list main l = function + | [] -> l + | tt :: m -> + let ltt = inspect_term main l tt in + inspect_list false ltt m +and inspect_ind l = function + | [] -> l + | (n, i, tt, uu) :: m -> + let ltt = inspect_term false l tt in + let luu = inspect_term false ltt uu in + inspect_ind luu m +and inspect_coind l = function + | [] -> l + | (n, tt, uu) :: m -> + let ltt = inspect_term false l tt in + let luu = inspect_term false ltt uu in + inspect_coind luu m + +let inspect t = inspect_term true [] t + +(* query building functions *) + +let build_select (r, b) n = + let rvar = "uri" ^ string_of_int n in + let svar = "s" ^ string_of_int n in + let mqs = if b then MQMConclusion else MQConclusion in + MQSelect (rvar, + MQUse (MQPattern r, svar), + MQIs (MQSVar svar, mqs) + ) + +let rec build_inter n = function + | [] -> MQPattern ("cic", [MQAstAst], "con", (None, None)) + | [ie] -> build_select ie n + | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) + +let locate s = + let locate_aux txt = + let query = + MQList (MQSelect ("uri", + MQPattern ("cic", [MQAstAst], "con", (None, None)), + MQIs (MQFunc (MQName, "uri"), + MQCons txt + ) + ) + ) + in + out_query query ^ nl () + in + match Str.split (Str.regexp "[ \t]+") s with + | [] -> "" + | head :: tail -> par () ^ locate_aux head + +let backward t = + let uil = inspect t in + let til = List.map tie_uie uil in + let query = MQList (build_inter 0 til) in + par () ^ out_query query ^ nl () (* par () ^ out_il uil ^ *) diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli new file mode 100644 index 000000000..d7889cb51 --- /dev/null +++ b/helm/gTopLevel/mquery.mli @@ -0,0 +1,45 @@ +(* 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 str_tref : Mathql.mqtref -> string (* string linearization of a tokenized reference *) + +val out_query : Mathql.mquery -> string (* HTML representation of a query *) + +val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *) + +val locate : string -> string (* LOCATE query building function *) + +val backward : Cic.term -> string (* BACKWARD query building function *) +