git.iko.soy/Idris-dev
on master help sign in
Make "getGuess" fail if there's no guess present

This makes its interface more similar to the other Elab operators.

commit5f9e5953cce1f348618b9366ab641976d805641e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 18 Oct 2015, 20:38 (11 years ago) parentc7bed76
2 files changed+4−12
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+2−2 src/Idris/Elab/Term.hs+2−10
libs/prelude/Language/Reflection/Elab.idr+2−2
@@ -113,7 +113,7 @@ data Elab : Type -> Type where
113113 Prim__Env : Elab (List (TTName, Binder TT))
114114 Prim__Goal : Elab (TTName, TT)
115115 Prim__Holes : Elab (List TTName)
116− Prim__Guess : Elab (Maybe TT)
116+ Prim__Guess : Elab TT
117117 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
118118 Prim__LookupDatatype : TTName -> Elab (List Datatype)
119119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
@@ -202,7 +202,7 @@ namespace Tactics
202202 getHoles = Prim__Holes
203203
204204 ||| If the current hole contains a guess, return it. Otherwise, fail.
205− getGuess : Elab (Maybe TT)
205+ getGuess : Elab TT
206206 getGuess = Prim__Guess
207207
208208 ||| 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
18311831 fmap fst . checkClosed $
18321832 mkList (Var $ reflm "TTName") (map reflectName hs)
18331833 | n == tacN "Prim__Guess", [] <- args
1834− = do ok <- is_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 $
1842− RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1843− (Var (reflm "TT"))
1834+ = do g <- get_guess
1835+ fmap fst . checkClosed $ reflect g
18441836 | n == tacN "Prim__LookupTy", [n] <- args
18451837 = do n' <- reifyTTName n
18461838 ctxt <- get_context