git.iko.soy/Idris-dev
on master help sign in
Add the ability to look up if a name is a TC to Elab

Now, Elab scripts can check whether a name denotes a type class.

commit76bcaf2fa392841aeee4da8f924a48d6f655b3e3 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 2 Oct 2015, 08:32 (11 years ago) parentc9973eb
4 files changed+17−4
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+8−1 src/Idris/Elab/Term.hs+5 test/meta002/Tacs.idr+3−2 test/meta002/expected+1−1
libs/prelude/Language/Reflection/Elab.idr+8−1
@@ -144,6 +144,7 @@ data Elab : Type -> Type where
144144 prim__DeclareType : TyDecl -> Elab ()
145145 prim__DefineFunction : FunDefn -> Elab ()
146146 prim__AddInstance : TTName -> TTName -> Elab ()
147+ prim__IsTCName : TTName -> Elab Bool
147148
148149 prim__ResolveTC : TTName -> Elab ()
149150 prim__Search : Int -> List TTName -> Elab ()
@@ -427,13 +428,19 @@ namespace Tactics
427428 defineFunction : FunDefn -> Elab ()
428429 defineFunction defun = prim__DefineFunction defun
429430
430− ||| Register a new instance for type class resolution
431+ ||| Register a new instance for type class resolution.
431432 |||
432433 ||| @ className the name of the class for which an instance is being registered
433434 ||| @ instName the name of the definition to use in instance search
434435 addInstance : (className, instName : TTName) -> Elab ()
435436 addInstance className instName = prim__AddInstance className instName
436437
438+ ||| Determine whether a name denotes a class.
439+ |||
440+ ||| @ name a name that might denote a class.
441+ isTCName : (name : TTName) -> Elab Bool
442+ isTCName name = prim__IsTCName name
443+
437444 ||| Attempt to solve the current goal with a type class dictionary
438445 |||
439446 ||| @ fn the name of the definition being elaborated (to prevent Idris
src/Idris/Elab/Term.hs+5
@@ -2002,6 +2002,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20022002 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
20032003 new_tyDecls e}
20042004 returnUnit
2005+ | n == tacN "prim__IsTCName", [n] <- args
2006+ = do n' <- reifyTTName n
2007+ case lookupCtxtExact n' (idris_classes ist) of
2008+ Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2009+ Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
20052010 | n == tacN "prim__ResolveTC", [fn] <- args
20062011 = do g <- goal
20072012 fn <- reifyTTName fn
test/meta002/Tacs.idr+3−2
@@ -11,7 +11,6 @@ import Data.Vect
1111
1212import Language.Reflection
1313import Language.Reflection.Errors
14−import Language.Reflection.Elab
1514import Language.Reflection.Utils
1615
1716%default total
@@ -33,7 +32,9 @@ foo = %runElab (do intro (UN "fnord")
3332 solve)
3433
3534
36−
35+%runElab (do n <- isTCName `{Nat}
36+ s <- isTCName `{Show}
37+ if n || not s then fail [TextPart "nope"] else return ())
3738
3839-- Note that <|> is equivalent to "try" in the old tactics.
3940-- In these tactics, we use ordinary do notation and ordinary documentation strings!
test/meta002/expected+1−1
@@ -1,3 +1,3 @@
1−Tacs.idr:290:15:
1+Tacs.idr:291:15:
22When checking right hand side of testElab3:
33Unifying ty and ARR ty t would lead to infinite value