Some micro-optimisations

Removing some unnecessary ++ and name lookups. Not really that
significant, but doing them anyway.

Author: edwinb

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)
 

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

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'

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