a5cb996 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1663 from edwinb/partial-eval

Propagate static flags into with blocks

commita5cb99639d609816a24b281f6def50907aca8725 authorEdwin Brady <edwin.brady@gmail.com> dateSun 19 Oct 2014, 01:15 (12 years ago) parent1dea97b a33670b

3 files changed+34−4

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+16−2 src/Idris/Elab/Utils.hs+17 src/Idris/PartialEval.hs+1−2

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

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

774774 let lhs_tm = orderPats (getInferTerm lhs')

775775 let lhs_ty = getInferType lhs'

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

777− logLvl 3 (show lhs_tm)

777+ let static_names = getStaticNames i lhs_tm

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

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

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

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

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

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

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

802803 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)

804805 let pvars = map fst (getPBtys cwvalty)

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

806807 -- rather than a de Bruijn index.

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

824825

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

826827 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+

827833 addIBC (IBCDef wname)

834+ addIBC (IBCImp wname)

835+ addIBC (IBCStatic wname)

836+

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

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

830839 addDeferred def''

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

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

867876 getImps _ = []

868877

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

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

880+ | otherwise = False : getStatics ns t

881+ getStatics _ _ = []

882+

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

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

871885 return $ PClauses fc o wname cs'

src/Idris/Elab/Utils.hs+17

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

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

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

237237

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+

238255

src/Idris/PartialEval.hs+1−2

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

267267 ga env f ++ ga env a ++

268268 case (lookupCtxt n (idris_statics ist),

269269 lookupCtxt n (idris_implicits ist)) of

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

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

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

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

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

274273 args -> [(n, args)]

275274-- _ -> []