@@ -16,6 +16,7 @@ import Idris.Primitives
16import Idris.Inliner
16import Idris.Inliner
17import Idris.PartialEval
17import Idris.PartialEval
18import Idris.DeepSeq
18import Idris.DeepSeq
19+import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
20import IRTS.Lang
20import Paths_idris
21import Paths_idris
@@ -36,6 +37,7 @@ import Data.Maybe
36import Debug.Trace
37import Debug.Trace
38import qualified Data.Map as Map
39import qualified Data.Map as Map
40+import qualified Data.Set as S
39import qualified Data.Text as T
41import qualified Data.Text as T
40import Data.Char(isLetter, toLower)
42import Data.Char(isLetter, toLower)
41import Data.List.Split (splitOn)
43import Data.List.Split (splitOn)
@@ -58,7 +60,8 @@ checkAddDef add toplvl fc [] = return []
58checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
60checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
59 = do ctxt <- getContext
61 = do ctxt <- getContext
60 (t', _) <- recheckC fc [] t
62 (t', _) <- recheckC fc [] t
61− when add $ addDeferred [(n, (i, top, t, toplvl))]
63+ when add $ do addDeferred [(n, (i, top, t, toplvl))]
62 ns' <- checkAddDef add toplvl fc ns
65 ns' <- checkAddDef add toplvl fc ns
63 return ((n, (i, top, t')) : ns')
66 return ((n, (i, top, t')) : ns')
64-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
67-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
@@ -80,10 +83,13 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
81 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
84 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
82 ty' <- addUsingConstraints syn fc ty'
85 ty' <- addUsingConstraints syn fc ty'
83− ty' <- implicit syn n ty'
86+ ty' <- implicit info syn n ty'
85− let ty = addImpl i ty'
88+ let ty = addImpl i ty'
89+ inacc = inaccessibleArgs 0 ty
86 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
90 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
91+ logLvl 5 $ "Inaccessible arguments: " ++ show inacc
87 ((tyT, defer, is), log) <-
93 ((tyT, defer, is), log) <-
88 tclift $ elaborate ctxt n (TType (UVal 0)) []
94 tclift $ elaborate ctxt n (TType (UVal 0)) []
89 (errAt "type of " n (erun fc (build i info False [] n ty)))
95 (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -128,8 +134,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
128 addDocStr n doc argDocs
134 addDocStr n doc argDocs
129 addIBC (IBCDoc n)
135 addIBC (IBCDoc n)
130 addIBC (IBCFlags n opts')
136 addIBC (IBCFlags n opts')
137+ saveInaccArgs n inacc
131 when (Implicit `elem` opts') $ do addCoercion n
138 when (Implicit `elem` opts') $ do addCoercion n
132 addIBC (IBCCoercion n)
139 addIBC (IBCCoercion n)
133 -- If the function is declared as an error handler and the language
141 -- If the function is declared as an error handler and the language
134 -- extension is enabled, then add it to the list of error handlers.
142 -- extension is enabled, then add it to the list of error handlers.
135 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
143 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
@@ -170,30 +178,40 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
170 , ns4 == map txt ["Errors","Reflection","Language"] = True
178 , ns4 == map txt ["Errors","Reflection","Language"] = True
171 tyIsHandler _ = False
179 tyIsHandler _ = False
181+-- Store the list of inaccessible arguments in the internal state.
182+saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
183+saveInaccArgs n is = do
185+ case lookupCtxt n (idris_optimisation ist) of
187+ putIState ist{ idris_optimisation =
188+ addDef n oi{ inaccessible = is } (idris_optimisation ist) }
191+ putIState ist{ idris_optimisation =
192+ addDef n (Optimise is False) (idris_optimisation ist) }
195+-- Get the list of (index, name) of inaccessible arguments from the type.
196+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
197+inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
198+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
199+inaccessibleArgs i (PPi plicity n ty t)
200+ | InaccessibleArg `elem` pargopts plicity
201+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
203+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}
204+inaccessibleArgs _ _ = []
174elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
206elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
175 FC -> FnOpts -> Name -> PTerm -> Idris ()
207 FC -> FnOpts -> Name -> PTerm -> Idris ()
176−elabPostulate info syn doc fc opts n ty
208+elabPostulate info syn doc fc opts n ty = do
177− = do elabType info syn doc [] fc opts n ty
209+ elabType info syn doc [] fc opts n ty
178− -- make sure it's collapsible, so it is never needed at run time
210+ putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
179− -- start by getting the elaborated type
211+ addIBC (IBCPostulate n)
180− ctxt <- getContext
212+
181− fty <- case lookupTy n ctxt of
182− [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
185− let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
186− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
187− let postOK = case ap of
188− P _ tn _ -> case lookupCtxt tn
189− (idris_optimisation ist) of
190− [oi] -> collapsible oi
194− $ tclift $ tfail (At fc (NonCollapsiblePostulate n))
195− -- remove it from the deferred definitions list
213+ -- remove it from the deferred definitions list
196− solveDeferred n
214+ solveDeferred n
198elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
216elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
217elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
@@ -202,13 +220,15 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
202 checkUndefined fc n
220 checkUndefined fc n
203 ctxt <- getContext
221 ctxt <- getContext
204 i <- getIState
222 i <- getIState
223+ -- TODO think: something more in info?
205− t_in <- implicit syn n t_in
224+ t_in <- implicit info syn n t_in
206 let t = addImpl i t_in
225 let t = addImpl i t_in
207 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
226 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
208 (erun fc (build i info False [] n t))
227 (erun fc (build i info False [] n t))
209 def' <- checkDef fc defer
228 def' <- checkDef fc defer
210 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
229 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
211 addDeferredTyCon def''
230 addDeferredTyCon def''
212 mapM_ (elabCaseBlock info []) is
232 mapM_ (elabCaseBlock info []) is
213 (cty, _) <- recheckC fc [] t'
233 (cty, _) <- recheckC fc [] t'
214 logLvl 2 $ "---> " ++ show cty
234 logLvl 2 $ "---> " ++ show cty
@@ -220,7 +240,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
220 undef <- isUndefined fc n
240 undef <- isUndefined fc n
221 ctxt <- getContext
241 ctxt <- getContext
222 i <- getIState
242 i <- getIState
223− t_in <- implicit syn n t_in
243+ t_in <- implicit info syn n t_in
224 let t = addImpl i t_in
244 let t = addImpl i t_in
225 ((t', defer, is), log) <-
245 ((t', defer, is), log) <-
226 tclift $ elaborate ctxt n (TType (UVal 0)) []
246 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -236,7 +256,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
236 logLvl 2 $ "---> " ++ show cty
256 logLvl 2 $ "---> " ++ show cty
237 -- temporary, to check cons
257 -- temporary, to check cons
238 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
258 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
259+ let cnameinfo = cinfo info (map cname dcons)
239− cons <- mapM (elabCon info syn n codata) dcons
260+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
240 ttag <- getName
261 ttag <- getName
241 i <- getIState
262 i <- getIState
242 let as = map (const Nothing) (getArgTys cty)
263 let as = map (const Nothing) (getArgTys cty)
@@ -253,15 +274,30 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
253 let metainf = DataMI params
274 let metainf = DataMI params
254 addIBC (IBCMetaInformation n metainf)
275 addIBC (IBCMetaInformation n metainf)
255 -- TMP HACK! Make this a data option
276 -- TMP HACK! Make this a data option
256− when (n /= sUN "Lazy'") $ collapseCons n cons
257 updateContext (addDatatype (Data n ttag cty cons))
277 updateContext (addDatatype (Data n ttag cty cons))
258 updateContext (setMetaInformation n metainf)
278 updateContext (setMetaInformation n metainf)
259 mapM_ (checkPositive n) cons
279 mapM_ (checkPositive n) cons
281+ -- if there's exactly one constructor,
282+ -- mark both the type and the constructor as detaggable
284+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n
285+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
288+ -- create an eliminator
260− if DefaultEliminator `elem` opts
289+ when (DefaultEliminator `elem` opts) $
261− then evalStateT (elabEliminator params n t dcons info) Map.empty
290+ evalStateT (elabEliminator params n t dcons info) Map.empty
292+ setDetaggable :: Name -> Idris ()
293+ setDetaggable n = do
295+ let opt = idris_optimisation ist
296+ case lookupCtxt n opt of
297+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
298+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
264− checkDefinedAs fc n t ctxt
300+ checkDefinedAs fc n t ctxt
265 = case lookupDef n ctxt of
301 = case lookupDef n ctxt of
266 [] -> return ()
302 [] -> return ()
267 [TyDecl _ ty] ->
303 [TyDecl _ ty] ->
@@ -319,6 +355,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
319 | otherwise = count n ts
355 | otherwise = count n ts
320 mParam args (_ : rest) = Nothing : mParam args rest
356 mParam args (_ : rest) = Nothing : mParam args rest
358+ cname (_, _, n, _, _, _) = n
360+ -- Abuse of ElabInfo.
361+ -- TODO Contemplate whether the ElabInfo type needs modification.
362+ cinfo :: ElabInfo -> [Name] -> ElabInfo
364+ = let newps = params info
365+ dsParams = map (\n -> (n, [])) ds
366+ newb = addAlist dsParams (inblock info)
367+ l = liftname info in
368+ info { params = newps,
370+ liftname = id -- Is this appropriate?
322type EliminatorState = StateT (Map.Map String Int) Idris
373type EliminatorState = StateT (Map.Map String Int) Idris
324-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
375-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
@@ -728,7 +779,8 @@ elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
728 PTerm -> Docstring -> Name -> PTerm -> Idris ()
779 PTerm -> Docstring -> Name -> PTerm -> Idris ()
729elabRecord info syn doc fc tyn ty cdoc cn cty
780elabRecord info syn doc fc tyn ty cdoc cn cty
730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
781 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
782+ -- TODO think: something more in info?
731− cty' <- implicit syn cn cty
783+ cty' <- implicit info syn cn cty
732 i <- getIState
784 i <- getIState
733 cty <- case lookupTy cn (tt_ctxt i) of
785 cty <- case lookupTy cn (tt_ctxt i) of
734 [t] -> return (delab i t)
786 [t] -> return (delab i t)
@@ -750,7 +802,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
803-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
753− isNonImp (PExp _ _ _, a) = Just a
805+ isNonImp (PExp _ _ _ _, a) = Just a
754 isNonImp _ = Nothing
806 isNonImp _ = Nothing
756 tryElabDecl info (fn, ty, val)
808 tryElabDecl info (fn, ty, val)
@@ -833,15 +885,22 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
833 (map pexp rhsArgs)) []
885 (map pexp rhsArgs)) []
834 return (pn, pfnTy, PClauses fc [] setname [pclause])
886 return (pn, pfnTy, PClauses fc [] setname [pclause])
888+-- FIXME: 'forcenames' is an almighty hack! Need a better way of
889+-- erasing non-forceable things
891+-- TODO: the above is a comment from the past;
892+-- forcenames is probably no longer needed
836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
893elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
837 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
894 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
895elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
839 = do checkUndefined fc n
896 = do checkUndefined fc n
840 ctxt <- getContext
897 ctxt <- getContext
841 i <- getIState
898 i <- getIState
842− t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
899+ t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
843 let t = addImpl i t_in
900 let t = addImpl i t_in
844 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
901 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
902+ let inacc = inaccessibleArgs 0 t
903+ logLvl 5 $ "Inaccessible args: " ++ show inacc
845 ((t', defer, is), log) <-
904 ((t', defer, is), log) <-
846 tclift $ elaborate ctxt n (TType (UVal 0)) []
905 tclift $ elaborate ctxt n (TType (UVal 0)) []
847 (errAt "constructor " n (erun fc (build i info False [] n t)))
906 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -859,10 +918,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
859 checkDocs fc argDocs t_in
918 checkDocs fc argDocs t_in
860 addDocStr n doc argDocs
919 addDocStr n doc argDocs
861 addIBC (IBCDoc n)
920 addIBC (IBCDoc n)
862− let fs = map (getNamePos 0 t) forcenames
921+ saveInaccArgs n inacc
863− -- FIXME: 'forcenames' is an almighty hack! Need a better way of
922+ addIBC (IBCOpt n)
864− -- erasing non-forceable things
865− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
866 return (n, cty')
923 return (n, cty')
868 tyIs (Bind n b sc) = tyIs sc
925 tyIs (Bind n b sc) = tyIs sc
@@ -873,7 +930,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
874 mkLazy (PPi pl n ty sc)
931 mkLazy (PPi pl n ty sc)
875 = let ty' = if getTyName ty
932 = let ty' = if getTyName ty
876− then PApp fc (PRef fc (sUN "Lazy'"))
933+ then PApp fc (PRef fc (sUN "Lazy'"))
877 [pexp (PRef fc (sUN "LazyCodata")),
934 [pexp (PRef fc (sUN "LazyCodata")),
879 else ty in
936 else ty in
@@ -895,6 +952,10 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
895elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
952elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
896elabClauses info fc opts n_in cs = let n = liftname info n_in in
953elabClauses info fc opts n_in cs = let n = liftname info n_in in
897 do ctxt <- getContext
954 do ctxt <- getContext
956+ let inacc = case lookupCtxt n (idris_optimisation ist) of
957+ [Optimise inacc _] -> map fst inacc
898 -- Check n actually exists, with no definition yet
959 -- Check n actually exists, with no definition yet
899 let tys = lookupTy n ctxt
960 let tys = lookupTy n ctxt
900 let reflect = Reflection `elem` opts
961 let reflect = Reflection `elem` opts
@@ -906,33 +967,19 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
906 tclift $ tfail $ At fc (NoTypeDecl n)
967 tclift $ tfail $ At fc (NoTypeDecl n)
907 [ty] -> return ty
968 [ty] -> return ty
908 let atys = map snd (getArgTys fty)
969 let atys = map snd (getArgTys fty)
909− pats_in <- mapM (elabClause info opts)
970+ cs_elab <- mapM (elabClause info opts)
910 (zip [0..] cs)
971 (zip [0..] cs)
972+ let (pats_in, cs_full) = unzip cs_elab
911 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
974 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
913− -- if the return type of 'ty' is collapsible, the optimised version should
916− let (ap, _) = unApply (getRetTy fty)
917− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
918− -- FIXME: Really ought to only do this for total functions!
919− let doNothing = case ap of
920− P _ tn _ -> case lookupCtxt tn
921− (idris_optimisation ist) of
922− [oi] -> collapsible oi
925 solveDeferred n
976 solveDeferred n
926 ist <- getIState
978 ist <- getIState
928− case lookupCtxt n (idris_optimisation ist) of
929− [oi] -> do let opts = addDef n (oi { collapsible = True })
930− (idris_optimisation ist)
931− putIState (ist { idris_optimisation = opts })
932− _ -> do let opts = addDef n (Optimise True False [] [])
979+ let opts = addDef n (Optimise [] False) (idris_optimisation ist)
933− (idris_optimisation ist)
934− putIState (ist { idris_optimisation = opts })
980+ in putIState (ist { idris_optimisation = opts })
935− addIBC (IBCOpt n)
981+ addIBC (IBCOpt n)
936 ist <- getIState
983 ist <- getIState
937 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
984 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
@@ -942,11 +989,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
942 let tcase = opt_typecase (idris_options ist)
989 let tcase = opt_typecase (idris_options ist)
944 -- Summary of what's about to happen: Definitions go:
991 -- Summary of what's about to happen: Definitions go:
946− -- pats_in -> pats -> optpats
993+ -- pats_in -> pats -> pdef -> pdef'
947− -- pdef comes from pats,
948− -- optpdef comes from optpats
949− -- Then pdef' is optpdef with forcing/collapsing applied everywhere
951 -- addCaseDef builds case trees from <pdef> and <pdef'>
995 -- addCaseDef builds case trees from <pdef> and <pdef'>
@@ -975,24 +1019,16 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
976 numArgs <- tclift $ sameLength pdef
1020 numArgs <- tclift $ sameLength pdef
978− -- patterns after collapsing optimisation applied
979− -- (i.e. check if the function should do nothing at run time)
980− optpats <- if doNothing
981− then return $ [Right (mkApp (P Bound n Erased)
982− (take numArgs (repeat Erased)), Erased)]
983− else stripCollapsed pats
985 case specNames opts of
1022 case specNames opts of
986 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
1023 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
987 _ -> return ()
1024 _ -> return ()
989− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
990 tree@(CaseDef scargs sc _) <- tclift $
1026 tree@(CaseDef scargs sc _) <- tclift $
991− simpleCase tcase False reflect CompileTime fc atys pdef
1027+ simpleCase tcase False reflect CompileTime fc inacc atys pdef
992 cov <- coverage
1028 cov <- coverage
993 pmissing <-
1029 pmissing <-
994 if cov && not (hasDefault cs)
1030 if cov && not (hasDefault cs)
995− then do missing <- genClauses fc n (map getLHS pdef) cs
1031+ then do missing <- genClauses fc n (map getLHS pdef) cs_full
996 -- missing <- genMissing n scargs sc
1032 -- missing <- genMissing n scargs sc
997 missing' <- filterM (checkPossible info fc True n) missing
1033 missing' <- filterM (checkPossible info fc True n) missing
998 let clhs = map getLHS pdef
1034 let clhs = map getLHS pdef
@@ -1010,7 +1046,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1010 let pcover = null pmissing
1046 let pcover = null pmissing
1012 -- pdef' is the version that gets compiled for run-time
1048 -- pdef' is the version that gets compiled for run-time
1013− pdef_in' <- applyOpts optpdef
1049+ pdef_in' <- applyOpts pdef
1014 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1050 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
1016 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
1052 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
@@ -1037,11 +1073,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1037 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
1073 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
1039 tree' <- tclift $ simpleCase tcase knowncovering reflect
1075 tree' <- tclift $ simpleCase tcase knowncovering reflect
1040− RunTime fc atys pdef'
1076+ RunTime fc inacc atys pdef'
1041− logLvl 3 (show tree)
1077+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
1042 logLvl 3 $ "Optimised: " ++ show tree'
1078 logLvl 3 $ "Optimised: " ++ show tree'
1043 ctxt <- getContext
1079 ctxt <- getContext
1044 ist <- getIState
1080 ist <- getIState
1081+ let opt = idris_optimisation ist
1045 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
1082 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
1046 (idris_patdefs ist) })
1083 (idris_patdefs ist) })
1047 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
1084 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)
@@ -1051,6 +1088,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1052 (AssertTotal `elem` opts)
1089 (AssertTotal `elem` opts)
1055 pdef pdef pdef_inl pdef' ty)
1093 pdef pdef pdef_inl pdef' ty)
1056 addIBC (IBCDef n)
1094 addIBC (IBCDef n)
@@ -1067,7 +1105,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
1067 let used = findUsedArgs sc' scargs'
1105 let used = findUsedArgs sc' scargs'
1068 -- let scg = buildSCG i sc scargs
1106 -- let scg = buildSCG i sc scargs
1069 -- add SCG later, when checking totality
1107 -- add SCG later, when checking totality
1070− let cg = CGInfo scargs' calls [] used []
1108+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore
1071 logLvl 2 $ "Called names: " ++ show cg
1109 logLvl 2 $ "Called names: " ++ show cg
1072 addToCG n cg
1110 addToCG n cg
1073 addToCalledG n (nub (map fst calls)) -- plus names in type!
1111 addToCalledG n (nub (map fst calls)) -- plus names in type!
@@ -1288,7 +1326,7 @@ checkPossible info fc tcgen fname lhs_in
1288 ((P _ x _, _), (P _ y _, _)) -> x == y
1326 ((P _ x _, _), (P _ y _, _)) -> x == y
1289 _ -> False
1327 _ -> False
1291−getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)
1329+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
1292 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1330 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1293getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1331getFixedInType i env (_ : is) (Bind n (Pi t) sc)
1294 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
1332 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
@@ -1350,16 +1388,19 @@ propagateParams ps t (PRef fc n)
1350 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1388 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1351propagateParams ps t x = x
1389propagateParams ps t x = x
1391+-- Return the elaborated LHS/RHS, and the original LHS with implicits added
1353elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1392elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1354− Idris (Either Term (Term, Term))
1393+ Idris (Either Term (Term, Term), PTerm)
1355elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1394elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1356 = do let tcgen = Dictionary `elem` opts
1395 = do let tcgen = Dictionary `elem` opts
1397+ let lhs = addImpl i lhs_in
1357 b <- checkPossible info fc tcgen fname lhs_in
1398 b <- checkPossible info fc tcgen fname lhs_in
1358 case b of
1399 case b of
1359 True -> tclift $ tfail (At fc
1400 True -> tclift $ tfail (At fc
1360 (Msg $ show lhs_in ++ " is a valid case"))
1401 (Msg $ show lhs_in ++ " is a valid case"))
1361 False -> do ptm <- mkPatTm lhs_in
1402 False -> do ptm <- mkPatTm lhs_in
1362− return (Left ptm)
1403+ return (Left ptm, lhs)
1363elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1404elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1364 = do let tcgen = Dictionary `elem` opts
1405 = do let tcgen = Dictionary `elem` opts
1365 ctxt <- getContext
1406 ctxt <- getContext
@@ -1416,10 +1457,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1416 -- Elaborate where block
1457 -- Elaborate where block
1417 ist <- getIState
1458 ist <- getIState
1418 windex <- getName
1459 windex <- getName
1419− let winfo = pinfo (pvars ist lhs_tm) whereblock windex
1420 let decls = nub (concatMap declared whereblock)
1460 let decls = nub (concatMap declared whereblock)
1421 let defs = nub (decls ++ concatMap defined whereblock)
1461 let defs = nub (decls ++ concatMap defined whereblock)
1422 let newargs = pvars ist lhs_tm
1462 let newargs = pvars ist lhs_tm
1463+ let winfo = pinfo info newargs defs windex
1423 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1464 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
1425 -- Split the where block into declarations with a type, and those
1466 -- Split the where block into declarations with a type, and those
@@ -1428,7 +1469,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1428 let (wbefore, wafter) = sepBlocks wb
1469 let (wbefore, wafter) = sepBlocks wb
1430 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1471 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1431− mapM_ (elabDecl' EAll info) wbefore
1472+ mapM_ (elabDecl' EAll winfo) wbefore
1432 -- Now build the RHS, using the type of the LHS as the goal.
1473 -- Now build the RHS, using the type of the LHS as the goal.
1433 i <- getIState -- new implicits from where block
1474 i <- getIState -- new implicits from where block
1434 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1475 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
@@ -1443,7 +1484,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1443 mapM_ setinj (nub (params ++ inj))
1484 mapM_ setinj (nub (params ++ inj))
1444 setNextName
1485 setNextName
1445 (_, _, is) <- errAt "right hand side of " fname
1486 (_, _, is) <- errAt "right hand side of " fname
1446− (erun fc (build i info False opts fname rhs))
1487+ (erun fc (build i winfo False opts fname rhs))
1447 errAt "right hand side of " fname
1488 errAt "right hand side of " fname
1448 (erun fc $ psolve lhs_tm)
1489 (erun fc $ psolve lhs_tm)
1449 hs <- get_holes
1490 hs <- get_holes
@@ -1471,8 +1512,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1471 -- Now the remaining deferred (i.e. no type declarations) clauses
1512 -- Now the remaining deferred (i.e. no type declarations) clauses
1472 -- from the where block
1513 -- from the where block
1474− mapM_ (elabDecl' EAll info) wafter
1515+ mapM_ (elabDecl' EAll winfo) wafter
1475− mapM_ (elabCaseBlock info opts) is
1516+ mapM_ (elabCaseBlock winfo opts) is
1477 ctxt <- getContext
1518 ctxt <- getContext
1478 logLvl 5 $ "Rechecking"
1519 logLvl 5 $ "Rechecking"
@@ -1500,8 +1541,21 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1500 when (rev || ErrorReverse `elem` opts) $ do
1541 when (rev || ErrorReverse `elem` opts) $ do
1501 addIBC (IBCErrRev (crhs, clhs))
1542 addIBC (IBCErrRev (crhs, clhs))
1502 addErrRev (crhs, clhs)
1543 addErrRev (crhs, clhs)
1503− return $ Right (clhs, crhs)
1544+ return $ (Right (clhs, crhs), lhs)
1546+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
1548+ = let newps = params info ++ ns
1549+ dsParams = map (\n -> (n, map fst newps)) ds
1550+ newb = addAlist dsParams (inblock info)
1551+ l = liftname info in
1552+ info { params = newps,
1554+ liftname = id -- (\n -> case lookupCtxt n newb of
1556+ -- _ -> MN i (show n)) . l
1505 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1559 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
1506 mkLHSapp t = t
1560 mkLHSapp t = t
@@ -1524,19 +1578,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1524 (b : bf, af)
1578 (b : bf, af)
1525 sepBlocks' ns [] = ([], [])
1579 sepBlocks' ns [] = ([], [])
1528− = let ds = concatMap declared ps
1529− newps = params info ++ ns
1530− dsParams = map (\n -> (n, map fst newps)) ds
1531− newb = addAlist dsParams (inblock info)
1532− l = liftname info in
1533− info { params = newps,
1535− liftname = id -- (\n -> case lookupCtxt n newb of
1537− -- _ -> MN i (show n)) . l
1541 -- if a hole is just an argument/result of a case block, treat it as
1582 -- if a hole is just an argument/result of a case block, treat it as
1542 -- the unit type. Hack to help elaborate case in do blocks.
1583 -- the unit type. Hack to help elaborate case in do blocks.
@@ -1667,7 +1708,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1667 mapM_ (elabCaseBlock info opts) is
1708 mapM_ (elabCaseBlock info opts) is
1668 logLvl 5 ("Checked RHS " ++ show rhs')
1709 logLvl 5 ("Checked RHS " ++ show rhs')
1669 (crhs, crhsty) <- recheckC fc [] rhs'
1710 (crhs, crhsty) <- recheckC fc [] rhs'
1670− return $ Right (clhs, crhs)
1711+ return $ (Right (clhs, crhs), lhs)
1672 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
1713 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
1673 getImps _ = []
1714 getImps _ = []
@@ -1801,7 +1842,7 @@ elabClass info syn doc fc constraints tn ps ds
1802 getMName (PTy _ _ _ _ _ n _) = nsroot n
1843 getMName (PTy _ _ _ _ _ n _) = nsroot n
1803 tdecl allmeths (PTy doc _ syn _ o n t)
1844 tdecl allmeths (PTy doc _ syn _ o n t)
1804− = do t' <- implicit' syn allmeths n t
1845+ = do t' <- implicit' info syn allmeths n t
1805 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1846 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1806 return ( (n, (toExp (map fst ps) Exp t')),
1847 return ( (n, (toExp (map fst ps) Exp t')),
1807 (n, (doc, o, (toExp (map fst ps) Imp t'))),
1848 (n, (doc, o, (toExp (map fst ps) Imp t'))),
@@ -2005,7 +2046,8 @@ elabInstance info syn what fc cs n ps t expn ds = do
2005 -- TODO: largely based upon elabType' - should try to abstract
2046 -- TODO: largely based upon elabType' - should try to abstract
2006 elabFindOverlapping i ci iname syn t
2047 elabFindOverlapping i ci iname syn t
2007 = do ty' <- addUsingConstraints syn fc t
2048 = do ty' <- addUsingConstraints syn fc t
2049+ -- TODO think: something more in info?
2008− ty' <- implicit syn iname ty'
2050+ ty' <- implicit info syn iname ty'
2009 let ty = addImpl i ty'
2051 let ty = addImpl i ty'
2010 ctxt <- getContext
2052 ctxt <- getContext
2011 ((tyT, _, _), _) <-
2053 ((tyT, _, _), _) <-
@@ -2043,9 +2085,9 @@ elabInstance info syn what fc cs n ps t expn ds = do
2043 methArgs i (PPi (Imp _ _ _) n ty sc)
2085 methArgs i (PPi (Imp _ _ _) n ty sc)
2044 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2086 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2045 methArgs i (PPi (Exp _ _ _) n ty sc)
2087 methArgs i (PPi (Exp _ _ _) n ty sc)
2046− = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2088+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
2047 methArgs i (PPi (Constraint _ _) n ty sc)
2089 methArgs i (PPi (Constraint _ _) n ty sc)
2048− = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc
2090+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
2049 methArgs i _ = []
2091 methArgs i _ = []
2051 papp fc f [] = f
2093 papp fc f [] = f
@@ -2061,7 +2103,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
2061 _ -> return ps'
2103 _ -> return ps'
2062 getWParams (_ : ps) = getWParams ps
2104 getWParams (_ : ps) = getWParams ps
2064− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2106+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2107 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2067 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
2109 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t