0c8c90d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Strictness annotations

0c8c90dEdwin Brady13 years ago

idris.cabal+2−1

compare with master

unifiedsplit

@@ -346,6 +346,7 @@ Library

346 , Idris.Core.Evaluate

347 , Idris.Core.Execute

348 , Idris.Core.ProofState

349+ , Idris.Core.TC

349 , Idris.Core.TT

350 , Idris.Core.TT

350 , Idris.Core.Typecheck

351 , Idris.Core.Typecheck

351 , Idris.Core.Unify

352 , Idris.Core.Unify

@@ -495,6 +496,6 @@ Executable idris

495 , transformers

496 , transformers

496

497

497 ghc-prof-options: -auto-all -caf-all

498 ghc-prof-options: -auto-all -caf-all

498− ghc-options: -threaded -rtsopts

499+ ghc-options: -threaded -rtsopts -funbox-strict-fields

499

500

501

src/IRTS/Simplified.hs+1

@@ -2,6 +2,7 @@ module IRTS.Simplified where

3import IRTS.Defunctionalise

4import Idris.Core.TT

5+import Idris.Core.Typecheck

5import Data.Maybe

6import Data.Maybe

6import Control.Monad.State

7import Control.Monad.State

src/Idris/Core/Constraints.hs+1

@@ -2,6 +2,7 @@

2module Idris.Core.Constraints(ucheck) where

4import Idris.Core.TT

5+import Idris.Core.Typecheck

6import Control.Applicative

7import Control.Applicative

7import Control.Arrow

8import Control.Arrow

src/Idris/Core/Elaborate.hs+40−46

@@ -19,7 +19,7 @@ import Idris.Core.Unify

19import Idris.Core.DeepSeq

21import Control.DeepSeq

22−import Control.Monad.State

22+import Control.Monad.State.Strict

23import Data.Char

24import Data.List

25import Debug.Trace

@@ -48,7 +48,7 @@ proofFail :: Elab' aux a -> Elab' aux a

48proofFail e = do s <- get

49 case runStateT e s of

