Module SyntaxData.Make

Parameters

Signature

module Cof = Kado.Syntax.Endo
type t =
  1. | Var of int
  2. | Global of Symbol.t
  3. | Let of t * Ident.t * t
  4. | Ann of t * tp
  5. | Zero
  6. | Suc of t
  7. | NatElim of t * t * t * t
  8. | Base
  9. | Loop of t
  10. | CircleElim of t * t * t * t
  11. | Lam of Ident.t * t
  12. | Ap of t * t
  13. | Pair of t * t
  14. | Fst of t
  15. | Snd of t
  16. | Struct of fields
  17. | Proj of t * Ident.t * int
  18. | Coe of t * t * t * t
  19. | HCom of t * t * t * t * t
  20. | Com of t * t * t * t * t
  21. | SubIn of t
  22. | SubOut of t
  23. | Dim0
  24. | Dim1
  25. | Cof of (t, t) Cof.t
  26. | ForallCof of t
  27. | CofSplit of (t * t) list
  28. | Prf
  29. | ElIn of t
  30. | ElOut of t
  31. | Box of t * t * t * t * t
  32. | Cap of t * t * t * t * t
  33. | VIn of t * t * t * t
  34. | VProj of t * t * t * t * t
  35. | CodeExt of int * t * [ `Global of t ] * t
  36. | CodePi of t * t
  37. | CodeSg of t * t
  38. | CodeSignature of kan_tele
  39. | CodeNat
  40. | CodeUniv
  41. | CodeV of t * t * t * t
  42. | CodeCircle
  43. | ESub of sub * t
    (*

    Explicit substition

    *)
and tp =
  1. | Univ
  2. | El of t
  3. | TpVar of int
  4. | TpDim
  5. | TpCof
  6. | TpPrf of t
  7. | TpCofSplit of (t * tp) list
  8. | Sub of tp * t * t
  9. | Pi of tp * Ident.t * tp
  10. | Sg of tp * Ident.t * tp
  11. | Signature of tele
  12. | Nat
  13. | Circle
  14. | TpESub of sub * tp
and tele =
  1. | ElTele of kan_tele
  2. | Cell of Ident.t * tp * tele
  3. | Empty
and kan_tele =
  1. | KCell of Ident.t * t * kan_tele
  2. | KEmpty
and fields =
  1. | Fields of (Ident.t * t) list
  2. | Unpack of Ident.t list * t
    (*

    Unpack a Struct into its list of fields.

    *)
  3. | MCoe of Ident.t * kan_tele * t * t * fields
    (*

    Coercion along a line in a telescope. The kan_tele has a free variable for a dimension variable.

    *)
  4. | MCom of kan_tele * t * t * t * fields
    (*

    Composition in a telescope, provided a list of systems.

    *)
and sub =
  1. | SbI
    (*

    The identity substitution Γ → Γ.

    *)
  2. | SbC of sub * sub
    (*

    The composition of substitutions δ ∘ γ.

    *)
  3. | Sb1
    (*

    The terminal substitution Γ → 1.

    *)
  4. | SbE of sub * t
    (*

    The universal substitution into an extended context <γ, a>.

    *)
  5. | SbP
    (*

    The projection from a extended context Γ.A → Γ.

    *)

The language of substitions from Abel, Coquand, and Pagano.

module CofBuilder : sig ... end