(* 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 (* string linearization of a reference *) let str_btoken = function | MQBC s -> s | MQBD -> "/" | MQBQ -> "?" | MQBS -> "*" | MQBSS -> "**" let str_ftoken = function | MQFC i -> "/" ^ string_of_int i | MQFS -> "/*" | MQFSS -> "/**" let str_prot = function | Some s -> s | None -> "*" let rec str_body = function | [] -> "" | head :: tail -> str_btoken head ^ str_body tail let str_frag l = let rec str_fi start = function | [] -> "" | t :: l -> (if start then "#1" else "") ^ str_ftoken t ^ str_fi false l in str_fi true l let str_tref (p, b, i) = str_prot p ^ ":/" ^ str_body b ^ str_frag i let str_uref (u, i) = let rec str_fi start = function | [] -> "" | i :: l -> (if start then "#1" else "") ^ string_of_int i ^ str_fi false l in UriManager.string_of_uri u ^ str_fi true i (* raw HTML representation *) let key s = "" ^ s ^ " " let sym s = s ^ " " let sep s = s let str s = "'" ^ s ^ "' " let pat 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 = pat (str_tref r) let out_pat p = out_tref p let out_func = function | MQName -> key "name" let out_str = function | MQCons s -> str 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 | 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 ")" 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 tref_uref u = let s = str_uref u in MQueryTParser.ref MQueryTLexer.rtoken (Lexing.from_string s) let parse_text ch = let lexbuf = Lexing.from_channel ch in MQueryTParser.query MQueryTLexer.qtoken lexbuf