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

@@ -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

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)

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
+                                              !(quote defs env act'))) exp
                   _ => failWith defs
     elabCon defs "Fail" [_,msg]
         = do msg' <- evalClosure defs msg

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",

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!

tests/idris2/reflection002/power.idr

@@ -6,9 +6,12 @@ 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
+powerFn' (S k)
+    = do powerk <- powerFn' k
          pure (\x => mult (powerk x) x)
 
 %macro

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

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

tests/idris2/reflection009/run

@@ -0,0 +1,3 @@
+$1 --check perf.idr
+
+rm -rf build