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

git.iko.soy/Idris-dev

Strictness annotations

Improves execution time slightly by using Strict state where appropriate, and strict constructor fields.

commit0c8c90d98596047e392862e2b126846ef59a9234 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jan 2014, 13:23 (13 years ago) parent66ec833

17 files changed+110−142

compare with master

unifiedsplit

idris.cabal+2−1 src/IRTS/Simplified.hs+1 src/Idris/Core/Constraints.hs+1 src/Idris/Core/Elaborate.hs+40−46 src/Idris/Core/Evaluate.hs+3−3 src/Idris/Core/ProofState.hs+7−5 src/Idris/Core/TC.hs+28 src/Idris/Core/TT.hs+13−26 src/Idris/Core/Unify.hs+1−1 src/Idris/Coverage.hs+1−1 src/Idris/DSL.hs+1−1 src/Idris/ElabDecls.hs+6−6 src/Idris/ElabTerm.hs+1−47 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+2−2 src/Idris/Imports.hs+1−1 src/Idris/Prover.hs+1−1

idris.cabal+2−1

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

346346 , Idris.Core.Evaluate

347347 , Idris.Core.Execute

348348 , Idris.Core.ProofState

349+ , Idris.Core.TC

349350 , Idris.Core.TT

350351 , Idris.Core.Typecheck

351352 , Idris.Core.Unify

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

495496 , transformers

496497

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

498− ghc-options: -threaded -rtsopts

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

499500

500501

src/IRTS/Simplified.hs+1

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

33import IRTS.Defunctionalise

44import Idris.Core.TT

5+import Idris.Core.Typecheck

56import Data.Maybe

67import Control.Monad.State

src/Idris/Core/Constraints.hs+1

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

22module Idris.Core.Constraints(ucheck) where

44import Idris.Core.TT

5+import Idris.Core.Typecheck

67import Control.Applicative

78import Control.Arrow

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

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

1919import Idris.Core.DeepSeq

2020

2121import Control.DeepSeq

22−import Control.Monad.State

22+import Control.Monad.State.Strict

2323import Data.Char

2424import Data.List

2525import Debug.Trace

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

4848proofFail e = do s <- get

4949 case runStateT e s of

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

51− return a

51+ return $! a

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

5353

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

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

7777 then MN (next+500) x

7878 else MN (next+100) x

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

80− return n'

80+ return $! n'

8181

8282setNextName :: Elab' aux ()

8383setNextName = do env <- get_env

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

9898errAt thing n elab = do s <- get

9999 case runStateT elab s of

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

101− return a

101+ return $! a

102102 Error (At f e) ->

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

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

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

107107erun f elab = do s <- get

108108 case runStateT elab s of

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

110− return a

110+ return $! a

111111 Error (ProofSearchFail (At f e))

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

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

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

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

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

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

128− return (a, str)

128+ return $! (a, str)

129129

130130force_term :: Elab' aux ()

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

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

137137

138138getAux :: Elab' aux aux

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

140− return a

140+ return $! a

141141

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

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

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

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

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

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

149− return ()

149+ return $! ()

150150

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

152152

153153-- get the global context

154154get_context :: Elab' aux Context

155155get_context = do ES p _ _ <- get

156− return (context (fst p))

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

157157

158158-- update the context

159159-- (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

165165-- get the proof term

166166get_term :: Elab' aux Term

167167get_term = do ES p _ _ <- get

168− return (pterm (fst p))

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

169169

170170-- get the proof term

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

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

180180

181181get_holes :: Elab' aux [Name]

182182get_holes = do ES p _ _ <- get

183− return (holes (fst p))

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

184184

185185get_probs :: Elab' aux Fails

186186get_probs = do ES p _ _ <- get

187− return (problems (fst p))

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

188188

189189-- get the current goal type

190190goal :: Elab' aux Type

191191goal = do ES p _ _ <- get

192192 b <- lift $ goalAtFocus (fst p)

193− return (binderTy b)

193+ return $! (binderTy b)

194194

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

196196get_guess :: Elab' aux Type

197197get_guess = do ES p _ _ <- get

198198 b <- lift $ goalAtFocus (fst p)

199199 case b of

200− Guess t v -> return v

200+ Guess t v -> return $! v

201201 _ -> fail "Not a guess"

202202

203203-- typecheck locally

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

205205get_type tm = do ctxt <- get_context

206206 env <- get_env

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

208− return (finalise ty)

208+ return $! (finalise ty)

209209

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

211211get_type_val tm = do ctxt <- get_context

212212 env <- get_env

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

214− return (finalise val, finalise ty)

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

215215

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

217217get_deferred :: Elab' aux [Name]

218218get_deferred = do ES p _ _ <- get

219− return (deferred (fst p))

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

220220

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

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

223− if isInj ctxt tm then return ()

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

224224 else lift $ tfail (NotInjective tm l r)

225225 where isInj ctxt (P _ n _)

226226 | isConName n ctxt = True

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

233233-- get instance argument names

234234get_instances :: Elab' aux [Name]

235235get_instances = do ES p _ _ <- get

236− return (instances (fst p))

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

237237

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

239239unique_hole = unique_hole' False

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

251251-- then return n

252252-- else getNameFrom n

253253-- _ -> getNameFrom n

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

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

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

256256 case n' of

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

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

259− _ -> return ()

260− return n'

259+ _ -> return $! ()

260+ return $! n'

261261 where

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

263263 where

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

273273

274274getLog :: Elab' aux String

275275getLog = do ES p logs _ <- get

276− return logs

276+ return $! logs

277277

278278-- The primitives, from ProofState

279279

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

357357 hs <- get_holes

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

359359 else do n' <- case n of

360− UN _ -> return n

360+ UN _ -> return $! n

361361 MN _ _ -> unique_hole n

362− NS _ _ -> return n

362+ NS _ _ -> return $! n

363363 processTactic' (PatVar n')

