Module Domain.Make

Parameters

Signature

include sig ... end
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. | `Circle
  2. | `Ext of int * 'a * [ `Global of 'a ] * 'a
  3. | `Nat
  4. | `Pi of 'a * 'a
  5. | `Sg of 'a * 'a
  6. | `Signature of kan_tele
  7. | `Univ
]
and !'a unstable_code = [
  1. | `HCom of dim * dim * cof * 'a
  2. | `V of dim * 'a * 'a * 'a
]
and env = {
  1. tpenv : tp Bwd.bwd;
  2. conenv : con Bwd.bwd;
}
and !'a clo =
  1. | Clo of 'a * env
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
  3. | LetSym of dim * DimProbe.t * con
  4. | Cut of {
    1. tp : tp;
    2. cut : 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
  13. | Dim0
  14. | Dim1
  15. | DimProbe of DimProbe.t
  16. | Cof of (con, con) Kado.Syntax.endo
  17. | Prf
  18. | FHCom of [ `Circle | `Nat ] * 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
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
  2. | Var of int
  3. | Coe of con * dim * dim * con
  4. | UnstableCut of cut * unstable_frm
and cut = hd * frm list
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
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
module CofBuilder : sig ... end

Convenience constructors

val dim_to_con : dim -> con
val cof_to_con : cof -> con
val mk_var : tp -> int -> con
val push : frm -> cut -> cut
val const_tm_clo : con -> tm_clo
val const_tp_clo : tp -> tp_clo
val un_lam : con -> tm_clo
val compose : con -> con -> con
val apply_to : con -> tm_clo
val fst : con
val snd : con
val proj : Ident.t -> int -> con
val el_out : con
val tm_abort : con
val tp_abort : tp
val tele_lbls : tele -> Ident.t list
val kan_tele_lbls : kan_tele -> Ident.t list
val empty_env : env
val extend_env : env -> con -> env

Pretty-printers

These are only for debugging.

val pp_dim : dim Basis.Pp.printer
val pp_cof : cof Basis.Pp.printer
val pp_tp : tp Basis.Pp.printer
val pp_con : con Basis.Pp.printer
val pp_cut : cut Basis.Pp.printer
val pp_hd : hd Basis.Pp.printer
val pp_frame : frm Basis.Pp.printer
val pp_spine : frm list Basis.Pp.printer
val pp_tele : tele Basis.Pp.printer
val pp_kan_tele : kan_tele Basis.Pp.printer