DomainData.Make
module Symbol : Basis.Symbol.S
module S : sig ... end
module CofVar : sig ... end
module Dim : sig ... end
module Cof : sig ... end
type dim = Dim.t
type cof_var = CofVar.t
type cof = Cof.t
type 'a stable_code = [
|
`Pi of 'a * 'a
Dependent product type
*)|
`Sg of 'a * 'a
Dependent sum type
*)|
`Signature of kan_tele
First-Class Record types
*)|
`Ext of int * 'a * [ `Global of 'a ] * 'a
Extension type
*)|
`Nat
Natural numbers type
*)|
`Circle
The circle S1
.
|
`Univ
A code for the universe (antinomous for now).
*) ]
A type code whose head constructor is stable under dimension substitution.
and 'a unstable_code = [
|
`HCom of dim * dim * cof * 'a
Formal composite types
*)|
`V of dim * 'a * 'a * 'a
V types, for univalence
*) ]
A type code which may or may not be stable under dimension substitution. That is, type codes with these constructors may or may not remain in normal forms under substitution.
A closure combines a semantic environment with a syntactic object binding an additional variable.
and kan_tele_clo = S.kan_tele clo
and con =
| Lam of Ident.t * tm_clo
| BindSym of DimProbe.t * con
A nominal binder of a dimension; these are used during the execution of coercion, which must probe a line of type codes with a fresh dimension.
*)| LetSym of dim * DimProbe.t * con
An explicit substitution of a dimension for a symbol.
*)| Cut of {
}
| Zero
| Suc of con
| Base
| Loop of dim
| Pair of con * con
| Struct of fields
| SubIn of con
| ElIn of con
The introduction form for the extension of a stable type code only (see ElStable
and ElUnstable
).
| Dim0
| Dim1
| DimProbe of DimProbe.t
| Cof of (con, con) Kado.Syntax.endo
A mixin of the language of cofibrations (as described in CofBuilder
), with dimensions and indeterminates in con
.
| Prf
| FHCom of [ `Nat | `Circle ] * dim * dim * cof * con
| StableCode of con stable_code
| UnstableCode of con unstable_code
| Box of dim * dim * cof * con * con
| VIn of dim * con * con * con
| Split of (cof * tm_clo) list
Value constructors are governed by con
; we do not maintain in the datatype a priori any invariant that these represent whnfs (weak head normal forms). Whether a value constructor is a whnf is contingent on the ambient local state, such as the cofibration theory.
A head is a variable (e.g. Global
, Var
), or it is some kind of unstable elimination form (Coe
, UnstableCut
). The geometry of cut
, hd
, unstable_frm
enables a very direct way to re-reduce a complex cut to whnf by following the unstable nodes to the root.
A stable frame is a dimension substitution-stable elimination form with a hole in place of its principal argument. Unstable elimination forms are governed by hd
to ease the "re-reduction" of a value to whnf under a stronger cofibration theory.
An unstable frame is a dimension substitution-unstable elimination form with a hole in place of its principal argument.
module CofBuilder : sig ... end