git.iko.soy/Idris-dev
on master help sign in
Make the rest of erasure use ASTUtils.
commite38b6c1a68e014f1726d1788293f82c250bae7cd authorMatus Tejiscak <ziman@functor.sk> dateMon 14 Apr 2014, 16:30 (13 years ago) parenteedcec1
3 files changed+38−15
compare with master
unifiedsplit
src/Idris/ASTUtils.hs+29−6 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Erasure.hs+7−8
src/Idris/ASTUtils.hs+29−6
@@ -36,29 +36,36 @@ fputState field x = fmodifyState field (const x)
3636fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
3737fmodifyState field f = modify $ fmodify field f
3838
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.
3943class InitialValue a where
4044 initialValue :: a
4145
46+-- Exact-name context lookup; uses the initial value if needed.
4247ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
4348ctxt_lookupExact n = Field
4449 { fget = fromMaybe initialValue . lookupCtxtExact n
4550 , fset = addDef n
4651 }
4752
53+
4854-----------------------------------
4955-- Individual records and fields --
5056-----------------------------------
5157
58+
59+-- OptInfo
60+----------
61+
5262instance InitialValue OptInfo where
5363 initialValue = Optimise [] False
5464
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
6066ist_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 })
6269
6370-- two fields of the optimisation record
6471opt_inaccessible :: Field OptInfo [(Int, Name)]
@@ -66,3 +73,19 @@ opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
6673
6774opt_detaggable :: Field OptInfo Bool
6875opt_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
177177!-}
178178
179179type SCGEntry = (Name, [Maybe (Int, SizeChange)])
180+type UsageReason = (Name, Int) -- fn_name, its_arg_number
180181
181182data CGInfo = CGInfo { argsdef :: [Name],
182183 calls :: [(Name, [[Name]])],
183184 scg :: [SCGEntry],
184185 argsused :: [Name],
185− usedpos :: [(Int, [(Name, Int)])] } -- (used_arg#, [(using_fn, its_arg#)])
186+ usedpos :: [(Int, [UsageReason])] }
186187 deriving Show
187188{-!
188189deriving instance Binary CGInfo
src/Idris/Erasure.hs+7−8
@@ -3,6 +3,7 @@
33module Idris.Erasure (performUsageAnalysis, mkFieldName) where
44
55import Idris.AbsSyntax
6+import Idris.ASTUtils
67import Idris.Core.CaseTree
78import Idris.Core.TT
89import Idris.Core.Evaluate
@@ -12,6 +13,9 @@ import Idris.Error
1213import Debug.Trace
1314import System.IO.Unsafe
1415
16+import Control.Category
17+import Prelude hiding (id, (.))
18+
1519import Control.Arrow
1620import Control.Applicative
1721import Control.Monad.State
@@ -97,7 +101,7 @@ performUsageAnalysis = do
97101 $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])
98102
99103 -- Store the usage info in the internal state.
100− mapM_ (storeUsage cg) usage
104+ mapM_ storeUsage usage
101105
102106 return $ S.toList reachableNames
103107 where
@@ -124,13 +128,8 @@ performUsageAnalysis = do
124128 | S.null rs = show i
125129 | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)
126130
127− storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()
128− storeUsage cg (n, args)
129− | Just x <- lookupCtxtExact n cg
130− = addToCG n x{ usedpos = flat } -- functions
131−
132− | otherwise
133− = addToCG n (CGInfo [] [] [] [] flat) -- data ctors
131+ storeUsage :: (Name, IntMap (Set Reason)) -> Idris ()
132+ storeUsage (n, args) = fputState (cg_usedpos . ist_callgraph n) flat
134133 where
135134 flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]
136135