mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 16:51:51 +03:00
9544e05da1
Still all they can do is check and log. Now scripts must return something of type TT, which is in practice a TTImp that goes to the elaborator for final checking
31 lines
635 B
Idris
31 lines
635 B
Idris
module Language.Reflection
|
|
|
|
import public Language.Reflection.TT
|
|
import public Language.Reflection.TTImp
|
|
|
|
public export
|
|
data Elab : Type -> Type where
|
|
Pure : a -> Elab a
|
|
Bind : Elab a -> (a -> Elab b) -> Elab b
|
|
Log : Nat -> String -> Elab ()
|
|
|
|
-- Check a TTImp term against the current goal type
|
|
Check : TTImp -> Elab TT
|
|
|
|
mutual
|
|
public export
|
|
Functor Elab where
|
|
map f e = do e' <- e
|
|
pure (f e')
|
|
|
|
public export
|
|
Applicative Elab where
|
|
pure = Pure
|
|
f <*> a = do f' <- f
|
|
a' <- a
|
|
pure (f' a')
|
|
|
|
public export
|
|
Monad Elab where
|
|
(>>=) = Bind
|