Module Core.Monads

All the monads in this file keep track of a cofibration theory.

module D := CodeUnit.Domain
module S := CodeUnit.Syntax
module St := RefineState
type 'a compute
type 'a evaluate
type 'a conversion
type 'a quote
module CmpM : sig ... end

The "computation" monad; contains enough state to run computations in the semantic domain, does not contain a variable environment or anything that would be needed for evaluation.

module EvM : sig ... end

The "evaluation" monad; like the computation monad but keeps a variable environment.

module ConvM : sig ... end

The conversion environment keeps track of De Bruijn indices for use in conversion checking.

module QuM : sig ... end

The quotation environment keeps track of De Bruijn indices for quotation.

module RefineM : sig ... end

The elaboration monad is the "maximal" monad that can run code from any of the other monads.