git.iko.soy/Idris-dev
on master help sign in
add a type alias for the TT Declaration as it is getting unwieldy
b30e112joe9
src/IRTS/CodegenCommon.hs+1−1
compare with master
unifiedsplit
@@ -40,7 +40,7 @@ data CodegenInfo = CodegenInfo {
40 , liftDecls :: [(Name, LDecl)]
40 , liftDecls :: [(Name, LDecl)]
41 , interfaces :: Bool
41 , interfaces :: Bool
42 , exportDecls :: [ExportIFace]
42 , exportDecls :: [ExportIFace]
43− , ttDecls :: [(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))]
43+ , ttDecls :: [(Name, TTDecl)]
44 }
44 }
45
45
46type CodeGenerator = CodegenInfo -> IO ()
46type CodeGenerator = CodegenInfo -> IO ()
src/IRTS/Compiler.hs+1−1
@@ -166,7 +166,7 @@ mkDecls used
166 decls <- mapM build ds
166 decls <- mapM build ds
167 return decls
167 return decls
168
168
169−getDeclarations :: [Name] -> Idris ([(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))])
169+getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
170getDeclarations used
170getDeclarations used
171 = do i <- getIState
171 = do i <- getIState
172 let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
172 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,
14 rt_simplify, simplify, inlineSmall,
14 rt_simplify, simplify, inlineSmall,
15 specialise, unfold, convEq, convEq',
15 specialise, unfold, convEq, convEq',
16 Def(..), CaseInfo(..), CaseDefs(..),
16 Def(..), CaseInfo(..), CaseDefs(..),
17− Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
17+ Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
18 Context, initContext, ctxtAlist, next_tvar,
18 Context, initContext, ctxtAlist, next_tvar,
19 addToCtxt, setAccess, setInjective, setTotal, setRigCount,
19 addToCtxt, setAccess, setInjective, setTotal, setRigCount,
20 setMetaInformation, addCtxtDef, addTyDecl,
20 setMetaInformation, addCtxtDef, addTyDecl,
@@ -872,9 +872,10 @@ data MetaInformation =
872-- 1 in a RigW, for example)
872-- 1 in a RigW, for example)
873data Context = MkContext {
873data Context = MkContext {
874 next_tvar :: Int,
874 next_tvar :: Int,
875− definitions :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
875+ definitions :: Ctxt TTDecl
876 } deriving (Show, Generic)
876 } deriving (Show, Generic)
877
877
878+type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
878
879
879-- | The initial empty context
880-- | The initial empty context
880initContext = MkContext 0 emptyContext
881initContext = MkContext 0 emptyContext