Agda.TypeChecking.Reduce

Documentation

traceFun :: MonadTCM tcm => String -> tcm a -> tcm a

traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a

class Instantiate t where

Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).

Methods

instantiate :: MonadTCM tcm => t -> tcm t

Instances

Instantiate Telescope

Instantiate Sort

Instantiate Type

Instantiate Term

Instantiate Constraint

Instantiate t => Instantiate [t]

Instantiate t => Instantiate (Arg t)

Instantiate t => Instantiate (Abs t)

Instantiate a => Instantiate (Blocked a)

Instantiate a => Instantiate (Closure a)

(Instantiate a, Instantiate b) => Instantiate (a, b)

(Ord k, Instantiate e) => Instantiate (Map k e)

(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c)

class Reduce t where

Methods

reduce :: MonadTCM tcm => t -> tcm t

reduceB :: MonadTCM tcm => t -> tcm (Blocked t)

Instances

Reduce Telescope

Reduce Sort

Reduce Type

Reduce Term

Reduce Constraint

Reduce t => Reduce [t]

Reduce t => Reduce (Arg t)

Reduce t => Reduce (Abs t)

Reduce a => Reduce (Closure a)

(Reduce a, Reduce b) => Reduce (a, b)

(Ord k, Reduce e) => Reduce (Map k e)

(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c)

unfoldDefinition :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term)

If the first argument is True, then a single delayed clause may be unfolded.

Normalisation

class Normalise t where

Methods

normalise :: MonadTCM tcm => t -> tcm t

Instances

Normalise Pattern

Normalise ClauseBody

Normalise Sort

Normalise Type

Normalise Term

Normalise DisplayForm

Normalise Constraint

Normalise t => Normalise [t]

Normalise a => Normalise (Maybe a)

Normalise t => Normalise (Arg t)

Normalise t => Normalise (Abs t)

Normalise a => Normalise (Tele a)

Normalise a => Normalise (Closure a)

(Normalise a, Normalise b) => Normalise (a, b)

(Ord k, Normalise e) => Normalise (Map k e)

(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c)

Full instantiation

class InstantiateFull t where

Methods

instantiateFull :: MonadTCM tcm => t -> tcm t

Instances

InstantiateFull Char

InstantiateFull ModuleName

InstantiateFull Name

InstantiateFull Pattern

InstantiateFull ClauseBody

InstantiateFull Clause

InstantiateFull Clauses

InstantiateFull Sort

InstantiateFull Type

InstantiateFull Term

InstantiateFull Scope

InstantiateFull CompiledClauses

InstantiateFull FunctionInverse

InstantiateFull Defn

InstantiateFull Definition

InstantiateFull DisplayTerm

InstantiateFull DisplayForm

InstantiateFull Section

InstantiateFull Signature

InstantiateFull Constraint

InstantiateFull Interface

InstantiateFull t => InstantiateFull [t]

InstantiateFull a => InstantiateFull (Maybe a)

InstantiateFull t => InstantiateFull (Arg t)

InstantiateFull t => InstantiateFull (Abs t)

InstantiateFull a => InstantiateFull (Tele a)

InstantiateFull a => InstantiateFull (Case a)

InstantiateFull a => InstantiateFull (Builtin a)

InstantiateFull a => InstantiateFull (Open a)

InstantiateFull a => InstantiateFull (Closure a)

(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b)

(Ord k, InstantiateFull e) => InstantiateFull (Map k e)

(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c)

telViewM :: MonadTCM tcm => Type -> tcm TelView