driver_lexer.mll 3.89 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14

{
  open Lexing
  open Driver_parser
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15 16

  let keywords = Hashtbl.create 97
17 18
  let () =
    List.iter
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19 20
      (fun (x,y) -> Hashtbl.add keywords x y)
      [ "theory", THEORY;
21 22
        "end", END;
        "syntax", SYNTAX;
23
        "overriding", OVERRIDING;
24 25 26
        "remove", REMOVE;
        "meta", META;
        "prelude", PRELUDE;
27
        "interface", INTERFACE;
28
        "printer", PRINTER;
29
	"steps", STEPS;
30
	"model_parser", MODEL_PARSER;
31 32
        "valid", VALID;
        "invalid", INVALID;
33
        "timeout", TIMEOUT;
34
        "outofmemory", OUTOFMEMORY;
35
        "steplimitexceeded", STEPLIMITEXCEEDED;
36
        "time",    TIME;
37 38
        "unknown", UNKNOWN;
        "fail", FAIL;
39
        "constant", CONSTANT;
40 41
        "function", FUNCTION;
        "predicate", PREDICATE;
42 43
        "type", TYPE;
        "prop", PROP;
44
        "allprops", ALL;
45
        "filename", FILENAME;
46
        "transformation", TRANSFORM;
47 48
        "plugin", PLUGIN;
        "blacklist", BLACKLIST;
49
        "prec", PREC;
50 51 52 53
        (* WhyML *)
        "module", MODULE;
        "exception", EXCEPTION;
        "val", VAL;
Clément Fumex's avatar
Clément Fumex committed
54
        "literal", LITERAL;
55
        "use", USE;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56
      ]
57 58
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59 60 61
let space = [' ' '\t' '\r']
let alpha = ['a'-'z' 'A'-'Z' '_']
let digit = ['0'-'9']
62 63
let idsuf = alpha | digit | '\''
let ident = alpha idsuf*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64

65
let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%' '\\'
66 67
               '!' '$' '&' '?' '@' '^' '.' ':' '|' '#']

68
rule token = parse
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69
  | '\n'
70
      { Lexing.new_line lexbuf; token lexbuf }
71
  | space+
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
72
      { token lexbuf }
73
  | "(*)"
74
      { Lexlib.backjump lexbuf 2; LEFTPAR }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
  | "(*"
76
      { Lexlib.comment lexbuf; token lexbuf }
77
  | '_'
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78 79 80
      { UNDERSCORE }
  | ident as id
      { try Hashtbl.find keywords id with Not_found -> IDENT id }
81 82
  | digit+ as i
      { INTEGER (int_of_string i) }
83 84 85 86 87 88
  | "<-"
      { LARROW }
  | "["
      { LEFTSQ }
  | "]"
      { RIGHTSQ }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89 90 91 92 93 94
  | "("
      { LEFTPAR }
  | ")"
      { RIGHTPAR }
  | "."
      { DOT }
95 96
  | ".."
      { DOTDOT }
97 98
  | ","
      { COMMA }
99 100
  | "'"
      { QUOTE }
101 102
  | "]" ("'"+ as s)
      { RIGHTSQ_QUOTE s }
103
  | ")" (['\'' '_'] ['a'-'z' 'A'-'Z'] idsuf* as s)
104 105
      { RIGHTPAR_QUOTE s }
  | op_char+ "'"* as op
106
      { OPERATOR op }
107
  | '"'
108
      { STRING (Lexlib.string lexbuf) }
109
  | "import" space* '"'
110
      { INPUT (Lexlib.string lexbuf) }
111
  | eof
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112 113
      { EOF }
  | _ as c
114
      { Lexlib.illegal_character c lexbuf }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
115 116

{
117
  let parse_file_gen parse input_lexbuf lexbuf =
118 119 120 121 122 123 124 125
    let s = Stack.create () in
    Stack.push lexbuf s;
    let rec multifile lex_dumb =
      let lexbuf = Stack.top s in
      let tok = token lexbuf in
      Loc.transfer_loc lexbuf lex_dumb;
      match tok with
        | INPUT filename ->
126
          let dirname = Filename.dirname lexbuf.lex_curr_p.pos_fname in
MARCHE Claude's avatar
MARCHE Claude committed
127
          let filename = Sysutil.concat dirname filename in
128 129 130 131 132 133 134
          Stack.push (input_lexbuf filename) s;
          multifile lex_dumb
        | EOF -> ignore (Stack.pop s);
          if Stack.is_empty s then EOF else multifile lex_dumb
        | _ -> tok in
    let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
    Loc.transfer_loc lexbuf lex_dumb;
135
    Loc.with_location (parse multifile) lex_dumb
136 137 138

  let parse_file = parse_file_gen Driver_parser.file
  let parse_file_extract = parse_file_gen Driver_parser.file_extract
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
}