1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Ferruccio Guidi <fguidi@cs.unibo.it> *)
34 (******************************************************************************)
41 let out s = if debug then prerr_endline s
44 let SPC = [' ' '\t' '\n']+
45 let ALPHA = ['A'-'Z' 'a'-'z' '_']
47 let IDEN = ALPHA (NUM | ALPHA)*
48 let QSTR = [^ '"' '\\']+
50 rule comm_token = parse
51 | "*)" { query_token lexbuf }
52 | [^ '*']* { comm_token lexbuf }
53 and string_token = parse
55 | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) }
56 | QSTR { STR (Lexing.lexeme lexbuf) }
58 and query_token = parse
59 | "(*" { comm_token lexbuf }
60 | SPC { query_token lexbuf }
61 | '"' { let str = qstr string_token lexbuf in
62 out ("STR " ^ str); STR str }
63 | '(' { out "LP"; LP }
64 | ')' { out "RP"; RP }
65 | '{' { out "LC"; LC }
66 | '}' { out "RC"; RC }
67 | '@' { out "AT"; AT }
68 | '%' { out "PC"; PC }
69 | '$' { out "DL"; DL }
70 | '.' { out "FS"; FS }
71 | ',' { out "CM"; CM }
72 | '/' { out "SL"; SL }
73 | "<-" { out "GETS" ; GETS }
74 | "and" { out "AND" ; AND }
75 | "attr" { out "ATTR" ; ATTR }
76 | "be" { out "BE" ; BE }
77 | "diff" { out "DIFF" ; DIFF }
78 | "eq" { out "EQ" ; EQ }
79 | "ex" { out "EX" ; EX }
80 | "false" { out "FALSE" ; FALSE }
81 | "fun" { out "FUN" ; FUN }
82 | "in" { out "IN" ; IN }
83 | "intersect" { out "INTER" ; INTER }
84 | "inverse" { out "INV" ; INV }
85 | "let" { out "LET" ; LET }
86 | "meet" { out "MEET" ; MEET }
87 | "not" { out "NOT" ; NOT }
88 | "or" { out "OR" ; OR }
89 | "pattern" { out "PAT" ; PAT }
90 | "property" { out "PROP" ; PROP }
91 | "ref" { out "REF" ; REF }
92 | "refof" { out "REFOF" ; REFOF }
93 | "relation" { out "REL" ; REL }
94 | "select" { out "SELECT"; SELECT }
95 | "sub" { out "SUB" ; SUB }
96 | "super" { out "SUPER" ; SUPER }
97 | "true" { out "TRUE" ; TRUE }
98 | "union" { out "UNION" ; UNION }
99 | "where" { out "WHERE" ; WHERE }
100 | IDEN { let id = Lexing.lexeme lexbuf in
101 out ("ID " ^ id); ID id }
102 | eof { out "EOF" ; EOF }
103 and result_token = parse
104 | SPC { result_token lexbuf }
105 | '"' { STR (qstr string_token lexbuf) }