git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1065 from ziman/fields

Lens-style IState updates

commitf03ee7e39fdacaaef3770536b36f45f1c01edfe4 authorEdwin Brady <edwin.brady@gmail.com> dateThu 17 Apr 2014, 11:58 (13 years ago) parent029f67c24ced57
7 files changed+151−47
compare with master
unifiedsplit
idris.cabal+1 src/IRTS/Compiler.hs+11−14 src/Idris/ASTUtils.hs+115 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Core/TT.hs+1 src/Idris/ElabDecls.hs+14−24 src/Idris/Erasure.hs+7−8
idris.cabal+1
@@ -456,6 +456,7 @@ Library
456456 , Idris.AbsSyntax
457457 , Idris.AbsSyntaxTree
458458 , Idris.Apropos
459+ , Idris.ASTUtils
459460 , Idris.CaseSplit
460461 , Idris.Chaser
461462 , Idris.Colours
src/IRTS/Compiler.hs+11−14
@@ -19,6 +19,7 @@ import IRTS.Inliner
1919
2020import Idris.AbsSyntax
2121import Idris.AbsSyntaxTree
22+import Idris.ASTUtils
2223import Idris.Erasure
2324import Idris.Error
2425
@@ -28,6 +29,9 @@ import Idris.Core.TT
2829import Idris.Core.Evaluate
2930import Idris.Core.CaseTree
3031
32+import Control.Category
33+import Prelude hiding (id, (.))
34+
3135import Control.Applicative
3236import Control.Monad.State
3337import Data.Maybe
@@ -172,10 +176,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
172176 (args, sc) = cases_runtime cd
173177
174178mkLDecl n (TyDecl (DCon tag arity) _) =
175− LConstructor n tag . erasedArity . lookup n <$> getIState
176− where
177− lookup n = lookupCtxtExact n . idris_callgraph
178− erasedArity = maybe 0 (length . usedpos)
179+ LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
179180
180181mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
181182mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
@@ -262,14 +263,13 @@ irTerm vs env tm@(App f a) = case unApply tm of
262263 ])
263264
264265 (P (DCon t arity) n _, args) -> do
265− ist <- getIState
266− let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267− used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268− args' = [a | (i,a) <- zip [0..] args, i `elem` used]
266+ detag <- fgetState (opt_detaggable . ist_optimisation n)
267+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
269268
270269 when (length args > arity) $
271270 ifail ("oversaturated data ctor: " ++ show tm)
272271
272+ let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
273273 if length args' == 1 && detag -- detaggable
274274 then irTerm vs env (head args') -- newtype
275275 else irCon vs env (length used) n args'
@@ -473,8 +473,8 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
473473irSC vs (Case n [alt]) = do
474474 replacement <- case alt of
475475 ConCase cn a ns sc -> do
476− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
477− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
476+ detag <- fgetState (opt_detaggable . ist_optimisation cn)
477+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
478478 if detag && length used == 1
479479 then return . Just $ substSC (ns !! head used) n sc
480480 else return Nothing
@@ -505,13 +505,10 @@ irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
505505
506506-- this leaves out all unused arguments of the constructor
507507irAlt vs _ (ConCase n t args sc) = do
508− used <- getUsed . lookup n <$> getIState
508+ used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
509509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
510510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
511511 where
512− lookup n = lookupCtxtExact n . idris_callgraph
513− getUsed = maybe [] (map fst . usedpos)
514−
515512 methodVars = case n of
516513 SN (InstanceCtorN className)
517514 -> M.fromList [(v, VI
src/Idris/ASTUtils.hsnew file+115
@@ -0,0 +1,115 @@
1+module Idris.ASTUtils where
2+
3+-- This implements just a few basic lens-like concepts to ease state updates.
4+-- Similar to fclabels in approach, just without the extra dependency.
5+--
6+-- We don't include an explicit export list
7+-- because everything here is meant to be exported.
8+--
9+-- Short synopsis:
10+-- ---------------
11+--
12+-- f :: Idris ()
13+-- f = do
14+-- -- these two steps:
15+-- detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
16+-- fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)
17+--
18+-- -- are equivalent to:
19+-- fmodifyState (opt_detaggable . ist_optimisation typeName) not
20+--
21+-- -- of course, the long accessor can be put in a variable;
22+-- -- everything is first-class
23+-- let detag n = opt_detaggable . ist_optimisation n
24+-- fputState (detag n1) True
25+-- fputState (detag n2) False
26+--
27+-- -- Note that all these operations handle missing items consistently
28+-- -- and transparently, as prescribed by the typeclass InitialValue.
29+
30+import Control.Category
31+import Control.Applicative
32+import Control.Monad.State.Class
33+import Data.Maybe
34+import Prelude hiding (id, (.))
35+
36+import Idris.Core.TT
37+import Idris.AbsSyntaxTree
38+
39+data Field rec fld = Field
40+ { fget :: rec -> fld
41+ , fset :: fld -> rec -> rec
42+ }
43+
44+fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
45+fmodify field f x = fset field (f $ fget field x) x
46+
47+instance Category Field where
48+ id = Field id const
49+ Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
50+
51+fgetState :: MonadState s m => Field s a -> m a
52+fgetState field = gets $ fget field
53+
54+fputState :: MonadState s m => Field s a -> a -> m ()
55+fputState field x = fmodifyState field (const x)
56+
57+fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
58+fmodifyState field f = modify $ fmodify field f
59+
60+-- Until now, we'd have just ad-hoc empty lists and Falses thrown around
61+-- whenever a new instance of a record was to be created.
62+--
63+-- This class formalises the notion of an initial value for a record.
64+class InitialValue a where
65+ initialValue :: a
66+
67+-- Exact-name context lookup; uses the initial value if needed.
68+ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
69+ctxt_lookupExact n = Field
70+ { fget = fromMaybe initialValue . lookupCtxtExact n
71+ , fset = addDef n
72+ }
73+
74+
75+-----------------------------------
76+-- Individual records and fields --
77+-----------------------------------
78+--
79+-- These could probably be generated; let's use lazy addition for now.
80+--
81+
82+
83+-- OptInfo
84+----------
85+
86+instance InitialValue OptInfo where
87+ initialValue = Optimise [] False
88+
89+-- the optimisation record for the given (exact) name
90+ist_optimisation :: Name -> Field IState OptInfo
91+ist_optimisation n = ctxt_lookupExact n
92+ . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
93+
94+-- two fields of the optimisation record
95+opt_inaccessible :: Field OptInfo [(Int, Name)]
96+opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
97+
98+opt_detaggable :: Field OptInfo Bool
99+opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
100+
101+
102+-- CGInfo
103+---------
104+
105+instance InitialValue CGInfo where
106+ initialValue = CGInfo [] [] [] [] []
107+
108+-- callgraph record for the given (exact) name
109+ist_callgraph :: Name -> Field IState CGInfo
110+ist_callgraph n = ctxt_lookupExact n
111+ . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
112+
113+-- some fields of the CGInfo record
114+cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
115+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/Core/TT.hs+1
@@ -383,6 +383,7 @@ implicitable _ = False
383383nsroot (NS n _) = n
384384nsroot n = n
385385
386+-- this will overwrite already existing definitions
386387addDef :: Name -> a -> Ctxt a -> Ctxt a
387388addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
388389 Nothing -> Map.insert (nsroot n)
src/Idris/ElabDecls.hs+14−24
@@ -4,6 +4,7 @@
44module Idris.ElabDecls where
55
66import Idris.AbsSyntax
7+import Idris.ASTUtils
78import Idris.DSL
89import Idris.Error
910import Idris.Delaborate
@@ -29,6 +30,10 @@ import Idris.Core.CaseTree
2930
3031import Idris.Docstrings
3132
33+import Prelude hiding (id, (.))
34+import Control.Category
35+
36+import Control.Applicative hiding (Const)
3237import Control.DeepSeq
3338import Control.Monad
3439import Control.Monad.State.Strict as State
@@ -88,7 +93,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
8893 let ty = addImpl i ty'
8994 inacc = inaccessibleArgs 0 ty
9095 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
91− logLvl 5 $ "Inaccessible arguments: " ++ show inacc
96+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc
9297
9398 ((tyT, defer, is), log) <-
9499 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -134,7 +139,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
134139 addDocStr n doc argDocs
135140 addIBC (IBCDoc n)
136141 addIBC (IBCFlags n opts')
137− saveInaccArgs n inacc
142+ fputState (opt_inaccessible . ist_optimisation n) inacc
143+ addIBC (IBCOpt n)
138144 when (Implicit `elem` opts') $ do addCoercion n
139145 addIBC (IBCCoercion n)
140146
@@ -178,24 +184,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
178184 , ns4 == map txt ["Errors","Reflection","Language"] = True
179185 tyIsHandler _ = False
180186
181−-- Store the list of inaccessible arguments in the internal state.
182−saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
183−saveInaccArgs n is = do
184− ist <- getIState
185− case lookupCtxt n (idris_optimisation ist) of
186− [oi] -> do
187− putIState ist{ idris_optimisation =
188− addDef n oi{ inaccessible = is } (idris_optimisation ist) }
189−
190− _ -> do
191− putIState ist{ idris_optimisation =
192− addDef n (Optimise is False) (idris_optimisation ist) }
193− addIBC (IBCOpt n)
194−
195187-- Get the list of (index, name) of inaccessible arguments from the type.
196188inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
197189inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
198− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
190+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
199191inaccessibleArgs i (PPi plicity n ty t)
200192 | InaccessibleArg `elem` pargopts plicity
201193 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
@@ -918,7 +910,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
918910 checkDocs fc argDocs t_in
919911 addDocStr n doc argDocs
920912 addIBC (IBCDoc n)
921− saveInaccArgs n inacc
913+ fputState (opt_inaccessible . ist_optimisation n) inacc
922914 addIBC (IBCOpt n)
923915 return (n, cty')
924916 where
@@ -953,9 +945,8 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
953945elabClauses info fc opts n_in cs = let n = liftname info n_in in
954946 do ctxt <- getContext
955947 ist <- getIState
956− let inacc = case lookupCtxt n (idris_optimisation ist) of
957− [Optimise inacc _] -> map fst inacc
958− _ -> []
948+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
949+
959950 -- Check n actually exists, with no definition yet
960951 let tys = lookupTy n ctxt
961952 let reflect = Reflection `elem` opts
@@ -975,9 +966,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
975966
976967 solveDeferred n
977968
978− ist <- getIState
979− let opts = addDef n (Optimise [] False) (idris_optimisation ist)
980− in putIState (ist { idris_optimisation = opts })
969+ -- just ensure that the structure exists
970+ fmodifyState (ist_optimisation n) id
981971 addIBC (IBCOpt n)
982972
983973 ist <- getIState
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