Module DomainData.Make

Parameters

Signature

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 = [
  1. | `Pi of 'a * 'a
    (*

    Dependent product type

    *)
  2. | `Sg of 'a * 'a
    (*

    Dependent sum type

    *)
  3. | `Signature of kan_tele
    (*

    First-Class Record types

    *)
  4. | `Ext of int * 'a * [ `Global of 'a ] * 'a
    (*

    Extension type

    *)
  5. | `Nat
    (*

    Natural numbers type

    *)
  6. | `Circle
    (*

    The circle S1.

    *)
  7. | `Univ
    (*

    A code for the universe (antinomous for now).

    *)
]

A type code whose head constructor is stable under dimension substitution.

and 'a unstable_code = [
  1. | `HCom of dim * dim * cof * 'a
    (*

    Formal composite types

    *)
  2. | `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.

and env = {
  1. tpenv : tp Bwd.bwd;
  2. conenv : con Bwd.bwd;
}
and 'a clo =
  1. | Clo of 'a * env

A closure combines a semantic environment with a syntactic object binding an additional variable.

and tp_clo = S.tp clo
and tm_clo = S.t clo
and tele_clo = S.tele clo
and kan_tele_clo = S.kan_tele clo
and con =
  1. | Lam of Ident.t * tm_clo
  2. | 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.

    *)
  3. | LetSym of dim * DimProbe.t * con
    (*

    An explicit substitution of a dimension for a symbol.

    *)
  4. | Cut of {
    1. tp : tp;
    2. cut : cut;
    }
    (*

    Our notion of neutral value, a type annotated cut.

    *)
  5. | Zero
  6. | Suc of con
  7. | Base
  8. | Loop of dim
  9. | Pair of con * con
  10. | Struct of fields
  11. | SubIn of con
  12. | ElIn of con
    (*

    The introduction form for the extension of a stable type code only (see ElStable and ElUnstable).

    *)
  13. | Dim0
  14. | Dim1
  15. | DimProbe of DimProbe.t
  16. | Cof of (con, con) Kado.Syntax.endo
    (*

    A mixin of the language of cofibrations (as described in CofBuilder), with dimensions and indeterminates in con.

    *)
  17. | Prf
  18. | FHCom of [ `Nat | `Circle ] * dim * dim * cof * con
  19. | StableCode of con stable_code
  20. | UnstableCode of con unstable_code
  21. | Box of dim * dim * cof * con * con
  22. | VIn of dim * con * con * con
  23. | 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.

and tp =
  1. | Sub of tp * cof * tm_clo
  2. | Univ
  3. | ElCut of cut
  4. | ElStable of con stable_code
  5. | ElUnstable of con unstable_code
  6. | TpDim
  7. | TpCof
  8. | TpPrf of cof
  9. | TpSplit of (cof * tp_clo) list
  10. | Pi of tp * Ident.t * tp_clo
  11. | Sg of tp * Ident.t * tp_clo
  12. | Signature of tele
  13. | Nat
  14. | Circle
and tele =
  1. | Cell of Ident.t * tp * S.tele clo
  2. | Empty
and kan_tele =
  1. | KCell of Ident.t * con * S.kan_tele clo
  2. | KEmpty
and fields =
  1. | Fields of (Ident.t * con) list
and hd =
  1. | Global of Symbol.t
    (*

    A top-level declaration

    *)
  2. | Var of int
    (*

    De Bruijn level

    *)
  3. | Coe of con * dim * dim * con
  4. | UnstableCut of cut * unstable_frm

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.

and cut = hd * frm list

A cut is a value that is blocked on the computation of a hd ("head"); when the head is computed, the list of stack frames (frm) carried by the cut will be enacted.

and frm =
  1. | KAp of tp * con
  2. | KFst
  3. | KSnd
  4. | KProj of Ident.t * int
  5. | KNatElim of con * con * con
  6. | KCircleElim of con * con * con
  7. | KElOut
    (*

    The elimination form for the extension of a stable type code only (see ElStable).

    *)

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.

and unstable_frm =
  1. | KHCom of dim * dim * cof * con
  2. | KCap of dim * dim * cof * con
  3. | KVProj of dim * con * con * con
  4. | KSubOut of cof * tm_clo

An unstable frame is a dimension substitution-unstable elimination form with a hole in place of its principal argument.

module CofBuilder : sig ... end