From f303e469fb6853d05e7ae24b3522fb2e8c462da8 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 17 Jul 2020 15:18:23 +0100 Subject: [PATCH] Improve elaborator reflection performance In a 'Bind', normalise the result of the first action, rather than quoting the HNF. This improves performance since the HNF could be quite big when quoted back. Ideally, we wouldn't have to quote and unquote here, and we can probably achieve this by tinkering with the evaluator. This has an unfortunate effect on the reflection002 test, in that the "typed template Idris" example now evaluates too much. But, I think the overall performance is too important for the primary motivation behind elaborator reflection. I will return to this! --- libs/base/Language/Reflection.idr | 21 +++++++++++++-- src/Core/LinearCheck.idr | 2 +- src/TTImp/Elab/RunElab.idr | 7 +++-- tests/Main.idr | 1 + tests/idris2/reflection002/expected | 2 +- tests/idris2/reflection002/power.idr | 7 +++-- tests/idris2/reflection009/expected | 13 ++++++++++ tests/idris2/reflection009/perf.idr | 39 ++++++++++++++++++++++++++++ tests/idris2/reflection009/run | 3 +++ 9 files changed, 85 insertions(+), 10 deletions(-) create mode 100644 tests/idris2/reflection009/expected create mode 100644 tests/idris2/reflection009/perf.idr create mode 100755 tests/idris2/reflection009/run diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index fbb3af805..3f6a7ee16 100644 --- a/libs/base/Language/Reflection.idr +++ b/libs/base/Language/Reflection.idr @@ -3,8 +3,9 @@ module Language.Reflection import public Language.Reflection.TT import public Language.Reflection.TTImp --- Elaboration scripts. Where types/terms are returned, binders will have --- unique, if not necessarily human readabe, names +||| Elaboration scripts +||| Where types/terms are returned, binders will have unique, if not +||| necessarily human readabe, names export data Elab : Type -> Type where Pure : a -> Elab a @@ -61,18 +62,22 @@ mutual Monad Elab where (>>=) = Bind +||| Report an error in elaboration export fail : String -> Elab a fail = Fail +||| Write a log message, if the log level is >= the given level export logMsg : Nat -> String -> Elab () logMsg = LogMsg +||| Write a log message and a rendered term, if the log level is >= the given level export logTerm : Nat -> String -> TTImp -> Elab () logTerm = LogTerm +||| Log the current goal type, if the log level is >= the given level export logGoal : Nat -> String -> Elab () logGoal n msg @@ -81,48 +86,60 @@ logGoal n msg Nothing => pure () Just t => logTerm n msg t +||| Check that some TTImp syntax has the expected type +||| Returns the type checked value export check : {expected : Type} -> TTImp -> Elab expected check = Check +||| Return TTImp syntax of a given value export quote : val -> Elab TTImp quote = Quote +||| Build a lambda expression export lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val)) lambda = Lambda +||| Get the goal type of the current elaboration export goal : Elab (Maybe TTImp) goal = Goal +||| Get the names of the local variables in scope export localVars : Elab (List Name) localVars = LocalVars +||| Generate a new unique name export genSym : String -> Elab Name genSym = GenSym +||| Given a name, return the name decorated with the current namespace export inCurrentNS : Name -> Elab Name inCurrentNS = InCurrentNS +||| Given a possibly ambiguous name, get all the matching names and their types export getType : Name -> Elab (List (Name, TTImp)) getType = GetType +||| Get the type of a local variable export getLocalType : Name -> Elab TTImp getLocalType = GetLocalType +||| Get the constructors of a fully qualified data type name export getCons : Name -> Elab (List Name) getCons = GetCons +||| Make some top level declarations export declare : List Decl -> Elab () declare = Declare diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index fb2021ee7..29e05c549 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -368,7 +368,7 @@ mutual NDelayed _ r narg => do defs <- get Ctxt pure (TForce fc r val', glueBack defs env narg, u) - _ => throw (GenericMsg fc "Not a delayed tyoe") + _ => throw (GenericMsg fc "Not a delayed type") lcheck rig erase env (PrimVal fc c) = pure (PrimVal fc c, gErased fc, []) lcheck rig erase env (Erased fc i) diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 3ccd54c34..cc0789fbd 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -55,10 +55,9 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp !(evalClosure defs act) exp case !(evalClosure defs k) of NBind _ x (Lam _ _ _) sc => - do empty <- clearDefs defs - elabScript fc nest env - !(sc defs (toClosure withAll env - !(quote empty env act'))) exp + elabScript fc nest env + !(sc defs (toClosure withAll env + !(quote defs env act'))) exp _ => failWith defs elabCon defs "Fail" [_,msg] = do msg' <- evalClosure defs msg diff --git a/tests/Main.idr b/tests/Main.idr index 35b85222b..fee8e28a3 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -96,6 +96,7 @@ idrisTests -- Quotation and reflection "reflection001", "reflection002", "reflection003", "reflection004", "reflection005", "reflection006", "reflection007", "reflection008", + "reflection009", -- Miscellaneous regressions "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007", "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", diff --git a/tests/idris2/reflection002/expected b/tests/idris2/reflection002/expected index 361def40a..a08ce16a8 100644 --- a/tests/idris2/reflection002/expected +++ b/tests/idris2/reflection002/expected @@ -3,6 +3,6 @@ Main> Main.cube : Nat -> Nat cube = \x => mult x (mult x (mult x (const (fromInteger 1) x))) Main> 27 Main> Main.cube' : Nat -> Nat -cube' = \x => mult (mult (mult (const (fromInteger 1) x) x) x) x +cube' = \x => mult (mult (plus x 0) x) x Main> 27 Main> Bye for now! diff --git a/tests/idris2/reflection002/power.idr b/tests/idris2/reflection002/power.idr index 2ed97847d..cfa9408b0 100644 --- a/tests/idris2/reflection002/power.idr +++ b/tests/idris2/reflection002/power.idr @@ -6,10 +6,13 @@ powerFn : Nat -> TTImp powerFn Z = `(const 1) powerFn (S k) = `(\x => mult x (~(powerFn k) x)) +-- Note: this example doesn't quite do what we want yet. Ideally, we'd find +-- a way to block reduction under the 'pure' while running the script powerFn' : Nat -> Elab (Nat -> Nat) powerFn' Z = pure (const 1) -powerFn' (S k) = do powerk <- powerFn' k - pure (\x => mult (powerk x) x) +powerFn' (S k) + = do powerk <- powerFn' k + pure (\x => mult (powerk x) x) %macro power : Nat -> Elab (Nat -> Nat) diff --git a/tests/idris2/reflection009/expected b/tests/idris2/reflection009/expected new file mode 100644 index 000000000..3268f0ca8 --- /dev/null +++ b/tests/idris2/reflection009/expected @@ -0,0 +1,13 @@ +1/1: Building perf (perf.idr) +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress +LOG 0: Progress diff --git a/tests/idris2/reflection009/perf.idr b/tests/idris2/reflection009/perf.idr new file mode 100644 index 000000000..843063446 --- /dev/null +++ b/tests/idris2/reflection009/perf.idr @@ -0,0 +1,39 @@ +module Main + +import Language.Reflection + +%language ElabReflection + +-- A performance test - previously this was slowing down hugely due to +-- quoting back HNFs on >>=, and as the environment gets bigger, the +-- environment of holes gets bigger and bigger, so quoting can start to take +-- far too long +perftest : Elab () +perftest = do + logMsg 0 "Progress" + traverse (traverse (logMsg 1 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 2 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 3 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 4 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 5 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 6 . show)) [[the Int 1..10]] -- minor difference + logMsg 0 "Progress" + traverse (traverse (logMsg 7 . show)) [[the Int 1..10]] -- 0.3s + logMsg 0 "Progress" + traverse (traverse (logMsg 8 . show)) [[the Int 1..10]] -- 0.4s + logMsg 0 "Progress" + traverse (traverse (logMsg 9 . show)) [[the Int 1..10]] -- 0.5s + logMsg 0 "Progress" + traverse (traverse (logMsg 10 . show)) [[the Int 1..10]] -- 1.5s + logMsg 0 "Progress" + traverse (traverse (logMsg 11 . show)) [[the Int 1..10]] -- 4s + logMsg 0 "Progress" + traverse (traverse (logMsg 12 . show)) [[the Int 1..10]] -- 13s + pure () + +%runElab perftest diff --git a/tests/idris2/reflection009/run b/tests/idris2/reflection009/run new file mode 100755 index 000000000..2e60ba8e0 --- /dev/null +++ b/tests/idris2/reflection009/run @@ -0,0 +1,3 @@ +$1 --check perf.idr + +rm -rf build