6cd99f3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'refs/remotes/origin/wip/tactical' into wip/tactical

6cd99f3David Raymond Christiansen11 years ago

src/Idris/Prover.hs+8

@@ -1,6 +1,14 @@

1{-# LANGUAGE PatternGuards #-}

2module Idris.Prover (prover, showProof, showRunElab) where

4+-- Hack for GHC 7.10 and earlier compat without CPP or warnings

5+-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

6+import Prelude (Eq(..), Show(..),

7+ Bool(..), Either(..), Maybe(..), String,

8+ (.), ($), (++),

9+ concatMap, id, elem, error, fst, flip, foldl, foldr, init,

10+ length, lines, map, not, null, repeat, reverse, tail, zip)

11+

4import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Elaborate hiding (Tactic(..))

5import Idris.Core.TT

13import Idris.Core.TT

6import Idris.Core.Evaluate

14import Idris.Core.Evaluate

src/Idris/Reflection.hs+8

@@ -161,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]

161 return $ Proj t'' i

162reifyTTApp t [tt]

163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)

164+reifyTTApp t [tt]

165+ | t == reflm "UType" = liftM UType (reifyUniverse tt)

164reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

166reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

165

167

168+reifyUniverse :: Term -> ElabD Universe

169+reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes

170+ | n == reflm "UniqueType" = return UniqueType

171+ | n == reflm "NullType" = return NullType

172+reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)

173+

166-- | Reify raw terms from their reflected representation

174-- | Reify raw terms from their reflected representation

167reifyRaw :: Term -> ElabD Raw

175reifyRaw :: Term -> ElabD Raw

168reifyRaw t@(App _ _ _)

176reifyRaw t@(App _ _ _)