lexer.mll 9.54 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    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
  (* lexical errors *)

29 30 31
  exception IllegalCharacter of char
  exception UnterminatedComment
  exception UnterminatedString
32
  exception AmbiguousPath of string * string
33

34
  let () = Exn_printer.register (fun fmt e -> match e with
35 36 37
    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
    | UnterminatedComment -> fprintf fmt "unterminated comment"
    | UnterminatedString -> fprintf fmt "unterminated string"
38 39
    | AmbiguousPath (f1, f2) ->
        fprintf fmt "ambiguous path:@ both `%s'@ and `%s'@ match" f1 f2
40
    | _ -> raise e)
41

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42
  let keywords = Hashtbl.create 97
43 44
  let () =
    List.iter
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
      (fun (x,y) -> Hashtbl.add keywords x y)
46
      [
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47 48 49
	"and", AND;
	"as", AS;
	"axiom", AXIOM;
50
	"clone", CLONE;
51
	"else", ELSE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52
	"end", END;
Andrei Paskevich's avatar
Andrei Paskevich committed
53
	"epsilon", EPSILON;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
54
	"exists", EXISTS;
55
	"export", EXPORT;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56 57 58 59
        "false", FALSE;
	"forall", FORALL;
	"goal", GOAL;
	"if", IF;
60 61
	"iff", IFF;
	"implies", IMPLIES;
62
	"import", IMPORT;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
63 64
	"in", IN;
	"inductive", INDUCTIVE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65
	"lemma", LEMMA;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67 68
	"let", LET;
	"logic", LOGIC;
	"match", MATCH;
69
	"meta", META;
70
	"namespace", NAMESPACE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71 72
	"not", NOT;
	"or", OR;
73
        "prop", PROP;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74
	"then", THEN;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
	"theory", THEORY;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76 77
	"true", TRUE;
	"type", TYPE;
78
	"use", USE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79
	"with", WITH;
80
	(* programs *)
81
	"abstract", ABSTRACT;
82 83 84 85 86 87 88 89 90 91 92 93
	"absurd", ABSURD;
	"any", ANY;
	"assert", ASSERT;
	"assume", ASSUME;
	"begin", BEGIN;
        "check", CHECK;
	"do", DO;
	"done", DONE;
 	"downto", DOWNTO;
	"exception", EXCEPTION;
	"for", FOR;
	"fun", FUN;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
	(* "ghost", GHOST; *)
95 96
	"invariant", INVARIANT;
	"label", LABEL;
97
	"loop", LOOP;
98 99 100 101 102 103 104 105 106 107 108 109 110
	"model", MODEL;
	"module", MODULE;
	"mutable", MUTABLE;
	"parameter", PARAMETER;
	"raise", RAISE;
	"raises", RAISES;
	"reads", READS;
	"rec", REC;
	"to", TO;
	"try", TRY;
	"variant", VARIANT;
	"while", WHILE;
        "writes", WRITES;
111
      ]
112

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113 114
  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
115
    lexbuf.lex_curr_p <-
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116 117
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }

118
  let string_start_loc = ref Loc.dummy_position
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119 120
  let string_buf = Buffer.create 1024

121 122
  let comment_start_loc = ref Loc.dummy_position

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123 124 125 126 127 128 129 130
  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
131
    lexbuf.lex_curr_p <-
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
132 133 134 135 136 137 138
      { 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 =
139
    let n = String.length s in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
140 141
    if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s

142
  let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb)
143

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144 145 146 147
}

let newline = '\n'
let space = [' ' '\t' '\r']
148 149 150
let lalpha = ['a'-'z' '_']
let ualpha = ['A'-'Z']
let alpha = lalpha | ualpha
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
151
let digit = ['0'-'9']
152 153
let lident = lalpha (alpha | digit | '\'')*
let uident = ualpha (alpha | digit | '\'')*
154 155 156 157 158 159 160 161 162 163
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
164 165
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']

166
let op_char_1 = ['=' '<' '>' '~']
167 168
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
169
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
170 171 172 173
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234

174 175
let op_char_pref = ['!' '?']

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
176
rule token = parse
177 178
  | "##" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
    space* (digit+ as line) space* (digit+ as char) space* "##"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179
      { update_loc lexbuf file line char; token lexbuf }
180 181 182 183 184
  | "#" space* "\"" ([^ '\010' '\013' '"' ]* as file) "\""
    space* (digit+ as line) space* (digit+ as bchar) space*
    (digit+ as echar) space* "#"
      { POSITION (Loc.user_position file (int_of_string line)
                 (int_of_string bchar) (int_of_string echar)) }
185
  | newline
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186
      { newline lexbuf; token lexbuf }
187
  | space+
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188
      { token lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190
  | '_'
      { UNDERSCORE }
191
  | lident as id
192
      { try Hashtbl.find keywords id with Not_found -> LIDENT id }
193
  | uident as id
194
      { UIDENT id }
195
  | int_literal as s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196 197 198 199
      { 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))?
200
      { FLOAT (RConstDecimal (i, f, Util.option_map remove_leading_plus e)) }
