ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Add missing reflection constructor

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-06-11 15:25:08 +02:00
parent d2beadc7d5
commit b2dc1fc720
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Idris/Reflection.hs
View File

@ -161,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]
return $ Proj t'' i
reifyTTApp t [tt]
| t == reflm "TType" = liftM TType (reifyTTUExp tt)
reifyTTApp t [tt]
| t == reflm "UType" = liftM UType (reifyUniverse tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
reifyUniverse :: Term -> ElabD Universe
reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
| n == reflm "UniqueType" = return UniqueType
| n == reflm "NullType" = return NullType
reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)
-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw t@(App _ _ _)