git.iko.soy/Idris-dev
on master help sign in
Recursive constructor disjointness + cleanup
65c301cMatus Tejiscak
.gitignore+2
compare with master
unifiedsplit
@@ -25,3 +25,5 @@ tutorial/*.out
25tutorial/*.toc
25tutorial/*.toc
26tutorial/*.fdb_latexmk
26tutorial/*.fdb_latexmk
27tutorial/*.fls
27tutorial/*.fls
28+tags
29+TAGS
idris.cabal−1
@@ -395,7 +395,6 @@ Executable idris
395 , haskeline >= 0.7
395 , haskeline >= 0.7
396 , language-java >= 0.2.6
396 , language-java >= 0.2.6
397 , mtl
397 , mtl
398− --, parsec >= 3
399 , parsers == 0.9
398 , parsers == 0.9
400 , pretty
399 , pretty
401 , process
400 , process
src/Core/TT.hs+1
@@ -285,6 +285,7 @@ showCG (SN s) = showCG' s
285 showCG' (MethodN m) = '!':showCG m
285 showCG' (MethodN m) = '!':showCG m
286 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
286 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
287 showCG' (CaseN c) = showCG c ++ "_case"
287 showCG' (CaseN c) = showCG c ++ "_case"
288+ showCG' (ElimN n) = "<<" ++ showCG n ++ ">>"
288showCG NErased = "_"
289showCG NErased = "_"
289
290
290
291
src/Idris/AbsSyntaxTree.hs+13−1
@@ -756,9 +756,21 @@ deriving instance Binary ClassInfo
756deriving instance NFData ClassInfo
756deriving instance NFData ClassInfo
757!-}
757!-}
758
758
759+-- An argument is conditionally forceable iff its forceability
760+-- depends on the collapsibility of the whole type.
761+data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)
762+
763+{-!
764+deriving instance Binary Forceability
765+deriving instance NFData Forceability
766+!-}
767+
759data OptInfo = Optimise { collapsible :: Bool,
768data OptInfo = Optimise { collapsible :: Bool,
760 isnewtype :: Bool,
769 isnewtype :: Bool,
770+ -- The following should actually be (IntMap Forceability)
771+ -- but the corresponding Binary instance seems to be broken.
772+ -- Let's store a list and convert it to IntMap whenever needed.
761− forceable :: [Int], -- argument positions
773+ forceable :: [(Int, Forceability)],
762 recursive :: [Int] }
774 recursive :: [Int] }
763 deriving Show
775 deriving Show
764{-!
776{-!
src/Idris/Coverage.hs−4
@@ -198,10 +198,6 @@ genAll i args
198 = PPair fc (getTm l) (getTm r)
198 = PPair fc (getTm l) (getTm r)
199 resugar t = t
199 resugar t = t
200
200
201− getForceable i n = case lookupCtxt n (idris_optimisation i) of
202− [o] -> forceable o
203− _ -> []
204−
205 dropForce force (x : xs) i | i `elem` force
201 dropForce force (x : xs) i | i `elem` force
206 = upd Placeholder x : dropForce force xs (i + 1)
202 = upd Placeholder x : dropForce force xs (i + 1)
207 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
203 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
src/Idris/DataOpts.hs+160−158
@@ -5,78 +5,118 @@ module Idris.DataOpts where
5-- Forcing, detagging and collapsing
5-- Forcing, detagging and collapsing
6
6
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8+import Idris.AbsSyntaxTree
8import Core.TT
9import Core.TT
9
10
11+import Control.Applicative
12+import qualified Data.IntMap.Strict as M
10import Data.List
13import Data.List
11import Data.Maybe
14import Data.Maybe
12import Debug.Trace
15import Debug.Trace
13
16
17+type ForceMap = M.IntMap Forceability
18+
14−-- Calculate the forceable arguments to a constructor and update the set of
19+-- Calculate the forceable arguments to a constructor
15−-- optimisations
20+-- and update the set of optimisations.
16−
17−forceArgs :: Name -> Type -> Idris ()
21+forceArgs :: Name -> Name -> Type -> Idris ()
18−forceArgs n t = do i <- getIState
22+forceArgs typeName n t = do
19− let fargs = force i 0 t
23+ ist <- getIState
24+ let fargs = getForcedArgs ist typeName t
20− copt <- case lookupCtxt n (idris_optimisation i) of
25+ copt = case lookupCtxt n (idris_optimisation ist) of
21− [] -> return $ Optimise False False [] []
26+ [] -> Optimise False False [] []
22− (op:_) -> return op
27+ op:_ -> op
23− let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)
28+ opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)
24− putIState (i { idris_optimisation = opts })
29+ putIState (ist { idris_optimisation = opts })
25− addIBC (IBCOpt n)
30+ addIBC (IBCOpt n)
26− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++
31+ iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t
27− show t
32+
33+getForcedArgs :: IState -> Name -> Type -> ForceMap
34+getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t
28 where
35 where
29− force :: IState -> Int -> Term -> [Int]
36+ maxUnion = M.unionWith max
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)
35− | (_, args) <- unApply sc
36− = nub $ concatMap guarded args
37− force _ _ _ = []
38−
39− collapsibleIn i t
40− | (P _ tn _, _) <- unApply t
41− = case lookupCtxt tn (idris_optimisation i) of
42− [oi] -> collapsible oi
43− _ -> False
44− | otherwise = False
45−
46− isF (P _ (MN force "?") _) = Just force
47− isF _ = Nothing
48−
49− guarded :: Term -> [Int]
50− guarded t@(App f a)
51−-- | (P (TCon _ _) _ _, args) <- unApply t
52−-- = mapMaybe isF args ++ concatMap guarded args
53− | (P (DCon _ _) _ _, args) <- unApply t
54− = mapMaybe isF args ++ concatMap guarded args
55− guarded t = mapMaybe isF [t]
56
37
57−-- Calculate whether a collection of constructors is collapsible
38+ -- Label all occurrences of the variable bound in Pi in the rest of
39+ -- the term with the number i so that we can recognize them anytime later.
40+ label i = instantiate $ P Bound (MN i "ctor_arg") Erased
41+
42+ addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap
43+ addCollapsibleArgs i (Bind vn (Pi ty) rest) alreadyForceable
44+ = addCollapsibleArgs (i+1) (label i rest) (forceable $ unApply ty)
45+ where
46+ -- forceable takes an un-applied type of a ctor argument
47+ forceable (P _ tn _, args)
48+ -- if `ty' is collapsible, the argument is unconditionally forceable
49+ | isCollapsible tn
50+ = M.insert i Unconditional alreadyForceable
51+
52+ -- a recursive occurrence with known indices is conditionally forceable
53+ | tn == typeName
54+ = M.insertWith max i Conditional alreadyForceable
55+
56+ forceable _ = alreadyForceable
57+
58+ isCollapsible :: Name -> Bool
59+ isCollapsible n = case lookupCtxt n (idris_optimisation ist) of
60+ [oi] -> collapsible oi
61+ _ -> False
62+
63+ addCollapsibleArgs _ _ fs = fs
58
64
65+ forcedInTarget :: Int -> Type -> ForceMap
66+ forcedInTarget i (Bind _ (Pi _) rest) = forcedInTarget (i+1) (label i rest)
67+ forcedInTarget i t@(App f a) | (_, as) <- unApply t = unionMap guardedArgs as
68+ forcedInTarget _ _ = M.empty
69+
70+ guardedArgs :: Term -> ForceMap
71+ guardedArgs t@(App f a) | (P (DCon _ _) _ _, args) <- unApply t
72+ = unionMap bareArg args `maxUnion` unionMap guardedArgs args
73+ guardedArgs t = bareArg t
74+
75+ bareArg :: Term -> ForceMap
76+ bareArg (P _ (MN i "ctor_arg") _) = M.singleton i Unconditional
77+ bareArg _ = M.empty
78+
79+ unionMap :: (a -> ForceMap) -> [a] -> ForceMap
80+ unionMap f = M.unionsWith max . map f
81+
82+-- Calculate whether a collection of constructors is collapsible
83+-- and update the state accordingly.
59collapseCons :: Name -> [(Name, Type)] -> Idris ()
84collapseCons :: Name -> [(Name, Type)] -> Idris ()
60−collapseCons ty cons =
85+collapseCons tn ctors = do
61− do i <- getIState
86+ ist <- getIState
62− let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
87+ case ctors of
63− allFR <- mapM (forceRec i) cons'
88+ _
64− if and allFR then detaggable (map getRetTy (map snd cons))
89+ | all (ctorCollapsible ist) ctors
90+ , disjointTerms ctorTargetArgs
91+ -> mapM_ setCollapsible (tn : map fst ctors)
92+
93+ [(cn, ct)]
65− else checkNewType cons'
94+ -> checkNewType ist cn ct
95+
96+ _ -> return () -- nothing can be done
66 where
97 where
98+ ctorTargetArgs = map (snd . unApply . getRetTy . snd) ctors
99+
100+ ctorArity :: Type -> Int
101+ ctorArity = length . getArgTys
102+
103+ ctorCollapsible :: IState -> (Name, Type) -> Bool
104+ ctorCollapsible ist (n, t) = all (`M.member` forceMap) [0 .. ctorArity t - 1]
105+ where
106+ forceMap = case lookupCtxt n (idris_optimisation ist) of
107+ oi:_ -> M.fromList $ forceable oi
108+ _ -> M.empty
109+
67 -- one constructor; if one remaining argument, treat as newtype
110 -- one constructor; if one remaining argument, treat as newtype
68− checkNewType [(n, ts)] = do
111+ checkNewType :: IState -> Name -> Type -> Idris ()
69− i <- getIState
112+ checkNewType ist cn ct
70− case lookupCtxt n (idris_optimisation i) of
113+ | oi:_ <- lookupCtxt cn opt
71− (oi:_) -> do let remaining = length ts - length (forceable oi)
114+ , length (getArgTys ct) == 1 + forcedCnt (M.fromList $ forceable oi)
72− if remaining == 1 then
115+ = putIState ist{ idris_optimisation = opt' oi }
116+ | otherwise = return ()
117+ where
118+ opt = idris_optimisation ist
73− do let oi' = oi { isnewtype = True }
119+ opt' oi = addDef cn oi{ isnewtype = True } opt
74− let opts = addDef n oi' (idris_optimisation i)
75− putIState (i { idris_optimisation = opts })
76− else return ()
77− _ -> return ()
78−
79− checkNewType _ = return ()
80
120
81 setCollapsible :: Name -> Idris ()
121 setCollapsible :: Name -> Idris ()
82 setCollapsible n
122 setCollapsible n
@@ -91,79 +131,49 @@ collapseCons ty cons =
91 putIState (i { idris_optimisation = opts })
131 putIState (i { idris_optimisation = opts })
92 addIBC (IBCOpt n)
132 addIBC (IBCOpt n)
93
133
94− forceRec :: IState -> (Name, [Type]) -> Idris Bool
134+ disjointTerms :: [[Term]] -> Bool
95− forceRec i (n, ts)
135+ disjointTerms [] = True
96− = case lookupCtxt n (idris_optimisation i) of
136+ disjointTerms [xs] = True
97− (oi:_) -> checkFR (forceable oi) 0 ts
137+ disjointTerms (xs : xss) =
98− _ -> return False
99− checkFR fs i [] = return True
100− checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
101− checkFR fs i (t : xs)
102− -- must be recursive or type is not collapsible
103− = do let (rtf, rta) = unApply $ getRetTy t
104− if (ty `elem` freeNames rtf)
105− then checkFR fs (i+1) xs
106− else return False
107−
108− detaggable :: [Type] -> Idris ()
109− detaggable rtys
110− = do let rtyArgs = map (snd . unApply) rtys
111− -- if every rtyArgs is disjoint with every other, it's detaggable,
138+ -- xs is disjoint with every pattern from xss
112− -- therefore also collapsible given forceable/recursive check
139+ all (or . zipWith disjoint xs) xss
113− if disjoint rtyArgs
114− then mapM_ setCollapsible (ty : map fst cons)
115− else return ()
116−
117− disjoint :: [[Term]] -> Bool
118− disjoint [] = True
119− disjoint [x] = True
140+ -- and xss is pairwise disjoint, too
120− disjoint (x : xs) = anyDisjoint x xs && disjoint xs
141+ && disjointTerms xss
121−
142+
122− anyDisjoint x [] = True
143+ -- Return True if the two patterns are provably disjoint.
123− anyDisjoint x (y : ys) = disjointCons x y
144+ -- Return False if they're not or if unsure.
124−
145+ disjoint :: Term -> Term -> Bool
125− disjointCons [] [] = False
146+ disjoint x y = case (cx, cy) of
126− disjointCons [] y = False
147+ -- data constructors -> compare their names
127− disjointCons x [] = False
128− disjointCons (x : xs) (y : ys)
129− = disjointCon x y || disjointCons xs ys
130−
131− disjointCon x y = let (cx, _) = unApply x
132− (cy, _) = unApply y in
133− case (cx, cy) of
134− (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
148+ (P (DCon _ _) nx _, P (DCon _ _) ny _)
149+ | nx /= ny -> True
150+ | otherwise -> or $ zipWith disjoint xargs yargs
135− _ -> False
151+ _ -> False
152+ where
153+ (cx, xargs) = unApply x
154+ (cy, yargs) = unApply y
136
155
137class Optimisable term where
156class Optimisable term where
138 applyOpts :: term -> Idris term
157 applyOpts :: term -> Idris term
139 stripCollapsed :: term -> Idris term
158 stripCollapsed :: term -> Idris term
140
159
141instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
160instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
142− applyOpts (x, y) = do x' <- applyOpts x
161+ applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
143− y' <- applyOpts y
144− return (x', y')
145− stripCollapsed (x, y) = do x' <- stripCollapsed x
162+ stripCollapsed (x, y) = (,) <$> stripCollapsed x <*> stripCollapsed y
146− y' <- stripCollapsed y
147− return (x', y')
148−
149
163
150instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
164instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
151− applyOpts (v, x, y) = do x' <- applyOpts x
165+ applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
152− y' <- applyOpts y
153− return (v, x', y')
154− stripCollapsed (v, x, y) = do x' <- stripCollapsed x
155− y' <- stripCollapsed y
166+ stripCollapsed (v, x, y) = (,,) v <$> stripCollapsed x <*> stripCollapsed y
156− return (v, x', y')
157
167
158instance Optimisable a => Optimisable [a] where
168instance Optimisable a => Optimisable [a] where
159 applyOpts = mapM applyOpts
169 applyOpts = mapM applyOpts
160 stripCollapsed = mapM stripCollapsed
170 stripCollapsed = mapM stripCollapsed
161
171
162instance Optimisable a => Optimisable (Either a (a, a)) where
172instance Optimisable a => Optimisable (Either a (a, a)) where
163− applyOpts (Left t) = do t' <- applyOpts t; return $ Left t'
173+ applyOpts (Left t) = Left <$> applyOpts t
164− applyOpts (Right t) = do t' <- applyOpts t; return $ Right t'
174+ applyOpts (Right t) = Right <$> applyOpts t
165− stripCollapsed (Left t) = do t' <- stripCollapsed t; return $ Left t'
175+ stripCollapsed (Left t) = Left <$> stripCollapsed t
166− stripCollapsed (Right t) = do t' <- stripCollapsed t; return $ Right t'
176+ stripCollapsed (Right t) = Right <$> stripCollapsed t
167
177
168-- Raw is for compile time optimisation (before type checking)
178-- Raw is for compile time optimisation (before type checking)
169-- Term is for run time optimisation (after type checking, collapsing allowed)
179-- Term is for run time optimisation (after type checking, collapsing allowed)
@@ -175,41 +185,39 @@ instance Optimisable Raw where
175 | (Var n, args) <- raw_unapply t -- MAGIC HERE
185 | (Var n, args) <- raw_unapply t -- MAGIC HERE
176 = do args' <- mapM applyOpts args
186 = do args' <- mapM applyOpts args
177 i <- getIState
187 i <- getIState
178− case lookupCtxt n (idris_optimisation i) of
188+ return $ case lookupCtxt n (idris_optimisation i) of
179− (oi:_) -> return $ applyDataOpt oi n args'
189+ oi:_ -> applyDataOpt oi n args'
180− _ -> return (raw_apply (Var n) args')
190+ _ -> raw_apply (Var n) args'
181− | otherwise = do f' <- applyOpts f
191+ | otherwise = RApp <$> applyOpts f <*> applyOpts a
182− a' <- applyOpts a
192+
183− return (RApp f' a')
184− applyOpts (RBind n b t) = do b' <- applyOpts b
193+ applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
185− t' <- applyOpts t
186− return (RBind n b' t')
187− applyOpts (RForce t) = applyOpts t
194+ applyOpts (RForce t) = applyOpts t
188 applyOpts t = return t
195 applyOpts t = return t
189
196
190 stripCollapsed t = return t
197 stripCollapsed t = return t
191
198
192instance Optimisable t => Optimisable (Binder t) where
199instance Optimisable t => Optimisable (Binder t) where
193− applyOpts (Let t v) = do t' <- applyOpts t
200+ applyOpts (Let t v) = Let <$> applyOpts t <*> applyOpts v
194− v' <- applyOpts v
195− return (Let t' v')
196 applyOpts b = do t' <- applyOpts (binderTy b)
201 applyOpts b = do t' <- applyOpts (binderTy b)
197 return (b { binderTy = t' })
202 return (b { binderTy = t' })
198− stripCollapsed (Let t v) = do t' <- stripCollapsed t
203+ stripCollapsed (Let t v) = Let <$> stripCollapsed t <*> stripCollapsed v
199− v' <- stripCollapsed v
200− return (Let t' v')
201 stripCollapsed b = do t' <- stripCollapsed (binderTy b)
204 stripCollapsed b = do t' <- stripCollapsed (binderTy b)
202 return (b { binderTy = t' })
205 return (b { binderTy = t' })
203
206
207+forcedArgSeq :: OptInfo -> [Maybe Forceability]
208+forcedArgSeq oi = map (\i -> M.lookup i forceMap) [0..]
209+ where
210+ forceMap = M.fromList $ forceable oi
211+
212+forcedCnt :: ForceMap -> Int
213+forcedCnt = length . filter (== Unconditional) . M.elems
204
214
205applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
215applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw
206−applyDataOpt oi n args
216+applyDataOpt oi n args
207− = let args' = zipWith doForce (map (\x -> x `elem` (forceable oi)) [0..])
217+ = raw_apply (Var n) $ zipWith doForce (forcedArgSeq oi) args
208− args in
209− raw_apply (Var n) args'
210 where
218 where
211− doForce True a = RForce a
219+ doForce (Just Unconditional) a = RForce a
212− doForce False a = a
220+ doForce _ a = a
213
221
214-- Run-time: do everything
222-- Run-time: do everything
215
223
@@ -268,10 +276,10 @@ instance Optimisable (TT Name) where
268
276
269applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
277applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
270applyDataOptRT oi n tag arity args
278applyDataOptRT oi n tag arity args
271− | length args == arity = doOpts n args (collapsible oi) (forceable oi)
279+ | length args == arity = doOpts n args (collapsible oi) (M.fromList $ forceable oi)
272 | otherwise = let extra = satArgs (arity - length args)
280 | otherwise = let extra = satArgs (arity - length args)
273 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
281 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
274− (collapsible oi) (forceable oi) in
282+ (collapsible oi) (M.fromList $ forceable oi) in
275 bind extra tm
283 bind extra tm
276 where
284 where
277 satArgs n = map (\i -> MN i "sat") [1..n]
285 satArgs n = map (\i -> MN i "sat") [1..n]
@@ -285,18 +293,12 @@ applyDataOptRT oi n tag arity args
285 doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _
293 doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _
286 = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))
294 = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))
287
295
288− doOpts n args True f = Erased
296+ doOpts n args True _ = Erased
289− doOpts n args _ forced
297+ doOpts n args _ forceMap
290− = let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])
291− args) in
292− if isnewtype oi
298+ | isnewtype oi = case args' of
293− then case args' of
294− [(_, val)] -> val
299+ [val] -> val
295− _ -> error "Can't happen (not isnewtype)"
300+ _ -> error $ "Can't happen (newtype not a singleton): " ++ show args'
296− else
301+ | otherwise = mkApp ctor' args'
302+ where
297− mkApp (P (DCon tag (arity - length forced)) n Erased)
303+ ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)
298− (map snd args')
304+ args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]
299−
300− keep (forced, _) = not forced
301−
302−
src/Idris/DeepSeq.hs+5
@@ -2,11 +2,16 @@ module Idris.DeepSeq where
2
2
3import Core.TT
3import Core.TT
4import Idris.AbsSyntax
4import Idris.AbsSyntax
5+import Idris.AbsSyntaxTree
5
6
6import Control.DeepSeq
7import Control.DeepSeq
7
8
8-- All generated by 'derive'
9-- All generated by 'derive'
9
10
11+instance NFData Forceability where
12+ rnf Conditional = ()
13+ rnf Unconditional = ()
14+
10instance NFData Raw where
15instance NFData Raw where
11 rnf (Var x1) = rnf x1 `seq` ()
16 rnf (Var x1) = rnf x1 `seq` ()
12 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
17 rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
src/Idris/ElabDecls.hs+1−1
@@ -792,7 +792,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
792 addIBC (IBCDef n)
792 addIBC (IBCDef n)
793 addDocStr n doc
793 addDocStr n doc
794 addIBC (IBCDoc n)
794 addIBC (IBCDoc n)
795− forceArgs n cty'
795+ forceArgs tn n cty'
796 return (n, cty')
796 return (n, cty')
797 where
797 where
798 tyIs (Bind n b sc) = tyIs sc
798 tyIs (Bind n b sc) = tyIs sc
src/Idris/IBC.hs+15−1
@@ -23,7 +23,7 @@ import Debug.Trace
23import Paths_idris
23import Paths_idris
24
24
25ibcVersion :: Word8
25ibcVersion :: Word8
26−ibcVersion = 46
26+ibcVersion = 47
27
27
28data IBCFile = IBCFile { ver :: Word8,
28data IBCFile = IBCFile { ver :: Word8,
29 sourcefile :: FilePath,
29 sourcefile :: FilePath,
@@ -833,6 +833,20 @@ instance Binary Accessibility where
833 2 -> return Hidden
833 2 -> return Hidden
834 _ -> error "Corrupted binary data for Accessibility"
834 _ -> error "Corrupted binary data for Accessibility"
835
835
836+safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
837+safeToEnum label x' = result
838+ where
839+ x = fromIntegral x'
840+ result
841+ | x < fromEnum (minBound `asTypeOf` result)
842+ || x > fromEnum (maxBound `asTypeOf` result)
843+ = error $ label ++ ": corrupted binary representation in IBC"
844+ | otherwise = toEnum x
845+
846+instance Binary Forceability where
847+ put = putWord8 . fromIntegral . fromEnum
848+ get = safeToEnum "Forceability" `fmap` getWord8
849+
836instance Binary PReason where
850instance Binary PReason where
837 put x
851 put x
838 = case x of
852 = case x of