build: Distribute src/.depend with tarball.
[goals.git] / src / lexer.mll
1 (* Goalfile lexer
2  * Copyright (C) 2019 Richard W.M. Jones
3  * Copyright (C) 2019 Red Hat Inc.
4  *
5  * This program is free software; you can redistribute it and/or modify
6  * it under the terms of the GNU General Public License as published by
7  * the Free Software Foundation; either version 2 of the License, or
8  * (at your option) any later version.
9  *
10  * This program is distributed in the hope that it will be useful,
11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13  * GNU General Public License for more details.
14  *
15  * You should have received a copy of the GNU General Public License along
16  * with this program; if not, write to the Free Software Foundation, Inc.,
17  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
18  *)
19
20 {
21 open Lexing
22 open Parser
23
24 open Printf
25
26 exception SyntaxError of string
27
28 let new_line lexbuf =
29   let pos = lexbuf.lex_curr_p in
30   lexbuf.lex_curr_p <-
31     { pos with pos_bol = pos.pos_cnum; pos_lnum = pos.pos_lnum + 1 }
32 }
33
34 let white = [' ' '\t']+
35 let newline = '\r' | '\n' | "\r\n"
36 let comment = '#' (_#'\n')*
37 let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']*
38
39 rule read =
40     parse
41     | white
42     | comment { read lexbuf }
43     | newline { new_line lexbuf; read lexbuf }
44     | ","     { COMMA }
45     | ":"     { COLON }
46     | ";"     { SEMICOLON }
47     | "="     { EQUALS }
48     | "("     { LEFT_PAREN }
49     | ")"     { RIGHT_PAREN }
50     | "["     { LEFT_ARRAY }
51     | "]"     { RIGHT_ARRAY }
52     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
53     | "{"     { read_code false (Ast.Substs.create ()) (ref 1) lexbuf }
54     | "@{"    { read_code true  (Ast.Substs.create ()) (ref 1) lexbuf }
55     | "goal"  { GOAL }
56     | "tactic"
57               { TACTIC_KEYWORD }
58     | "function"
59               { FUNCTION }
60     | "pure"  { PURE }
61     | "let"   { LET }
62     | "include"
63               { INCLUDE }
64     | "-include"
65               { OPTINCLUDE }
66     | "returning"
67               { RETURNING }
68     | "expression"
69               { EXPRESSION }
70     | "string"
71               { STRING_KEYWORD }
72     | "strings"
73               { STRINGS }
74     | "*" id  { (* NB: The initial '*' is part of the name. *)
75                 TACTIC (Lexing.lexeme lexbuf) }
76     | id      { ID (Lexing.lexeme lexbuf) }
77     | _       { raise (SyntaxError ("unexpected character: " ^
78                                     Lexing.lexeme lexbuf)) }
79     | eof     { EOF }
80
81 (* Parse "STRING" literal with %-substitutions. *)
82 and read_string buf =
83     parse
84     | '\\' '"'
85               { Ast.Substs.add_char buf '"'; read_string buf lexbuf }
86     | '\\' 'a'
87               { Ast.Substs.add_char buf '\007'; read_string buf lexbuf }
88     | '\\' 'b'
89               { Ast.Substs.add_char buf '\008'; read_string buf lexbuf }
90     | '\\' 't'
91               { Ast.Substs.add_char buf '\009'; read_string buf lexbuf }
92     | '\\' 'n'
93               { Ast.Substs.add_char buf '\010'; read_string buf lexbuf }
94     | '\\' 'v'
95               { Ast.Substs.add_char buf '\011'; read_string buf lexbuf }
96     | '\\' 'f'
97               { Ast.Substs.add_char buf '\012'; read_string buf lexbuf }
98     | '\\' 'r'
99               { Ast.Substs.add_char buf '\013'; read_string buf lexbuf }
100     | '\\' '\\'
101               { Ast.Substs.add_char buf '\\'; read_string buf lexbuf }
102     | '"'     { STRING (Ast.Substs.get buf) }
103     | newline { Ast.Substs.add_char buf '\n';
104                 new_line lexbuf; read_string buf lexbuf }
105     | '%' '%' { Ast.Substs.add_char buf '%'; read_string buf lexbuf }
106     | '%' id  { let id = Lexing.lexeme lexbuf in
107                 let len = String.length id in
108                 Ast.Substs.add_var buf (String.sub id 1 (len-1));
109                 read_string buf lexbuf }
110     | '%' _   { raise (SyntaxError ("illegal character in %-substitution: " ^
111                                     Lexing.lexeme lexbuf)) }
112     | [^ '"' '\\' '\r' '\n' '%' ]+
113               { Ast.Substs.add_string buf (Lexing.lexeme lexbuf);
114                 read_string buf lexbuf }
115     | _       { raise (SyntaxError ("illegal character in string: " ^
116                                       Lexing.lexeme lexbuf)) }
117     | eof     { raise (SyntaxError ("unterminated string")) }
118
119 (* Parse { CODE } literal with %-substitutions.
120  *
121  * Note the range of %-substitutions possible is larger than
122  * for strings.
123  *)
124 and read_code quiet buf level =
125     parse
126     | '{'     { Ast.Substs.add_char buf '{';
127                 incr level; read_code quiet buf level lexbuf }
128     | '}'     { decr level;
129                 if !level = 0 then CODE (Ast.Substs.get buf, quiet)
130                 else (
131                   Ast.Substs.add_char buf '}';
132                   read_code quiet buf level lexbuf
133                 ) }
134     | newline { Ast.Substs.add_char buf '\n';
135                 new_line lexbuf; read_code quiet buf level lexbuf }
136     | '%' '%' { Ast.Substs.add_char buf '%'; read_code quiet buf level lexbuf }
137     | '%' '@' { Ast.Substs.add_var buf "@"; read_code quiet buf level lexbuf }
138     | '%' '<' { Ast.Substs.add_var buf "<"; read_code quiet buf level lexbuf }
139     | '%' '^' { Ast.Substs.add_var buf "^"; read_code quiet buf level lexbuf }
140     | '%' id  { let id = Lexing.lexeme lexbuf in
141                 let len = String.length id in
142                 Ast.Substs.add_var buf (String.sub id 1 (len-1));
143                 read_code quiet buf level lexbuf }
144     | '%' _   { raise (SyntaxError ("illegal character in %-substitution: " ^
145                                       Lexing.lexeme lexbuf)) }
146     | [^ '{' '}' '\r' '\n' '%' ]+
147               { Ast.Substs.add_string buf (Lexing.lexeme lexbuf);
148                 read_code quiet buf level lexbuf }
149     | _       { raise (SyntaxError ("illegal character in code section: " ^
150                                       Lexing.lexeme lexbuf)) }
151     | eof     { raise (SyntaxError ("unterminated code section")) }