git.iko.soy/Idris-dev
on master help sign in
Make "getGuess" fail if there's no guess present
5f9e595David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+2−2
compare with master
unifiedsplit
@@ -113,7 +113,7 @@ data Elab : Type -> Type where
113 Prim__Env : Elab (List (TTName, Binder TT))
113 Prim__Env : Elab (List (TTName, Binder TT))
114 Prim__Goal : Elab (TTName, TT)
114 Prim__Goal : Elab (TTName, TT)
115 Prim__Holes : Elab (List TTName)
115 Prim__Holes : Elab (List TTName)
116− Prim__Guess : Elab (Maybe TT)
116+ Prim__Guess : Elab TT
117 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
117 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
118 Prim__LookupDatatype : TTName -> Elab (List Datatype)
118 Prim__LookupDatatype : TTName -> Elab (List Datatype)
119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
@@ -202,7 +202,7 @@ namespace Tactics
202 getHoles = Prim__Holes
202 getHoles = Prim__Holes
203
203
204 ||| If the current hole contains a guess, return it. Otherwise, fail.
204 ||| If the current hole contains a guess, return it. Otherwise, fail.
205− getGuess : Elab (Maybe TT)
205+ getGuess : Elab TT
206 getGuess = Prim__Guess
206 getGuess = Prim__Guess
207
207
208 ||| Look up the types of every overloading of a name.
208 ||| Look up the types of every overloading of a name.
src/Idris/Elab/Term.hs+2−10
@@ -1831,16 +1831,8 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1831 fmap fst . checkClosed $
1831 fmap fst . checkClosed $
1832 mkList (Var $ reflm "TTName") (map reflectName hs)
1832 mkList (Var $ reflm "TTName") (map reflectName hs)
1833 | n == tacN "Prim__Guess", [] <- args
1833 | n == tacN "Prim__Guess", [] <- args
1834− = do ok <- is_guess
1834+ = do g <- get_guess
1835− if ok
1836− then do guess <- fmap forget get_guess
1837− fmap fst . get_type_val $
1838− RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1839− (Var (reflm "TT")))
1840− guess
1841− else fmap fst . checkClosed $
1835+ fmap fst . checkClosed $ reflect g
1842− RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1843− (Var (reflm "TT"))
1844 | n == tacN "Prim__LookupTy", [n] <- args
1836 | n == tacN "Prim__LookupTy", [n] <- args
1845 = do n' <- reifyTTName n
1837 = do n' <- reifyTTName n
1846 ctxt <- get_context
1838 ctxt <- get_context