9b80d0d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add an "inaccessible" field to OptData.

9b80d0dMatus Tejiscak13 years ago

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

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

852 -- but the corresponding Binary instance seems to be broken.

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

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

855− recursive :: [Int] }

855+ recursive :: [Int],

856+ inaccessible :: [Int] }

856 deriving Show

857 deriving Show

857{-!

858{-!

858deriving instance Binary OptInfo

859deriving instance Binary OptInfo

src/Idris/DataOpts.hs+2−2

@@ -23,7 +23,7 @@ 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 [] []

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

27 op:_ -> op

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

29 zip expforce (repeat Unconditional) })

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

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 [] []

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

133 let opts = addDef n oi (idris_optimisation i)

134 putIState (i { idris_optimisation = opts })

135 addIBC (IBCOpt n)

src/Idris/DeepSeq.hs+2−2

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

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

291

292instance NFData OptInfo where

293− rnf (Optimise x1 x2 x3 x4)

293+ rnf (Optimise x1 x2 x3 x4 x5)

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

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

295

296instance NFData TypeInfo where

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

src/Idris/ElabDecls.hs+17−2

@@ -87,7 +87,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

87 let ty = addImpl i ty'

88 inacc = inaccessible 0 ty

89 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

90− logLvl 5 $ "Erased params: " ++ show inacc

90+ logLvl 5 $ "Inaccessible arguments: " ++ show inacc

92 ((tyT, defer, is), log) <-

93 tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -133,8 +133,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

133 addDocStr n doc argDocs

134 addIBC (IBCDoc n)

135 addIBC (IBCFlags n opts')

136+ saveInaccArgs n inacc

136 when (Implicit `elem` opts') $ do addCoercion n

137 when (Implicit `elem` opts') $ do addCoercion n

137 addIBC (IBCCoercion n)

138 addIBC (IBCCoercion n)

139+

138 -- If the function is declared as an error handler and the language

140 -- If the function is declared as an error handler and the language

139 -- extension is enabled, then add it to the list of error handlers.

141 -- extension is enabled, then add it to the list of error handlers.

140 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

142 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

@@ -164,6 +166,19 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

164 lst = txt "List"

166 lst = txt "List"

165 errrep = txt "ErrorReportPart"

167 errrep = txt "ErrorReportPart"

166

168

169+ saveInaccArgs :: Name -> [Int] -> Idris ()

170+ saveInaccArgs n is = do

171+ ist <- getIState

172+ case lookupCtxt n (idris_optimisation ist) of

173+ [oi] -> do

174+ putIState ist{ idris_optimisation =

175+ addDef n oi{ inaccessible = is } (idris_optimisation ist) }

176+

177+ _ -> do

178+ putIState ist{ idris_optimisation =

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

180+ addIBC (IBCOpt n)

181+

167 inaccessible :: Int -> PTerm -> [Int]

182 inaccessible :: Int -> PTerm -> [Int]

168 inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)

183 inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)

169 = i : inaccessible (i+1) t -- unbound implicit

184 = i : inaccessible (i+1) t -- unbound implicit

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

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

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

966 (idris_optimisation ist)

981 (idris_optimisation ist)

967 putIState (ist { idris_optimisation = opts })

982 putIState (ist { idris_optimisation = opts })

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

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

969 (idris_optimisation ist)

984 (idris_optimisation ist)

970 putIState (ist { idris_optimisation = opts })

985 putIState (ist { idris_optimisation = opts })

971 addIBC (IBCOpt n)

986 addIBC (IBCOpt n)

src/Idris/IBC.hs+4−2

@@ -2102,17 +2102,19 @@ instance Binary ClassInfo where

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

2103

2104instance Binary OptInfo where

2105− put (Optimise x1 x2 x3 x4)

2105+ put (Optimise x1 x2 x3 x4 x5)

2106 = do put x1

2107 put x2

2108 put x3

2109 put x4

2110+ put x5

2110 get

2111 get

2111 = do x1 <- get

2112 = do x1 <- get

2112 x2 <- get

2113 x2 <- get

2113 x3 <- get

2114 x3 <- get

2114 x4 <- get

2115 x4 <- get

2116+ x5 <- get

2115− return (Optimise x1 x2 x3 x4)

2117+ return (Optimise x1 x2 x3 x4 x5)

2116

2118

2117instance Binary TypeInfo where

2119instance Binary TypeInfo where

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

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