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