a33670b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Propagate static flags into with blocks

a33670bEdwin Brady12 years ago

src/Idris/Elab/Clause.hs+16−2

compare with master

unifiedsplit

@@ -774,7 +774,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

774 let lhs_tm = orderPats (getInferTerm lhs')

775 let lhs_ty = getInferType lhs'

776 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

777+ let static_names = getStaticNames i lhs_tm

777− logLvl 3 (show lhs_tm)

778+ logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

778 (clhs, clhsty) <- recheckC fc [] lhs_tm

779 (clhs, clhsty) <- recheckC fc [] lhs_tm

779 logLvl 5 ("Checked " ++ show clhs)

780 logLvl 5 ("Checked " ++ show clhs)

780 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

781 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

@@ -800,7 +801,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

800 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

801 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

801 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

802 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

802 let cwvalN = explicitNames (normalise ctxt [] cwval)

803 let cwvalN = explicitNames (normalise ctxt [] cwval)

803− logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

804+ logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

804 let pvars = map fst (getPBtys cwvalty)

805 let pvars = map fst (getPBtys cwvalty)

805 -- we need the unelaborated term to get the names it depends on

806 -- we need the unelaborated term to get the names it depends on

806 -- rather than a de Bruijn index.

807 -- rather than a de Bruijn index.

@@ -824,7 +825,15 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

824

825

825 let imps = getImps wtype -- add to implicits context

826 let imps = getImps wtype -- add to implicits context

826 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

827 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

828+ let statics = getStatics static_names wtype

829+ logLvl 5 ("Static positions " ++ show statics)

830+ i <- getIState

831+ putIState (i { idris_statics = addDef wname statics (idris_statics i) })

832+

827 addIBC (IBCDef wname)

833 addIBC (IBCDef wname)

834+ addIBC (IBCImp wname)

835+ addIBC (IBCStatic wname)

836+

828 def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

837 def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

829 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

838 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

830 addDeferred def''

839 addDeferred def''

@@ -866,6 +875,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

866 getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

875 getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

867 getImps _ = []

876 getImps _ = []

868

877

878+ getStatics ns (Bind n (Pi _ _) t)

879+ | n `elem` ns = True : getStatics ns t

880+ | otherwise = False : getStatics ns t

881+ getStatics _ _ = []

882+

869 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

883 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

870 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

884 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

871 return $ PClauses fc o wname cs'

885 return $ PClauses fc o wname cs'

src/Idris/Elab/Utils.hs+17

@@ -235,4 +235,21 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

235 getUniqB env us (NLet t v) = do getUniq env us t; getUniq env us v

236 getUniqB env us b = getUniq env us (binderTy b)

237

238+-- In a functional application, return the names which are used

239+-- directly in a static position

240+getStaticNames :: IState -> Term -> [Name]

241+getStaticNames ist (Bind n (PVar _) sc)

242+ = getStaticNames ist (instantiate (P Bound n Erased) sc)

243+getStaticNames ist tm

244+ | (P _ fn _, args) <- unApply tm

245+ = case lookupCtxtExact fn (idris_statics ist) of

246+ Just stpos -> getStatics args stpos

247+ _ -> []

248+ where

249+ getStatics (P _ n _ : as) (True : ss) = n : getStatics as ss

250+ getStatics (_ : as) (_ : ss) = getStatics as ss

251+ getStatics _ _ = []

252+getStaticNames _ _ = []

253+

254+

238

255

src/Idris/PartialEval.hs+1−2

@@ -267,9 +267,8 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

267 ga env f ++ ga env a ++

268 case (lookupCtxt n (idris_statics ist),

269 lookupCtxt n (idris_implicits ist)) of

270− ([statics], [imps]) ->

270+ ([statics], [imps]) ->

271 if (length statics == length args && or statics) then

272−-- trace (show (n, statics, imps, args)) $

273 case buildApp env statics imps args [0..] of

272 case buildApp env statics imps args [0..] of

274 args -> [(n, args)]

273 args -> [(n, args)]

275-- _ -> []

274-- _ -> []