b30e112 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

add a type alias for the TT Declaration as it is getting unwieldy

commitb30e112f40ad9bd78bbc7610bff2a9d3a85999c1 authorjoe9 <joe9mail@gmail.com> dateFri 20 Jan 2017, 13:06 (10 years ago) parent2339c66

3 files changed+5−4

compare with master

unifiedsplit

src/IRTS/CodegenCommon.hs+1−1 src/IRTS/Compiler.hs+1−1 src/Idris/Core/Evaluate.hs+3−2

src/IRTS/CodegenCommon.hs+1−1

@@ -40,7 +40,7 @@ data CodegenInfo = CodegenInfo {

4040 , liftDecls :: [(Name, LDecl)]

4141 , interfaces :: Bool

4242 , exportDecls :: [ExportIFace]

43− , ttDecls :: [(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))]

43+ , ttDecls :: [(Name, TTDecl)]

4444 }

4545

4646type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+1−1

@@ -166,7 +166,7 @@ mkDecls used

166166 decls <- mapM build ds

167167 return decls

168168

169−getDeclarations :: [Name] -> Idris ([(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))])

169+getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])

170170getDeclarations used

171171 = do i <- getIState

172172 let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)

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

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

1414 rt_simplify, simplify, inlineSmall,

1515 specialise, unfold, convEq, convEq',

1616 Def(..), CaseInfo(..), CaseDefs(..),

17− Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),

17+ Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),

1818 Context, initContext, ctxtAlist, next_tvar,

1919 addToCtxt, setAccess, setInjective, setTotal, setRigCount,

2020 setMetaInformation, addCtxtDef, addTyDecl,

@@ -872,9 +872,10 @@ data MetaInformation =

872872-- 1 in a RigW, for example)

873873data Context = MkContext {

874874 next_tvar :: Int,

875− definitions :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)

875+ definitions :: Ctxt TTDecl

876876 } deriving (Show, Generic)

877877

878+type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)

878879

879880-- | The initial empty context

880881initContext = MkContext 0 emptyContext