Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Translation.InternalToAbstract

Description

Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.

TODO

  • numbers on metas
  • fake dependent functions to independent functions
  • meta parameters
  • shadowing

Synopsis

Documentation

class Reify i a | i -> a where #

Minimal complete definition

reify

Methods

reify :: i -> TCM a #

reifyWhen :: Bool -> i -> TCM a #

Instances

Reify MetaId Expr # 

Methods

reify :: MetaId -> TCM Expr #

reifyWhen :: Bool -> MetaId -> TCM Expr #

Reify Name Name # 

Methods

reify :: Name -> TCM Name #

reifyWhen :: Bool -> Name -> TCM Name #

Reify Literal Expr # 
Reify Level Expr # 

Methods

reify :: Level -> TCM Expr #

reifyWhen :: Bool -> Level -> TCM Expr #

Reify Sort Expr # 

Methods

reify :: Sort -> TCM Expr #

reifyWhen :: Bool -> Sort -> TCM Expr #

Reify Telescope Telescope # 
Reify Type Expr # 

Methods

reify :: Type -> TCM Expr #

reifyWhen :: Bool -> Type -> TCM Expr #

Reify Term Expr # 

Methods

reify :: Term -> TCM Expr #

reifyWhen :: Bool -> Term -> TCM Expr #

Reify Expr Expr # 

Methods

reify :: Expr -> TCM Expr #

reifyWhen :: Bool -> Expr -> TCM Expr #

Reify DisplayTerm Expr # 
Reify NamedClause Clause # 
Reify (QNamed Clause) Clause # 
Reify i a => Reify [i] [a] # 

Methods

reify :: [i] -> TCM [a] #

reifyWhen :: Bool -> [i] -> TCM [a] #

Reify i a => Reify (Dom i) (Arg a) # 

Methods

reify :: Dom i -> TCM (Arg a) #

reifyWhen :: Bool -> Dom i -> TCM (Arg a) #

Reify i a => Reify (Arg i) (Arg a) #

Skip reification of implicit and irrelevant args if option is off.

Methods

reify :: Arg i -> TCM (Arg a) #

reifyWhen :: Bool -> Arg i -> TCM (Arg a) #

Reify i a => Reify (Elim' i) (Elim' a) # 

Methods

reify :: Elim' i -> TCM (Elim' a) #

reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) #

(Free i, Reify i a) => Reify (Abs i) (Name, a) # 

Methods

reify :: Abs i -> TCM (Name, a) #

reifyWhen :: Bool -> Abs i -> TCM (Name, a) #

(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) # 

Methods

reify :: (i1, i2) -> TCM (a1, a2) #

reifyWhen :: Bool -> (i1, i2) -> TCM (a1, a2) #

Reify i a => Reify (Named n i) (Named n a) # 

Methods

reify :: Named n i -> TCM (Named n a) #

reifyWhen :: Bool -> Named n i -> TCM (Named n a) #

(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) # 

Methods

reify :: (i1, i2, i3) -> TCM (a1, a2, a3) #

reifyWhen :: Bool -> (i1, i2, i3) -> TCM (a1, a2, a3) #

(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) # 

Methods

reify :: (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) #

reifyWhen :: Bool -> (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) #

data NamedClause #

Constructors

NamedClause QName Bool Clause

Also tracks whether module parameters should be dropped from the patterns.

reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern] #

Assumes that pattern variables have been added to the context already. Picks pattern variable names from context.