git.iko.soy/Idris-dev
on master help sign in
Make the rest of erasure use ASTUtils.
e38b6c1Matus Tejiscak
src/Idris/ASTUtils.hs+29−6
compare with master
unifiedsplit
@@ -36,29 +36,36 @@ fputState field x = fmodifyState field (const x)
36fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
36fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
37fmodifyState field f = modify $ fmodify field f
37fmodifyState field f = modify $ fmodify field f
38
38
39+-- Until now, we'd have just ad-hoc empty lists and Falses thrown around
40+-- whenever a new instance of a record was to be created.
41+--
42+-- This class formalises the notion of an initial value for a record.
39class InitialValue a where
43class InitialValue a where
40 initialValue :: a
44 initialValue :: a
41
45
46+-- Exact-name context lookup; uses the initial value if needed.
42ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
47ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
43ctxt_lookupExact n = Field
48ctxt_lookupExact n = Field
44 { fget = fromMaybe initialValue . lookupCtxtExact n
49 { fget = fromMaybe initialValue . lookupCtxtExact n
45 , fset = addDef n
50 , fset = addDef n
46 }
51 }
47
52
53+
48-----------------------------------
54-----------------------------------
49-- Individual records and fields --
55-- Individual records and fields --
50-----------------------------------
56-----------------------------------
51
57
58+
59+-- OptInfo
60+----------
61+
52instance InitialValue OptInfo where
62instance InitialValue OptInfo where
53 initialValue = Optimise [] False
63 initialValue = Optimise [] False
54
64
55−-- raw context, probably won't be used much
56−ist_optimisation_ctxt :: Field IState (Ctxt OptInfo)
57−ist_optimisation_ctxt = Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
58−
59−-- the optimisation record for the given name
65+-- the optimisation record for the given (exact) name
60ist_optimisation :: Name -> Field IState OptInfo
66ist_optimisation :: Name -> Field IState OptInfo
61−ist_optimisation n = ctxt_lookupExact n . ist_optimisation_ctxt
67+ist_optimisation n = ctxt_lookupExact n
68+ . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
62
69
63-- two fields of the optimisation record
70-- two fields of the optimisation record
64opt_inaccessible :: Field OptInfo [(Int, Name)]
71opt_inaccessible :: Field OptInfo [(Int, Name)]
@@ -66,3 +73,19 @@ opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
66
73
67opt_detaggable :: Field OptInfo Bool
74opt_detaggable :: Field OptInfo Bool
68opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
75opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
76+
77+
78+-- CGInfo
79+---------
80+
81+instance InitialValue CGInfo where
82+ initialValue = CGInfo [] [] [] [] []
83+
84+-- callgraph record for the given (exact) name
85+ist_callgraph :: Name -> Field IState CGInfo
86+ist_callgraph n = ctxt_lookupExact n
87+ . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
88+
89+-- some fields of the CGInfo record
90+cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
91+cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })
src/Idris/AbsSyntaxTree.hs+2−1
@@ -177,12 +177,13 @@ deriving instance NFData SizeChange
177!-}
177!-}
178
178
179type SCGEntry = (Name, [Maybe (Int, SizeChange)])
179type SCGEntry = (Name, [Maybe (Int, SizeChange)])
180+type UsageReason = (Name, Int) -- fn_name, its_arg_number
180
181
181data CGInfo = CGInfo { argsdef :: [Name],
182data CGInfo = CGInfo { argsdef :: [Name],
182 calls :: [(Name, [[Name]])],
183 calls :: [(Name, [[Name]])],
183 scg :: [SCGEntry],
184 scg :: [SCGEntry],
184 argsused :: [Name],
185 argsused :: [Name],
185− usedpos :: [(Int, [(Name, Int)])] } -- (used_arg#, [(using_fn, its_arg#)])
186+ usedpos :: [(Int, [UsageReason])] }
186 deriving Show
187 deriving Show
187{-!
188{-!
188deriving instance Binary CGInfo
189deriving instance Binary CGInfo
src/Idris/Erasure.hs+7−8
@@ -3,6 +3,7 @@
3module Idris.Erasure (performUsageAnalysis, mkFieldName) where
3module Idris.Erasure (performUsageAnalysis, mkFieldName) where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6+import Idris.ASTUtils
6import Idris.Core.CaseTree
7import Idris.Core.CaseTree
7import Idris.Core.TT
8import Idris.Core.TT
8import Idris.Core.Evaluate
9import Idris.Core.Evaluate
@@ -12,6 +13,9 @@ import Idris.Error
12import Debug.Trace
13import Debug.Trace
13import System.IO.Unsafe
14import System.IO.Unsafe
14
15
16+import Control.Category
17+import Prelude hiding (id, (.))
18+
15import Control.Arrow
19import Control.Arrow
16import Control.Applicative
20import Control.Applicative
17import Control.Monad.State
21import Control.Monad.State
@@ -97,7 +101,7 @@ performUsageAnalysis = do
97 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])
101 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])
98
102
99 -- Store the usage info in the internal state.
103 -- Store the usage info in the internal state.
100− mapM_ (storeUsage cg) usage
104+ mapM_ storeUsage usage
101
105
102 return $ S.toList reachableNames
106 return $ S.toList reachableNames
103 where
107 where
@@ -124,13 +128,8 @@ performUsageAnalysis = do
124 | S.null rs = show i
128 | S.null rs = show i
125 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)
129 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)
126
130
127− storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()
131+ storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
128− storeUsage cg (n, args)
132+ storeUsage (n, args) = fputState (cg_usedpos . ist_callgraph n) flat
129− | Just x <- lookupCtxtExact n cg
130− = addToCG n x{ usedpos = flat } -- functions
131−
132− | otherwise
133− = addToCG n (CGInfo [] [] [] [] flat) -- data ctors
134 where
133 where
135 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
134 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
136
135