mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 06:29:37 +03:00
Reduce space leak through ugly DeepSeq hack
The space leak documented in issue #2386 is helped by forcing the state in a few places. Now, with the empty module, no space leak occurs, while it grows by about 1 MB per 200 reloads with a large module. While deepseqing the state is a hack, and should be better, I've not yet improved on this and it does make Idris usable for repeated reloads of large modules when using the interactive editing features.
This commit is contained in:
David Raymond Christiansen
parent
6d426003ae
commit
1cdc9ddfdc
@ -1,3 +1,4 @@
|
||||
{-# LANGUAGE BangPatterns, ViewPatterns #-}
|
||||
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
|
||||
|
||||
module Idris.Core.DeepSeq where
|
||||
@ -16,6 +17,48 @@ instance NFData Name where
|
||||
rnf (SN x1) = rnf x1 `seq` ()
|
||||
rnf (SymRef x1) = rnf x1 `seq` ()
|
||||
|
||||
instance NFData Context where
|
||||
rnf ctxt = rnf (next_tvar ctxt) `seq` rnf (definitions ctxt) `seq` ()
|
||||
|
||||
-- | Forcing the contents of a context, for diagnosing and working
|
||||
-- around space leaks
|
||||
forceDefCtxt :: Context -> Context
|
||||
forceDefCtxt (force -> !ctxt) = ctxt
|
||||
|
||||
instance NFData NameOutput where
|
||||
rnf TypeOutput = ()
|
||||
rnf FunOutput = ()
|
||||
rnf DataOutput = ()
|
||||
rnf MetavarOutput = ()
|
||||
rnf PostulateOutput = ()
|
||||
|
||||
instance NFData TextFormatting where
|
||||
rnf BoldText = ()
|
||||
rnf ItalicText = ()
|
||||
rnf UnderlineText = ()
|
||||
|
||||
instance NFData Ordering where
|
||||
rnf LT = ()
|
||||
rnf EQ = ()
|
||||
rnf GT = ()
|
||||
|
||||
instance NFData OutputAnnotation where
|
||||
rnf (AnnName x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
|
||||
rnf (AnnBoundName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (AnnConst x1) = rnf x1 `seq` ()
|
||||
rnf (AnnData x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (AnnType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (AnnKeyword) = ()
|
||||
rnf (AnnFC x) = rnf x `seq` ()
|
||||
rnf (AnnTextFmt x) = rnf x `seq` ()
|
||||
rnf (AnnLink x) = rnf x `seq` ()
|
||||
rnf (AnnTerm x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (AnnSearchResult x1) = rnf x1 `seq` ()
|
||||
rnf (AnnErr x1) = rnf x1 `seq` ()
|
||||
rnf (AnnNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (AnnQuasiquote) = ()
|
||||
rnf (AnnAntiquote) = ()
|
||||
|
||||
instance NFData SpecialName where
|
||||
rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
|
||||
rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,
|
||||
PatternGuards #-}
|
||||
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
|
||||
|
||||
@ -802,12 +802,14 @@ data Context = MkContext {
|
||||
definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)
|
||||
} deriving Show
|
||||
|
||||
|
||||
-- | The initial empty context
|
||||
initContext = MkContext 0 emptyContext
|
||||
|
||||
|
||||
mapDefCtxt :: (Def -> Def) -> Context -> Context
|
||||
mapDefCtxt f (MkContext t defs) = MkContext t (mapCtxt f' defs)
|
||||
where f' (d, a, t, m) = f' (f d, a, t, m)
|
||||
mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)
|
||||
where f' (!d, a, t, m) = f' (f d, a, t, m)
|
||||
|
||||
-- | Get the definitions from a context
|
||||
ctxtAlist :: Context -> [(Name, Def)]
|
||||
@ -818,44 +820,44 @@ veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
|
||||
addToCtxt :: Name -> Term -> Type -> Context -> Context
|
||||
addToCtxt n tm ty uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in
|
||||
!ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in
|
||||
uctxt { definitions = ctxt' }
|
||||
|
||||
setAccess :: Name -> Accessibility -> Context -> Context
|
||||
setAccess n a uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in
|
||||
!ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in
|
||||
uctxt { definitions = ctxt' }
|
||||
|
||||
setTotal :: Name -> Totality -> Context -> Context
|
||||
setTotal n t uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in
|
||||
!ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in
|
||||
uctxt { definitions = ctxt' }
|
||||
|
||||
setMetaInformation :: Name -> MetaInformation -> Context -> Context
|
||||
setMetaInformation n m uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in
|
||||
!ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in
|
||||
uctxt { definitions = ctxt' }
|
||||
|
||||
addCtxtDef :: Name -> Def -> Context -> Context
|
||||
addCtxtDef n d c = let ctxt = definitions c
|
||||
ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in
|
||||
!ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in
|
||||
c { definitions = ctxt' }
|
||||
|
||||
addTyDecl :: Name -> NameType -> Type -> Context -> Context
|
||||
addTyDecl n nt ty uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in
|
||||
!ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in
|
||||
uctxt { definitions = ctxt' }
|
||||
|
||||
addDatatype :: Datatype Name -> Context -> Context
|
||||
addDatatype (Data n tag ty unique cons) uctxt
|
||||
= let ctxt = definitions uctxt
|
||||
ty' = normalise uctxt [] ty
|
||||
ctxt' = addCons 0 cons (addDef n
|
||||
(TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in
|
||||
!ctxt' = addCons 0 cons (addDef n
|
||||
(TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in
|
||||
uctxt { definitions = ctxt' }
|
||||
where
|
||||
addCons tag [] ctxt = ctxt
|
||||
|
||||
@ -51,6 +51,7 @@ import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
|
||||
|
||||
import Control.Applicative (Applicative (..), Alternative)
|
||||
import qualified Control.Applicative as A (Alternative (..))
|
||||
import Control.DeepSeq (($!!))
|
||||
import Control.Monad.State.Strict
|
||||
import Control.Monad.Trans.Except (Except (..))
|
||||
import Debug.Trace
|
||||
@ -438,11 +439,11 @@ traceWhen False _ a = a
|
||||
|
||||
-- | Names are hierarchies of strings, describing scope (so no danger of
|
||||
-- duplicate names, but need to be careful on lookup).
|
||||
data Name = UN T.Text -- ^ User-provided name
|
||||
| NS Name [T.Text] -- ^ Root, namespaces
|
||||
| MN Int T.Text -- ^ Machine chosen names
|
||||
data Name = UN !T.Text -- ^ User-provided name
|
||||
| NS !Name [T.Text] -- ^ Root, namespaces
|
||||
| MN !Int !T.Text -- ^ Machine chosen names
|
||||
| NErased -- ^ Name of something which is never used in scope
|
||||
| SN SpecialName -- ^ Decorated function names
|
||||
| SN !SpecialName -- ^ Decorated function names
|
||||
| SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
|
||||
deriving (Eq, Ord, Data, Typeable)
|
||||
|
||||
@ -463,7 +464,7 @@ sUN :: String -> Name
|
||||
sUN s = UN (txt s)
|
||||
|
||||
sNS :: Name -> [String] -> Name
|
||||
sNS n ss = NS n (map txt ss)
|
||||
sNS n ss = NS n $!! (map txt ss)
|
||||
|
||||
sMN :: Int -> String -> Name
|
||||
sMN i s = MN i (txt s)
|
||||
@ -473,15 +474,15 @@ deriving instance Binary Name
|
||||
deriving instance NFData Name
|
||||
!-}
|
||||
|
||||
data SpecialName = WhereN Int Name Name
|
||||
| WithN Int Name
|
||||
| InstanceN Name [T.Text]
|
||||
| ParentN Name T.Text
|
||||
| MethodN Name
|
||||
| CaseN Name
|
||||
| ElimN Name
|
||||
| InstanceCtorN Name
|
||||
| MetaN Name Name
|
||||
data SpecialName = WhereN !Int !Name !Name
|
||||
| WithN !Int !Name
|
||||
| InstanceN !Name [T.Text]
|
||||
| ParentN !Name !T.Text
|
||||
| MethodN !Name
|
||||
| CaseN !Name
|
||||
| ElimN !Name
|
||||
| InstanceCtorN !Name
|
||||
| MetaN !Name !Name
|
||||
deriving (Eq, Ord, Data, Typeable)
|
||||
{-!
|
||||
deriving instance Binary SpecialName
|
||||
|
||||
@ -6,6 +6,10 @@ import Idris.Core.DeepSeq
|
||||
import Idris.Docstrings
|
||||
import Idris.Core.TT
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Colours
|
||||
import IRTS.Lang (PrimFn(..))
|
||||
import IRTS.CodegenCommon (OutputType (..))
|
||||
import Util.DynamicLinker
|
||||
|
||||
import Control.DeepSeq
|
||||
|
||||
@ -18,6 +22,281 @@ instance NFData a => NFData (D.Docstring a) where
|
||||
instance NFData CT.Options where
|
||||
rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
|
||||
|
||||
instance NFData ConsoleWidth where
|
||||
rnf InfinitelyWide = ()
|
||||
rnf (ColsWide x) = rnf x `seq` ()
|
||||
rnf AutomaticWidth = ()
|
||||
|
||||
instance NFData PrimFn where
|
||||
rnf (LPlus x) = rnf x `seq` ()
|
||||
rnf (LMinus x) = rnf x `seq` ()
|
||||
rnf (LTimes x) = rnf x `seq` ()
|
||||
rnf (LUDiv x) = rnf x `seq` ()
|
||||
rnf (LSDiv x) = rnf x `seq` ()
|
||||
rnf (LURem x) = rnf x `seq` ()
|
||||
rnf (LSRem x) = rnf x `seq` ()
|
||||
rnf (LAnd x) = rnf x `seq` ()
|
||||
rnf (LOr x) = rnf x `seq` ()
|
||||
rnf (LXOr x) = rnf x `seq` ()
|
||||
rnf (LCompl x) = rnf x `seq` ()
|
||||
rnf (LSHL x) = rnf x `seq` ()
|
||||
rnf (LLSHR x) = rnf x `seq` ()
|
||||
rnf (LASHR x) = rnf x `seq` ()
|
||||
rnf (LEq x) = rnf x `seq` ()
|
||||
rnf (LLt x) = rnf x `seq` ()
|
||||
rnf (LLe x) = rnf x `seq` ()
|
||||
rnf (LGt x) = rnf x `seq` ()
|
||||
rnf (LGe x) = rnf x `seq` ()
|
||||
rnf (LSLt x) = rnf x `seq` ()
|
||||
rnf (LSLe x) = rnf x `seq` ()
|
||||
rnf (LSGt x) = rnf x `seq` ()
|
||||
rnf (LSGe x) = rnf x `seq` ()
|
||||
rnf (LSExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (LZExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (LTrunc x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (LStrConcat) = ()
|
||||
rnf (LStrLt) = ()
|
||||
rnf (LStrEq) = ()
|
||||
rnf (LStrLen) = ()
|
||||
rnf (LIntFloat x) = rnf x `seq` ()
|
||||
rnf (LFloatInt x) = rnf x `seq` ()
|
||||
rnf (LIntStr x) = rnf x `seq` ()
|
||||
rnf (LStrInt x) = rnf x `seq` ()
|
||||
rnf (LFloatStr) = ()
|
||||
rnf (LStrFloat) = ()
|
||||
rnf (LChInt x) = rnf x `seq` ()
|
||||
rnf (LIntCh x) = rnf x `seq` ()
|
||||
rnf (LBitCast x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
|
||||
rnf (LFExp) = ()
|
||||
rnf (LFLog) = ()
|
||||
rnf (LFSin) = ()
|
||||
rnf (LFCos) = ()
|
||||
rnf (LFTan) = ()
|
||||
rnf (LFASin) = ()
|
||||
rnf (LFACos) = ()
|
||||
rnf (LFATan) = ()
|
||||
rnf (LFSqrt) = ()
|
||||
rnf (LFFloor) = ()
|
||||
rnf (LFCeil) = ()
|
||||
rnf (LFNegate) = ()
|
||||
rnf (LStrHead) = ()
|
||||
rnf (LStrTail) = ()
|
||||
rnf (LStrCons) = ()
|
||||
rnf (LStrIndex) = ()
|
||||
rnf (LStrRev) = ()
|
||||
rnf (LReadStr) = ()
|
||||
rnf (LWriteStr) = ()
|
||||
rnf (LSystemInfo) = ()
|
||||
rnf (LFork) = ()
|
||||
rnf (LPar) = ()
|
||||
rnf (LExternal x) = rnf x `seq` ()
|
||||
rnf (LNoOp) = ()
|
||||
|
||||
instance NFData SyntaxRules where
|
||||
rnf (SyntaxRules xs) = rnf xs `seq` ()
|
||||
|
||||
instance NFData DynamicLib where
|
||||
rnf (Lib x _) = rnf x `seq` ()
|
||||
|
||||
|
||||
instance NFData Opt where
|
||||
rnf (Filename str) = rnf str `seq` ()
|
||||
rnf (Quiet) = ()
|
||||
rnf (NoBanner) = ()
|
||||
rnf (ColourREPL bool) = rnf bool `seq` ()
|
||||
rnf (Idemode) = ()
|
||||
rnf (IdemodeSocket) = ()
|
||||
rnf (ShowLibs) = ()
|
||||
rnf (ShowLibdir) = ()
|
||||
rnf (ShowIncs) = ()
|
||||
rnf (ShowPkgs) = ()
|
||||
rnf (NoBasePkgs) = ()
|
||||
rnf (NoPrelude) = ()
|
||||
rnf (NoBuiltins) = ()
|
||||
rnf (NoREPL) = ()
|
||||
rnf (OLogging i) = rnf i `seq` ()
|
||||
rnf (Output str) = rnf str `seq` ()
|
||||
rnf (Interface) = ()
|
||||
rnf (TypeCase) = ()
|
||||
rnf (TypeInType) = ()
|
||||
rnf (DefaultTotal) = ()
|
||||
rnf (DefaultPartial) = ()
|
||||
rnf (WarnPartial) = ()
|
||||
rnf (WarnReach) = ()
|
||||
rnf (EvalTypes) = ()
|
||||
rnf (NoCoverage) = ()
|
||||
rnf (ErrContext) = ()
|
||||
rnf (ShowImpl) = ()
|
||||
rnf (Verbose) = ()
|
||||
rnf (Port str) = rnf str `seq` ()
|
||||
rnf (IBCSubDir str) = rnf str `seq` ()
|
||||
rnf (ImportDir str) = rnf str `seq` ()
|
||||
rnf (PkgBuild str) = rnf str `seq` ()
|
||||
rnf (PkgInstall str) = rnf str `seq` ()
|
||||
rnf (PkgClean str) = rnf str `seq` ()
|
||||
rnf (PkgCheck str) = rnf str `seq` ()
|
||||
rnf (PkgREPL str) = rnf str `seq` ()
|
||||
rnf (PkgMkDoc str) = rnf str `seq` ()
|
||||
rnf (PkgTest str) = rnf str `seq` ()
|
||||
rnf (PkgIndex fp) = rnf fp `seq` ()
|
||||
rnf (WarnOnly) = ()
|
||||
rnf (Pkg str) = rnf str `seq` ()
|
||||
rnf (BCAsm str) = rnf str `seq` ()
|
||||
rnf (DumpDefun str) = rnf str `seq` ()
|
||||
rnf (DumpCases str) = rnf str `seq` ()
|
||||
rnf (UseCodegen cg) = rnf cg `seq` ()
|
||||
rnf (CodegenArgs str) = rnf str `seq` ()
|
||||
rnf (OutputTy ot) = rnf ot `seq` ()
|
||||
rnf (Extension le) = rnf le `seq` ()
|
||||
rnf (InterpretScript str) = rnf str `seq` ()
|
||||
rnf (EvalExpr str) = rnf str `seq` ()
|
||||
rnf (TargetTriple str) = rnf str `seq` ()
|
||||
rnf (TargetCPU str) = rnf str `seq` ()
|
||||
rnf (OptLevel i) = rnf i `seq` ()
|
||||
rnf (AddOpt o) = rnf o `seq` ()
|
||||
rnf (RemoveOpt o) = rnf o `seq` ()
|
||||
rnf (Client str) = rnf str `seq` ()
|
||||
rnf (ShowOrigErr) = ()
|
||||
rnf (AutoWidth) = ()
|
||||
rnf (AutoSolve) = ()
|
||||
rnf (UseConsoleWidth cw) = rnf cw `seq` ()
|
||||
rnf (DumpHighlights) = ()
|
||||
|
||||
|
||||
instance NFData TIData where
|
||||
rnf TIPartial = ()
|
||||
rnf (TISolution xs) = rnf xs `seq` ()
|
||||
|
||||
instance NFData IOption where
|
||||
rnf (IOption
|
||||
opt_logLevel
|
||||
opt_typecase
|
||||
opt_typeintype
|
||||
opt_coverage
|
||||
opt_showimp
|
||||
opt_errContext
|
||||
opt_repl
|
||||
opt_verbose
|
||||
opt_nobanner
|
||||
opt_quiet
|
||||
opt_codegen
|
||||
opt_outputTy
|
||||
opt_ibcsubdir
|
||||
opt_importdirs
|
||||
opt_triple
|
||||
opt_cpu
|
||||
opt_cmdline
|
||||
opt_origerr
|
||||
opt_autoSolve
|
||||
opt_autoImport
|
||||
opt_optimise
|
||||
opt_printdepth
|
||||
opt_evaltypes) =
|
||||
rnf opt_logLevel
|
||||
`seq` rnf opt_typecase
|
||||
`seq` rnf opt_typeintype
|
||||
`seq` rnf opt_coverage
|
||||
`seq` rnf opt_showimp
|
||||
`seq` rnf opt_errContext
|
||||
`seq` rnf opt_repl
|
||||
`seq` rnf opt_verbose
|
||||
`seq` rnf opt_nobanner
|
||||
`seq` rnf opt_quiet
|
||||
`seq` rnf opt_codegen
|
||||
`seq` rnf opt_outputTy
|
||||
`seq` rnf opt_ibcsubdir
|
||||
`seq` rnf opt_importdirs
|
||||
`seq` rnf opt_triple
|
||||
`seq` rnf opt_cpu
|
||||
`seq` rnf opt_cmdline
|
||||
`seq` rnf opt_origerr
|
||||
`seq` rnf opt_autoSolve
|
||||
`seq` rnf opt_autoImport
|
||||
`seq` rnf opt_optimise
|
||||
`seq` rnf opt_printdepth
|
||||
`seq` rnf opt_evaltypes
|
||||
`seq` ()
|
||||
|
||||
instance NFData LanguageExt where
|
||||
rnf TypeProviders = ()
|
||||
rnf ErrorReflection = ()
|
||||
|
||||
instance NFData Optimisation where
|
||||
rnf PETransform = ()
|
||||
|
||||
instance NFData ColourTheme where
|
||||
rnf (ColourTheme keywordColour
|
||||
boundVarColour
|
||||
implicitColour
|
||||
functionColour
|
||||
typeColour
|
||||
dataColour
|
||||
promptColour
|
||||
postulateColour) =
|
||||
rnf keywordColour
|
||||
`seq` rnf boundVarColour
|
||||
`seq` rnf implicitColour
|
||||
`seq` rnf functionColour
|
||||
`seq` rnf typeColour
|
||||
`seq` rnf dataColour
|
||||
`seq` rnf promptColour
|
||||
`seq` rnf postulateColour
|
||||
`seq` ()
|
||||
|
||||
instance NFData IdrisColour where
|
||||
rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
|
||||
|
||||
instance NFData OutputType where
|
||||
rnf Raw = ()
|
||||
rnf Object = ()
|
||||
rnf Executable = ()
|
||||
rnf MavenProject = ()
|
||||
|
||||
instance NFData IBCWrite where
|
||||
rnf (IBCFix fixDecl) = rnf fixDecl `seq` ()
|
||||
rnf (IBCImp name) = rnf name `seq` ()
|
||||
rnf (IBCStatic name) = rnf name `seq` ()
|
||||
rnf (IBCClass name) = rnf name `seq` ()
|
||||
rnf (IBCInstance b1 b2 n1 n2) = rnf b1 `seq` rnf b2 `seq` rnf n1 `seq` rnf n2 `seq` ()
|
||||
rnf (IBCDSL name) = rnf name `seq` ()
|
||||
rnf (IBCData name) = rnf name `seq` ()
|
||||
rnf (IBCOpt name) = rnf name `seq` ()
|
||||
rnf (IBCMetavar name) = rnf name `seq` ()
|
||||
rnf (IBCSyntax syntax) = rnf syntax `seq` ()
|
||||
rnf (IBCKeyword string) = rnf string `seq` ()
|
||||
rnf (IBCImport imp) = rnf imp `seq` ()
|
||||
rnf (IBCImportDir filePath) = rnf filePath `seq` ()
|
||||
rnf (IBCObj codegen filePath) = rnf codegen `seq` rnf filePath `seq` ()
|
||||
rnf (IBCLib codegen string) = rnf codegen `seq` rnf string `seq` ()
|
||||
rnf (IBCCGFlag codegen string) = rnf codegen `seq` rnf string `seq` ()
|
||||
rnf (IBCDyLib string) = rnf string `seq` ()
|
||||
rnf (IBCHeader codegen string) = rnf codegen `seq` rnf string `seq` ()
|
||||
rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()
|
||||
rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()
|
||||
rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()
|
||||
rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()
|
||||
rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()
|
||||
rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()
|
||||
rnf (IBCErrRev terms) = rnf terms `seq` ()
|
||||
rnf (IBCCG name) = rnf name `seq` ()
|
||||
rnf (IBCDoc name) = rnf name `seq` ()
|
||||
rnf (IBCCoercion name) = rnf name `seq` ()
|
||||
rnf (IBCDef name) = rnf name `seq` ()
|
||||
rnf (IBCNameHint names) = rnf names `seq` ()
|
||||
rnf (IBCLineApp filePath int pTerm) = rnf filePath `seq` rnf int `seq` rnf pTerm `seq` ()
|
||||
rnf (IBCErrorHandler name) = rnf name `seq` ()
|
||||
rnf (IBCFunctionErrorHandler n1 n2 n3) = rnf n1 `seq` rnf n2 `seq` rnf n3 `seq` ()
|
||||
rnf (IBCPostulate name) = rnf name `seq` ()
|
||||
rnf (IBCExtern extern) = rnf extern `seq` ()
|
||||
rnf (IBCTotCheckErr fc string) = rnf fc `seq` rnf string `seq` ()
|
||||
rnf (IBCParsedRegion fc) = rnf fc `seq` ()
|
||||
rnf (IBCModDocs name) = rnf name `seq` ()
|
||||
rnf (IBCUsage usage) = rnf usage `seq` ()
|
||||
rnf (IBCExport name) = rnf name `seq` ()
|
||||
rnf (IBCAutoHint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()
|
||||
rnf (IBCRecord x) = rnf x `seq` ()
|
||||
|
||||
|
||||
instance NFData a => NFData (D.Block a) where
|
||||
rnf (D.Para lines) = rnf lines `seq` ()
|
||||
rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()
|
||||
@ -394,3 +673,18 @@ instance NFData SyntaxInfo where
|
||||
rnf x4 `seq`
|
||||
rnf x5 `seq`
|
||||
rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()
|
||||
|
||||
instance NFData OutputMode where
|
||||
rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
|
||||
rnf (IdeMode x y) = rnf x `seq` ()
|
||||
|
||||
|
||||
instance NFData IState where
|
||||
rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
|
||||
x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
|
||||
x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60
|
||||
x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73)
|
||||
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`
|
||||
rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`
|
||||
rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`
|
||||
rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` ()
|
||||
|
||||
@ -309,7 +309,7 @@ ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f
|
||||
getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b
|
||||
getEntry alt f a = case findEntryByPath f a of
|
||||
Nothing -> return alt
|
||||
Just e -> return $ (force . decode . fromEntry) e
|
||||
Just e -> return $! (force . decode . fromEntry) e
|
||||
|
||||
process :: Bool -- ^ Reexporting
|
||||
-> Archive -> FilePath -> Idris ()
|
||||
|
||||
@ -327,10 +327,13 @@ runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =
|
||||
reverse unused)]
|
||||
runIO . hPutStrLn h $ IdeMode.convSExp "return" good id
|
||||
runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename toline) =
|
||||
-- The $!! here prevents a space leak on reloading.
|
||||
-- This isn't a solution - but it's a temporary stopgap.
|
||||
-- See issue #2386
|
||||
do i <- getIState
|
||||
clearErr
|
||||
putIState (orig { idris_options = idris_options i,
|
||||
idris_outputmode = (IdeMode id h) })
|
||||
putIState $!! orig { idris_options = idris_options i,
|
||||
idris_outputmode = (IdeMode id h) }
|
||||
mods <- loadInputs [filename] toline
|
||||
isetPrompt (mkPrompt mods)
|
||||
-- Report either success or failure
|
||||
@ -686,17 +689,23 @@ processInput cmd orig inputs efile
|
||||
Failure err -> do iputStrLn $ show (fixColour c err)
|
||||
return (Just inputs)
|
||||
Success (Right Reload) ->
|
||||
do putIState $ orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
, imported = imported i
|
||||
}
|
||||
-- The $!! here prevents a space leak on reloading.
|
||||
-- This isn't a solution - but it's a temporary stopgap.
|
||||
-- See issue #2386
|
||||
do putIState $!! orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
, imported = imported i
|
||||
}
|
||||
clearErr
|
||||
mods <- loadInputs inputs Nothing
|
||||
return (Just mods)
|
||||
Success (Right (Load f toline)) ->
|
||||
do putIState orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
}
|
||||
-- The $!! here prevents a space leak on reloading.
|
||||
-- This isn't a solution - but it's a temporary stopgap.
|
||||
-- See issue #2386
|
||||
do putIState $!! orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
}
|
||||
clearErr
|
||||
mod <- loadInputs [f] toline
|
||||
return (Just mod)
|
||||
@ -746,9 +755,9 @@ edit f orig
|
||||
let args = line ++ [fixName f]
|
||||
runIO $ rawSystem editor args
|
||||
clearErr
|
||||
putIState $ orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
}
|
||||
putIState $!! orig { idris_options = idris_options i
|
||||
, idris_colourTheme = idris_colourTheme i
|
||||
}
|
||||
loadInputs [f] Nothing
|
||||
-- clearOrigPats
|
||||
iucheck
|
||||
@ -1510,13 +1519,13 @@ loadInputs inputs toline -- furthest line to read in input source files
|
||||
-- If it worked, load the whole thing from all the ibcs together
|
||||
case errSpan inew of
|
||||
Nothing ->
|
||||
do putIState (ist { idris_tyinfodata = tidata })
|
||||
do putIState $!! ist { idris_tyinfodata = tidata }
|
||||
ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))
|
||||
tryLoad True (mapMaybe id ibcfiles)
|
||||
_ -> return ()
|
||||
ist <- getIState
|
||||
putIState (ist { idris_tyinfodata = tidata,
|
||||
idris_patdefs = patdefs })
|
||||
putIState $! ist { idris_tyinfodata = tidata,
|
||||
idris_patdefs = patdefs }
|
||||
exports <- findExports
|
||||
|
||||
case opt getOutput opts of
|
||||
@ -1560,11 +1569,15 @@ loadInputs inputs toline -- furthest line to read in input source files
|
||||
let tidata = idris_tyinfodata inew
|
||||
let patdefs = idris_patdefs inew
|
||||
ok <- noErrors
|
||||
when ok $ do when (not keepstate) $ putIState ist
|
||||
ist <- getIState
|
||||
putIState (ist { idris_tyinfodata = tidata,
|
||||
idris_patdefs = patdefs })
|
||||
tryLoad keepstate fs
|
||||
when ok $
|
||||
-- The $!! here prevents a space leak on reloading.
|
||||
-- This isn't a solution - but it's a temporary stopgap.
|
||||
-- See issue #2386
|
||||
do when (not keepstate) $ putIState $!! ist
|
||||
ist <- getIState
|
||||
putIState $!! ist { idris_tyinfodata = tidata,
|
||||
idris_patdefs = patdefs }
|
||||
tryLoad keepstate fs
|
||||
|
||||
ibc (IBC _ _) = True
|
||||
ibc _ = False
|
||||
|
||||
Loading…
Reference in New Issue
Block a user