A Golang runtime and compilation backend for Delta Interaction Nets.
1package lambda
2
3import (
4 "fmt"
5 "unicode"
6)
7
8type TokenType int
9
10const (
11 TokenEOF TokenType = iota
12 TokenIdent
13 TokenColon
14 TokenEqual
15 TokenSemicolon
16 TokenLParen
17 TokenRParen
18 TokenLet
19 TokenIn
20)
21
22type Token struct {
23 Type TokenType
24 Literal string
25}
26
27type Parser struct {
28 input string
29 pos int
30 current Token
31}
32
33func NewParser(input string) *Parser {
34 p := &Parser{input: input}
35 p.next()
36 return p
37}
38
39func (p *Parser) next() {
40 p.skipWhitespace()
41 if p.pos >= len(p.input) {
42 p.current = Token{Type: TokenEOF}
43 return
44 }
45
46 ch := p.input[p.pos]
47 switch {
48 case isLetter(ch):
49 start := p.pos
50 for p.pos < len(p.input) && (isLetter(p.input[p.pos]) || isDigit(p.input[p.pos])) {
51 p.pos++
52 }
53 lit := p.input[start:p.pos]
54 if lit == "let" {
55 p.current = Token{Type: TokenLet, Literal: lit}
56 } else if lit == "in" {
57 p.current = Token{Type: TokenIn, Literal: lit}
58 } else {
59 p.current = Token{Type: TokenIdent, Literal: lit}
60 }
61 case ch == ':':
62 p.current = Token{Type: TokenColon, Literal: ":"}
63 p.pos++
64 case ch == '=':
65 p.current = Token{Type: TokenEqual, Literal: "="}
66 p.pos++
67 case ch == ';':
68 p.current = Token{Type: TokenSemicolon, Literal: ";"}
69 p.pos++
70 case ch == '(':
71 p.current = Token{Type: TokenLParen, Literal: "("}
72 p.pos++
73 case ch == ')':
74 p.current = Token{Type: TokenRParen, Literal: ")"}
75 p.pos++
76 default:
77 // Treat unknown chars as identifiers for now (e.g. +)
78 // Or maybe just single char symbols
79 p.current = Token{Type: TokenIdent, Literal: string(ch)}
80 p.pos++
81 }
82}
83
84func (p *Parser) skipWhitespace() {
85 for p.pos < len(p.input) && unicode.IsSpace(rune(p.input[p.pos])) {
86 p.pos++
87 }
88}
89
90func isLetter(ch byte) bool {
91 return (ch >= 'a' && ch <= 'z') || (ch >= 'A' && ch <= 'Z') || ch == '_'
92}
93
94func isDigit(ch byte) bool {
95 return ch >= '0' && ch <= '9'
96}
97
98func (p *Parser) Parse() (Term, error) {
99 return p.parseTerm()
100}
101
102// Term ::= Abs | Let | App
103func (p *Parser) parseTerm() (Term, error) {
104 if p.current.Type == TokenLet {
105 return p.parseLet()
106 }
107
108 // Try to parse an abstraction or application
109 // Since application is left-associative and abstraction extends to the right,
110 // we need to be careful.
111 // Nix syntax: x: Body
112 // App: M N
113
114 // We parse a list of "atoms" and combine them as application.
115 // If we see an identifier followed by colon, it's an abstraction.
116 // But we need lookahead or backtracking.
117 // Actually, `x: ...` starts with ident then colon.
118 // `x y` starts with ident then ident.
119
120 // Let's parse "Atom" first.
121 // Atom ::= Ident | ( Term )
122
123 // If current is Ident:
124 // Check next token. If Colon, it's Abs.
125 // Else, it's an Atom (Var), and we continue parsing more Atoms for App.
126
127 if p.current.Type == TokenIdent {
128 // Lookahead
129 savePos := p.pos
130 saveTok := p.current
131
132 // Peek next
133 p.next()
134 if p.current.Type == TokenColon {
135 // It's an abstraction
136 arg := saveTok.Literal
137 p.next() // consume colon
138 body, err := p.parseTerm()
139 if err != nil {
140 return nil, err
141 }
142 return Abs{Arg: arg, Body: body}, nil
143 }
144
145 // Not an abstraction, backtrack
146 p.pos = savePos
147 p.current = saveTok
148 }
149
150 return p.parseApp()
151}
152
153func (p *Parser) parseApp() (Term, error) {
154 left, err := p.parseAtom()
155 if err != nil {
156 return nil, err
157 }
158
159 for {
160 if p.current.Type == TokenEOF || p.current.Type == TokenRParen || p.current.Type == TokenSemicolon || p.current.Type == TokenIn {
161 break
162 }
163 // Also stop if we see something that looks like the start of an abstraction?
164 // `x: ...` inside an app? `(x: x) y` is valid. `x y: z` -> `x (y: z)`?
165 // Usually lambda extends as far right as possible.
166 // So `x y: z` parses as `x (y: z)`.
167 // If we see Ident Colon, we should parse it as Abs and append to App.
168
169 if p.current.Type == TokenIdent {
170 // Check for colon
171 savePos := p.pos
172 saveTok := p.current
173 p.next()
174 if p.current.Type == TokenColon {
175 // It's an abstraction `arg: body`
176 // This abstraction is the argument to the current application
177 argName := saveTok.Literal
178 p.next() // consume colon
179 body, err := p.parseTerm()
180 if err != nil {
181 return nil, err
182 }
183 left = App{Fun: left, Arg: Abs{Arg: argName, Body: body}}
184 // After parsing an abstraction (which consumes everything to the right),
185 // we are done with this application chain?
186 // Yes, because `x y: z a` -> `x (y: z a)`.
187 return left, nil
188 }
189 // Backtrack
190 p.pos = savePos
191 p.current = saveTok
192 }
193
194 right, err := p.parseAtom()
195 if err != nil {
196 // If we can't parse an atom, maybe we are done
197 break
198 }
199 left = App{Fun: left, Arg: right}
200 }
201
202 return left, nil
203}
204
205func (p *Parser) parseAtom() (Term, error) {
206 switch p.current.Type {
207 case TokenIdent:
208 name := p.current.Literal
209 p.next()
210 return Var{Name: name}, nil
211 case TokenLParen:
212 p.next()
213 term, err := p.parseTerm()
214 if err != nil {
215 return nil, err
216 }
217 if p.current.Type != TokenRParen {
218 return nil, fmt.Errorf("expected ')'")
219 }
220 p.next()
221 return term, nil
222 default:
223 return nil, fmt.Errorf("unexpected token: %v", p.current)
224 }
225}
226
227func (p *Parser) parseLet() (Term, error) {
228 p.next() // consume 'let'
229
230 // Parse bindings: x = M; y = N; ...
231 type binding struct {
232 name string
233 val Term
234 }
235 var bindings []binding
236
237 for {
238 if p.current.Type != TokenIdent {
239 return nil, fmt.Errorf("expected identifier in let binding")
240 }
241 name := p.current.Literal
242 p.next()
243
244 if p.current.Type != TokenEqual {
245 return nil, fmt.Errorf("expected '='")
246 }
247 p.next()
248
249 val, err := p.parseTerm()
250 if err != nil {
251 return nil, err
252 }
253
254 bindings = append(bindings, binding{name, val})
255
256 if p.current.Type == TokenSemicolon {
257 p.next()
258 // Check if next is 'in' or another ident
259 if p.current.Type == TokenIn {
260 p.next()
261 break
262 }
263 // Continue to next binding
264 } else if p.current.Type == TokenIn {
265 p.next()
266 break
267 } else {
268 return nil, fmt.Errorf("expected ';' or 'in'")
269 }
270 }
271
272 body, err := p.parseTerm()
273 if err != nil {
274 return nil, err
275 }
276
277 // Desugar: let x=M; y=N in B -> (\x. (\y. B) N) M
278 // We iterate backwards
279 term := body
280 for i := len(bindings) - 1; i >= 0; i-- {
281 b := bindings[i]
282 term = App{
283 Fun: Abs{Arg: b.name, Body: term},
284 Arg: b.val,
285 }
286 }
287
288 return term, nil
289}
290
291// Parse parses a lambda term from a string.
292func Parse(input string) (Term, error) {
293 p := NewParser(input)
294 return p.Parse()
295}