Module Syntax.Make

Parameters

Signature

include sig ... end
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
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
  3. | MCoe of Ident.t * kan_tele * t * t * fields
  4. | MCom of kan_tele * t * t * t * fields
and sub =
  1. | SbI
  2. | SbC of sub * sub
  3. | Sb1
  4. | SbE of sub * t
  5. | SbP
module CofBuilder : sig ... end
val tm_abort : t

Convenience constructors

val tp_abort : tp
val tele_lbls : tele -> Ident.t list
val kan_tele_lbls : kan_tele -> Ident.t list
val rename_tele : (Ident.t -> Ident.t option) -> tele -> tele
val rename_kan_tele : (Ident.t -> Ident.t option) -> kan_tele -> kan_tele
val append_tele : tele -> tele -> tele

Append two kan telescopes together. INVARIANT: The second telescope is well-scoped with regard to the first.

val append_kan_tele : kan_tele -> kan_tele -> kan_tele

Append two kan telescopes together. INVARIANT: The second telescope is well-scoped with regard to the first.

Pretty printers

For display

These pretty printers are context sensitive, in order to recall user-specified names for binders.

Print a core language term.

Print a signature.

Print a core language type.

val pp_sequent : lbl:string option -> (Ident.t * tp) list -> tp Basis.Pp.printer

Vertically print an iterated dependent product type as if it were a sequent, for display of goals.

val pp_partial_sequent : [< `BdrySat | `BdryUnsat ] -> (Ident.t * tp) list -> (t * tp) Basis.Pp.printer

Vertically print an iterated dependent product type as if it were a sequent, for display of goals. This variant will also print out a partially constructed terms, as well as display if the boundary conditions are met.

For debugging

When debugging, we are not likely to have enough context to use the nice pretty printers above; as a last resort, dump and dump_tp may be used.

val dump : t Basis.Pp.printer
val dump_tele : tele Basis.Pp.printer
val dump_kan_tele : kan_tele Basis.Pp.printer
val dump_tp : tp Basis.Pp.printer