66ec833 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+21

compare with master

unifiedsplit

@@ -302,6 +302,27 @@ getInternalApp fp l = do i <- getIState

302 Nothing -> return Placeholder

303 -- TODO: What if it's not there?

304

305+-- Pattern definitions are only used for coverage checking, so erase them

306+-- when we're done

307+clearOrigPats :: Idris ()

308+clearOrigPats = do i <- get

309+ let ps = idris_patdefs i

310+ let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps

311+ put (i { idris_patdefs = ps' })

312+

313+-- Erase types from Ps in the context (basically ending up with what's in

314+-- the .ibc, which is all we need after all the analysis is done)

315+clearPTypes :: Idris ()

316+clearPTypes = do i <- get

317+ let ctxt = tt_ctxt i

318+ put (i { tt_ctxt = mapDefCtxt pErase ctxt })

319+ where pErase (CaseOp c t tys orig tot cds)

320+ = CaseOp c t tys orig [] (pErase' cds)

321+ pErase x = x

322+ pErase' (CaseDefs _ (cs, c) _ rs)

323+ = let c' = (cs, fmap pEraseType c) in

324+ CaseDefs c' c' c' rs

325+

305checkUndefined :: FC -> Name -> Idris ()

326checkUndefined :: FC -> Name -> Idris ()

306checkUndefined fc n

327checkUndefined fc n

307 = do i <- getContext

328 = do i <- getContext

src/Idris/Core/CaseTree.hs+4−2

@@ -21,7 +21,8 @@ data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

21 | ImpossibleCase -- ^ already checked to be impossible

22 deriving (Eq, Ord, Functor)

23{-!

24−deriving instance Binary SC

24+deriving instance Binary SC'

25+deriving instance NFData SC'

25!-}

26!-}

26

27

27type SC = SC' Term

28type SC = SC' Term

@@ -33,7 +34,8 @@ data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

33 | DefaultCase !(SC' t)

34 | DefaultCase !(SC' t)

34 deriving (Show, Eq, Ord, Functor)

35 deriving (Show, Eq, Ord, Functor)

35{-!

36{-!

36−deriving instance Binary CaseAlt

37+deriving instance Binary CaseAlt'

38+deriving instance NFData CaseAlt'

37!-}

39!-}

38

40

39type CaseAlt = CaseAlt' Term

41type CaseAlt = CaseAlt' Term

src/Idris/Core/DeepSeq.hs+15

@@ -1,6 +1,7 @@

1module Idris.Core.DeepSeq where

2

3import Idris.Core.TT

4+import Idris.Core.CaseTree

4

5

5import Control.DeepSeq

6import Control.DeepSeq

6

7

@@ -97,3 +98,17 @@ instance (NFData n) => NFData (TT n) where

97 rnf Impossible = ()

98 rnf Impossible = ()

98 rnf (TType x1) = rnf x1 `seq` ()

99 rnf (TType x1) = rnf x1 `seq` ()

99

100

101+instance (NFData t) => NFData (SC' t) where

102+ rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

103+ rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104+ rnf (STerm x1) = rnf x1 `seq` ()

105+ rnf (UnmatchedCase x1) = rnf x1 `seq` ()

106+ rnf ImpossibleCase = ()

107+

108+instance (NFData t) => NFData (CaseAlt' t) where

109+ rnf (ConCase x1 x2 x3 x4)

110+ = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()

111+ rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()

112+ rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()

113+ rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()

114+ rnf (DefaultCase x1) = rnf x1 `seq` ()

src/Idris/Core/Evaluate.hs+5

@@ -9,6 +9,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

12+ mapDefCtxt,

12 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13 Value(..), Quote(..), initEval, uniqueNameCtxt) where

14 Value(..), Quote(..), initEval, uniqueNameCtxt) where

14

15

@@ -696,6 +697,10 @@ data Context = MkContext {

696-- | The initial empty context

697-- | The initial empty context

697initContext = MkContext [] 0 emptyContext

698initContext = MkContext [] 0 emptyContext

698

699

700+mapDefCtxt :: (Def -> Def) -> Context -> Context

701+mapDefCtxt f (MkContext c t defs) = MkContext c t (mapCtxt f' defs)

702+ where f' (d, a, t, m) = f' (f d, a, t, m)

703+

699-- | Get the definitions from a context

704-- | Get the definitions from a context

700ctxtAlist :: Context -> [(Name, Def)]

705ctxtAlist :: Context -> [(Name, Def)]

701ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

706ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

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

@@ -23,7 +23,7 @@ module Idris.Core.TT where

23import Control.Monad.State

24import Control.Monad.Trans.Error (Error(..))

25import Debug.Trace

26−import qualified Data.Map as Map

26+import qualified Data.Map.Strict as Map

27import Data.Char

28import Data.List

29import Data.Vector.Unboxed (Vector)

@@ -314,6 +314,9 @@ showCG NErased = "_"

314type Ctxt a = Map.Map Name (Map.Map Name a)

315emptyContext = Map.empty

316

317+mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

318+mapCtxt = fmap . fmap

319+

317tcname (UN ('@':_)) = True

320tcname (UN ('@':_)) = True

318tcname (NS n _) = tcname n

321tcname (NS n _) = tcname n

319tcname (SN (InstanceN _ _)) = True

322tcname (SN (InstanceN _ _)) = True

@@ -756,6 +759,15 @@ finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))

756finalise (App f a) = App (finalise f) (finalise a)

759finalise (App f a) = App (finalise f) (finalise a)

757finalise t = t

760finalise t = t

758

761

762+-- Once we've finished checking everything about a term we no longer need

763+-- the type on the 'P' so erase it so save memory

764+

765+pEraseType :: TT n -> TT n

766+pEraseType (P nt t _) = P nt t Erased

767+pEraseType (App f a) = App (pEraseType f) (pEraseType a)

768+pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)

769+pEraseType t = t

770+

759subst :: Eq n => n -> TT n -> TT n -> TT n

771subst :: Eq n => n -> TT n -> TT n -> TT n

760subst n v tm = instantiate v (pToV n tm)

772subst n v tm = instantiate v (pToV n tm)

761

773

src/Idris/DeepSeq.hs−1

@@ -2,7 +2,6 @@ module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

2

3import Idris.Core.DeepSeq

4import Idris.Core.TT

5−import Idris.AbsSyntax

6import Idris.AbsSyntaxTree

5import Idris.AbsSyntaxTree

7

6

8import Control.DeepSeq

7import Control.DeepSeq

src/Idris/ElabDecls.hs+9−6

@@ -91,8 +91,10 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

91 let nty' = normalise ctxt [] nty

92

93 -- Add normalised type to internals

94+ rep <- useREPL

95+ when rep $ do

94− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

96+ addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

95− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

97+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

96

98

97 let (t, _) = unApply (getRetTy nty')

99 let (t, _) = unApply (getRetTy nty')

98 let corec = case t of

100 let corec = case t of

@@ -675,8 +677,7 @@ elabTransform info fc safe lhs_in rhs_in

675 erun fc (build i info False [] (UN "transform") rhs)

677 erun fc (build i info False [] (UN "transform") rhs)

676 erun fc $ psolve lhs_tm

678 erun fc $ psolve lhs_tm

677 tt <- get_term

679 tt <- get_term

678− let (tm, ds) = runState (collectDeferred Nothing tt) []

680+ return (runState (collectDeferred Nothing tt) []))

679− return (tm, ds))

680 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

681 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

681 logLvl 3 ("Transform RHS " ++ show crhs_tm)

682 logLvl 3 ("Transform RHS " ++ show crhs_tm)

682 when safe $ case converts ctxt [] clhs_tm crhs_tm of

683 when safe $ case converts ctxt [] clhs_tm crhs_tm of

@@ -1268,8 +1269,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1268

1269

1269 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

1270 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

1270

1271

1272+ rep <- useREPL

1273+ when rep $ do

1271− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1274+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1272− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

1275+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

1273

1276

1274 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

1277 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

1275 -- Elaborate where block

1278 -- Elaborate where block

src/Idris/REPL.hs+2

@@ -408,6 +408,7 @@ edit f orig

408 , idris_colourTheme = idris_colourTheme i

409 }

410 loadInputs stdout [f]

411+ clearOrigPats

411 iucheck

412 iucheck

412 return ()

413 return ()

413 where getEditor env | Just ed <- lookup "EDITOR" env = ed

414 where getEditor env | Just ed <- lookup "EDITOR" env = ed

@@ -1220,6 +1221,7 @@ idrisMain opts =

1220 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

1221 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

1221

1222

1222 when (runrepl && not idesl) $ do

1223 when (runrepl && not idesl) $ do

1224+ clearOrigPats

1223 initScript

1225 initScript

1224 startServer orig inputs

1226 startServer orig inputs

1225 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1227 runInputT (replSettings (Just historyFile)) $ repl orig inputs