lexer.mll 7.22 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12

{
13
  open Format
14
  open Parser
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15

16
  exception IllegalCharacter of char
17

18
  let () = Exn_printer.register (fun fmt e -> match e with
19
    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
20
    | _ -> raise e)
21

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
22
  let keywords = Hashtbl.create 97
23 24
  let () =
    List.iter
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25
      (fun (x,y) -> Hashtbl.add keywords x y)
26
      [
27 28
        "as", AS;
        "axiom", AXIOM;
Martin Clochard's avatar
Martin Clochard committed
29
        "by", BY;
30
        "clone", CLONE;
31
        "coinductive", COINDUCTIVE;
32
        "constant", CONSTANT;
33 34 35 36 37
        "else", ELSE;
        "end", END;
        "epsilon", EPSILON;
        "exists", EXISTS;
        "export", EXPORT;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
        "false", FALSE;
Clément Fumex's avatar
Clément Fumex committed
39
        "float", FLOAT;
40
        "forall", FORALL;
Andrei Paskevich's avatar
Andrei Paskevich committed
41
        "function", FUNCTION;
42 43 44 45 46 47 48 49 50 51 52
        "goal", GOAL;
        "if", IF;
        "import", IMPORT;
        "in", IN;
        "inductive", INDUCTIVE;
        "lemma", LEMMA;
        "let", LET;
        "match", MATCH;
        "meta", META;
        "namespace", NAMESPACE;
        "not", NOT;
Andrei Paskevich's avatar
Andrei Paskevich committed
53
        "predicate", PREDICATE;
54
        "prop", PROP;
Clément Fumex's avatar
Clément Fumex committed
55
        "range", RANGE;
Martin Clochard's avatar
Martin Clochard committed
56
        "so", SO;
57 58 59 60 61 62 63 64 65 66 67 68 69
        "then", THEN;
        "theory", THEORY;
        "true", TRUE;
        "type", TYPE;
        "use", USE;
        "with", WITH;
        (* programs *)
        "abstract", ABSTRACT;
        "absurd", ABSURD;
        "any", ANY;
        "assert", ASSERT;
        "assume", ASSUME;
        "begin", BEGIN;
70
        "check", CHECK;
71
        "diverges", DIVERGES;
72 73
        "do", DO;
        "done", DONE;
Andrei Paskevich's avatar
Andrei Paskevich committed
74
        "downto", DOWNTO;
75
        "ensures", ENSURES;
76 77 78
        "exception", EXCEPTION;
        "for", FOR;
        "fun", FUN;
79
        "ghost", GHOST;
80 81 82 83 84
        "invariant", INVARIANT;
        "loop", LOOP;
        "model", MODEL;
        "module", MODULE;
        "mutable", MUTABLE;
85
        "private", PRIVATE;
86 87 88 89
        "raise", RAISE;
        "raises", RAISES;
        "reads", READS;
        "rec", REC;
90 91
        "requires", REQUIRES;
        "returns", RETURNS;
92 93
        "to", TO;
        "try", TRY;
Andrei Paskevich's avatar
Andrei Paskevich committed
94
        "val", VAL;
95 96
        "variant", VARIANT;
        "while", WHILE;
97
        "writes", WRITES;
98
      ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99 100 101
}

let space = [' ' '\t' '\r']
102 103 104
let lalpha = ['a'-'z' '_']
let ualpha = ['A'-'Z']
let alpha = lalpha | ualpha
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
let digit = ['0'-'9']
Clément Fumex's avatar
Clément Fumex committed
106 107 108 109 110 111 112
let digit_or_us = ['0'-'9' '_']
let alpha_no_us = ['a'-'z' 'A'-'Z']
let suffix = (alpha_no_us | '\''* digit_or_us)* '\''*
let lident = lalpha suffix
let uident = ualpha suffix
let lident_quote = lident ('\'' alpha_no_us suffix)+
let uident_quote = uident ('\'' alpha_no_us suffix)+
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113 114
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']

115
let op_char_1 = ['=' '<' '>' '~']
116
let op_char_2 = ['+' '-']
117
let op_char_3 = ['*' '/' '\\' '%']
118
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
119 120 121 122
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

123 124
let op_char_pref = ['!' '?']

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
125
rule token = parse
126 127
  | "##" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
    space* (digit+ as line) space* (digit+ as char) space* "##"
128 129
      { Lexlib.update_loc lexbuf file (int_of_string line) (int_of_string char);
        token lexbuf }
130 131 132 133 134
  | "#" 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)) }
135 136
  | '\n'
      { Lexlib.newline lexbuf; token lexbuf }
