Syntax.Make
module Symbol : Basis.Symbol.S
include sig ... end
type t =
| Var of int
| Global of Symbol.t
| Let of t * Ident.t * t
| Ann of t * tp
| Zero
| Suc of t
| NatElim of t * t * t * t
| Base
| Loop of t
| CircleElim of t * t * t * t
| Lam of Ident.t * t
| Ap of t * t
| Pair of t * t
| Fst of t
| Snd of t
| Struct of fields
| Proj of t * Ident.t * int
| Coe of t * t * t * t
| HCom of t * t * t * t * t
| Com of t * t * t * t * t
| SubIn of t
| SubOut of t
| Dim0
| Dim1
| Cof of (t, t) Cof.t
| ForallCof of t
| CofSplit of (t * t) list
| Prf
| ElIn of t
| ElOut of t
| Box of t * t * t * t * t
| Cap of t * t * t * t * t
| VIn of t * t * t * t
| VProj of t * t * t * t * t
| CodeExt of int * t * [ `Global of t ] * t
| CodePi of t * t
| CodeSg of t * t
| CodeSignature of kan_tele
| CodeNat
| CodeUniv
| CodeV of t * t * t * t
| CodeCircle
| ESub of sub * t
module CofBuilder : sig ... end
val tm_abort : t
Convenience constructors
val tp_abort : tp
Append two kan telescopes together. INVARIANT: The second telescope is well-scoped with regard to the first.
Append two kan telescopes together. INVARIANT: The second telescope is well-scoped with regard to the first.
These pretty printers are context sensitive, in order to recall user-specified names for binders.
val pp : Basis.Pp.env -> t Basis.Pp.printer
Print a core language term.
val pp_tele : Basis.Pp.env -> tele Basis.Pp.printer
Print a signature.
val pp_tp : Basis.Pp.env -> tp Basis.Pp.printer
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.
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