50 OK (a, s') -> do put s'

51− return a

51+ return $! a

52 Error err -> lift $ Error (ProofSearchFail err)

54explicit :: Name -> Elab' aux ()

@@ -77,7 +77,7 @@ getNameFrom n = do (ES (p, a) s e) <- get

77 then MN (next+500) x

78 else MN (next+100) x

79 NS (UN x) s -> MN (next+100) x

80− return n'

80+ return $! n'

82setNextName :: Elab' aux ()

83setNextName = do env <- get_env

@@ -98,7 +98,7 @@ errAt :: String -> Name -> Elab' aux a -> Elab' aux a

98errAt thing n elab = do s <- get

99 case runStateT elab s of

100 OK (a, s') -> do put s'

101− return a

101+ return $! a

102 Error (At f e) ->

103 lift $ Error (At f (Elaborating thing n e))

104 Error e -> lift $ Error (Elaborating thing n e)

@@ -107,7 +107,7 @@ erun :: FC -> Elab' aux a -> Elab' aux a

107erun f elab = do s <- get

108 case runStateT elab s of

109 OK (a, s') -> do put s'

110− return a

110+ return $! a

111 Error (ProofSearchFail (At f e))

112 -> lift $ Error (ProofSearchFail (At f e))

113 Error (At f e) -> lift $ Error (At f e)

@@ -125,7 +125,7 @@ initElaborator = newProof

125elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

126elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty

127 (a, ES ps' str _) <- runElab d elab ps

128− return (a, str)

128+ return $! (a, str)

129

130force_term :: Elab' aux ()

131force_term = do ES (ps, a) l p <- get

@@ -137,7 +137,7 @@ updateAux f = do ES (ps, a) l p <- get

137

138getAux :: Elab' aux aux

139getAux = do ES (ps, a) _ _ <- get

140− return a

140+ return $! a

141

142unifyLog :: Bool -> Elab' aux ()

143unifyLog log = do ES (ps, a) l p <- get

@@ -146,14 +146,14 @@ unifyLog log = do ES (ps, a) l p <- get

146processTactic' t = do ES (p, a) logs prev <- get

147 (p', log) <- lift $ processTactic t p

148 put (ES (p', a) (logs ++ log) prev)

149− return ()

149+ return $! ()

150

151-- Some handy gadgets for pulling out bits of state

152

153-- get the global context

154get_context :: Elab' aux Context

155get_context = do ES p _ _ <- get

156− return (context (fst p))

156+ return $! (context (fst p))

157

158-- update the context

159-- (should only be used for adding temporary definitions or all sorts of

@@ -165,7 +165,7 @@ set_context ctxt = do ES (p, a) logs prev <- get

165-- get the proof term

166get_term :: Elab' aux Term

167get_term = do ES p _ _ <- get

168− return (pterm (fst p))

168+ return $! (pterm (fst p))

169

170-- get the proof term

171update_term :: (Term -> Term) -> Elab' aux ()

@@ -180,24 +180,24 @@ get_env = do ES p _ _ <- get

180

181get_holes :: Elab' aux [Name]

182get_holes = do ES p _ _ <- get

183− return (holes (fst p))

183+ return $! (holes (fst p))

184

185get_probs :: Elab' aux Fails

186get_probs = do ES p _ _ <- get

187− return (problems (fst p))

187+ return $! (problems (fst p))

188

189-- get the current goal type

190goal :: Elab' aux Type

191goal = do ES p _ _ <- get

192 b <- lift $ goalAtFocus (fst p)

193− return (binderTy b)

193+ return $! (binderTy b)

194

195-- Get the guess at the current hole, if there is one

196get_guess :: Elab' aux Type

197get_guess = do ES p _ _ <- get

198 b <- lift $ goalAtFocus (fst p)

199 case b of

200− Guess t v -> return v

200+ Guess t v -> return $! v

201 _ -> fail "Not a guess"

202

203-- typecheck locally

@@ -205,22 +205,22 @@ get_type :: Raw -> Elab' aux Type

205get_type tm = do ctxt <- get_context

206 env <- get_env

207 (val, ty) <- lift $ check ctxt env tm

208− return (finalise ty)

208+ return $! (finalise ty)

209

210get_type_val :: Raw -> Elab' aux (Term, Type)

211get_type_val tm = do ctxt <- get_context

212 env <- get_env

213 (val, ty) <- lift $ check ctxt env tm

214− return (finalise val, finalise ty)

214+ return $! (finalise val, finalise ty)

215

216-- get holes we've deferred for later definition

217get_deferred :: Elab' aux [Name]

218get_deferred = do ES p _ _ <- get

219− return (deferred (fst p))

219+ return $! (deferred (fst p))

220

221checkInjective :: (Term, Term, Term) -> Elab' aux ()

222checkInjective (tm, l, r) = do ctxt <- get_context

223− if isInj ctxt tm then return ()

223+ if isInj ctxt tm then return $! ()

224 else lift $ tfail (NotInjective tm l r)

225 where isInj ctxt (P _ n _)

226 | isConName n ctxt = True

@@ -233,7 +233,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

233-- get instance argument names

234get_instances :: Elab' aux [Name]

235get_instances = do ES p _ _ <- get

236− return (instances (fst p))

236+ return $! (instances (fst p))

237

238-- given a desired hole name, return a unique hole name

239unique_hole = unique_hole' False

@@ -251,13 +251,13 @@ unique_hole' reusable n

251-- then return n

252-- else getNameFrom n

253-- _ -> getNameFrom n

254− return $ uniqueNameCtxt (context (fst p)) n nouse

254+ return $! uniqueNameCtxt (context (fst p)) n nouse

255 ES (p, a) s u <- get

256 case n' of

257 MN i _ -> when (i >= nextname p) $

258 put (ES (p { nextname = i + 1 }, a) s u)

259− _ -> return ()

259+ _ -> return $! ()

260− return n'

260+ return $! n'

261 where

262 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

263 where

@@ -273,7 +273,7 @@ elog str = do ES p logs prev <- get

273

274getLog :: Elab' aux String

275getLog = do ES p logs _ <- get

276− return logs

276+ return $! logs

277

278-- The primitives, from ProofState

279

@@ -357,9 +357,9 @@ patvar n = do env <- get_env

357 hs <- get_holes

358 if (n `elem` map fst env) then do apply (Var n) []; solve

359 else do n' <- case n of

360− UN _ -> return n

360+ UN _ -> return $! n

361 MN _ _ -> unique_hole n

362− NS _ _ -> return n

362+ NS _ _ -> return $! n

363 processTactic' (PatVar n')

364

365patbind :: Name -> Elab' aux ()

@@ -399,7 +399,7 @@ reorder_claims n = processTactic' (Reorder n)

399qed :: Elab' aux Term

400qed = do processTactic' QED

401 ES p _ _ <- get

402− return (pterm (fst p))

402+ return $! (pterm (fst p))

403

404undo :: Elab' aux ()

405undo = processTactic' Undo

@@ -420,7 +420,7 @@ prepare_apply fn imps =

420-- case claims of

421-- [] -> return ()

422-- (h : _) -> reorder_claims h

423− return claims

423+ return $! claims

424 where

425 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

426 do let t = rebind hs t_in

@@ -431,7 +431,7 @@ prepare_apply fn imps =

431 claim n (forget t)

432 when i (movelast n)

433 mkClaims sc' is (n : claims) hs

434− mkClaims t [] claims _ = return (reverse claims)

434+ mkClaims t [] claims _ = return $! (reverse claims)

435 mkClaims _ _ _ _

436 | Var n <- fn

437 = do ctxt <- get_context

@@ -462,13 +462,10 @@ match_apply = apply' match_fill

462apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

463apply' fillt fn imps =

464 do args <- prepare_apply fn (map fst imps)

465− env <- get_env

466− g <- goal

467 -- _Don't_ solve the arguments we're specifying by hand.

465 -- _Don't_ solve the arguments we're specifying by hand.

468 -- (remove from unified list before calling end_unify)

466 -- (remove from unified list before calling end_unify)

469 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

467 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

470 -- so do nothing

468 -- so do nothing

471− ptm <- get_term

472 hs <- get_holes

469 hs <- get_holes

473 ES (p, a) s prev <- get

470 ES (p, a) s prev <- get

474 let dont = head hs : dontunify p ++

471 let dont = head hs : dontunify p ++

@@ -484,12 +481,9 @@ apply' fillt fn imps =

484 put (ES (p { dontunify = dont, unified = (n, unify),

481 put (ES (p { dontunify = dont, unified = (n, unify),

485 notunified = notunify ++ notunified p }, a) s prev)

482 notunified = notunify ++ notunified p }, a) s prev)

486 fillt (raw_apply fn (map Var args))

483 fillt (raw_apply fn (map Var args))

487− ptm <- get_term

488− g <- goal

489-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

484-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

490 end_unify

485 end_unify

491− ptm <- get_term

492− return (map (updateUnify unify) args)

486+ return $! (map (updateUnify unify) args)

493 where updateUnify us n = case lookup n us of

487 where updateUnify us n = case lookup n us of

494 Just (P _ t _) -> t

488 Just (P _ t _) -> t

495 _ -> n

489 _ -> n

@@ -503,7 +497,7 @@ apply2 fn elabs =

503 let (n, hs) = unified p

497 let (n, hs) = unified p

504 end_unify

498 end_unify

505 solve

499 solve

506− where elabArgs [] [] = return ()

500+ where elabArgs [] [] = return $! ()

507 elabArgs (n:ns) (Just e:es) = do focus n; e

501 elabArgs (n:ns) (Just e:es) = do focus n; e

508 elabArgs ns es

502 elabArgs ns es

509 elabArgs (n:ns) (_:es) = elabArgs ns es

503 elabArgs (n:ns) (_:es) = elabArgs ns es

@@ -534,18 +528,18 @@ apply_elab n args =

534 let sc' = instantiate (P Bound n t) sc

528 let sc' = instantiate (P Bound n t) sc

535 claim n (forget t)

529 claim n (forget t)

536 case i of

530 case i of

537− Nothing -> return ()

531+ Nothing -> return $! ()

538 Just _ -> -- don't solve by unification as there is an explicit value

532 Just _ -> -- don't solve by unification as there is an explicit value

539 do ES (p, a) s prev <- get

533 do ES (p, a) s prev <- get

540 put (ES (p { dontunify = n : dontunify p }, a) s prev)

534 put (ES (p { dontunify = n : dontunify p }, a) s prev)

541 doClaims sc' is ((n, i) : claims)

535 doClaims sc' is ((n, i) : claims)

542− doClaims t [] claims = return (reverse claims)

536+ doClaims t [] claims = return $! (reverse claims)

543 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n

537 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n

544

538

545 elabClaims failed r []

539 elabClaims failed r []

546− | null failed = return ()

540+ | null failed = return $! ()

547 | otherwise = if r then elabClaims [] False failed

541 | otherwise = if r then elabClaims [] False failed

548− else return ()

542+ else return $! ()

549 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

543 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

550 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)

544 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)

551 | r = try (do ES p _ _ <- get

545 | r = try (do ES p _ _ <- get

@@ -563,7 +557,7 @@ checkPiGoal :: Name -> Elab' aux ()

563checkPiGoal n

557checkPiGoal n

564 = do g <- goal

558 = do g <- goal

565 case g of

559 case g of

566− Bind _ (Pi _) _ -> return ()

560+ Bind _ (Pi _) _ -> return $! ()

567 _ -> do a <- getNameFrom (MN 0 "pargTy")

561 _ -> do a <- getNameFrom (MN 0 "pargTy")

568 b <- getNameFrom (MN 0 "pretTy")

562 b <- getNameFrom (MN 0 "pretTy")

569 f <- getNameFrom (MN 0 "pf")

563 f <- getNameFrom (MN 0 "pf")

@@ -623,7 +617,7 @@ no_errors tac

623 ((x,y,env,err) : _) ->

617 ((x,y,env,err) : _) ->

624 let env' = map (\(x, b) -> (x, binderTy b)) env in

618 let env' = map (\(x, b) -> (x, binderTy b)) env in

625 lift $ tfail $ CantUnify False x y err env' 0

619 lift $ tfail $ CantUnify False x y err env' 0

626− else return ()

620+ else return $! ()

627

621

628-- Try a tactic, if it fails, try another

622-- Try a tactic, if it fails, try another

629try :: Elab' aux a -> Elab' aux a -> Elab' aux a

623try :: Elab' aux a -> Elab' aux a -> Elab' aux a

@@ -635,10 +629,10 @@ try' t1 t2 proofSearch

635 ps <- get_probs

629 ps <- get_probs

636 case prunStateT 999999 False ps t1 s of

630 case prunStateT 999999 False ps t1 s of

637 OK ((v, _), s') -> do put s'

631 OK ((v, _), s') -> do put s'

638− return v

632+ return $! v

639 Error e1 -> if recoverableErr e1 then

633 Error e1 -> if recoverableErr e1 then

640 do case runStateT t2 s of

634 do case runStateT t2 s of

641− OK (v, s') -> do put s'; return v

635+ OK (v, s') -> do put s'; return $! v

642 Error e2 -> if score e1 >= score e2

636 Error e2 -> if score e1 >= score e2

643 then lift (tfail e1)

637 then lift (tfail e1)

644 else lift (tfail e2)

638 else lift (tfail e2)

@@ -675,8 +669,8 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)

675 case prunStateT pmax True ps x s of

669 case prunStateT pmax True ps x s of

676 OK ((v, newps), s') ->

670 OK ((v, newps), s') ->

677 do let cs' = if (newps < pmax)

671 do let cs' = if (newps < pmax)

678− then [do put s'; return v]

672+ then [do put s'; return $! v]

679− else (do put s'; return v) : cs

673+ else (do put s'; return $! v) : cs

680 tryAll' cs' newps f xs

674 tryAll' cs' newps f xs

681 Error err -> do put s

675 Error err -> do put s

682 if (score err) < 100

676 if (score err) < 100

src/Idris/Core/Evaluate.hs+3−3

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

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

16import Debug.Trace

17−import Control.Monad.State

17+import Control.Monad.State -- not Strict!

18import qualified Data.Binary as B

19import Data.Binary hiding (get, put)

@@ -513,9 +513,9 @@ wknV i t = return t

513

514convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

515

516−convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool

516+convEq :: Context -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

517convEq ctxt = ceq [] where

518− ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

518+ ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

519 ceq ps (P xt x _) (P yt y _)

520 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

521 | otherwise = sameDefs ps x y

src/Idris/Core/ProofState.hs+7−5

@@ -13,7 +13,7 @@ import Idris.Core.Evaluate

13import Idris.Core.TT

14import Idris.Core.Unify

16−import Control.Monad.State

16+import Control.Monad.State.Strict

17import Control.Applicative hiding (empty)

18import Data.List

19import Debug.Trace

@@ -743,12 +743,14 @@ updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

743 updateSolved' xs x

744updateSolved' [] x = x

745updateSolved' xs (Bind n (Hole ty) t)

746− | Just v <- lookup n xs = case xs of

746+ | Just v <- lookup n xs

747+ = case xs of

747− [_] -> psubst n v t

748+ [_] -> psubst n v t

748− _ -> psubst n v (updateSolved' xs t)

749+ _ -> psubst n v (updateSolved' xs t)

749updateSolved' xs (Bind n b t)

750updateSolved' xs (Bind n b t)

750 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

751 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

752+updateSolved' xs (App f a)

751−updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)

753+ = App (updateSolved' xs f) (updateSolved' xs a)

752updateSolved' xs (P _ n@(MN _ _) _)

754updateSolved' xs (P _ n@(MN _ _) _)

753 | Just v <- lookup n xs = v

755 | Just v <- lookup n xs = v

754updateSolved' xs t = t

756updateSolved' xs t = t

src/Idris/Core/TC.hsnew file+28

@@ -0,0 +1,28 @@

1+{-# LANGUAGE DeriveFunctor #-}

3+module Idris.Core.TC(TC'(..)) where

5+import Control.Monad

6+import Control.Monad.Trans.Error(Error(..))

8+data TC' e a = OK !a

9+ | Error e

10+ deriving (Eq, Functor)

11+

12+bindTC :: TC' e a -> (a -> TC' e b) -> TC' e b

13+bindTC x k = case x of

14+ OK v -> k v

15+ Error e -> Error e

16+{-# INLINE bindTC #-}

17+

18+instance Error e => Monad (TC' e) where

19+ return x = OK x

20+ x >>= k = bindTC x k

21+ fail e = Error (strMsg e)

22+

23+instance Error e => MonadPlus (TC' e) where

24+ mzero = fail "Unknown error"

25+ (OK x) `mplus` _ = OK x

26+ _ `mplus` (OK y) = OK y

27+ err `mplus` _ = err

28+

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

@@ -18,9 +18,11 @@

18 programs with implicit syntax into fully explicit terms.

19-}

21−module Idris.Core.TT where

21+module Idris.Core.TT(module Idris.Core.TT, module Idris.Core.TC) where

23+import Idris.Core.TC

24+

23−import Control.Monad.State

25+import Control.Monad.State.Strict

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

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

25import Debug.Trace

27import Debug.Trace

26import qualified Data.Map.Strict as Map

28import qualified Data.Map.Strict as Map

@@ -182,13 +184,11 @@ instance Pretty Err where

182 pretty _ = text "Error"

184 pretty _ = text "Error"

183

185

184instance Error Err where

186instance Error Err where

185− strMsg = Msg

187+ strMsg = InternalMsg

186

188

187−data TC a = OK a

189+type TC = TC' Err

188− | Error Err

189− deriving (Eq, Functor)

190

191−instance Pretty a => Pretty (TC a) where

191+instance (Pretty a) => Pretty (TC a) where

192 pretty (OK ok) = pretty ok

193 pretty (Error err) =

194 if size err > breakingSize then

@@ -200,29 +200,16 @@ instance Show a => Show (TC a) where

200 show (OK x) = show x

201 show (Error str) = "Error: " ++ show str

202

203−-- at some point, this instance should also carry type checking options

204−-- (e.g. Type:Type)

205−

206−instance Monad TC where

207− return = OK

208− x >>= k = case x of

209− OK v -> k v

210− Error e -> Error e

211− fail e = Error (InternalMsg e)

212−

213tfail :: Err -> TC a

203tfail :: Err -> TC a

214tfail e = Error e

204tfail e = Error e

215

205

206+failMsg :: String -> TC a

207+failMsg str = Error (Msg str)

208+

216trun :: FC -> TC a -> TC a

209trun :: FC -> TC a -> TC a

217trun fc (OK a) = OK a

210trun fc (OK a) = OK a

218trun fc (Error e) = Error (At fc e)

211trun fc (Error e) = Error (At fc e)

219

212

220−instance MonadPlus TC where

221− mzero = fail "Unknown error"

222− (OK x) `mplus` _ = OK x

223− _ `mplus` (OK y) = OK y

224− err `mplus` _ = err

225−

226discard :: Monad m => m a -> m ()

213discard :: Monad m => m a -> m ()

227discard f = f >> return ()

214discard f = f >> return ()

228

215

@@ -598,12 +585,12 @@ instance Eq NameType where

598

585

599-- | Terms in the core language

586-- | Terms in the core language

600data TT n = P NameType n (TT n) -- ^ named references

587data TT n = P NameType n (TT n) -- ^ named references

601− | V Int -- ^ a resolved de Bruijn-indexed variable

588+ | V !Int -- ^ a resolved de Bruijn-indexed variable

602 | Bind n (Binder (TT n)) (TT n) -- ^ a binding

589 | Bind n (Binder (TT n)) (TT n) -- ^ a binding

603 | App (TT n) (TT n) -- ^ function, function type, arg

590 | App (TT n) (TT n) -- ^ function, function type, arg

604 | Constant Const -- ^ constant

591 | Constant Const -- ^ constant

605− | Proj (TT n) Int -- ^ argument projection; runtime only

592+ | Proj (TT n) !Int -- ^ argument projection; runtime only

606− -- (-1) is a special case for 'subtract one from BI'

593+ -- (-1) is a special case for 'subtract one from BI'

607 | Erased -- ^ an erased term

594 | Erased -- ^ an erased term

608 | Impossible -- ^ special case for totality checking

595 | Impossible -- ^ special case for totality checking

609 | TType UExp -- ^ the type of types at some level

596 | TType UExp -- ^ the type of types at some level

src/Idris/Core/Unify.hs+1−1

@@ -6,7 +6,7 @@ import Idris.Core.TT

6import Idris.Core.Evaluate

8import Control.Monad

9−import Control.Monad.State

9+import Control.Monad.State.Strict

10import Data.List

11import Debug.Trace

src/Idris/Coverage.hs+1−1

@@ -15,7 +15,7 @@ import Data.Either

15import Data.Maybe

16import Debug.Trace

18−import Control.Monad.State

18+import Control.Monad.State.Strict

20mkPatTm :: PTerm -> Idris Term

21mkPatTm t = do i <- getIState

src/Idris/DSL.hs+1−1

@@ -8,7 +8,7 @@ import Paths_idris

8import Idris.Core.TT

9import Idris.Core.Evaluate

11−import Control.Monad.State

11+import Control.Monad.State.Strict

12import Debug.Trace

14debindApp :: SyntaxInfo -> PTerm -> PTerm

src/Idris/ElabDecls.hs+6−6

@@ -28,7 +28,7 @@ import Idris.Core.CaseTree

29import Control.DeepSeq

30import Control.Monad

31−import Control.Monad.State

31+import Control.Monad.State.Strict as State

32import Data.List

33import Data.Maybe

34import Debug.Trace

@@ -321,13 +321,13 @@ elabEliminator paramPos n ty cons info = do

321 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

322 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

323 elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef

324− Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

324+ State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

325 -- Do not elaborate clauses if there aren't any

326 case eliminatorClauses of

327 [] -> return ()

328− _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())

328+ _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())

329 where elimLog :: String -> EliminatorState ()

330− elimLog s = Control.Monad.State.lift (logLvl 2 s)

330+ elimLog s = State.lift (logLvl 2 s)

331

332 elimFC :: FC

333 elimFC = fileFC "(eliminator)"

@@ -464,7 +464,7 @@ elabEliminator paramPos n ty cons info = do

464

465 implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]

466 implicitIndexes (cns@(doc, cnm, ty, fc)) = do

467− i <- Control.Monad.State.lift getIState

467+ i <- State.lift getIState

468 implargs' <- case lookupCtxt cnm (idris_implicits i) of

469 [] -> do fail $ "Error while showing implicits for " ++ show cnm

470 [args] -> do return args

@@ -517,7 +517,7 @@ elabEliminator paramPos n ty cons info = do

517 generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do

518 let cons' = replaceParams paramPos generalParameters ty

519 let (args, resTy) = splitPi cons'

520− i <- Control.Monad.State.lift getIState

520+ i <- State.lift getIState

521 implidxs <- implicitIndexes (doc, cnm, ty, fc)

522 let (_, generalIdxs') = splitArgPms resTy

523 let generalIdxs = map pexp generalIdxs'

src/Idris/ElabTerm.hs+1−47

@@ -14,7 +14,7 @@ import Idris.Core.Evaluate

14import Idris.Core.Typecheck (check)

16import Control.Monad

17−import Control.Monad.State

17+import Control.Monad.State.Strict

18import Data.List

19import Data.Maybe (mapMaybe)

@@ -418,8 +418,6 @@ elab ist info pattern opts fn tm

418 ctxt <- get_context

419 let guarded = isConName f ctxt

420 ns <- apply (Var f) (map isph args)

421− ptm <- get_term

422− g <- goal

423 -- Sort so that the implicit tactics go last

421 -- Sort so that the implicit tactics go last

424 let (ns', eargs) = unzip $

422 let (ns', eargs) = unzip $

425 sortBy (\(_,x) (_,y) ->

423 sortBy (\(_,x) (_,y) ->

@@ -427,11 +425,8 @@ elab ist info pattern opts fn tm

427 (zip ns args)

425 (zip ns args)

428 elabArgs (ina || not isinf, guarded, inty)

426 elabArgs (ina || not isinf, guarded, inty)

429 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

427 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

430− mkSpecialised ist fc f (map getTm args) tm

431 solve

428 solve

432− ptm <- get_term

433 ivs' <- get_instances

429 ivs' <- get_instances

434− ps' <- get_probs

435 -- Attempt to resolve any type classes which have 'complete' types,

430 -- Attempt to resolve any type classes which have 'complete' types,

436 -- i.e. no holes in them

431 -- i.e. no holes in them

437 when (not pattern || (ina && not tcgen && not guarded)) $

432 when (not pattern || (ina && not tcgen && not guarded)) $

@@ -1546,44 +1541,3 @@ envTupleType

1546

1541

1547solveAll = try (do solve; solveAll) (return ())

1542solveAll = try (do solve; solveAll) (return ())

1548

1543

1549−-- If the function application is specialisable, make a new

1550−-- top level function by normalising the application

1551−-- and elaborating the new expression.

1552−

1553−mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm

1554−mkSpecialised i fc n args def

1555− = do let tm' = def

1556− case lookupCtxt n (idris_statics i) of

1557− [as] -> if (not (or as)) then return tm' else

1558− mkSpecDecl i n (zip args as) tm'

1559− _ -> return tm'

1560−

1561−mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm

1562−mkSpecDecl i n pargs tm'

1563− = do t <- goal

1564− g <- get_guess

1565− let (f, args) = unApply g

1566− let sargs = zip args (map snd pargs)

1567− let staticArgs = map fst (filter (\ (_,x) -> x) sargs)

1568− let ns = group (sort (concatMap staticFnNames staticArgs))

1569− let ntimes = map (\xs -> (head xs, length xs - 1)) ns

1570− if (not (null ns)) then

1571− do env <- get_env

1572− let g' = g -- specialise ctxt env ntimes g

1573− return tm'

1574−-- trace (show t ++ "\n" ++

1575−-- show ntimes ++ "\n" ++

1576−-- show (delab i g) ++ "\n" ++ show (delab i g')) $ return tm' -- TODO

1577− else return tm'

1578− where

1579− ctxt = tt_ctxt i

1580− cg = idris_callgraph i

1581−

1582− staticFnNames tm | (P _ f _, as) <- unApply tm

1583− = if not (isFnName f ctxt) then []

1584− else case lookupCtxt f cg of

1585− [ns] -> f : f : [] --(ns \\ [f])

1586− [] -> [f,f]

1587− _ -> []

1588− staticFnNames _ = []

1589−

src/Idris/Error.hs+1−1

@@ -12,7 +12,7 @@ import Idris.Core.Constraints

13import System.Console.Haskeline

14import System.Console.Haskeline.MonadException

15−import Control.Monad.State

15+import Control.Monad.State.Strict

16import Control.Monad.Error (throwError, catchError)

17import System.IO.Error(isUserError, ioeGetErrorString)

18import Data.Char

src/Idris/IBC.hs+2−2

@@ -15,8 +15,8 @@ import Data.Vector.Binary

15import Data.List

16import Data.ByteString.Lazy as B hiding (length, elem, map)

17import Control.Monad

18−import Control.Monad.State hiding (get, put)

18+import Control.Monad.State.Strict hiding (get, put)

19−import qualified Control.Monad.State as ST

19+import qualified Control.Monad.State.Strict as ST

20import System.FilePath

21import System.Directory

22import Codec.Compression.Zlib

src/Idris/Imports.hs+1−1

@@ -7,7 +7,7 @@ import Paths_idris

8import System.FilePath

9import System.Directory

10−import Control.Monad.State

10+import Control.Monad.State.Strict

12data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

13 deriving (Show, Eq)

src/Idris/Prover.hs+1−1

@@ -20,7 +20,7 @@ import Text.Trifecta.Result(Result(..))

21import System.Console.Haskeline

22import System.Console.Haskeline.History

23−import Control.Monad.State

23+import Control.Monad.State.Strict

25import Util.Pretty

26import Debug.Trace