aufbau 0.3.1

// ML — a featured functional core in the unification model.
//
// Syntax is a strict subset of standard OCaml: fun/(parens)/->  lambdas,
// lowercase type names (int, bool), = for equality, -> in match arms.
// This makes the corpus directly parseable by the OCaml typechecker for
// differential certification without any translation layer.
//
// Type constructors are *labeled* productions (e.g. ListType(list)).  The
// label marks a node as carrying its own structure so a unary constructor
// like `list` can be distinguished from transparent grouping by shape alone.

// ===================== Identifiers =====================
Identifier ::= /[a-z_][a-z0-9_]*/
TypeName ::= /[a-z][a-z0-9_]*/

// ===================== Type annotations =====================
// Precedence, loosest to tightest:  ->   then  *   then postfix  list.
AtomicType ::= TypeName | '(' Type ')'
Factor ::= AtomicType | ListType
ListType(list) ::= Factor 'list'
ProductType ::= Factor '*' ProductType | Factor
FunctionType ::= ProductType '->' Type
Type* ::= FunctionType | ProductType

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

// ===================== Operators =====================
// `*` is the product connective so arithmetic keeps only `+` and `-`;
// otherwise `?A * ?B` would parse ambiguously as a type.
IntOp ::= '+' | '-'
CompOp ::= '=' | '<' | '<=' | '>' | '>='

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

Variable(var) ::= Identifier[x]

// Lambda:  fun (x : int) -> body
Lambda(lambda) ::= 'fun' '(' Identifier[param] ':' Type[τ] ')' '->' Expression[body]

// Pair and the empty list as atoms.
Pair(pair) ::= '(' Expression[fst] ',' Expression[snd] ')'
Nil(nil) ::= '[' ']'

// Divergence: assert false inhabits every type. This is the universal
// inhabitant that puts the grammar in the complete class (every live
// prefix is realizable) — see Completeness in typing::complete.
Diverge(diverge) ::= 'assert' 'false'

Paren ::= '(' Expression ')'

AtomicExpression ::= Variable
                   | Integer
                   | Boolean
                   | Lambda
                   | Pair
                   | Nil
                   | Diverge
                   | Paren

// Projections.
Fst(fst) ::= 'fst' AtomicExpression[pair]
Snd(snd) ::= 'snd' AtomicExpression[pair]

// Application: a function atom applied to an argument.
Application(app) ::= AtomicExpression[func] '(' Expression[arg] ')'
                   | Application[func] '(' Expression[arg] ')'

// Cons (right-associative):  head :: tail
Cons(cons) ::= AtomicExpression[head] '::' Expression[tail]

// Binary integer operation and comparison.
IntBinary(bin_int) ::= Expression[left] IntOp[op] Expression[right]
Compare(compare) ::= Expression[left] CompOp[op] Expression[right]

// Conditional:  if c then a else b
If(if) ::= 'if' Expression[cond] 'then' Expression[then_branch] 'else' Expression[else_branch]

// List elimination:  match xs with [] -> e1 | h :: t -> e2
Match(match) ::= 'match' Expression[scrutinee] 'with' '[' ']' '->' Expression[nil_case] '|' Identifier[head] '::' Identifier[tail] '->' Expression[cons_case]

// let and recursive let.
Let(let) ::= 'let' Identifier[name] ':' Type[τ] '=' Expression[value] 'in' Expression[body]
LetRec(letrec) ::= 'let' 'rec' Identifier[name] ':' Type[τ] '=' Expression[value] 'in' Expression[body]

Expression ::= IntBinary
             | Compare
             | Cons
             | Application
             | Fst
             | Snd
             | If
             | Match
             | Let
             | LetRec
             | AtomicExpression


// ===================== Typing rules =====================

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

// Literals
----------- (int)
'int'

----------- (bool)
'bool'

// assert false diverges, so it has every type.
------------------ (diverge)
?A

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

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

// Pair introduction and projections
Γ ⊢ fst : ?A, Γ ⊢ snd : ?B
--------------------------- (pair)
?A * ?B

Γ ⊢ pair : ?A * ?B
------------------ (fst)
?A

Γ ⊢ pair : ?A * ?B
------------------ (snd)
?B

// Lists: the empty list is a list of any element type; cons fixes it.
----------- (nil)
?A list

Γ ⊢ head : ?A, Γ ⊢ tail : ?A list
--------------------------------- (cons)
?A list

// Arithmetic and comparison
Γ ⊢ left : 'int', Γ ⊢ right : 'int'
----------------------------------- (bin_int)
'int'

Γ ⊢ left : 'int', Γ ⊢ right : 'int'
----------------------------------- (compare)
'bool'

// Conditional: branches agree, condition is bool
Γ ⊢ cond : 'bool', Γ ⊢ then_branch : ?T, Γ ⊢ else_branch : ?T
------------------------------------------------------------- (if)
?T

// match: the scrutinee is a list; both arms produce the same ?T. The cons arm
// binds the head (?A) and tail (?A list) drawn from the element type, so the
// element type flows from the scrutinee into the arm by unification.
Γ ⊢ scrutinee : ?A list, Γ ⊢ nil_case : ?T, Γ[head:?A][tail:?A list] ⊢ cons_case : ?T
------------------------------------------------------------------------------------- (match)
?T

// let: bind the value's type for the body
Γ ⊢ value : τ, Γ[name:τ] ⊢ body : ?R
------------------------------------- (let)
?R

// let rec: the name is in scope for its own value and the body
Γ[name:τ] ⊢ value : τ, Γ[name:τ] ⊢ body : ?R
--------------------------------------------- (letrec)
?R