]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/binaries/transcript/grafiteLexer.mll
Bad variable name fixed.
[helm.git] / helm / software / components / binaries / transcript / grafiteLexer.mll
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 {
27    module O = Options
28    module P = GrafiteParser
29
30    let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s)
31 }
32
33 let SPC   = [' ' '\t' '\n' '\r']+
34 let ALPHA = ['A'-'Z' 'a'-'z']
35 let FIG   = ['0'-'9']
36 let DECOR = "?" | "'" | "`"
37 let IDENT = ALPHA (ALPHA | '_' | FIG )* DECOR*
38
39 rule token = parse
40    | "(*"              { let s = Lexing.lexeme lexbuf in out "OK" s; P.OK s   }
41    | "*)"              { let s = Lexing.lexeme lexbuf in out "CK" s; P.CK s   }
42    | SPC               { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s }
43    | "axiom"           { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
44    | "definition"      { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
45    | "theorem"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
46    | "lemma"           { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
47 (*    
48    | "fact"            { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
49 *)   
50    | "remark"          { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
51    | "variant"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
52    | "inductive"       { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
53    | "coinductive"     { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
54    | "record"          { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
55    | "let rec"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
56    | "let corec"       { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
57    | "notation"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
58    | "interpretation"  { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
59    | "alias"           { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
60    | "coercion"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
61    | "prefer coercion" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
62    | "default"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
63    | "include"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
64    | "inline"          { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
65    | "pump"            { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
66    | "qed"             { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
67    | "elim"            { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
68    | "apply"           { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
69    | "intros"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
70    | "assume"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
71    | "the"             { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
72    | "rewrite"         { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
73    | IDENT             { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s   }
74    | "." SPC           { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }
75    | "."               { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }
76    | _                 { let s = Lexing.lexeme lexbuf in out "RAW" s; P.RAW s }
77    | eof               { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF   }