X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;fp=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=c5a8382fec9d3ce0a537900833c32cae736abce4;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml deleted file mode 100644 index c5a8382fe..000000000 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ /dev/null @@ -1,155 +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 *) -(* *) -(* *) -(******************************************************************************) - -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