5b62302 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add "detaggable" as an argument to OptInfo.

commit5b62302d762d819b22e5b328ebbb9b6ea69c43ce authorMatus Tejiscak <ziman@functor.sk> dateMon 24 Feb 2014, 18:13 (13 years ago) parentbc79ee8

7 files changed+27−12

compare with master

unifiedsplit

src/IRTS/Compiler.hs+13−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/DataOpts.hs+2−2 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+3−3 src/Idris/Erasure.hs+1−1 src/Idris/IBC.hs+4−2

src/IRTS/Compiler.hs+13−1

@@ -18,6 +18,7 @@ import Util.LLVMStubs

1818import IRTS.Inliner

1919

2020import Idris.AbsSyntax

21+import Idris.AbsSyntaxTree

2122import Idris.Erasure

2223import Idris.Error

2324

@@ -149,7 +150,18 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

149150 = let (args, sc) = cases_runtime cd in

150151 do e <- ir (args, sc)

151152 return (declArgs [] (case_inlinable ci) n e)

152−mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

153+

154+mkLDecl n (TyDecl (DCon t a) _) = do

155+ cg <- idris_callgraph <$> getIState

156+ return $ LConstructor n t a

157+{-

158+ case lookupCtxt n cg of

159+ [CGInfo _ _ _ _ [(i, _)]]

160+ | -> iLOG $ "USED: " ++ show n ++ ": " ++ show used

161+ [CGInfo _ _ _ _ used] -> iLOG $ "USED: " ++ show n ++ ": " ++ show used

162+ _ -> return $ LConstructor n t a

163+-}

164+

153165mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

154166mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

155167

src/Idris/AbsSyntaxTree.hs+2−1

@@ -847,7 +847,8 @@ data OptInfo = Optimise { collapsible :: Bool,

847847 -- Let's store a list and convert it to IntMap whenever needed.

848848 forceable :: [(Int, Forceability)],

849849 recursive :: [Int],

850− inaccessible :: [(Int,Name)] } -- arg name for error reporting

850+ inaccessible :: [(Int,Name)], -- names for error reporting

851+ detaggable :: Bool }

851852 deriving Show

852853{-!

853854deriving instance Binary OptInfo

src/Idris/DataOpts.hs+2−2

@@ -23,7 +23,7 @@ forceArgs typeName n expforce t = do

2323 ist <- getIState

2424 let fargs = getForcedArgs ist typeName t

2525 copt = case lookupCtxt n (idris_optimisation ist) of

26− [] -> Optimise False False [] [] []

26+ [] -> Optimise False False [] [] [] False

2727 op:_ -> op

2828 opts = addDef n (copt { forceable = M.toList fargs ++

2929 zip expforce (repeat Unconditional) })

@@ -129,7 +129,7 @@ collapseCons tn ctors = do

129129 (oi:_) -> do let oi' = oi { collapsible = True }

130130 let opts = addDef n oi' (idris_optimisation i)

131131 putIState (i { idris_optimisation = opts })

132− [] -> do let oi = Optimise True False [] [] []

132+ [] -> do let oi = Optimise True False [] [] [] False

133133 let opts = addDef n oi (idris_optimisation i)

134134 putIState (i { idris_optimisation = opts })

135135 addIBC (IBCOpt n)

src/Idris/DeepSeq.hs+2−2

@@ -290,8 +290,8 @@ instance NFData ClassInfo where

290290 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

291291

292292instance NFData OptInfo where

293− rnf (Optimise x1 x2 x3 x4 x5)

294− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

293+ rnf (Optimise x1 x2 x3 x4 x5 x6)

294+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

295295

296296instance NFData TypeInfo where

297297 rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/ElabDecls.hs+3−3

@@ -188,7 +188,7 @@ saveInaccArgs n is = do

188188

189189 _ -> do

190190 putIState ist{ idris_optimisation =

191− addDef n (Optimise False False [] [] is) (idris_optimisation ist) }

191+ addDef n (Optimise False False [] [] is False) (idris_optimisation ist) }

192192 addIBC (IBCOpt n)

193193

194194-- Get the list of (index, name) of inaccessible arguments from the type.

@@ -951,7 +951,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

951951 do ctxt <- getContext

952952 ist <- getIState

953953 let inacc = case lookupCtxt n (idris_optimisation ist) of

954− [Optimise _ _ _ _ inacc] -> map fst inacc

954+ [Optimise _ _ _ _ inacc _] -> map fst inacc

955955 _ -> []

956956 -- Check n actually exists, with no definition yet

957957 let tys = lookupTy n ctxt

@@ -989,7 +989,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

989989 [oi] -> do let opts = addDef n (oi { collapsible = True })

990990 (idris_optimisation ist)

991991 putIState (ist { idris_optimisation = opts })

992− _ -> do let opts = addDef n (Optimise True False [] [] [])

992+ _ -> do let opts = addDef n (Optimise True False [] [] [] False)

993993 (idris_optimisation ist)

994994 putIState (ist { idris_optimisation = opts })

995995 addIBC (IBCOpt n)

src/Idris/Erasure.hs+1−1

@@ -115,7 +115,7 @@ performUsageAnalysis = do

115115

116116 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()

117117 checkAccessibility opt (n, reachable)

118− | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt

118+ | [Optimise col nt forc rec inaccessible dt] <- lookupCtxt n opt

119119 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]

120120 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs

121121

src/Idris/IBC.hs+4−2

@@ -2100,19 +2100,21 @@ instance Binary ClassInfo where

21002100 return (CI x1 x2 x3 x4 x5 [])

21012101

21022102instance Binary OptInfo where

2103− put (Optimise x1 x2 x3 x4 x5)

2103+ put (Optimise x1 x2 x3 x4 x5 x6)

21042104 = do put x1

21052105 put x2

21062106 put x3

21072107 put x4

21082108 put x5

2109+ put x6

21092110 get

21102111 = do x1 <- get

21112112 x2 <- get

21122113 x3 <- get

21132114 x4 <- get

21142115 x5 <- get

2115− return (Optimise x1 x2 x3 x4 x5)

2116+ x6 <- get

2117+ return (Optimise x1 x2 x3 x4 x5 x6)

21162118

21172119instance Binary TypeInfo where

21182120 put (TI x1 x2 x3 x4) = do put x1