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 | "(*" { comm_token lexbuf; comm_token lexbuf }
53 | ['*' '('] { comm_token lexbuf }
54 | [^ '*' '(']* { comm_token lexbuf }
55 and string_token = parse
57 | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) }
58 | QSTR { STR (Lexing.lexeme lexbuf) }
60 and query_token = parse
61 | "(*" { comm_token lexbuf; query_token lexbuf }
62 | SPC { query_token lexbuf }
63 | '"' { let str = qstr string_token lexbuf in
64 out ("STR " ^ str); STR str }
65 | '(' { out "LP"; LP }
66 | ')' { out "RP"; RP }
67 | '{' { out "LC"; LC }
68 | '}' { out "RC"; RC }
69 | '@' { out "AT"; AT }
70 | '%' { out "PC"; PC }
71 | '$' { out "DL"; DL }
72 | '.' { out "FS"; FS }
73 | ',' { out "CM"; CM }
74 | '/' { out "SL"; SL }
75 | "<-" { out "GETS" ; GETS }
76 | "and" { out "AND" ; AND }
77 | "attr" { out "ATTR" ; ATTR }
78 | "be" { out "BE" ; BE }
79 | "diff" { out "DIFF" ; DIFF }
80 | "eq" { out "EQ" ; EQ }
81 | "ex" { out "EX" ; EX }
82 | "false" { out "FALSE" ; FALSE }
83 | "fun" { out "FUN" ; FUN }
84 | "in" { out "IN" ; IN }
85 | "intersect" { out "INTER" ; INTER }
86 | "inverse" { out "INV" ; INV }
87 | "let" { out "LET" ; LET }
88 | "meet" { out "MEET" ; MEET }
89 | "not" { out "NOT" ; NOT }
90 | "or" { out "OR" ; OR }
91 | "pattern" { out "PAT" ; PAT }
92 | "property" { out "PROP" ; PROP }
93 | "ref" { out "REF" ; REF }
94 | "refof" { out "REFOF" ; REFOF }
95 | "relation" { out "REL" ; REL }
96 | "select" { out "SELECT"; SELECT }
97 | "sub" { out "SUB" ; SUB }
98 | "super" { out "SUPER" ; SUPER }
99 | "true" { out "TRUE" ; TRUE }
100 | "union" { out "UNION" ; UNION }
101 | "where" { out "WHERE" ; WHERE }
102 | IDEN { let id = Lexing.lexeme lexbuf in
103 out ("ID " ^ id); ID id }
104 | eof { out "EOF" ; EOF }
105 and result_token = parse
106 | SPC { result_token lexbuf }
107 | '"' { STR (qstr string_token lexbuf) }