From 5ac441ac05046f8a3be19568deed1ebc7fb16262 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 16 May 2021 15:10:05 +0100
Subject: [PATCH] Some micro-optimisations

Removing some unnecessary ++ and name lookups. Not really that
significant, but doing them anyway.
---
 src/Core/CaseBuilder.idr | 4 ++++
 src/Core/Normalise.idr   | 7 +++++--
 src/Core/Unify.idr       | 2 +-
 src/TTImp/Elab/App.idr   | 2 +-
 4 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr
index 26780f7c5..62b27c967 100644
--- a/src/Core/CaseBuilder.idr
+++ b/src/Core/CaseBuilder.idr
@@ -194,6 +194,10 @@ Weaken ArgType where
   weaken (Stuck fty) = Stuck (weaken fty)
   weaken Unknown = Unknown
 
+  weakenNs s (Known c ty) = Known c (weakenNs s ty)
+  weakenNs s (Stuck fty) = Stuck (weakenNs s fty)
+  weakenNs s Unknown = Unknown
+
 Weaken (PatInfo p) where
   weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty)
 
diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index c39f5d72b..b241cfbc1 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -216,8 +216,11 @@ parameters (defs : Defs, topopts : EvalOpts)
                FC -> Name -> Int -> List (Closure free) ->
                Stack free -> Core (NF free)
     evalMeta env fc nm i args stk
-        = evalRef env True fc Func (Resolved i) (map (EmptyFC,) args ++ stk)
-                  (NApp fc (NMeta nm i args) stk)
+        = let args' = if isNil stk then map (EmptyFC,) args
+                         else map (EmptyFC,) args ++ stk
+                        in
+              evalRef env True fc Func (Resolved i) args'
+                          (NApp fc (NMeta nm i args) stk)
 
     -- The commented out logging here might still be useful one day, but
     -- evalRef is used a lot and even these tiny checks turn out to be
diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
index 1ab9482c5..ff62a2c72 100644
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@@ -865,7 +865,7 @@ mutual
   unifyHole swap mode loc env fc mname mref margs margs' tmnf
       = do defs <- get Ctxt
            empty <- clearDefs defs
-           let args = margs ++ margs'
+           let args = if isNil margs' then margs else margs ++ margs'
            logC "unify.hole" 10
                    (do args' <- traverse (evalArg empty) args
                        qargs <- traverse (quote empty env) args'
diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index 6b011b17d..bef599672 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -69,7 +69,7 @@ getNameType rigc env fc x
                  [(pname, i, def)] <- lookupCtxtName x (gamma defs)
                       | [] => undefinedName fc x
                       | ns => throw (AmbiguousName fc (map fst ns))
-                 checkVisibleNS fc !(getFullName pname) (visibility def)
+                 checkVisibleNS fc (fullname def) (visibility def)
                  rigSafe (multiplicity def) rigc
                  let nt = case definition def of
                                PMDef _ _ _ _ _ => Func