git.iko.soy/Idris-dev
on master help sign in
Add accessibility to data constructors.
c7ae580Matus Tejiscak
src/Idris/ElabDecls.hs+29−24
compare with master
unifiedsplit
@@ -85,7 +85,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
85 ty' <- implicit info syn n ty'
85 ty' <- implicit info syn n ty'
86
86
87 let ty = addImpl i ty'
87 let ty = addImpl i ty'
88− inacc = inaccessible 0 ty
88+ inacc = inaccessibleArgs 0 ty
89 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
89 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
90 logLvl 5 $ "Inaccessible arguments: " ++ show inacc
90 logLvl 5 $ "Inaccessible arguments: " ++ show inacc
91
91
@@ -166,29 +166,6 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
166 lst = txt "List"
166 lst = txt "List"
167 errrep = txt "ErrorReportPart"
167 errrep = txt "ErrorReportPart"
168
168
169− saveInaccArgs :: Name -> [(Int,Name)] -> 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−
182− inaccessible :: Int -> PTerm -> [(Int, Name)]
183− inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)
184− = (i,n) : inaccessible (i+1) t -- unbound implicit
185− inaccessible i (PPi plicity n ty t)
186− | InaccessibleArg `elem` pargopts plicity
187− = (i,n) : inaccessible (i+1) t -- an .{erased : Implicit}
188− | otherwise
189− = inaccessible (i+1) t -- a {regular : Implicit}
190− inaccessible _ _ = []
191−
192 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
169 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
193 (App (P _ (NS (UN m) ns2) _)
170 (App (P _ (NS (UN m) ns2) _)
194 (App (P _ (NS (UN l) ns3) _)
171 (App (P _ (NS (UN l) ns3) _)
@@ -200,6 +177,30 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
200 , ns4 == map txt ["Errors","Reflection","Language"] = True
177 , ns4 == map txt ["Errors","Reflection","Language"] = True
201 tyIsHandler _ = False
178 tyIsHandler _ = False
202
179
180+-- Store the list of inaccessible arguments in the internal state.
181+saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
182+saveInaccArgs n is = do
183+ ist <- getIState
184+ case lookupCtxt n (idris_optimisation ist) of
185+ [oi] -> do
186+ putIState ist{ idris_optimisation =
187+ addDef n oi{ inaccessible = is } (idris_optimisation ist) }
188+
189+ _ -> do
190+ putIState ist{ idris_optimisation =
191+ addDef n (Optimise False False [] [] is) (idris_optimisation ist) }
192+ addIBC (IBCOpt n)
193+
194+-- Get the list of (index, name) of inaccessible arguments from the type.
195+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
196+inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)
197+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
198+inaccessibleArgs i (PPi plicity n ty t)
199+ | InaccessibleArg `elem` pargopts plicity
200+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
201+ | otherwise
202+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}
203+inaccessibleArgs _ _ = []
203
204
204elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
205elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
205 FC -> FnOpts -> Name -> PTerm -> Idris ()
206 FC -> FnOpts -> Name -> PTerm -> Idris ()
@@ -891,6 +892,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
891 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
892 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
892 let t = addImpl i t_in
893 let t = addImpl i t_in
893 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
894 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
895+ let inacc = inaccessibleArgs 0 t
896+ logLvl 5 $ "Inaccessible args: " ++ show inacc
894 ((t', defer, is), log) <-
897 ((t', defer, is), log) <-
895 tclift $ elaborate ctxt n (TType (UVal 0)) []
898 tclift $ elaborate ctxt n (TType (UVal 0)) []
896 (errAt "constructor " n (erun fc (build i info False [] n t)))
899 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -908,6 +911,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
908 checkDocs fc argDocs t_in
911 checkDocs fc argDocs t_in
909 addDocStr n doc argDocs
912 addDocStr n doc argDocs
910 addIBC (IBCDoc n)
913 addIBC (IBCDoc n)
914+ saveInaccArgs n inacc
915+ addIBC (IBCOpt n)
911 let fs = map (getNamePos 0 t) forcenames
916 let fs = map (getNamePos 0 t) forcenames
912 -- FIXME: 'forcenames' is an almighty hack! Need a better way of
917 -- FIXME: 'forcenames' is an almighty hack! Need a better way of
913 -- erasing non-forceable things
918 -- erasing non-forceable things