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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.EtaContract

Description

Compute eta short normal forms.

Synopsis

- data BinAppView
  - = App Term (Arg Term)
  - | NoApp Term
- binAppView :: Term -> BinAppView
- etaContract :: (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a
- etaOnce :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term
- etaCon :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => ConHead -> ConInfo -> Elims -> (QName -> ConHead -> ConInfo -> Args -> m Term) -> m Term
- etaLam :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => ArgInfo -> ArgName -> Term -> m Term

# Documentation

data BinAppView Source #

Constructors

App Term (Arg Term) |
NoApp Term |

binAppView :: Term -> BinAppView Source #

etaContract :: (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a Source #

Contracts all eta-redexes it sees without reducing.

etaOnce :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term Source #

etaCon Source #

Arguments

:: (MonadTCEnv m, HasConstInfo m, HasOptions m) |
=> ConHead | Constructor name `c`.
-> ConInfo | Constructor info `ci`.
-> Elims | Constructor arguments `args`.
-> (QName -> ConHead -> ConInfo -> Args -> m Term) | Eta-contraction workhorse, gets also name of record type.
-> m Term | Returns `Con c ci args` or its eta-contraction.

If record constructor, call eta-contraction function.

etaLam Source #

Arguments

:: (MonadTCEnv m, HasConstInfo m, HasOptions m) |
=> ArgInfo | Info `i` of the `Lam`.
-> ArgName | Name `x` of the abstraction.
-> Term | Body (`Term`) `b` of the `Abs`.
-> m Term | `Lam i (Abs x b)`, eta-contracted if possible.

Try to contract a lambda-abstraction `Lam i (Abs x b)`.