git.iko.soy/Idris-dev
on master help sign in
Fix inaccessibility elaboration.
commiteedcec18906ef7e5f87cd5613de0c3367252a8b3 authorMatus Tejiscak <ziman@functor.sk> dateMon 14 Apr 2014, 15:58 (13 years ago) parentbb6873c
2 files changed+20−24
compare with master
unifiedsplit
src/Idris/ASTUtils.hs+8−2 src/Idris/ElabDecls.hs+12−22
src/Idris/ASTUtils.hs+8−2
@@ -52,9 +52,15 @@ ctxt_lookupExact n = Field
5252instance InitialValue OptInfo where
5353 initialValue = Optimise [] False
5454
55−ist_optimisation :: Field IState (Ctxt OptInfo)
56−ist_optimisation = Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
55+-- raw context, probably won't be used much
56+ist_optimisation_ctxt :: Field IState (Ctxt OptInfo)
57+ist_optimisation_ctxt = Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
5758
59+-- the optimisation record for the given name
60+ist_optimisation :: Name -> Field IState OptInfo
61+ist_optimisation n = ctxt_lookupExact n . ist_optimisation_ctxt
62+
63+-- two fields of the optimisation record
5864opt_inaccessible :: Field OptInfo [(Int, Name)]
5965opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
6066
src/Idris/ElabDecls.hs+12−22
@@ -4,6 +4,7 @@
44module Idris.ElabDecls where
55
66import Idris.AbsSyntax
7+import Idris.ASTUtils
78import Idris.DSL
89import Idris.Error
910import Idris.Delaborate
@@ -29,6 +30,10 @@ import Idris.Core.CaseTree
2930
3031import Idris.Docstrings
3132
33+import Prelude hiding (id, (.))
34+import Control.Category
35+
36+import Control.Applicative hiding (Const)
3237import Control.DeepSeq
3338import Control.Monad
3439import Control.Monad.State.Strict as State
@@ -134,7 +139,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
134139 addDocStr n doc argDocs
135140 addIBC (IBCDoc n)
136141 addIBC (IBCFlags n opts')
137− saveInaccArgs n inacc
142+ fputState (opt_inaccessible . ist_optimisation n) inacc
143+ addIBC (IBCOpt n)
138144 when (Implicit `elem` opts') $ do addCoercion n
139145 addIBC (IBCCoercion n)
140146
@@ -178,20 +184,6 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
178184 , ns4 == map txt ["Errors","Reflection","Language"] = True
179185 tyIsHandler _ = False
180186
181−-- Store the list of inaccessible arguments in the internal state.
182−saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
183−saveInaccArgs n is = do
184− ist <- getIState
185− case lookupCtxtExact n (idris_optimisation ist) of
186− Just oi -> do
187− putIState ist{ idris_optimisation =
188− addDef n oi{ inaccessible = is } (idris_optimisation ist) }
189−
190− Nothing -> do
191− putIState ist{ idris_optimisation =
192− addDef n (Optimise is False) (idris_optimisation ist) }
193− addIBC (IBCOpt n)
194−
195187-- Get the list of (index, name) of inaccessible arguments from the type.
196188inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
197189inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
@@ -918,7 +910,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
918910 checkDocs fc argDocs t_in
919911 addDocStr n doc argDocs
920912 addIBC (IBCDoc n)
921− saveInaccArgs n inacc
913+ fputState (opt_inaccessible . ist_optimisation n) inacc
922914 addIBC (IBCOpt n)
923915 return (n, cty')
924916 where
@@ -953,9 +945,8 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
953945elabClauses info fc opts n_in cs = let n = liftname info n_in in
954946 do ctxt <- getContext
955947 ist <- getIState
956− let inacc = case lookupCtxt n (idris_optimisation ist) of
957− [Optimise inacc _] -> map fst inacc
958− _ -> []
948+ inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
949+
959950 -- Check n actually exists, with no definition yet
960951 let tys = lookupTy n ctxt
961952 let reflect = Reflection `elem` opts
@@ -975,9 +966,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
975966
976967 solveDeferred n
977968
978− ist <- getIState
979− let opts = addDef n (Optimise [] False) (idris_optimisation ist)
980− in putIState (ist { idris_optimisation = opts })
969+ -- just ensure that the structure exists
970+ fmodifyState (ist_optimisation n) id
981971 addIBC (IBCOpt n)
982972
983973 ist <- getIState