@@ -15,8 +15,8 @@ import Debug.Trace
1515-- optimisations
1616
1717forceArgs :: Name -> Type -> Idris ()
18−forceArgs n t = do let fargs = force 0 t
19− i <- getIState
18+forceArgs n t = do i <- getIState
19+ let fargs = force i 0 t
2020 copt <- case lookupCtxt Nothing n (idris_optimisation i) of
2121 [] -> return $ Optimise False [] []
2222 (op:_) -> return op
@@ -26,13 +26,22 @@ forceArgs n t = do let fargs = force 0 t
2626 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++
2727 show t
2828 where
29− force :: Int -> Term -> [Int]
30− force i (Bind _ (Pi _) sc)
31− = force (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc
32− force _ sc@(App f a)
29+ force :: IState -> Int -> Term -> [Int]
30+ force ist i (Bind _ (Pi ty) sc)
31+ | collapsibleIn ist ty
32+ = nub $ i : (force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc)
33+ | otherwise = force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc
34+ force _ _ sc@(App f a)
3335 | (_, args) <- unApply sc
3436 = nub $ concatMap guarded args
35− force _ _ = []
37+ force _ _ _ = []
38+
39+ collapsibleIn i t
40+ | (P _ tn _, _) <- unApply t
41+ = case lookupCtxt Nothing tn (idris_optimisation i) of
42+ [oi] -> collapsible oi
43+ _ -> False
44+ | otherwise = False
3645
3746 isF (P _ (MN force "?") _) = Just force
3847 isF _ = Nothing
@@ -49,24 +58,98 @@ forceArgs n t = do let fargs = force 0 t
4958
5059collapseCons :: Name -> [(Name, Type)] -> Idris ()
5160collapseCons ty cons =
52− do i <- getIState
53− return ()
61+ do i <- getIState
62+ let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
63+ allFR <- mapM (forceRec i) cons'
64+ if and allFR then detaggable (map getRetTy (map snd cons))
65+ else return () -- not collapsible as not detaggable
66+ where
67+ setCollapsible :: Name -> Idris ()
68+ setCollapsible n
69+ = do i <- getIState
70+ iLOG $ show n ++ " collapsible"
71+ case lookupCtxt Nothing n (idris_optimisation i) of
72+ (oi:_) -> do let oi' = oi { collapsible = True }
73+ let opts = addDef n oi' (idris_optimisation i)
74+ putIState (i { idris_optimisation = opts })
75+ [] -> do let oi = Optimise True [] []
76+ let opts = addDef n oi (idris_optimisation i)
77+ putIState (i { idris_optimisation = opts })
78+ addIBC (IBCOpt n)
79+
80+ forceRec :: IState -> (Name, [Type]) -> Idris Bool
81+ forceRec i (n, ts)
82+ = case lookupCtxt Nothing n (idris_optimisation i) of
83+ (oi:_) -> checkFR (forceable oi) 0 ts
84+ _ -> return False
85+ checkFR fs i [] = return True
86+ checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
87+ checkFR fs i (t : xs)
88+ -- must be recursive or type is not collapsible
89+ = do let rt = getRetTy t
90+ if (ty `elem` freeNames rt)
91+ then checkFR fs (i+1) xs
92+ else return False
93+
94+ detaggable :: [Type] -> Idris ()
95+ detaggable rtys
96+ = do let rtyArgs = map (snd . unApply) rtys
97+ -- if every rtyArgs is disjoint with every other, it's detaggable,
98+ -- therefore also collapsible given forceable/recursive check
99+ if disjoint rtyArgs
100+ then mapM_ setCollapsible (ty : map fst cons)
101+ else return ()
102+
103+ disjoint :: [[Term]] -> Bool
104+ disjoint [] = True
105+ disjoint [x] = True
106+ disjoint (x : xs) = anyDisjoint x xs && disjoint xs
107+
108+ anyDisjoint x [] = True
109+ anyDisjoint x (y : ys) = disjointCons x y
110+
111+ disjointCons [] [] = False
112+ disjointCons [] y = False
113+ disjointCons x [] = False
114+ disjointCons (x : xs) (y : ys)
115+ = disjointCon x y || disjointCons xs ys
116+
117+ disjointCon x y = let (cx, _) = unApply x
118+ (cy, _) = unApply y in
119+ case (cx, cy) of
120+ (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
121+ _ -> False
54122
55123class Optimisable term where
56124 applyOpts :: term -> Idris term
125+ stripCollapsed :: term -> Idris term
57126
58127instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
59128 applyOpts (x, y) = do x' <- applyOpts x
60129 y' <- applyOpts y
61130 return (x', y')
131+ stripCollapsed (x, y) = do x' <- stripCollapsed x
132+ y' <- stripCollapsed y
133+ return (x', y')
134+
62135
63136instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
64137 applyOpts (v, x, y) = do x' <- applyOpts x
65138 y' <- applyOpts y
66139 return (v, x', y')
140+ stripCollapsed (v, x, y) = do x' <- stripCollapsed x
141+ y' <- stripCollapsed y
142+ return (v, x', y')
67143
68144instance Optimisable a => Optimisable [a] where
69145 applyOpts = mapM applyOpts
146+ stripCollapsed = mapM stripCollapsed
147+
148+instance Optimisable a => Optimisable (Either a (a, a)) where
149+ applyOpts (Left t) = do t' <- applyOpts t; return $ Left t'
150+ applyOpts (Right t) = do t' <- applyOpts t; return $ Right t'
151+ stripCollapsed (Left t) = do t' <- stripCollapsed t; return $ Left t'
152+ stripCollapsed (Right t) = do t' <- stripCollapsed t; return $ Right t'
70153
71154-- Raw is for compile time optimisation (before type checking)
72155-- Term is for run time optimisation (after type checking, collapsing allowed)
@@ -90,12 +173,19 @@ instance Optimisable Raw where
90173 applyOpts (RForce t) = applyOpts t
91174 applyOpts t = return t
92175
176+ stripCollapsed t = return t
177+
93178instance Optimisable t => Optimisable (Binder t) where
94179 applyOpts (Let t v) = do t' <- applyOpts t
95180 v' <- applyOpts v
96181 return (Let t' v')
97182 applyOpts b = do t' <- applyOpts (binderTy b)
98183 return (b { binderTy = t' })
184+ stripCollapsed (Let t v) = do t' <- stripCollapsed t
185+ v' <- stripCollapsed v
186+ return (Let t' v')
187+ stripCollapsed b = do t' <- stripCollapsed (binderTy b)
188+ return (b { binderTy = t' })
99189
100190
101191applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
@@ -110,6 +200,11 @@ applyDataOpt oi n args
110200-- Run-time: do everything
111201
112202instance Optimisable (TT Name) where
203+ applyOpts c@(P (DCon t arity) n _)
204+ = do i <- getIState
205+ case lookupCtxt Nothing n (idris_optimisation i) of
206+ (oi:_) -> return $ applyDataOptRT oi n t arity []
207+ _ -> return c
113208 applyOpts t@(App f a)
114209 | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE
115210 = do args' <- mapM applyOpts args
@@ -123,8 +218,25 @@ instance Optimisable (TT Name) where
123218 applyOpts (Bind n b t) = do b' <- applyOpts b
124219 t' <- applyOpts t
125220 return (Bind n b' t')
221+ applyOpts (Proj t i) = do t' <- applyOpts t
222+ return (Proj t' i)
126223 applyOpts t = return t
127224
225+ stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x
226+ = do i <- getIState
227+ case lookupCtxt Nothing ty (idris_optimisation i) of
228+ [oi] -> if collapsible oi
229+ then do t' <- stripCollapsed t
230+ return (Bind n (PVar x) (instantiate Erased t'))
231+ else do t' <- stripCollapsed t
232+ return (Bind n (PVar x) t')
233+ _ -> do t' <- stripCollapsed t
234+ return (Bind n (PVar x) t')
235+ stripCollapsed (Bind n (PVar x) t)
236+ = do t' <- stripCollapsed t
237+ return (Bind n (PVar x) t')
238+ stripCollapsed t = return t
239+
128240-- Need to saturate arguments first to ensure that erasure happens uniformly
129241
130242applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
@@ -148,3 +260,4 @@ applyDataOptRT oi n tag arity args
148260
149261 keep (forced, _) = not forced
150262
263+