From 6c04191a9045120d3cf5f6046eee627d6499e5c9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 22 May 2002 16:54:11 +0000 Subject: [PATCH] textual parser and other utilities for mathql --- helm/ocaml/mathql/.depend | 8 ++ helm/ocaml/mathql/Makefile | 16 +++ helm/ocaml/mathql/mQueryTLexer.mll | 88 ++++++++++++++++ helm/ocaml/mathql/mQueryTParser.mly | 119 +++++++++++++++++++++ helm/ocaml/mathql/mQueryUtil.ml | 155 ++++++++++++++++++++++++++++ helm/ocaml/mathql/mQueryUtil.mli | 44 ++++++++ helm/ocaml/mathql/mathQL.ml | 107 +++++++++++++++++++ 7 files changed, 537 insertions(+) create mode 100644 helm/ocaml/mathql/.depend create mode 100644 helm/ocaml/mathql/Makefile create mode 100644 helm/ocaml/mathql/mQueryTLexer.mll create mode 100644 helm/ocaml/mathql/mQueryTParser.mly create mode 100644 helm/ocaml/mathql/mQueryUtil.ml create mode 100644 helm/ocaml/mathql/mQueryUtil.mli create mode 100644 helm/ocaml/mathql/mathQL.ml diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend new file mode 100644 index 000000000..0d8aa0719 --- /dev/null +++ b/helm/ocaml/mathql/.depend @@ -0,0 +1,8 @@ +mQueryTParser.cmi: mathQL.cmo +mQueryUtil.cmi: mathQL.cmo +mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi +mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi +mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi +mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi +mQueryTLexer.cmo: mQueryTParser.cmi +mQueryTLexer.cmx: mQueryTParser.cmx diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile new file mode 100644 index 000000000..52a5eb155 --- /dev/null +++ b/helm/ocaml/mathql/Makefile @@ -0,0 +1,16 @@ +PACKAGE = mathql +REQUIRES = helm-urimanager +PREDICATES = + +INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli + +IMPLEMENTATION_FILES = mathQL.ml $(INTERFACE_FILES:%.mli=%.ml) \ + mQueryTLexer.ml + +EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ + mQueryTLexer.mll mQueryTParser.mly + +EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ + mQueryTLexer.ml + +include ../Makefile.common diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll new file mode 100644 index 000000000..0075f3ac1 --- /dev/null +++ b/helm/ocaml/mathql/mQueryTLexer.mll @@ -0,0 +1,88 @@ +(* 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 *) +(* 23/05/2002 *) +(* *) +(* *) +(******************************************************************************) + +{ + open MQueryTParser +} + +let SPC = [' ' '\t' '\n']+ +let ALPHA = ['A'-'Z' 'a'-'z'] +let NUM = ['0'-'9'] +let IDEN = ALPHA (NUM | ALPHA)* +let DQ = '"' +let SQ = ''' +let QSTR = [^ ''']* +let USTR = [^ '"' ':' '/' '#' '?' '*']+ + +rule rtoken = parse + | DQ { DQT } + | ":/" { PROT } + | "/" { SLASH } + | "#1" { FRAG } + | "?" { QUEST } + | "**" { SSTAR } + | "*" { STAR } + | USTR { STR (Lexing.lexeme lexbuf) } +and stoken = parse + | SQ { SQT } + | QSTR { STR (Lexing.lexeme lexbuf) } +and qtoken = parse + | SPC { qtoken lexbuf } + | '(' { LPR } + | ')' { RPR } + | '$' { DLR } + | SQ { STR (qstr stoken lexbuf) } + | DQ { REF (ref rtoken lexbuf) } + | "name" { NAME } + | "mainconclusion" { MCONCL } + | "conclusion" { CONCL } + | "true" { TRUE } + | "false" { FALSE } + | "and" { AND } + | "or" { OR } + | "not" { NOT } + | "is" { IS } + | "select" { SELECT } + | "in" { IN } + | "where" { WHERE } + | "use" { USE } + | "position" { POS } + | "usedby" { USEDBY } + | "pattern" { PATT } + | "union" { UNION } + | "intersect" { INTER } + | IDEN { ID (Lexing.lexeme lexbuf) } + | eof { EOF } + diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly new file mode 100644 index 000000000..dea5f4883 --- /dev/null +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -0,0 +1,119 @@ +/* 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 */ +/* 23/05/2002 */ +/* */ +/* */ +/******************************************************************************/ + +%{ + open MathQL +%} + %token ID STR + %token REF + %token LPR RPR DLR SQT DQT EOF PROT SLASH FRAG QUEST STAR SSTAR + %token NAME + %token MCONCL CONCL + %token TRUE FALSE AND OR NOT IS + %token SELECT IN WHERE USE POS USEDBY PATT UNION INTER + %left OR UNION + %left AND INTER + %nonassoc NOT + %start qstr ref query + %type qstr + %type ref + %type query +%% + prot: + | STR { Some $1 } + | STAR { None } + ; + body: + | { [] } + | SLASH body { MQBD :: $2 } + | QUEST body { MQBQ :: $2 } + | SSTAR body { MQBSS :: $2 } + | STAR body { MQBS :: $2 } + | STR body { MQBC $1 :: $2 } + frag: + | { [] } + | SLASH SSTAR frag { MQFSS :: $3 } + | SLASH STAR frag { MQFS :: $3 } + | SLASH STR frag { try let i = int_of_string $2 in + if i < 1 then raise Parsing.Parse_error; + MQFC i :: $3 + with e -> raise Parsing.Parse_error + } + ; + ref: + | prot PROT body DQT { ($1, $3, []) } + | prot PROT body FRAG frag DQT { ($1, $3, $5) } + ; + qstr: + | STR SQT { $1 } + ; + rvar: + | ID { $1 } + ; + svar: + | DLR ID { $2 } + ; + func: + | NAME { MQName } + ; + str: + | MCONCL { MQMConclusion } + | CONCL { MQConclusion } + | STR { MQCons $1 } + | rvar { MQRVar $1 } + | svar { MQSVar $1 } + | func rvar { MQFunc ($1, $2) } + ; + boole: + | TRUE { MQTrue } + | FALSE { MQFalse } + | str IS str { MQIs ($1, $3) } + | NOT boole { MQNot $2 } + | boole AND boole { MQAnd ($1, $3) } + | boole OR boole { MQOr ($1, $3) } + | LPR boole RPR { $2 } + ; + rlist: + | PATT REF { MQPattern $2 } + | rlist UNION rlist { MQUnion ($1, $3) } + | rlist INTER rlist { MQIntersect ($1, $3) } + | USE rlist POS svar { MQUse ($2, $4) } + | USEDBY rlist POS svar { MQUsedBy ($2, $4) } + | SELECT rvar IN rlist WHERE boole { MQSelect ($2, $4, $6) } + | LPR rlist RPR { $2 } + ; + query: + rlist EOF { MQList $1 } + ; diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml new file mode 100644 index 000000000..c5a8382fe --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -0,0 +1,155 @@ +(* 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 diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli new file mode 100644 index 000000000..139cb0181 --- /dev/null +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -0,0 +1,44 @@ +(* 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_uref : MathQL.mquref -> string (* string linearization of a UriManager reference *) + +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 parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *) diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml new file mode 100644 index 000000000..d1e89decf --- /dev/null +++ b/helm/ocaml/mathql/mathQL.ml @@ -0,0 +1,107 @@ +(* 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 mqpt = string option (* PROTOCOL TOKENS *) + (* Some = constant string *) + (* None = single star: '*' *) + +type mqbt = (* BODY TOKENS *) + | MQBC of string (* a constant string *) + | MQBD (* a slash: '/' *) + | MQBQ (* a question mark: '?' *) + | MQBS (* a single star: '*' *) + | MQBSS (* a double star: '**' *) + +type mqft = (* FRAGMENT TOKENS *) + | MQFC of int (* a constant integer *) + | MQFS (* a single star: '*' *) + | MQFSS (* a double star: '**' *) + +type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized reference *) + +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 *) + | MQUsedBy of mqlist * mqsvar (* list, Position attribute *) + | MQPattern of mqpattern (* pattern *) + | MQUnion of mqlist * mqlist (* operands *) + | MQIntersect of mqlist * mqlist (* operands *) + +type mquery = + | MQList of mqlist + +(* Output types *************************************************************) +(* main type is mqresult *) + +(* TODO: usare le uri in questo formato *) +type mquref = UriManager.uri * (int list) (* uri, fragment identifier *) + +type mqrefs = string list (* list of references (helper) *) + +type mqresult = + | MQRefs of mqrefs -- 2.39.2