git.iko.soy/Idris-dev
on master help sign in
Remove collapsibility and forceability altogether.
eedf489Matus Tejiscak
src/Idris/AbsSyntaxTree.hs+1−17
compare with master
unifiedsplit
@@ -833,23 +833,7 @@ data TIData = TIPartial -- ^ a function with a partially defined type
833 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
833 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
834 deriving Show
834 deriving Show
835
835
836−-- An argument is conditionally forceable iff its forceability
837−-- depends on the collapsibility of the whole type.
838−data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)
839−
840−{-!
841−deriving instance Binary Forceability
842−deriving instance NFData Forceability
843−!-}
844−
845−data OptInfo = Optimise { collapsible :: Bool,
846− isnewtype :: Bool,
847− -- The following should actually be (IntMap Forceability)
848− -- but the corresponding Binary instance seems to be broken.
849− -- Let's store a list and convert it to IntMap whenever needed.
850− forceable :: [(Int, Forceability)],
851− recursive :: [Int],
852− inaccessible :: [(Int,Name)], -- names for error reporting
836+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
853 detaggable :: Bool }
837 detaggable :: Bool }
854 deriving Show
838 deriving Show
855{-!
839{-!
src/Idris/DataOpts.hs+14−231
@@ -9,224 +9,48 @@ import Idris.AbsSyntaxTree
9import Idris.Core.TT
9import Idris.Core.TT
10
10
11import Control.Applicative
11import Control.Applicative
12−import qualified Data.IntMap as M
13import Data.List
12import Data.List
14import Data.Maybe
13import Data.Maybe
15import Debug.Trace
14import Debug.Trace
16
15
17−type ForceMap = M.IntMap Forceability
18−
19−-- Calculate the forceable arguments to a constructor
20−-- and update the set of optimisations.
21−forceArgs :: Name -> Name -> [Int] -> Type -> Idris ()
22−forceArgs typeName n expforce t = do
23− ist <- getIState
24− let fargs = getForcedArgs ist typeName t
25− copt = case lookupCtxt n (idris_optimisation ist) of
26− [] -> Optimise False False [] [] [] False
27− op:_ -> op
28− opts = addDef n (copt { forceable = M.toList fargs ++
29− zip expforce (repeat Unconditional) })
30− (idris_optimisation ist)
31− putIState (ist { idris_optimisation = opts })
32− addIBC (IBCOpt n)
33− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t
34−
35−getForcedArgs :: IState -> Name -> Type -> ForceMap
36−getForcedArgs ist typeName t = M.empty -- addCollapsibleArgs 0 t $ forcedInTarget 0 t
37− where
38− maxUnion = M.unionWith max
39−
40− -- Label all occurrences of the variable bound in Pi in the rest of
41− -- the term with the number i so that we can recognize them anytime later.
42− label i = instantiate $ P Bound (sMN i "ctor_arg") Erased
43−
44− addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap
45− addCollapsibleArgs i (Bind vn (Pi ty) rest) alreadyForceable
46− = addCollapsibleArgs (i+1) (label i rest) (forceable $ unApply ty)
47− where
48− -- forceable takes an un-applied type of a ctor argument
49− forceable (P _ tn _, args)
50− -- if `ty' is collapsible, the argument is unconditionally forceable
51− | isCollapsible tn
52− = M.insert i Unconditional alreadyForceable
53−
54− -- a recursive occurrence with known indices is conditionally forceable
55− | tn == typeName
56− = M.insertWith max i Conditional alreadyForceable
57−
58− forceable _ = alreadyForceable
59−
60− isCollapsible :: Name -> Bool
61− isCollapsible n = case lookupCtxt n (idris_optimisation ist) of
62− [oi] -> collapsible oi
63− _ -> False
64−
65− addCollapsibleArgs _ _ fs = fs
66−
67− forcedInTarget :: Int -> Type -> ForceMap
68− forcedInTarget i (Bind _ (Pi _) rest) = forcedInTarget (i+1) (label i rest)
69− forcedInTarget i t@(App f a) | (_, as) <- unApply t = unionMap guardedArgs as
70− forcedInTarget _ _ = M.empty
71−
72− guardedArgs :: Term -> ForceMap
73− guardedArgs t@(App f a) | (P (DCon _ _) _ _, args) <- unApply t
74− = unionMap bareArg args `maxUnion` unionMap guardedArgs args
75− guardedArgs t = bareArg t
76−
77− bareArg :: Term -> ForceMap
78− bareArg (P _ (MN i ctor_arg) _)
79− | ctor_arg == txt "ctor_arg" = M.singleton i Unconditional
80− bareArg _ = M.empty
81−
82− unionMap :: (a -> ForceMap) -> [a] -> ForceMap
83− unionMap f = M.unionsWith max . map f
84−
85−-- Calculate whether a collection of constructors is collapsible
86−-- and update the state accordingly.
87−collapseCons :: Name -> [(Name, Type)] -> Idris ()
88−collapseCons tn ctors = do
89− ist <- getIState
90− case ctors of
91− _
92− | all (ctorCollapsible ist) ctors
93− , disjointTerms ctorTargetArgs
94− -> return () -- mapM_ setCollapsible (tn : map fst ctors)
95−
96− [(cn, ct)]
97− -> checkNewType ist cn ct
98−
99− _ -> return () -- nothing can be done
100− where
101− ctorTargetArgs = map (snd . unApply . getRetTy . snd) ctors
102−
103− ctorArity :: Type -> Int
104− ctorArity = length . getArgTys
105−
106− ctorCollapsible :: IState -> (Name, Type) -> Bool
107− ctorCollapsible ist (n, t) = all (`M.member` forceMap) [0 .. ctorArity t - 1]
108− where
109− forceMap = case lookupCtxt n (idris_optimisation ist) of
110− oi:_ -> M.fromList $ forceable oi
111− _ -> M.empty
112−
113− -- one constructor; if one remaining argument, treat as newtype
114− checkNewType :: IState -> Name -> Type -> Idris ()
115− checkNewType ist cn ct
116− | oi:_ <- lookupCtxt cn opt
117− , length (getArgTys ct) == 1 + forcedCnt (M.fromList $ forceable oi)
118− = putIState ist{ idris_optimisation = opt' oi }
119− | otherwise = return ()
120− where
121− opt = idris_optimisation ist
122− opt' oi = addDef cn oi{ isnewtype = True } opt
123−
124− setCollapsible :: Name -> Idris ()
125− setCollapsible n
126− = do i <- getIState
127− iLOG $ show n ++ " collapsible"
128− case lookupCtxt n (idris_optimisation i) of
129− (oi:_) -> do let oi' = oi { collapsible = True }
130− let opts = addDef n oi' (idris_optimisation i)
131− putIState (i { idris_optimisation = opts })
132− [] -> do let oi = Optimise True False [] [] [] False
133− let opts = addDef n oi (idris_optimisation i)
134− putIState (i { idris_optimisation = opts })
135− addIBC (IBCOpt n)
136−
137− disjointTerms :: [[Term]] -> Bool
138− disjointTerms [] = True
139− disjointTerms [xs] = True
140− disjointTerms (xs : xss) =
141− -- xs is disjoint with every pattern from xss
142− all (or . zipWith disjoint xs) xss
143− -- and xss is pairwise disjoint, too
144− && disjointTerms xss
145−
146− -- Return True if the two patterns are provably disjoint.
147− -- Return False if they're not or if unsure.
148− disjoint :: Term -> Term -> Bool
149− disjoint x y = case (cx, cy) of
150− -- data constructors -> compare their names
151− (P (DCon _ _) nx _, P (DCon _ _) ny _)
152− | nx /= ny -> True
153− | otherwise -> or $ zipWith disjoint xargs yargs
154− _ -> False
155− where
156− (cx, xargs) = unApply x
157− (cy, yargs) = unApply y
158−
159class Optimisable term where
16class Optimisable term where
160 applyOpts :: term -> Idris term
17 applyOpts :: term -> Idris term
161− stripCollapsed :: term -> Idris term
162
18
163instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
19instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
164 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
20 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
165− stripCollapsed (x, y) = (,) <$> stripCollapsed x <*> stripCollapsed y
166
21
167instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
22instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
168 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
23 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
169− stripCollapsed (v, x, y) = (,,) v <$> stripCollapsed x <*> stripCollapsed y
170
24
171instance Optimisable a => Optimisable [a] where
25instance Optimisable a => Optimisable [a] where
172 applyOpts = mapM applyOpts
26 applyOpts = mapM applyOpts
173− stripCollapsed = mapM stripCollapsed
174
27
175instance Optimisable a => Optimisable (Either a (a, a)) where
28instance Optimisable a => Optimisable (Either a (a, a)) where
176 applyOpts (Left t) = Left <$> applyOpts t
29 applyOpts (Left t) = Left <$> applyOpts t
177 applyOpts (Right t) = Right <$> applyOpts t
30 applyOpts (Right t) = Right <$> applyOpts t
178− stripCollapsed (Left t) = Left <$> stripCollapsed t
179− stripCollapsed (Right t) = Right <$> stripCollapsed t
180
31
181-- Raw is for compile time optimisation (before type checking)
32-- Raw is for compile time optimisation (before type checking)
182-- Term is for run time optimisation (after type checking, collapsing allowed)
33-- Term is for run time optimisation (after type checking, collapsing allowed)
183−
184-- Compile time: no collapsing
34-- Compile time: no collapsing
185
35
186instance Optimisable Raw where
36instance Optimisable Raw where
187 applyOpts t@(RApp f a)
37 applyOpts t@(RApp f a)
188 | (Var n, args) <- raw_unapply t -- MAGIC HERE
38 | (Var n, args) <- raw_unapply t -- MAGIC HERE
189− = do args' <- mapM applyOpts args
39+ = raw_apply (Var n) <$> mapM applyOpts args
190− i <- getIState
191− return $ case lookupCtxt n (idris_optimisation i) of
192− oi:_ -> applyDataOpt oi n args'
193− _ -> raw_apply (Var n) args'
194 | otherwise = RApp <$> applyOpts f <*> applyOpts a
40 | otherwise = RApp <$> applyOpts f <*> applyOpts a
195
41
196 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
42 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
197 applyOpts (RForce t) = applyOpts t
43 applyOpts (RForce t) = applyOpts t
198 applyOpts t = return t
44 applyOpts t = return t
199
45
200− stripCollapsed t = return t
201−
202-- Erase types (makes ibc smaller, and we don't need them)
46-- Erase types (makes ibc smaller, and we don't need them)
203instance Optimisable (Binder (TT Name)) where
47instance Optimisable (Binder (TT Name)) where
204 applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v
48 applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v
205 applyOpts b = return (b { binderTy = Erased })
49 applyOpts b = return (b { binderTy = Erased })
206− stripCollapsed (Let t v) = Let <$> return Erased <*> stripCollapsed v
207− stripCollapsed b = return (b { binderTy = Erased })
208
50
209instance Optimisable (Binder Raw) where
51instance Optimisable (Binder Raw) where
210 applyOpts b = do t' <- applyOpts (binderTy b)
52 applyOpts b = do t' <- applyOpts (binderTy b)
211 return (b { binderTy = t' })
53 return (b { binderTy = t' })
212− stripCollapsed (Let t v) = Let <$> stripCollapsed t <*> stripCollapsed v
213− stripCollapsed b = do t' <- stripCollapsed (binderTy b)
214− return (b { binderTy = t' })
215−
216−forcedArgSeq :: OptInfo -> [Maybe Forceability]
217−forcedArgSeq oi = map (\i -> M.lookup i forceMap) [0..]
218− where
219− forceMap = M.fromList $ forceable oi
220−
221−forcedCnt :: ForceMap -> Int
222−forcedCnt = length . filter (== Unconditional) . M.elems
223−
224−applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
225−applyDataOpt oi n args
226− = raw_apply (Var n) $ zipWith doForce (forcedArgSeq oi) args
227− where
228− doForce (Just Unconditional) a = RForce a
229− doForce _ a = a
230
54
231-- Run-time: do everything
55-- Run-time: do everything
232
56
@@ -249,54 +73,22 @@ instance Optimisable (TT Name) where
249 | fn == txt "toIntegerNat" && mod == prel
73 | fn == txt "toIntegerNat" && mod == prel
250 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)
74 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)
251 applyOpts c@(P (DCon t arity) n _)
75 applyOpts c@(P (DCon t arity) n _)
252− = do i <- getIState
253− case lookupCtxt n (idris_optimisation i) of
254− (oi:_) -> return $ applyDataOptRT oi n t arity []
76+ = return $ applyDataOptRT n t arity []
255− _ -> return c
256 applyOpts t@(App f a)
77 applyOpts t@(App f a)
257 | (c@(P (DCon t arity) n _), args) <- unApply t
78 | (c@(P (DCon t arity) n _), args) <- unApply t
258− = do args' <- mapM applyOpts args
259− i <- getIState
260− case lookupCtxt n (idris_optimisation i) of
261− (oi:_) -> do return $ applyDataOptRT oi n t arity args'
79+ = applyDataOptRT n t arity <$> mapM applyOpts args
262− _ -> return (mkApp c args')
80+ | otherwise = App <$> applyOpts f <*> applyOpts a
263− | otherwise = do f' <- applyOpts f
264− a' <- applyOpts a
265− return (App f' a')
266− applyOpts (Bind n b t) = do b' <- applyOpts b
81+ applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t
267− t' <- applyOpts t
268− return (Bind n b' t')
269− applyOpts (Proj t i) = do t' <- applyOpts t
82+ applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i
270− return (Proj t' i)
271 applyOpts t = return t
83 applyOpts t = return t
272
84
273− stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x
274− = do i <- getIState
275− -- NOTE: This assumes that 'ty' is in normal form, which it
276− -- has to be before now because we're not keeping track of
277− -- an environment so we can't do it here.
278− case lookupCtxt ty (idris_optimisation i) of
279− [oi] -> if collapsible oi
280− then do t' <- stripCollapsed t
281− return (Bind n (PVar x) (instantiate Erased t'))
282− else do t' <- stripCollapsed t
283− return (Bind n (PVar x) t')
284− _ -> do t' <- stripCollapsed t
285− return (Bind n (PVar x) t')
286− stripCollapsed (Bind n (PVar x) t)
287− = do t' <- stripCollapsed t
288− return (Bind n (PVar x) t')
289− stripCollapsed t = return t
290−
291−-- Need to saturate arguments first to ensure that erasure happens uniformly
85+-- Need to saturate arguments first to ensure that optimisation happens uniformly
292−
293−applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
86+applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term
294−applyDataOptRT oi n tag arity args
87+applyDataOptRT n tag arity args
295− | length args == arity = doOpts n args (collapsible oi) (M.fromList $ forceable oi)
88+ | length args == arity = doOpts n args
296 | otherwise = let extra = satArgs (arity - length args)
89 | otherwise = let extra = satArgs (arity - length args)
297 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
90 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
298− (collapsible oi) (M.fromList $ forceable oi) in
299− bind extra tm
91+ in bind extra tm
300 where
92 where
301 satArgs n = map (\i -> sMN i "sat") [1..n]
93 satArgs n = map (\i -> sMN i "sat") [1..n]
302
94
@@ -305,20 +97,11 @@ applyDataOptRT oi n tag arity args
305
97
306 -- Nat special cases
98 -- Nat special cases
307 -- TODO: Would be nice if this was configurable in idris source!
99 -- TODO: Would be nice if this was configurable in idris source!
308− doOpts (NS (UN z) [nat, prelude]) [] _ _
100+ doOpts (NS (UN z) [nat, prelude]) []
309 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
101 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
310 = Constant (BI 0)
102 = Constant (BI 0)
311− doOpts (NS (UN s) [nat, prelude]) [k] _ _
103+ doOpts (NS (UN s) [nat, prelude]) [k]
312 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"
104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"
313 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
314
106
315− doOpts n args True _ = Erased
316− doOpts n args _ forceMap
317− | isnewtype oi = case args' of
318− [val] -> val
319− _ -> error $ "Can't happen (newtype not a singleton): " ++ show args'
320− | otherwise = mkApp ctor' args'
321− where
322− ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)
107+ doOpts n args = mkApp (P (DCon tag arity) n Erased) args
323− args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]
324−
src/Idris/DeepSeq.hs+2−6
@@ -50,10 +50,6 @@ instance NFData CT.NumWrapper where
50
50
51-- All generated by 'derive'
51-- All generated by 'derive'
52
52
53−instance NFData Forceability where
54− rnf Conditional = ()
55− rnf Unconditional = ()
56−
57instance NFData IntTy where
53instance NFData IntTy where
58 rnf (ITFixed x1) = rnf x1 `seq` ()
54 rnf (ITFixed x1) = rnf x1 `seq` ()
59 rnf ITNative = ()
55 rnf ITNative = ()
@@ -290,8 +286,8 @@ instance NFData ClassInfo where
290 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
286 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
291
287
292instance NFData OptInfo where
288instance NFData OptInfo where
293− rnf (Optimise x1 x2 x3 x4 x5 x6)
289+ rnf (Optimise x1 x2)
294− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
290+ = rnf x1 `seq` rnf x2 `seq` ()
295
291
296instance NFData TypeInfo where
292instance NFData TypeInfo where
297 rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
293 rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
src/Idris/ElabDecls.hs+18−67
@@ -189,7 +189,7 @@ saveInaccArgs n is = do
189
189
190 _ -> do
190 _ -> do
191 putIState ist{ idris_optimisation =
191 putIState ist{ idris_optimisation =
192− addDef n (Optimise False False [] [] is False) (idris_optimisation ist) }
192+ addDef n (Optimise is False) (idris_optimisation ist) }
193 addIBC (IBCOpt n)
193 addIBC (IBCOpt n)
194
194
195-- Get the list of (index, name) of inaccessible arguments from the type.
195-- Get the list of (index, name) of inaccessible arguments from the type.
@@ -212,29 +212,6 @@ elabPostulate info syn doc fc opts n ty = do
212 -- remove it from the deferred definitions list
212 -- remove it from the deferred definitions list
213 solveDeferred n
213 solveDeferred n
214
214
215−{- NB. this check has been superseded by usage analysis
216− -
217− -- make sure it's collapsible, so it is never needed at run time
218− -- start by getting the elaborated type
219− ctxt <- getContext
220− fty <- case lookupTy n ctxt of
221− [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
222− [ty] -> return ty
223− ist <- getIState
224− let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
225−
226− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
227− let postOK = case ap of
228− P _ tn _ -> case lookupCtxt tn
229− (idris_optimisation ist) of
230− [oi] -> collapsible oi
231− _ -> False
232− _ -> False
233− when (not postOK)
234− $ tclift $ tfail (At fc (NonCollapsiblePostulate n))
235−-}
236−
237−
238elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
215elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
239elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
216elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
240 = do let codata = Codata `elem` opts
217 = do let codata = Codata `elem` opts
@@ -296,12 +273,12 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
296 let metainf = DataMI params
273 let metainf = DataMI params
297 addIBC (IBCMetaInformation n metainf)
274 addIBC (IBCMetaInformation n metainf)
298 -- TMP HACK! Make this a data option
275 -- TMP HACK! Make this a data option
299− when (n /= sUN "Lazy'") $ collapseCons n cons
300 updateContext (addDatatype (Data n ttag cty cons))
276 updateContext (addDatatype (Data n ttag cty cons))
301 updateContext (setMetaInformation n metainf)
277 updateContext (setMetaInformation n metainf)
302 mapM_ (checkPositive n) cons
278 mapM_ (checkPositive n) cons
303
279
304− -- if there's exactly one constructor, mark both the type and the constructor
280+ -- if there's exactly one constructor,
281+ -- mark both the type and the constructor as detaggable
305 case cons of
282 case cons of
306 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
283 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
307 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
284 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
@@ -317,7 +294,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
317 let opt = idris_optimisation ist
294 let opt = idris_optimisation ist
318 case lookupCtxt n opt of
295 case lookupCtxt n opt of
319 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
296 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
320− _ -> putIState ist{ idris_optimisation = addDef n (Optimise False False [] [] [] True) opt }
297+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
321
298
322 checkDefinedAs fc n t ctxt
299 checkDefinedAs fc n t ctxt
323 = case lookupDef n ctxt of
300 = case lookupDef n ctxt of
@@ -907,6 +884,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
907 (map pexp rhsArgs)) []
884 (map pexp rhsArgs)) []
908 return (pn, pfnTy, PClauses fc [] setname [pclause])
885 return (pn, pfnTy, PClauses fc [] setname [pclause])
909
886
887+-- FIXME: 'forcenames' is an almighty hack! Need a better way of
888+-- erasing non-forceable things
889+-- ^^^
890+-- TODO: the above is a comment from the past;
891+-- forcenames is probably no longer needed
910elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
892elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
911 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
893 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
912elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
894elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
@@ -937,10 +919,6 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
937 addIBC (IBCDoc n)
919 addIBC (IBCDoc n)
938 saveInaccArgs n inacc
920 saveInaccArgs n inacc
939 addIBC (IBCOpt n)
921 addIBC (IBCOpt n)
940− let fs = map (getNamePos 0 t) forcenames
941− -- FIXME: 'forcenames' is an almighty hack! Need a better way of
942− -- erasing non-forceable things
943− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
944 return (n, cty')
922 return (n, cty')
945 where
923 where
946 tyIs (Bind n b sc) = tyIs sc
924 tyIs (Bind n b sc) = tyIs sc
@@ -975,7 +953,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
975 do ctxt <- getContext
953 do ctxt <- getContext
976 ist <- getIState
954 ist <- getIState
977 let inacc = case lookupCtxt n (idris_optimisation ist) of
955 let inacc = case lookupCtxt n (idris_optimisation ist) of
978− [Optimise _ _ _ _ inacc _] -> map fst inacc
956+ [Optimise inacc _] -> map fst inacc
979 _ -> []
957 _ -> []
980 -- Check n actually exists, with no definition yet
958 -- Check n actually exists, with no definition yet
981 let tys = lookupTy n ctxt
959 let tys = lookupTy n ctxt
@@ -994,29 +972,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
994
972
995 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
973 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
996
974
997− -- if the return type of 'ty' is collapsible, the optimised version should
998− -- just do nothing
999− ist <- getIState
1000− let (ap, _) = unApply (getRetTy fty)
1001− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
1002− -- FIXME: Really ought to only do this for total functions!
1003− let doNothing = case ap of
1004− P _ tn _ -> case lookupCtxt tn
1005− (idris_optimisation ist) of
1006− [oi] -> collapsible oi
1007− _ -> False
1008− _ -> False
1009 solveDeferred n
975 solveDeferred n
976+
1010 ist <- getIState
977 ist <- getIState
1011− when doNothing $
1012− case lookupCtxt n (idris_optimisation ist) of
1013− [oi] -> do let opts = addDef n (oi { collapsible = True })
1014− (idris_optimisation ist)
1015− putIState (ist { idris_optimisation = opts })
1016− _ -> do let opts = addDef n (Optimise True False [] [] [] False)
978+ let opts = addDef n (Optimise [] False) (idris_optimisation ist)
1017− (idris_optimisation ist)
1018− putIState (ist { idris_optimisation = opts })
979+ in putIState (ist { idris_optimisation = opts })
1019− addIBC (IBCOpt n)
980+ addIBC (IBCOpt n)
981+
1020 ist <- getIState
982 ist <- getIState
1021 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
983 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
1022
984
@@ -1026,11 +988,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1026 let tcase = opt_typecase (idris_options ist)
988 let tcase = opt_typecase (idris_options ist)
1027
989
1028 -- Summary of what's about to happen: Definitions go:
990 -- Summary of what's about to happen: Definitions go:
1029−
991+ --
1030− -- pats_in -> pats -> optpats
992+ -- pats_in -> pats -> pdef -> pdef'
1031− -- pdef comes from pats,
1032− -- optpdef comes from optpats
1033− -- Then pdef' is optpdef with forcing/collapsing applied everywhere
1034
993
1035 -- addCaseDef builds case trees from <pdef> and <pdef'>
994 -- addCaseDef builds case trees from <pdef> and <pdef'>
1036
995
@@ -1059,18 +1018,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1059
1018
1060 numArgs <- tclift $ sameLength pdef
1019 numArgs <- tclift $ sameLength pdef
1061
1020
1062− -- patterns after collapsing optimisation applied
1063− -- (i.e. check if the function should do nothing at run time)
1064− optpats <- if doNothing
1065− then return $ [Right (mkApp (P Bound n Erased)
1066− (take numArgs (repeat Erased)), Erased)]
1067− else stripCollapsed pats
1068−
1069 case specNames opts of
1021 case specNames opts of
1070 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
1022 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
1071 _ -> return ()
1023 _ -> return ()
1072
1024
1073− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
1074 tree@(CaseDef scargs sc _) <- tclift $
1025 tree@(CaseDef scargs sc _) <- tclift $
1075 simpleCase tcase False reflect CompileTime fc inacc atys pdef
1026 simpleCase tcase False reflect CompileTime fc inacc atys pdef
1076 cov <- coverage
1027 cov <- coverage
@@ -1094,7 +1045,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1094 let pcover = null pmissing
1045 let pcover = null pmissing
1095
1046
1096 -- pdef' is the version that gets compiled for run-time
1047 -- pdef' is the version that gets compiled for run-time
1097− pdef_in' <- applyOpts optpdef
1048+ pdef_in' <- applyOpts pdef
1098 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1049 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1099
1050
1100 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
1051 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
src/Idris/Erasure.hs+1−1
@@ -128,7 +128,7 @@ performUsageAnalysis = do
128
128
129 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
129 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
130 checkAccessibility opt (n, reachable)
130 checkAccessibility opt (n, reachable)
131− | [Optimise col nt forc rec inaccessible dt] <- lookupCtxt n opt
131+ | [Optimise inaccessible dt] <- lookupCtxt n opt
132 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
132 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
133 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
133 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
134
134
src/Idris/IBC.hs+2−14
@@ -1093,10 +1093,6 @@ safeToEnum label x' = result
1093 = error $ label ++ ": corrupted binary representation in IBC"
1093 = error $ label ++ ": corrupted binary representation in IBC"
1094 | otherwise = toEnum x
1094 | otherwise = toEnum x
1095
1095
1096−instance Binary Forceability where
1097− put = putWord8 . fromIntegral . fromEnum
1098− get = safeToEnum "Forceability" `fmap` getWord8
1099−
1100instance Binary PReason where
1096instance Binary PReason where
1101 put x
1097 put x
1102 = case x of
1098 = case x of
@@ -2100,21 +2096,13 @@ instance Binary ClassInfo where
2100 return (CI x1 x2 x3 x4 x5 [])
2096 return (CI x1 x2 x3 x4 x5 [])
2101
2097
2102instance Binary OptInfo where
2098instance Binary OptInfo where
2103− put (Optimise x1 x2 x3 x4 x5 x6)
2099+ put (Optimise x1 x2)
2104 = do put x1
2100 = do put x1
2105 put x2
2101 put x2
2106− put x3
2107− put x4
2108− put x5
2109− put x6
2110 get
2102 get
2111 = do x1 <- get
2103 = do x1 <- get
2112 x2 <- get
2104 x2 <- get
2113− x3 <- get
2114− x4 <- get
2115− x5 <- get
2116− x6 <- get
2117− return (Optimise x1 x2 x3 x4 x5 x6)
2105+ return (Optimise x1 x2)
2118
2106
2119instance Binary TypeInfo where
2107instance Binary TypeInfo where
2120 put (TI x1 x2 x3 x4) = do put x1
2108 put (TI x1 x2 x3 x4) = do put x1