2aaff41 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Stop erasing binder types in executor

commit2aaff410d85a6124713b7a9bd7a428ef532d5359 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 19 Aug 2014, 14:57 (12 years ago) parent51a9b69

3 files changed+10−5

compare with master

unifiedsplit

idris.cabal+2 src/Idris/Core/Execute.hs+5−4 src/Idris/Core/TT.hs+3−1

idris.cabal+2

@@ -690,6 +690,8 @@ Library

690690 , zlib

691691 , optparse-applicative >= 0.8

692692 Extensions: MultiParamTypeClasses

693+ , DeriveFoldable

694+ , DeriveTraversable

693695 , FunctionalDependencies

694696 , FlexibleContexts

695697 , FlexibleInstances

src/Idris/Core/Execute.hs+5−4

@@ -23,9 +23,10 @@ import Control.Exception

2323import Control.Monad.Trans

2424import Control.Monad.Trans.State.Strict

2525import Control.Monad.Trans.Error

26−import Control.Monad

26+import Control.Monad hiding (forM)

2727import Data.Maybe

2828import Data.Bits

29+import Data.Traversable (forM)

2930import qualified Data.Map as M

3031

3132#ifdef IDRIS_FFI

@@ -175,9 +176,9 @@ doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

175176doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

176177 doExec ((n, v'):env) ctxt body

177178doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

178−doExec env ctxt tm@(Bind n b body) = return $

179− EBind n (fmap (\_->EErased) b)

180− (\arg -> doExec ((n, arg):env) ctxt body)

179+doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

180+ return $

181+ EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)

181182doExec env ctxt a@(App _ _) =

182183 do let (f, args) = unApply a

183184 f' <- doExec env ctxt f

src/Idris/Core/TT.hs+3−1

@@ -31,6 +31,8 @@ import Numeric (showIntAtBase)

3131import qualified Data.Text as T

3232import Data.List

3333import Data.Maybe (listToMaybe)

34+import Data.Foldable (Foldable)

35+import Data.Traversable (Traversable)

3436import Data.Vector.Unboxed (Vector)

3537import qualified Data.Vector.Unboxed as V

3638import qualified Data.Binary as B

@@ -638,7 +640,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

638640 | PVar { binderTy :: !b }

639641 -- ^ A pattern variable

640642 | PVTy { binderTy :: !b }

641− deriving (Show, Eq, Ord, Functor)

643+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

642644{-!

643645deriving instance Binary Binder

644646deriving instance NFData Binder