(*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
;;
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
+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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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)
=
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 =
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)) ;
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* Domenico Lordi <lordi@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <fguidi@cs.unibo.it> *)
+(* 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 = "<font color=\"blue\">" ^ s ^ " </font>"
+
+let sym s = s ^ " "
+
+let sep s = s
+
+let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
+
+let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
+
+let nl () = "<br>"
+
+let par () = "<p>"
+
+(* 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 ^ *)
projects / helm.git / commitdiff