364364

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

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

399399qed :: Elab' aux Term

400400qed = do processTactic' QED

401401 ES p _ _ <- get

402− return (pterm (fst p))

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

403403

404404undo :: Elab' aux ()

405405undo = processTactic' Undo

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

420420-- case claims of

421421-- [] -> return ()

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

423− return claims

423+ return $! claims

424424 where

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

426426 do let t = rebind hs t_in

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

431431 claim n (forget t)

432432 when i (movelast n)

433433 mkClaims sc' is (n : claims) hs

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

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

435435 mkClaims _ _ _ _

436436 | Var n <- fn

437437 = do ctxt <- get_context

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

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

463463apply' fillt fn imps =

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

465− env <- get_env

466− g <- goal

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

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

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

470468 -- so do nothing

471− ptm <- get_term

472469 hs <- get_holes

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

474471 let dont = head hs : dontunify p ++

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

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

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

486483 fillt (raw_apply fn (map Var args))

487− ptm <- get_term

488− g <- goal

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

490485 end_unify

491− ptm <- get_term

492− return (map (updateUnify unify) args)

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

493487 where updateUnify us n = case lookup n us of

494488 Just (P _ t _) -> t

495489 _ -> n

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

503497 let (n, hs) = unified p

504498 end_unify

505499 solve

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

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

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

508502 elabArgs ns es

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

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

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

535529 claim n (forget t)

536530 case i of

537− Nothing -> return ()

531+ Nothing -> return $! ()

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

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

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

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

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

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

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

544538

545539 elabClaims failed r []

546− | null failed = return ()

540+ | null failed = return $! ()

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

548− else return ()

542+ else return $! ()

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

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

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

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

563557checkPiGoal n

564558 = do g <- goal

565559 case g of

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

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

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

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

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

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

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

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

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

626− else return ()

620+ else return $! ()

627621

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

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

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

635629 ps <- get_probs

636630 case prunStateT 999999 False ps t1 s of

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

638− return v

632+ return $! v

639633 Error e1 -> if recoverableErr e1 then

640634 do case runStateT t2 s of

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

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

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

643637 then lift (tfail e1)

644638 else lift (tfail e2)

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

675669 case prunStateT pmax True ps x s of

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

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

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

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

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

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

680674 tryAll' cs' newps f xs

681675 Error err -> do put s

682676 if (score err) < 100

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

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

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

1515

1616import Debug.Trace

17−import Control.Monad.State

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

1818import qualified Data.Binary as B

1919import Data.Binary hiding (get, put)

2020

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

513513

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

515515

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

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

517517convEq 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

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

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

521521 | otherwise = sameDefs ps x y

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

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

1313import Idris.Core.TT

1414import Idris.Core.Unify

1515

16−import Control.Monad.State

16+import Control.Monad.State.Strict

1717import Control.Applicative hiding (empty)

1818import Data.List

1919import Debug.Trace

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

743743 updateSolved' xs x

744744updateSolved' [] x = x

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

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

747− [_] -> psubst n v t

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

746+ | Just v <- lookup n xs

747+ = case xs of

748+ [_] -> psubst n v t

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

749750updateSolved' xs (Bind n b t)

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

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

752+updateSolved' xs (App f a)

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

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

753755 | Just v <- lookup n xs = v

754756updateSolved' 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 @@

1818 programs with implicit syntax into fully explicit terms.

