lexer.mll 6.65 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19 20

{
21
  open Format
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22
  open Lexing
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23
  open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24 25 26
  open Ptree
  open Parser

27 28 29 30 31 32 33
  (* lexical errors *)

  type error = 
    | IllegalCharacter of char
    | UnterminatedComment
    | UnterminatedString

34
  exception Error of error
35 36 37 38 39 40

  let report fmt = function
    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
    | UnterminatedComment -> fprintf fmt "unterminated comment"
    | UnterminatedString -> fprintf fmt "unterminated string"

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41 42 43 44
  let keywords = Hashtbl.create 97
  let () = 
    List.iter 
      (fun (x,y) -> Hashtbl.add keywords x y)
45
      [ 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46 47 48
	"and", AND;
	"as", AS;
	"axiom", AXIOM;
49
	"clone", CLONE;
50
	"else", ELSE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
51 52
	"end", END;
	"exists", EXISTS;
53
	"export", EXPORT;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
54 55 56 57
        "false", FALSE;
	"forall", FORALL;
	"goal", GOAL;
	"if", IF;
58
	"import", IMPORT;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59 60
	"in", IN;
	"inductive", INDUCTIVE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
61
	"lemma", LEMMA;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62 63 64
	"let", LET;
	"logic", LOGIC;
	"match", MATCH;
65
	"namespace", NAMESPACE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67 68
	"not", NOT;
	"or", OR;
	"then", THEN;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69
	"theory", THEORY;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70 71
	"true", TRUE;
	"type", TYPE;
72
	"use", USE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
73
	"with", WITH;
74
      ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75 76 77 78 79 80
	       
  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <- 
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }

81
  let string_start_loc = ref Loc.dummy_position
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82 83
  let string_buf = Buffer.create 1024

84 85
  let comment_start_loc = ref Loc.dummy_position

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
  let char_for_backslash = function
    | 'n' -> '\n'
    | 't' -> '\t'
    | c -> c

  let update_loc lexbuf file line chars =
    let pos = lexbuf.lex_curr_p in
    let new_file = match file with None -> pos.pos_fname | Some s -> s in
    lexbuf.lex_curr_p <- 
      { pos with
	  pos_fname = new_file;
	  pos_lnum = int_of_string line;
	  pos_bol = pos.pos_cnum - int_of_string chars;
      }

  let remove_leading_plus s =
    let n = String.length s in 
    if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s

105 106
  let loc lb = (lexeme_start_p lb, lexeme_end_p lb)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107 108 109 110
}

let newline = '\n'
let space = [' ' '\t' '\r']
111 112 113
let lalpha = ['a'-'z' '_']
let ualpha = ['A'-'Z']
let alpha = lalpha | ualpha
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
let digit = ['0'-'9']
115 116
let lident = lalpha (alpha | digit | '\'')*
let uident = ualpha (alpha | digit | '\'')*
117 118 119 120 121 122 123 124 125 126
let decimal_literal =
  ['0'-'9'] ['0'-'9' '_']*
let hex_literal =
  '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']*
let oct_literal =
  '0' ['o' 'O'] ['0'-'7'] ['0'-'7' '_']*
let bin_literal =
  '0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']*
let int_literal =
  decimal_literal | hex_literal | oct_literal | bin_literal
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127 128 129 130 131 132 133 134 135 136
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']

rule token = parse
  | "#" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
    space* (digit+ as line) space* (digit+ as char) space* "#"
      { update_loc lexbuf file line char; token lexbuf }
  | newline 
      { newline lexbuf; token lexbuf }
  | space+  
      { token lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137 138
  | '_'
      { UNDERSCORE }
139 140 141 142
  | lident as id  
      { try Hashtbl.find keywords id with Not_found -> LIDENT id }
  | uident as id  
      { UIDENT id }
143
  | int_literal as s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144 145 146 147
      { INTEGER s }
  | (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)
  | (digit+ as i) '.' (digit* as f) (['e' 'E'] (['-' '+']? digit+ as e))?
  | (digit* as i) '.' (digit+ as f) (['e' 'E'] (['-' '+']? digit+ as e))?
148
      { FLOAT (RConstDecimal (i, f, Util.option_map remove_leading_plus e)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
149 150 151 152 153 154
  | '0' ['x' 'X'] ((hexadigit* as i) '.' (hexadigit+ as f) 
                  |(hexadigit+ as i) '.' (hexadigit* as f)
		  |(hexadigit+ as i) ("" as f))
    ['p' 'P'] (['-' '+']? digit+ as e)
      { FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
  | "(*"
155
      { comment_start_loc := loc lexbuf; comment lexbuf; token lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
  | "'"
      { QUOTE }
  | ","
      { COMMA }
  | "("
      { LEFTPAR }
  | ")"
      { RIGHTPAR }
  | "!"
      { BANG }
  | ":"
      { COLON }
  | "->"
      { ARROW }
  | "<->"
      { LRARROW }
  | "="
      { EQUAL }
174
  | "<>" | "<" | "<=" | ">" | ">=" as s
175 176 177
      { OP0 s }
  | "+" | "-" as c
      { OP2 (String.make 1 c) }
178
  | "*" | "/" | "%" as c
179
      { OP3 (String.make 1 c) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
  | "@"
      { AT }
  | "."
      { DOT }
  | "["
      { LEFTSQ }
  | "]"
      { RIGHTSQ }
  | "{"
      { LEFTB }
  | "}"
      { RIGHTB }
  | "|"
      { BAR }
  | "\""
195
      { string_start_loc := loc lexbuf; STRING (string lexbuf) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196 197 198
  | eof 
      { EOF }
  | _ as c
199
      { raise (Error (IllegalCharacter c)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200 201 202 203 204 205 206 207 208

and comment = parse
  | "*)" 
      { () }
  | "(*" 
      { comment lexbuf; comment lexbuf }
  | newline 
      { newline lexbuf; comment lexbuf }
  | eof
209
      { raise (Loc.Located (!comment_start_loc, Error UnterminatedComment)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210 211 212 213 214
  | _ 
      { comment lexbuf }

and string = parse
  | "\""
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215 216 217
      { let s = Buffer.contents string_buf in
	Buffer.clear string_buf; 
	s }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218 219 220 221 222
  | "\\" (_ as c)
      { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
  | newline 
      { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
  | eof
223
      { raise (Loc.Located (!string_start_loc, Error UnterminatedString)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
224 225 226 227 228 229 230 231
  | _ as c
      { Buffer.add_char string_buf c; string lexbuf }



{

  let with_location f lb =
232 233 234 235 236
    try 
      f lb 
    with 
      | Loc.Located _ as e -> raise e
      | e -> raise (Loc.Located (loc lb, e))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
237

238 239
  let parse_logic_file = with_location (logic_file token)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240
  let parse_lexpr = with_location (lexpr token)
241
  let parse_list0_decl = with_location (list0_decl token)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242 243 244 245 246

}

(*
Local Variables: 
247
compile-command: "unset LANG; make -C ../.. test"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248 249 250
End: 
*)