1(****************************************************************************)
2(* Copyright (C) 2007-2009 Gacek                                            *)
3(* Copyright (C) 2013-2018 Inria (Institut National de Recherche            *)
4(*                         en Informatique et en Automatique)               *)
5(*                                                                          *)
6(* This file is part of Abella.                                             *)
7(*                                                                          *)
8(* Abella is free software: you can redistribute it and/or modify           *)
9(* it under the terms of the GNU General Public License as published by     *)
10(* the Free Software Foundation, either version 3 of the License, or        *)
11(* (at your option) any later version.                                      *)
12(*                                                                          *)
13(* Abella is distributed in the hope that it will be useful,                *)
14(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
15(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
16(* GNU General Public License for more details.                             *)
17(*                                                                          *)
18(* You should have received a copy of the GNU General Public License        *)
19(* along with Abella.  If not, see <http://www.gnu.org/licenses/>.          *)
20(****************************************************************************)
21
22{
23  open Parser
24  open Lexing
25
26  let keyword_table : (string, token) Hashtbl.t = Hashtbl.create 89 ;;
27  let () = List.iter (fun (k, t) -> Hashtbl.add keyword_table k t) [
28    "Close",         CLOSE ;
29    "CoDefine",      CODEFINE ;
30    "Define",        DEFINE ;
31    "Import",        IMPORT ;
32    "Kind",          KKIND ;
33    "Query",         QUERY ;
34    "Quit",          QUIT ;
35    "Set",           SET ;
36    "Show",          SHOW ;
37    "Specification", SPECIFICATION ;
38    "Split",         SSPLIT ;
39    "Theorem",       THEOREM ;
40    "Type",          TTYPE ;
41    "abbrev",        ABBREV ;
42    "abort",         ABORT ;
43    "accum_sig",     ACCUMSIG ;
44    "accumulate",    ACCUM ;
45    "all",           ALL ;
46    "apply",         APPLY ;
47    "as",            AS ;
48    "assert",        ASSERT ;
49    "async",         ASYNC ;
50    "backchain",     BACKCHAIN ;
51    "by",            BY ;
52    "case",          CASE ;
53    "clear",         CLEAR ;
54    "coinduction",   COIND ;
55    "cut",           CUT ;
56    "end",           END ;
57    "exists",        EXISTS ;
58    "false",         FALSE ;
59    "forall",        FORALL ;
60    "from",          FROM ;
61    "induction",     IND ;
62    "inst",          INST ;
63    "intros",        INTROS ;
64    "keep",          KEEP ;
65    "kind",          KIND ;
66    "left",          LEFT ;
67    "module",        MODULE ;
68    "monotone",      MONOTONE ;
69    "nabla",         NABLA ;
70    "on",            ON ;
71    "permute",       PERMUTE ;
72    "rename",        RENAME ;
73    "right",         RIGHT ;
74    "search",        SEARCH ;
75    "sig",           SIG ;
76    "skip",          SKIP ;
77    "split",         SPLIT ;
78    "split*",        SPLITSTAR ;
79    "to",            TO ;
80    "true",          TRUE ;
81    "type",          TYPE ;
82    "unabbrev",      UNABBREV ;
83    "undo",          UNDO ;
84    "unfold",        UNFOLD ;
85    "with",          WITH ;
86    "witness",       WITNESS ;
87  ] ;;
88
89  let incrline lexbuf =
90    lexbuf.lex_curr_p <- {
91        lexbuf.lex_curr_p with
92          pos_bol = lexbuf.lex_curr_p.pos_cnum ;
93          pos_lnum = 1 + lexbuf.lex_curr_p.pos_lnum }
94
95  let comment_level = ref 0
96}
97
98let number = ['0'-'9'] +
99
100(* Initial characters for variables *)
101let ichar = ['A'-'Z' 'a'-'z' '-' '^' '=' '`' '\'' '?' '$']
102
103(* Characters allowed only in the body of variables. *)
104let bchar = ['0'-'9' '_' '/' '*' '@' '+' '#' '!' '~']
105
106let name = ichar (ichar|bchar)*
107let blank = ' ' | '\t' | '\r'
108
109rule token = parse
110| "/*"               { incr comment_level; comment lexbuf }
111| "%:" (name as s) ":" [^'\n']* '\n'
112                     { incrline lexbuf; CLAUSENAME s }
113| '%' [^'\n']* '\n'? { incrline lexbuf; token lexbuf }
114
115| blank              { token lexbuf }
116| '\n'               { incrline lexbuf; token lexbuf }
117
118| '"' ([^ '"']* as s) '"'
119                     { QSTRING s }
120
121| "#back"            { BACK }
122| "#reset"           { RESET }
123
124| "=>"               { IMP }
125| "<="               { IF }
126| "&"                { AMP }
127| ":-"               { CLAUSEEQ }
128| ":="               { DEFEQ }
129| ","                { COMMA }
130| "."                { DOT }
131| ";"                { SEMICOLON }
132| "\\"               { BSLASH }
133| "("                { LPAREN }
134| ")"                { RPAREN }
135| "|-"               { TURN }
136| "::"               { CONS }
137| "="                { EQ }
138
139| ":"                { COLON }
140| "->"               { RARROW }
141| "*"                { STAR }
142| "@"                { AT }
143| "#"                { HASH }
144| "+"                { PLUS }
145| "\\/"              { OR }
146| "/\\"              { AND }
147| "{"                { LBRACE }
148| "}"                { RBRACE }
149| "["                { LBRACK }
150| "]"                { RBRACK }
151
152| "_"                { UNDERSCORE }
153| number as n        { NUM (int_of_string n) }
154| name as id          { try Hashtbl.find keyword_table id
155                       with Not_found -> STRINGID id }
156
157| eof                { EOF }
158
159| '\x04'             { EOF }   (* ctrl-D *)
160
161| _                  {
162    let open Lexing in
163    let pos = lexeme_start_p lexbuf in
164    let msg = "Illegal character '" ^ String.escaped (lexeme lexbuf) ^ "' in input" in
165    let msg = match pos.pos_fname with
166      | "" -> msg
167      | fname -> Printf.sprintf "File %S, line %d, character %d: %s"
168                   fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol) msg
169    in
170    failwith msg
171  }
172
173and comment = parse
174| [^ '*' '/' '\n']+  { comment lexbuf }
175| "/*"               { incr comment_level; comment lexbuf }
176| "*/"               { decr comment_level ;
177                       if !comment_level = 0 then
178                         token lexbuf
179                       else
180                         comment lexbuf }
181| "*"                { comment lexbuf }
182| "/"                { comment lexbuf }
183| "\n"               { incrline lexbuf; comment lexbuf }
184| eof                { print_endline
185                         "Warning: comment not closed at end of file" ;
186                       token lexbuf }
187