mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 00:31:57 +03:00
106235c165
If available (sometimes, say a top level expression, it might need inferring so there'll be no goal available). Also add the ability to log the current goal, or indeed any term.
60 lines
1.2 KiB
Idris
60 lines
1.2 KiB
Idris
module Language.Reflection
|
|
|
|
import public Language.Reflection.TT
|
|
import public Language.Reflection.TTImp
|
|
|
|
export
|
|
data Elab : Type -> Type where
|
|
Pure : a -> Elab a
|
|
Bind : Elab a -> (a -> Elab b) -> Elab b
|
|
LogMsg : Nat -> String -> Elab ()
|
|
LogTerm : Nat -> String -> TTImp -> Elab ()
|
|
|
|
-- Check a TTImp term against the current goal type
|
|
Check : TTImp -> Elab TT
|
|
-- Get the current goal type, if known
|
|
-- (it might need to be inferred from the solution)
|
|
Goal : Elab (Maybe TTImp)
|
|
|
|
mutual
|
|
export
|
|
Functor Elab where
|
|
map f e = do e' <- e
|
|
pure (f e')
|
|
|
|
export
|
|
Applicative Elab where
|
|
pure = Pure
|
|
f <*> a = do f' <- f
|
|
a' <- a
|
|
pure (f' a')
|
|
|
|
export
|
|
Monad Elab where
|
|
(>>=) = Bind
|
|
|
|
export
|
|
logMsg : Nat -> String -> Elab ()
|
|
logMsg = LogMsg
|
|
|
|
export
|
|
logTerm : Nat -> String -> TTImp -> Elab ()
|
|
logTerm = LogTerm
|
|
|
|
export
|
|
logGoal : Nat -> String -> Elab ()
|
|
logGoal n msg
|
|
= do g <- Goal
|
|
case g of
|
|
Nothing => pure ()
|
|
Just t => logTerm n msg t
|
|
|
|
-- Check a TTImp term against the current goal type
|
|
export
|
|
check : TTImp -> Elab TT
|
|
check = Check
|
|
|
|
export
|
|
goal : Elab (Maybe TTImp)
|
|
goal = Goal
|