ef0ce29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Set a limit on partial evaluation depth

There's reasonable situations where it could go forever if unchecked, such as interfaces on nested types, where it won't stop because it needs to specialise for each level of nesting. This limit stops it elaborating forever. Ideally it would also be looking for whether it had partially evaluated the specific function - this limit may be a bit limiting for partially evaluated DSLs. Fixes #3191

commitef0ce29e1101f43db9585dc09c6160e7b778f20e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 31 May 2016, 01:53 (10 years ago) parent4d00ed4

4 files changed+15−5

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Elab/Clause.hs+10−2 src/Idris/Elab/Term.hs+2−1 src/Idris/ElabDecls.hs+1−1

src/Idris/AbsSyntaxTree.hs+2−1

@@ -67,6 +67,7 @@ data ElabInfo = EInfo {

6767 , liftname :: Name -> Name

6868 , namespace :: Maybe [String]

6969 , elabFC :: Maybe FC

70+ , pe_depth :: Int

7071

7172 -- | We may, recursively, collect transformations to do on the rhs,

7273 -- e.g. rewriting recursive calls to functions defined by 'with'

@@ -75,7 +76,7 @@ data ElabInfo = EInfo {

7576 }

7677

7778toplevel :: ElabInfo

78−toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")

79+toplevel = EInfo [] emptyContext id Nothing Nothing 0 id (\_ _ _ -> fail "Not implemented")

7980

8081eInfoNames :: ElabInfo -> [Name]

8182eInfoNames info = map fst (params info) ++ M.keys (inblock info)

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

@@ -348,6 +348,13 @@ elabClauses info' fc opts n_in cs =

348348-- | Find 'static' applications in a term and partially evaluate them.

349349-- Return any new transformation rules

350350elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

351+-- Don't go deeper than 5 nested partially evaluated definitions in one go

352+-- (make this configurable? It's a good limit for most cases, certainly for

353+-- interfaces and polymorphic definitions, but maybe not for DSLs and

354+-- interpreters in complicated cases.

355+-- Possibly only worry about the limit if we've specialised the same function

356+-- a number of times in one go.)

357+elabPE info fc caller r | pe_depth info > 5 = return []

351358elabPE info fc caller r =

352359 do ist <- getIState

353360 let sa = filter (\ap -> fst ap /= caller) $ getSpecApps ist [] r

@@ -399,7 +406,7 @@ elabPE info fc caller r =

399406 logElab 3 $ "New name: " ++ show newnm

400407 logElab 3 $ "PE definition type : " ++ (show specTy)

401408 ++ "\n" ++ show opts

402− logElab 3 $ "PE definition " ++ show newnm ++ ":\n" ++

409+ logElab 5 $ "PE definition " ++ show newnm ++ ":\n" ++

403410 showSep "\n"

404411 (map (\ (lhs, rhs) ->

405412 (showTmImpls lhs ++ " = " ++

@@ -414,7 +421,8 @@ elabPE info fc caller r =

414421 PClause fc newnm lhs' [] rhs [])

415422 (pe_clauses specdecl)

416423 trans <- elabTransform info fc False rhs lhs

417− elabClauses info fc (PEGenerated:opts) newnm def

424+ elabClauses (info {pe_depth = pe_depth info + 1}) fc

425+ (PEGenerated:opts) newnm def

418426 return [trans]

419427 else return [])

420428 -- if it doesn't work, just don't specialise. Could happen for lots

src/Idris/Elab/Term.hs+2−1

@@ -2719,7 +2719,8 @@ processTacticDecls info steps =

27192719 cty (_, _, t) = t

27202720 addIBC (IBCDef tyn)

27212721 mapM_ (addIBC . IBCDef . cn) ctors

2722− let params = findParams tyn tyconTy (map cty ctors)

2722+ ctxt <- getContext

2723+ let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)

27232724 let typeInfo = TI (map cn ctors) False [] params []

27242725 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.

27252726 -- otherwise writing the IBC just fails silently!

src/Idris/ElabDecls.hs+1−1

@@ -72,7 +72,7 @@ import Util.Pretty(pretty, text)

7272

7373-- | Top level elaborator info, supporting recursive elaboration

7474recinfo :: ElabInfo

75−recinfo = EInfo [] emptyContext id Nothing Nothing id elabDecl'

75+recinfo = EInfo [] emptyContext id Nothing Nothing 0 id elabDecl'

7676

7777-- | Return the elaborated term which calls 'main'

7878elabMain :: Idris Term