aufbau 0.1.2

Generalized prefix parsing for a class of context-dependent languages
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

// Fun — a functional language with modern syntax but STLC semantics
// Type system has same power as STLC: no polymorphism, just monomorphic functions

// ===================== Identifiers =====================
Identifier ::= /[a-z][a-z0-9]*/
TypeName ::= /[A-Z][a-z0-9]*/

// ===================== Type Annotations =====================
BaseType ::= TypeName | '(' Type ')'
FunctionType ::= BaseType '->' Type
Type ::= BaseType | FunctionType

// ===================== Literals =====================
Integer(int) ::= /[0-9]+/
Boolean(bool) ::= 'true' | 'false'
Float(float) ::= /[0-9]+\.[0-9]+/


// ===================== Operators =====================

// Integer operators
IntOp ::= '+' | '-' | '*' | '/'

// Float operators (OCaml-style)
FloatOp ::= '+.' | '-.' | '*.' | '/.'


// ===================== Expressions =====================

// Variable reference
Variable(var) ::= Identifier[x]

// Lambda: (x: Int) => x + 1
Lambda(lambda) ::= '(' Identifier[param] ':' Type[τ] ')' '=>' Expression[body]

// Parenthesized expression
Paren ::= '(' Expression ')'

// Let binding
Let(let) ::= 'let' Identifier[name] ':' Type[τ] '=' Expression[value] ';' Expression[body]

// Atomic expressions
AtomicExpression ::= Variable
                   | Integer
                   | Float
                   | Boolean
                   | Lambda
                   | Paren

// Postfix application: allow repeated application without extra parentheses
PostfixTail ::= '(' Expression ')' PostfixTail | ε
PostfixExpression ::= AtomicExpression PostfixTail

// Binary integer operation
IntBinary(bin_int) ::= Expression[left] IntOp[op] Expression[right]

// Binary float operation
FloatBinary(bin_float) ::= Expression[left] FloatOp[op] Expression[right]

// Application: each production exposes the bindings required by (app)
Application(app) ::= AtomicExpression[func] '(' Expression[arg] ')'
                   | Application[func] '(' Expression[arg] ')'

// Top-level expression
Expression ::= IntBinary
             | FloatBinary
             | Application
             | Let
             | AtomicExpression


// ===================== Typing Rules =====================

// Variable lookup
x ∈ Γ
----------- (var)
Γ(x)

// Integer literal
----------- (int)
'Int'

// Float literal
----------- (float)
'Float'

// Boolean literal
----------- (bool)
'Bool'

// Lambda
Γ[param:τ] ⊢ body : ?R
----------------------- (lambda)
τ -> ?R

// Let
Γ ⊢ value : τ, Γ[name:τ] ⊢ body : ?R
------------------------------------- (let)
?R

// Integer binary operators
Γ ⊢ left : 'Int', Γ ⊢ right : 'Int'
---------------------------------- (bin_int)
'Int'

// Float binary operators
Γ ⊢ left : 'Float', Γ ⊢ right : 'Float'
-------------------------------------- (bin_float)
'Float'

// Application
Γ ⊢ func : ?A -> ?R, Γ ⊢ arg : ?A
---------------------------------- (app)
?R