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/.
28 module P = Gallina8Parser
30 let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s)
33 let c = Char.code s.[0] in
34 if c <= 127 then s else
35 let escaped = Printf.sprintf "\\%3u\\" c in
37 if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped;
43 let SPC = [' ' '\t' '\n' '\r']+
44 let ALPHA = ['A'-'Z' 'a'-'z' '_']
46 let ID = ALPHA (ALPHA | FIG | "\'")*
47 let RAWID = QT [^ '"']* QT
51 | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s }
52 | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
53 | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
54 | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
55 | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
56 | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
57 | "CoFixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
58 | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
59 | "Save" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
60 | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
61 | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s }
62 | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
63 | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
64 | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
65 | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
66 | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s }
67 | "Parameter" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s }
68 | "Parameters" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s }
69 | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s }
70 | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s }
71 | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s }
72 | "Scheme" { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s }
73 | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
74 | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s }
75 | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
76 | "Hints" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
77 | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
78 | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
79 | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
80 | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
81 | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
82 | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
83 | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
84 | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s }
85 | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s }
86 | "Import" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s }
87 | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s }
88 | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
89 | "Reset" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
90 | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
91 | "Delimit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
92 | "Bind" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
93 | "Arguments" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
94 | "Open" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
95 | "V7only" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
96 | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
97 | "Reserved" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
98 | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
99 | "Grammar" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
100 | "Syntax" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
101 | "Add" SPC "Morphism"
102 { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s }
103 | "Add" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
104 | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s }
105 | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s }
106 | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s }
107 | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s }
108 | "with" { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s }
109 | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s }
110 | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s }
111 | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s }
112 | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s }
113 | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s }
114 | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s }
115 | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s }
116 | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s }
117 | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s }
118 | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s }
119 | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s }
120 | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s }
121 | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s }
122 | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s }
123 | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s }
124 | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s }
125 | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s }
126 | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s }
128 { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s }
129 | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF }