76bcaf2 · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Elab.idr+8−1

compare with master

unifiedsplit

@@ -144,6 +144,7 @@ data Elab : Type -> Type where

144 prim__DeclareType : TyDecl -> Elab ()

145 prim__DefineFunction : FunDefn -> Elab ()

146 prim__AddInstance : TTName -> TTName -> Elab ()

147+ prim__IsTCName : TTName -> Elab Bool

147

148

148 prim__ResolveTC : TTName -> Elab ()

149 prim__ResolveTC : TTName -> Elab ()

149 prim__Search : Int -> List TTName -> Elab ()

150 prim__Search : Int -> List TTName -> Elab ()

@@ -427,13 +428,19 @@ namespace Tactics

427 defineFunction : FunDefn -> Elab ()

428 defineFunction : FunDefn -> Elab ()

428 defineFunction defun = prim__DefineFunction defun

429 defineFunction defun = prim__DefineFunction defun

429

430

430− ||| Register a new instance for type class resolution

431+ ||| Register a new instance for type class resolution.

431 |||

432 |||

432 ||| @ className the name of the class for which an instance is being registered

433 ||| @ className the name of the class for which an instance is being registered

433 ||| @ instName the name of the definition to use in instance search

434 ||| @ instName the name of the definition to use in instance search

434 addInstance : (className, instName : TTName) -> Elab ()

435 addInstance : (className, instName : TTName) -> Elab ()

435 addInstance className instName = prim__AddInstance className instName

436 addInstance className instName = prim__AddInstance className instName

436

437

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+

437 ||| Attempt to solve the current goal with a type class dictionary

444 ||| Attempt to solve the current goal with a type class dictionary

438 |||

445 |||

439 ||| @ fn the name of the definition being elaborated (to prevent Idris

446 ||| @ 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

2002 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

2003 new_tyDecls e}

2004 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"])

2005 | n == tacN "prim__ResolveTC", [fn] <- args

2010 | n == tacN "prim__ResolveTC", [fn] <- args

2006 = do g <- goal

2011 = do g <- goal

2007 fn <- reifyTTName fn

2012 fn <- reifyTTName fn

test/meta002/Tacs.idr+3−2

@@ -11,7 +11,6 @@ import Data.Vect

11

12import Language.Reflection

13import Language.Reflection.Errors

14−import Language.Reflection.Elab

15import Language.Reflection.Utils

14import Language.Reflection.Utils

16

15

17%default total

16%default total

@@ -33,7 +32,9 @@ foo = %runElab (do intro (UN "fnord")

33 solve)

32 solve)

34

33

35

34

36−

35+%runElab (do n <- isTCName `{Nat}

36+ s <- isTCName `{Show}

37+ if n || not s then fail [TextPart "nope"] else return ())

37

38

38-- Note that <|> is equivalent to "try" in the old tactics.

39-- Note that <|> is equivalent to "try" in the old tactics.

39-- In these tactics, we use ordinary do notation and ordinary documentation strings!

40-- 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:

2When checking right hand side of testElab3:

3Unifying ty and ARR ty t would lead to infinite value