201
  | '0' ['x' 'X'] ((hexadigit* as i) '.' (hexadigit+ as f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202 203 204 205
                  |(hexadigit+ as i) '.' (hexadigit* as f)
		  |(hexadigit+ as i) ("" as f))
    ['p' 'P'] (['-' '+']? digit+ as e)
      { FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
206 207
  | "(*)"
      { LEFTPAR_STAR_RIGHTPAR }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
208
  | "(*"
209
      { comment_start_loc := loc lexbuf; comment lexbuf; token lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210 211
  | "'"
      { QUOTE }
212 213
  | "`"
      { BACKQUOTE }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
214 215 216 217 218 219
  | ","
      { COMMA }
  | "("
      { LEFTPAR }
  | ")"
      { RIGHTPAR }
220 221 222 223
  | "{"
      { LEFTBRC }
  | "}"
      { RIGHTBRC }
224 225 226 227
  | "{|"
      { LEFTREC }
  | "|}"
      { RIGHTREC }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
228 229
  | ":"
      { COLON }
230 231
  | ";"
      { SEMICOLON }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232 233 234 235
  | "->"
      { ARROW }
  | "<->"
      { LRARROW }
236 237 238 239
  | "&&"
      { AMPAMP }
  | "||"
      { BARBAR }
240 241 242 243 244
  | "/\\"
      { AND }
  | "\\/"
      { OR }
   | "\\"
Andrei Paskevich's avatar
Andrei Paskevich committed
245
      { LAMBDA }
246 247 248 249
  | "\\?"
      { PRED }
  | "\\!"
      { FUNC }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250 251
  | "."
      { DOT }
252 253 254 255
  | "|"
      { BAR }
  | "="
      { EQUAL }
256 257
  | "<>"
      { LTGT }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258 259 260 261
  | "["
      { LEFTSQ }
  | "]"
      { RIGHTSQ }
262 263
  | "~"
      { TILDE }
264 265
  | op_char_pref op_char_4* as s
      { OPPREF s }
266 267 268 269 270 271 272 273
  | op_char_1234* op_char_1 op_char_1234* as s
      { OP1 s }
  | op_char_234*  op_char_2 op_char_234*  as s
      { OP2 s }
  | op_char_34*   op_char_3 op_char_34*  as s
      { OP3 s }
  | op_char_4+ as s
      { OP4 s }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274
  | "\""
275
      { string_start_loc := loc lexbuf; STRING (string lexbuf) }
276
  | eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277 278
      { EOF }
  | _ as c
279
      { raise (IllegalCharacter c) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280 281

and comment = parse
282 283
  | "(*)"
      { comment lexbuf }
284
  | "*)"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
285
      { () }
286
  | "(*"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287
      { comment lexbuf; comment lexbuf }
288
  | newline
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289 290
      { newline lexbuf; comment lexbuf }
  | eof
291
      { raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
292
  | _
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
293 294 295 296
      { comment lexbuf }

and string = parse
  | "\""
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
297
      { let s = Buffer.contents string_buf in
298
	Buffer.clear string_buf;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299
	s }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300 301
  | "\\" (_ as c)
      { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
302
  | newline
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303 304
      { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
  | eof
305
      { raise (Loc.Located (!string_start_loc, UnterminatedString)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
306 307 308 309 310
  | _ as c
      { Buffer.add_char string_buf c; string lexbuf }

{
  let with_location f lb =
311 312
    if Debug.test_flag Debug.stack_trace then f lb else
    try f lb with
313 314
      | Loc.Located _ as e -> raise e
      | e -> raise (Loc.Located (loc lb, e))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315

316 317 318 319 320 321 322
  let parse_logic_file env = with_location (logic_file_eof env token)

  let parse_list0_decl env lenv uc =
    with_location (list0_decl_eof env lenv uc token)

  let parse_lexpr = with_location (lexpr_eof token)

323 324
  let parse_program_file = with_location (program_file token)

325 326 327 328
  let read_channel env file c =
    let lb = Lexing.from_channel c in
    Loc.set_file file lb;
    parse_logic_file env lb
329

330 331
  (* searches file [f] in loadpath [lp] *)
  let locate_file lp f =
332
    let fl = List.map (fun dir -> Filename.concat dir f) lp in
333
    match List.filter Sys.file_exists fl with
334 335 336
      | [] -> raise Not_found
      | [file] -> file
      | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
337 338 339 340

  let create_env lp =
    let ret_chan sl = 
      let f = List.fold_left Filename.concat "" sl in
341 342
      let file = locate_file lp f in
      file, open_in file
343 344 345 346 347 348 349 350 351 352 353
    in
    let retrieve env sl =
      let f = List.fold_left Filename.concat "" sl ^ ".why" in
      let file = locate_file lp f in
      let c = open_in file in
      try
	let tl = read_channel env file c in
	close_in c;
	tl
      with
	| e -> close_in c; raise e
354
    in
355
    Env.create_env ret_chan retrieve
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
356

357
  let () = Env.register_format "why" ["why"] read_channel
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358 359 360
}

(*
361
Local Variables:
362
compile-command: "unset LANG; make -C ../.. test"
363
End:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
364 365
*)