ef0ce29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Set a limit on partial evaluation depth

ef0ce29Edwin Brady10 years ago

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

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

67 , liftname :: Name -> Name

68 , namespace :: Maybe [String]

69 , elabFC :: Maybe FC

70+ , pe_depth :: Int

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

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

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

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

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

75 }

76 }

77toplevel :: ElabInfo

78toplevel :: ElabInfo

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

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

80eInfoNames :: ElabInfo -> [Name]

81eInfoNames :: ElabInfo -> [Name]

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

82eInfoNames 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 =

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

349-- Return any new transformation rules

350elabPE :: 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 []

351elabPE info fc caller r =

358elabPE info fc caller r =

352 do ist <- getIState

359 do ist <- getIState

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

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

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

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

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

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

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

401 ++ "\n" ++ show opts

408 ++ "\n" ++ show opts

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

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

403 showSep "\n"

410 showSep "\n"

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

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

405 (showTmImpls lhs ++ " = " ++

412 (showTmImpls lhs ++ " = " ++

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

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

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

415 (pe_clauses specdecl)

422 (pe_clauses specdecl)

416 trans <- elabTransform info fc False rhs lhs

423 trans <- elabTransform info fc False rhs lhs

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

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

425+ (PEGenerated:opts) newnm def

418 return [trans]

426 return [trans]

419 else return [])

427 else return [])

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

428 -- 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 =

2719 cty (_, _, t) = t

2720 addIBC (IBCDef tyn)

2721 mapM_ (addIBC . IBCDef . cn) ctors

2722+ ctxt <- getContext

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

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

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

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

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

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

2725 -- otherwise writing the IBC just fails silently!

2726 -- otherwise writing the IBC just fails silently!

src/Idris/ElabDecls.hs+1−1

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

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

74recinfo :: ElabInfo

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

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

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

78elabMain :: Idris Term