Proof language

The elaborator

This page is a draft. Rainbow's authors are reviewing it, and details may change.

rainbow.elaborate (source) is the whole surface language, a “small deterministic surface-to-core elaborator for explicit function propositions”. It turns names into de Bruijn indices and aliases into content ids. It sits outside the trusted base, and the kernel checks what it produces.

(type-expression surface) accepts Prop, bound names, :sort, :-> and :forall, enough for statements without constants such as pure logic over Prop. (core-expression environment surface) also accepts :nat, :const, :app, :fn and :let and resolves aliases in the environment. Proof modules use it for every :type and :value. Both return :elaborated with the core term, or :rejected with an error:

{:status :elaborated
 :surface surface
 :term    core-term
 :trace   [{:operation :explicit-core-elaboration :input surface}]}

{:status :rejected
 :error   {:error/category ... }
 :message "..."}

Surface forms

surface	core result
`Prop`	`[:sort [:zero]]`
a symbol `x`	`[:bound i]`, where `i` is the position of the nearest binder named `x`
`[:sort level]`	`[:sort level]`
`[:nat n]`	`[:nat n]`, for a natural number `n`
`[:const alias levels]`	`[:const id levels]`. `alias` is a symbol or a `"sha256:..."` id.
`[:app f a b ...]`	`[:app [:app f a] b] ...`, at least one argument
`[:-> A B ... Z]`	non-dependent `:pi` from `A` to the arrow of the rest, at least two parts
`[:forall [binding ...] body]`	one `:pi` per binding
`[:fn [binding ...] body]`	one `:lam` per binding
`[:let name type value body]`	`[:let type value body]`, with `name` bound in `body`

A binding is [name type] or [name type mode], with mode :explicit (the default) or :implicit.

An inner binder shadows an outer one with the same name:

(elaborate/core-expression (environment/empty-environment)
                           '[:forall [[x Prop] [x [:-> x x]]] x])
;; :term
[:pi [:sort [:zero]]
     [:pi [:pi [:bound 0] [:bound 1] :explicit] [:bound 0] :explicit]
     :explicit]

The type of the second x refers to the first one, and the body refers to the second. An arrow’s binder has no name, so in [:-> A B] the type B cannot mention the argument. Use :forall when the codomain depends on it.

(elaborate/type-expression '[:forall [[P Prop] [Q Prop]] [:-> P Q P]])
;; :term
[:pi [:sort [:zero]]
     [:pi [:sort [:zero]]
          [:pi [:bound 1] [:pi [:bound 1] [:bound 3] :explicit] :explicit]
          :explicit]
     :explicit]

(elaborate/type-expression '[:forall [[P Prop :implicit]] [:-> P P]])
;; :term
[:pi [:sort [:zero]] [:pi [:bound 0] [:bound 1] :explicit] :implicit]

In the first, P is [:bound 1] under one binder and [:bound 3] under three: Q and the two arrow arguments.

Errors

category	cause
`:elaborate/unknown-name`	a symbol with no binder in scope. The error lists the names in scope.
`:elaborate/unknown-constant`	an alias the environment does not know, or a malformed `:const` form
`:elaborate/invalid-forall`, `:elaborate/invalid-lambda`, `:elaborate/invalid-let`	a malformed binder form
`:elaborate/invalid-binder`	a binder name that is not a symbol
`:elaborate/invalid-sort`	`[:sort x]` where `x` is not a level
`:elaborate/invalid-literal`	`[:nat n]` where `n` is not a natural number
`:elaborate/arrow-arity`	an arrow with fewer than two parts
`:elaborate/application-arity`	`[:app f]` with no argument
`:elaborate/unsupported-form`	anything else, such as `:app`, `:const` or `:fn` in `type-expression`

(elaborate/type-expression 'y)
;=> {:status :rejected,
;    :error {:name y, :context [], :error/category :elaborate/unknown-name},
;    :message "Unknown surface name"}

You write every argument

The elaborator has no type inference, unification, implicit arguments, overloading, notation or holes. You write every argument, universe level and type annotation. An ill-typed term still comes back :elaborated, and the kernel rejects it when you check it.

For abbreviations, write Clojure functions that return surface vectors, such as (defn- accuracy [correct total] ...) in the accuracy module. Terms and binders lists the helpers the corpus shares.