137
  | space+
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
138
      { token lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139 140
  | '_'
      { UNDERSCORE }
141
  | lident as id
142
      { try Hashtbl.find keywords id with Not_found -> LIDENT id }
Clément Fumex's avatar
Clément Fumex committed
143 144
  | lident_quote as id
      { LIDENT_QUOTE id }
145
  | uident as id
146
      { UIDENT id }
Clément Fumex's avatar
Clément Fumex committed
147 148
  | uident_quote as id
      { UIDENT_QUOTE id }
149
  | ['0'-'9'] ['0'-'9' '_']* as s
150
      { INTEGER (Number.int_const_dec (Lexlib.remove_underscores s)) }
151
  | '0' ['x' 'X'] (['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']* as s)
152
      { INTEGER (Number.int_const_hex (Lexlib.remove_underscores s)) }
153
  | '0' ['o' 'O'] (['0'-'7'] ['0'-'7' '_']* as s)
154
      { INTEGER (Number.int_const_oct (Lexlib.remove_underscores s)) }
155
  | '0' ['b' 'B'] (['0'-'1'] ['0'-'1' '_']* as s)
156
      { INTEGER (Number.int_const_bin (Lexlib.remove_underscores s)) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
157 158 159
  | (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))?
Clément Fumex's avatar
Clément Fumex committed
160
      { REAL (Number.real_const_dec i f
161
          (Opt.map Lexlib.remove_leading_plus e)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
  | '0' ['x' 'X'] (hexadigit+ as i) ("" as f) ['p' 'P'] (['-' '+']? digit+ as e)
  | '0' ['x' 'X'] (hexadigit+ as i) '.' (hexadigit* as f)
164
        (['p' 'P'] (['-' '+']? digit+ as e))?
Andrei Paskevich's avatar
Andrei Paskevich committed
165
  | '0' ['x' 'X'] (hexadigit* as i) '.' (hexadigit+ as f)
166
        (['p' 'P'] (['-' '+']? digit+ as e))?
Clément Fumex's avatar
Clément Fumex committed
167
      { REAL (Number.real_const_hex i f
168
          (Opt.map Lexlib.remove_leading_plus e)) }
169 170
  | "(*)"
      { LEFTPAR_STAR_RIGHTPAR }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
171
  | "(*"
172
      { Lexlib.comment lexbuf; token lexbuf }
173 174 175 176 177 178
  | "~'" (lident as id)
      { OPAQUE_QUOTE_LIDENT id }
  | "'" (lident as id)
      { QUOTE_LIDENT id }
  | "'" (uident as id)
      { QUOTE_UIDENT id }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179 180 181 182 183 184
  | ","
      { COMMA }
  | "("
      { LEFTPAR }
  | ")"
      { RIGHTPAR }
185 186 187 188
  | "{"
      { LEFTBRC }
  | "}"
      { RIGHTBRC }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
189 190
  | ":"
      { COLON }
191 192
  | ";"
      { SEMICOLON }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193 194
  | "->"
      { ARROW }
195 196
  | "<-"
      { LARROW }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197 198
  | "<->"
      { LRARROW }
199 200 201 202
  | "&&"
      { AMPAMP }
  | "||"
      { BARBAR }
203 204 205 206
  | "/\\"
      { AND }
  | "\\/"
      { OR }
Andrei Paskevich's avatar
Andrei Paskevich committed
207
  | "\\"
Andrei Paskevich's avatar
Andrei Paskevich committed
208
      { LAMBDA }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
209 210
  | "."
      { DOT }
211 212
  | ".."
      { DOTDOT }
213 214
  | "|"
      { BAR }
Clément Fumex's avatar
Clément Fumex committed
215 216 217 218
  | "<"
      { LT }
  | ">"
      { GT }
219 220
  | "<>"
      { LTGT }
Clément Fumex's avatar
Clément Fumex committed
221 222
  | "="
      { EQUAL }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223 224 225 226
  | "["
      { LEFTSQ }
  | "]"
      { RIGHTSQ }
227 228
  | op_char_pref op_char_4* as s
      { OPPREF s }
229 230 231 232 233 234 235 236
  | 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
237
  | "\""
238
      { STRING (Lexlib.string lexbuf) }
239
  | eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240 241
      { EOF }
  | _ as c
242
      { raise (IllegalCharacter c) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243 244

{
245
  let parse_logic_file env path lb =
246
    open_file token (Lexing.from_string "") (Typing.open_file env path);
247
    Loc.with_location (logic_file token) lb;
248
    Typing.close_file ()
249

250 251
  let parse_program_file inc lb =
    open_file token (Lexing.from_string "") inc;
252
    Loc.with_location (program_file token) lb
253

254
  let read_channel env path file c =
255 256
    let lb = Lexing.from_channel c in
    Loc.set_file file lb;
257
    parse_logic_file env path lb
258

259 260
  let () = Env.register_format Env.base_language "why" ["why"] read_channel
    ~desc:"WhyML@ logical@ language"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
}