Some small performances improvements

The biggest one being that logging wasn't taking the String as a lazy
argument!

src/Core/Core.idr

@@ -433,7 +433,7 @@ cond [] def = def
 cond ((x, y) :: xs) def = if x then y else cond xs def
 
 export
-log : Nat -> String -> Core ()
+log : Nat -> Lazy String -> Core ()
 log lvl msg
     = do opts <- getOpts
          if logLevel opts >= lvl

src/Core/LinearCheck.idr

@@ -26,10 +26,6 @@ Show (Usage vars) where
       showAll [el] = show el
       showAll (x :: xs) = show x ++ ", " ++ show xs
 
-Weaken Usage where
-  weaken [] = []
-  weaken (MkVar x :: xs) = MkVar (Later x) :: weaken xs
-
 doneScope : Usage (n :: vars) -> Usage vars
 doneScope [] = []
 doneScope (MkVar First :: xs) = doneScope xs

src/Core/Normalise.idr

@@ -39,6 +39,10 @@ evalWithOpts : {vars : _} ->
 export
 evalClosure : Defs -> Closure free -> Core (NF free)
 
+export
+evalArg : Defs -> (AppInfo, Closure free) -> Core (NF free)
+evalArg defs (p, c) = evalClosure defs c
+
 export
 toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer
 toClosure opts env tm = MkClosure opts [] env tm
@@ -107,12 +111,18 @@ parameters (defs : Defs, topopts : EvalOpts)
                 Stack free ->
                 Core (NF free)
     evalLocal {vars = []} env locs fc mrig idx prf stk
-        = case getBinder prf env of
-               Let _ val _ => 
-                   if not (holesOnly topopts || argHolesOnly topopts)
-                      then eval env [] val stk
-                      else pure $ NApp fc (NLocal mrig idx prf) stk
-               _ => pure $ NApp fc (NLocal mrig idx prf) stk
+        = if not (holesOnly topopts || argHolesOnly topopts) && isLet idx env
+             then
+               case getBinder prf env of
+                    Let _ val _ => eval env [] val stk
+                    _ => pure $ NApp fc (NLocal mrig idx prf) stk
+             else pure $ NApp fc (NLocal mrig idx prf) stk
+      where
+        isLet : Nat -> Env tm vars -> Bool
+        isLet Z (Let _ _ _ :: env) = True
+        isLet Z _ = False
+        isLet (S k) (b :: env) = isLet k env
+        isLet (S k) [] = False
     evalLocal env (MkClosure opts locs' env' tm' :: locs) fc mrig Z First stk
         = evalWithOpts defs opts env' locs' tm' stk
     evalLocal {free} {vars = x :: xs} 
@@ -573,9 +583,9 @@ interface Convert (tm : List Name -> Type) where
 
 mutual
   allConv : Ref QVar Int -> Defs -> Env Term vars ->
-            List (Closure vars) -> List (Closure vars) -> Core Bool
+            List (a, Closure vars) -> List (a, Closure vars) -> Core Bool
   allConv q defs env [] [] = pure True
-  allConv q defs env (x :: xs) (y :: ys)
+  allConv q defs env ((_, x) :: xs) ((_, y) :: ys)
       = pure $ !(convGen q defs env x y) && !(allConv q defs env xs ys)
   allConv q defs env _ _ = pure False
 
@@ -585,7 +595,7 @@ mutual
   chkConvHead q defs env (NRef _ n) (NRef _ n') = pure $ n == n'
   chkConvHead q defs env (NMeta n i args) (NMeta n' i' args') 
      = if i == i'
-          then allConv q defs env (map snd args) (map snd args')
+          then allConv q defs env args args'
           else pure False
   chkConvHead q defs env _ _ = pure False
 
@@ -639,16 +649,16 @@ mutual
 
     convGen q defs env (NApp _ val args) (NApp _ val' args')
         = if !(chkConvHead q defs env val val')
-             then allConv q defs env (map snd args) (map snd args')
+             then allConv q defs env args args'
              else pure False
 
     convGen q defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
         = if tag == tag'
-             then allConv q defs env (map snd args) (map snd args')
+             then allConv q defs env args args'
              else pure False
     convGen q defs env (NTCon _ nm tag _ args) (NTCon _ nm' tag' _ args')
         = if nm == nm'
-             then allConv q defs env (map snd args) (map snd args')
+             then allConv q defs env args args'
              else pure False
     convGen q defs env (NAs _ _ tm) (NAs _ _ tm')
         = convGen q defs env tm tm'

src/Core/Unify.idr

@@ -208,13 +208,13 @@ toSubVars (n :: ns) xs
 patternEnv : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {vars : _} ->
-             Env Term vars -> List (Closure vars) -> 
+             Env Term vars -> List (AppInfo, Closure vars) -> 
              Core (Maybe (newvars ** (List (Var newvars),
                                      SubVars newvars vars)))
 patternEnv env args
     = do defs <- get Ctxt
          empty <- clearDefs defs
-         args' <- traverse (evalClosure empty) args
+         args' <- traverse (evalArg empty) args
          case getVars args' of
               Nothing => pure Nothing
               Just vs => 
@@ -393,12 +393,12 @@ mutual
       = do defs <- get Ctxt
            empty <- clearDefs defs
            let args = margs ++ margs'
-           logC 10 (do args' <- traverse (evalClosure empty) (map snd args)
+           logC 10 (do args' <- traverse (evalArg empty) args
                        qargs <- traverse (quote empty env) args'
                        qtm <- quote empty env tmnf
                        pure $ "Unifying: " ++ show mname ++ " " ++ show qargs ++
                               " with " ++ show qtm)
-           case !(patternEnv env (map snd args)) of
+           case !(patternEnv env args) of
                 Nothing => unifyPatVar mode loc env mname mref args tmnf
                 Just (newvars ** (locs, submv)) => 
                   do tm <- quote empty env tmnf

src/TTImp/Elab/App.idr

@@ -202,7 +202,7 @@ mutual
                                    (gnfOpts withHoles (letToLam env) argv)
                         pure ()
                   _ => pure ()
-             removeHoleName nm
+             removeHole idx
              pure (tm, gty)
            else do
              logNF 10 ("Argument type " ++ show x) env aty

src/TTImp/Elab/Check.idr

@@ -460,7 +460,9 @@ convert fc elabinfo env x y
                 = case elabMode elabinfo of
                        InLHS _ => InLHS
                        _ => InTerm in
-          catch (do vs <- unify umode fc env !(getNF x) !(getNF y)
+          catch (do logGlue 10 "Unify" env x
+                    logGlue 10 ".....with" env y
+                    vs <- unify umode fc env !(getNF x) !(getNF y)
                     when (holesSolved vs) $
                       solveConstraints umode Normal
                     pure (constraints vs))

src/TTImp/Elab/Term.idr

@@ -37,7 +37,7 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
     bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ Implicit _) sc)
         = pure (Just tm)
     bindLamTm tm (Bind fc n (Pi c Implicit ty) sc)
-        = do n' <- genVarName ("imp_" ++ show n)
+        = do n' <- genVarName (nameRoot n)
              Just sc' <- bindLamTm tm sc
                  | Nothing => pure Nothing
              pure $ Just (ILam fc c Implicit (Just n') (Implicit fc False) sc')
@@ -53,7 +53,7 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
         = pure tm
     bindLamNF tm (NBind fc n (Pi c Implicit ty) sc)
         = do defs <- get Ctxt
-             n' <- genVarName ("imp_" ++ show n)
+             n' <- genVarName (nameRoot n)
              sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
              sc' <- bindLamNF tm sctm
              pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'