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

git.iko.soy/Idris-dev

Add an "inaccessible" field to OptData.

commit9b80d0d0d179efc46349a95b61bb0cf1eccf8cfc authorMatus Tejiscak <ziman@functor.sk> dateTue 11 Feb 2014, 14:15 (13 years ago) parentec85560

5 files changed+27−9

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/DataOpts.hs+2−2 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+17−2 src/Idris/IBC.hs+4−2

src/Idris/AbsSyntaxTree.hs+2−1

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

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

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

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

855− recursive :: [Int] }

855+ recursive :: [Int],

856+ inaccessible :: [Int] }

856857 deriving Show

857858{-!

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

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

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)

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

293+ rnf (Optimise x1 x2 x3 x4 x5)

294+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `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+17−2

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

8787 let ty = addImpl i ty'

8888 inacc = inaccessible 0 ty

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

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

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

9191

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

9393 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

133133 addDocStr n doc argDocs

134134 addIBC (IBCDoc n)

135135 addIBC (IBCFlags n opts')

136+ saveInaccArgs n inacc

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

137138 addIBC (IBCCoercion n)

139+

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

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

140142 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

164166 lst = txt "List"

165167 errrep = txt "ErrorReportPart"

166168

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+

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

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

169184 = 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

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

966981 (idris_optimisation ist)

967982 putIState (ist { idris_optimisation = opts })

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

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

969984 (idris_optimisation ist)

970985 putIState (ist { idris_optimisation = opts })

971986 addIBC (IBCOpt n)

src/Idris/IBC.hs+4−2

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

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

21032103

21042104instance Binary OptInfo where

2105− put (Optimise x1 x2 x3 x4)

2105+ put (Optimise x1 x2 x3 x4 x5)

21062106 = do put x1

21072107 put x2

21082108 put x3

21092109 put x4

2110+ put x5

21102111 get

21112112 = do x1 <- get

21122113 x2 <- get

21132114 x3 <- get

21142115 x4 <- get

2115− return (Optimise x1 x2 x3 x4)

2116+ x5 <- get

2117+ return (Optimise x1 x2 x3 x4 x5)

21162118

21172119instance Binary TypeInfo where

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