1919-}

2020

21−module Idris.Core.TT where

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

2222

23−import Control.Monad.State

23+import Idris.Core.TC

24+

25+import Control.Monad.State.Strict

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

2527import Debug.Trace

2628import qualified Data.Map.Strict as Map

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

182184 pretty _ = text "Error"

183185

184186instance Error Err where

185− strMsg = Msg

187+ strMsg = InternalMsg

186188

187−data TC a = OK a

188− | Error Err

189− deriving (Eq, Functor)

189+type TC = TC' Err

190190

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

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

192192 pretty (OK ok) = pretty ok

193193 pretty (Error err) =

194194 if size err > breakingSize then

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

200200 show (OK x) = show x

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

202202

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−

213203tfail :: Err -> TC a

214204tfail e = Error e

215205

206+failMsg :: String -> TC a

207+failMsg str = Error (Msg str)

208+

216209trun :: FC -> TC a -> TC a

217210trun fc (OK a) = OK a

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

219212

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−

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

227214discard f = f >> return ()

228215

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

598585

599586-- | Terms in the core language

600587data 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

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

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

604591 | Constant Const -- ^ constant

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

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

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

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

607594 | Erased -- ^ an erased term

608595 | Impossible -- ^ special case for totality checking

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

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

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

66import Idris.Core.Evaluate

88import Control.Monad

9−import Control.Monad.State

9+import Control.Monad.State.Strict

1010import Data.List

1111import Debug.Trace

1212

src/Idris/Coverage.hs+1−1

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

1515import Data.Maybe

1616import Debug.Trace

1717

18−import Control.Monad.State

18+import Control.Monad.State.Strict

1919

2020mkPatTm :: PTerm -> Idris Term

2121mkPatTm t = do i <- getIState

src/Idris/DSL.hs+1−1

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

88import Idris.Core.TT

99import Idris.Core.Evaluate

1010

11−import Control.Monad.State

11+import Control.Monad.State.Strict

1212import Debug.Trace

1313

1414debindApp :: SyntaxInfo -> PTerm -> PTerm

src/Idris/ElabDecls.hs+6−6

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

2828

2929import Control.DeepSeq

3030import Control.Monad

31−import Control.Monad.State

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

3232import Data.List

3333import Data.Maybe

3434import Debug.Trace

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

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

322322 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

323323 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 ())

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

326326 case eliminatorClauses of

327327 [] -> return ()

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

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

329329 where elimLog :: String -> EliminatorState ()

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

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

331331

332332 elimFC :: FC

333333 elimFC = fileFC "(eliminator)"

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

464464

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

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

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

467+ i <- State.lift getIState

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

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

470470 [args] -> do return args

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

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

518518 let cons' = replaceParams paramPos generalParameters ty

519519 let (args, resTy) = splitPi cons'

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

520+ i <- State.lift getIState

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

522522 let (_, generalIdxs') = splitArgPms resTy

523523 let generalIdxs = map pexp generalIdxs'

src/Idris/ElabTerm.hs+1−47

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

1414import Idris.Core.Typecheck (check)

1515

1616import Control.Monad

17−import Control.Monad.State

17+import Control.Monad.State.Strict

1818import Data.List

1919import Data.Maybe (mapMaybe)

2020

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

418418 ctxt <- get_context

419419 let guarded = isConName f ctxt

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

421− ptm <- get_term

422− g <- goal

423421 -- Sort so that the implicit tactics go last

424422 let (ns', eargs) = unzip $

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

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

427425 (zip ns args)

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

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

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

431428 solve

432− ptm <- get_term

433429 ivs' <- get_instances

434− ps' <- get_probs

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

436431 -- i.e. no holes in them

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

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

15461541

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

15481543

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

1212

1313import System.Console.Haskeline

1414import System.Console.Haskeline.MonadException

15−import Control.Monad.State

15+import Control.Monad.State.Strict

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

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

1818import Data.Char

src/Idris/IBC.hs+2−2

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

1515import Data.List

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

1717import Control.Monad

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

19−import qualified Control.Monad.State as ST

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

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

2020import System.FilePath

2121import System.Directory

2222import Codec.Compression.Zlib

src/Idris/Imports.hs+1−1

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

88import System.FilePath

99import System.Directory

10−import Control.Monad.State

10+import Control.Monad.State.Strict

1111

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

1313 deriving (Show, Eq)

src/Idris/Prover.hs+1−1

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

2020

2121import System.Console.Haskeline

2222import System.Console.Haskeline.History

23−import Control.Monad.State

23+import Control.Monad.State.Strict

2424

2525import Util.Pretty

2626import Debug.Trace