definition for a toy barebones dependently typed language

AST.lean

/-
  we use different types for the name of a variable when *binding* (i.e. declaring)
  as opposed to *referencing* it. these two types will often be similar or identical,
  but in general there are reasons for them to differ; some examples are:
  - **namespacing**: when binding a variable you specify an identifier (a name) and it
    gets placed in the current namespace. but when referencing we may want to reach
    for another namespace or subnamespace.
  - **autonaming**: names are discarded when the proof is serialized for production use.
    the production interpreter auto-assigns names based on e.g. autoincrementing, so
    no info is required when binding a variable (`VarName := Unit`) but a natural index
    is required to reference it (`VarRef := Nat`).
  - **unnamed variables**: `VarRef := α` but `VarName := Option α`, to allow not giving
    the variable a name.

  unless stated otherwise, when you find a `VarName` or `Binding` below, the new variable
  is added to the scope for any expressions that follow, and only those. for example in
  a `Lambda` node, the `param` variable is in scope for `body`; in an `InductiveType`
  node, the `type` variable is in scope for the `constructors`.
-/
variable (VarName VarRef : Type)

mutual

  /-- a variable declared with a certain name and type. `type` MUST be a type -/
  structure Binding where
    name : VarName
    type : Term

  /--
    input representation of a value in our type theory, i.e. an AST node.

    in the descriptions below, "MUST" is a requirement for the node to typecheck. \
    an implied requirement is that any subnode MUST typecheck. \
    when we say that a term "MUST be a type" means it MUST typecheck to `Universe`.
  -/
  inductive Term where
    /-- **universe type** (the type of all types) -/
    | Universe

    /-- **reference to a variable**, which MUST be in scope -/
    | Variable (name : VarRef)

    /--
      **function call** ("application" in lambda calculus).
      `function` MUST typecheck to a function type, and `argument` MUST typecheck to the function type's argument type.
    -/
    | Call (function argument : Term)

    /--
      **let..in expression**, i.e. syntactic sugar for `result` but with references to variable `name`
      replaced with `value`. you might think this could be achieved with a self-calling lambda
      (`(λ name. result)(value)`) but that doesn't work because for the lambda to be well-typed,
      any references to `name` in it cannot be allowed to expand to `value`. of course we could
      have the type-checker detect this pattern and apply the substitution *before* the
      type-checking (effectively bypassing the requirement for the lambda to be well typed, since
      it's never otherwise observed) but this could produce unexpected results,
      and even then you still need to state the type of `value` (which this node does not require).
    -/
    | Let (value : Term) (name : VarName) (result : Term)

    /-- **anonymous function** ("abstraction" in lambda calculus) -/
    | Lambda (param : Binding) (body : Term)

    /-- **function type**. `body` MUST be a type -/
    | FunctionType (param : Binding) (body : Term)

    /--
      **inductive type (or indexed type family)**. there are several complex restrictions:
      - the binding's term MUST normalize to a chain of function types ending in `Universe`.
      - each of `constructors` MUST be a chain of function types ending in *a fully applied reference to the binding*.
        - each of these parameter types MUST either not reference the binding at all, or normalize to
          a chain of function types ending in *a fully applied reference to the binding*.
    -/
    | InductiveType (type : Binding) (constructors : Array Term)

    /-- **inductive type constructor**. `type` MUST be an inductive type and `index` MUST be a valid constructor index -/
    | Constructor (type : Term) (index : Nat)

    /-- **inductive type eliminator** (induction principle). `type` MUST be an inductive type. -/
    | Destructor (type : Term)

end

Format.lean

import Test.minilang.AST
namespace Format

class ShowVar (α : Type) where
  fmt : α → String

instance : ShowVar Nat where
  fmt n := s!"#{n}"

def reservedIdents := #["let", "ctor", "elim", "inductive", "with"]
def allowedChars := ".αβ_-⊥∑׬".chars.toArray

instance : ShowVar String where
  fmt n :=
    if n.all (λ c ↦ c.isAlphanum || allowedChars.contains c) && !(reservedIdents.contains n)
      then n else s!"#{repr n}"

class ShowVarName (α : Type) extends ShowVar α where
  isNamed : α → Bool

instance : ShowVarName Nat where
  isNamed _ := true
instance : ShowVarName String where
  isNamed n := n != "_"

variable {VarName VarRef : Type} [ShowVarName VarName] [ShowVar VarRef]

inductive Context where
| None
| WeakBinder -- syntactically like None, but the surrounding context is visually weak, so quote further weak binders
| CallFunction
| FunctionTypeAnonArg
| Atomic
deriving BEq, Ord

instance : LT Context := ltOfOrd
instance : LE Context := leOfOrd

-- maximum allowed precedence value to omit quoting a term
def maxUnquotedContext : Term VarName VarRef → Context
| .Universe => .Atomic
| .Variable _ => .Atomic
| .Constructor _ _ => .Atomic
| .Destructor _ => .Atomic
| .Call _ _ => .FunctionTypeAnonArg
| .Lambda _ _ => .None
| .Let _ _ _ => .None
| _ => .WeakBinder

def format (term : Term VarName VarRef) (ctx : Context := .None) : Std.Format :=
  -- check if the spot we're printing for requires this term to be quoted
  let quoted := !( ctx <= maxUnquotedContext term )
  -- if this term is being quoted, then we forget any context restrictions
  let ctx := if quoted then .None else ctx

  let result := match term with
  -- atoms
  | .Universe => .text "𝓤"
  | .Variable name => .text (ShowVar.fmt name)
  -- atom-like
  | .Constructor type idx => .text "ctor" ++ (format type).paren ++ .text s!"#{idx}"
  | .Destructor type => .text "elim" ++ (format type).paren
  -- modifier nodes (end with a 'body' term that mostly decides its result / type, and inherits context restrictions)
  | .FunctionType (.mk name type) body =>
    let header := match ShowVarName.isNamed name with
    | true => .text s!"({ShowVar.fmt name} :" ++ (format type).indentD ++ .text ") →"
    | false => (format type .FunctionTypeAnonArg) ++ .text " →"
    .group header ++ .line ++ format body ctx
  | .Lambda (.mk name type) body =>
    let header := .text s!"λ {ShowVar.fmt name} :" ++ (format type .WeakBinder).indentD ++ .text ","
    .group header ++ .line ++ format body ctx
  | .Let value name result =>
    let header := .text s!"let {ShowVar.fmt name} =" ++ (format value).indentD ++ .text ";"
    .group header ++ .line ++ format result ctx
  -- others
  | .InductiveType (.mk name type) ctors =>
    let header := .text s!"inductive {ShowVar.fmt name} :" ++ (format type).indentD ++ .line ++ .text "with "
    .group header ++ .sbracket (.line ++ .joinSep (ctors.map format).toList (.text " |" ++ .line) ++ .text " ")
  | .Call func arg =>
    let repr := (format func .CallFunction) ++ .indentD (format arg .Atomic)
    if ctx == .CallFunction then repr else repr.group

  if quoted then result.paren else result

instance : Std.ToFormat (Term VarName VarRef) := { format }