Agda.TypeChecking.Reduce

Documentation

traceFun :: String -> TCM a -> TCM a

traceFun' :: Show a => 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 :: t -> TCM t

Instances

Instantiate Telescope

Instantiate LevelAtom

Instantiate PlusLevel

Instantiate Level

Instantiate Sort

Instantiate Elim

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 :: t -> TCM t

reduceB :: t -> TCM (Blocked t)

Instances

Reduce Telescope

Reduce LevelAtom

Reduce PlusLevel

Reduce Level

Reduce Sort

Reduce Elim

Reduce Type

Reduce Term

Reduce Constraint

Reduce t => Reduce [t]

Reduce t => Reduce (Arg t)

(Raise 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 :: 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 :: t -> TCM t

Instances

Normalise Pattern

Normalise ClauseBody

Normalise LevelAtom

Normalise PlusLevel

Normalise Level

Normalise Sort

Normalise Elim

Normalise Type

Normalise Term

Normalise DisplayForm

Normalise Constraint

Normalise ProblemConstraint

Normalise t => Normalise [t]

Normalise a => Normalise (Maybe a)

Normalise t => Normalise (Arg t)

(Raise t, Normalise t) => Normalise (Abs t)

(Raise a, 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 :: t -> TCM t

Instances

InstantiateFull Char

InstantiateFull ModuleName

InstantiateFull Name

InstantiateFull Pattern

InstantiateFull ClauseBody

InstantiateFull Clause

InstantiateFull LevelAtom

InstantiateFull PlusLevel

InstantiateFull Level

InstantiateFull Sort

InstantiateFull Elim

InstantiateFull Type

InstantiateFull Term

InstantiateFull CompiledClauses

InstantiateFull Scope

InstantiateFull FunctionInverse

InstantiateFull Defn

InstantiateFull Definition

InstantiateFull DisplayTerm

InstantiateFull DisplayForm

InstantiateFull Section

InstantiateFull Signature

InstantiateFull Constraint

InstantiateFull ProblemConstraint

InstantiateFull Interface

InstantiateFull t => InstantiateFull [t]

InstantiateFull a => InstantiateFull (Maybe a)

InstantiateFull t => InstantiateFull (Arg t)

(Raise t, InstantiateFull t) => InstantiateFull (Abs t)

(Raise a, 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 :: Type -> TCM TelView

telViewM t is like telView' t, but it reduces t to expose function type constructors.