Allow setting logging mid term

Sometimes this makes debugging easier since the logging is more
localised.

libs/base/Data/List.idr

@@ -297,11 +297,13 @@ tail [] impossible
 tail (x :: xs) = xs
 
 ||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
+export
 head' : List a -> Maybe a
 head' []      = Nothing
 head' (x::xs) = Just x
 
 ||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
+export
 tail' : List a -> Maybe (List a)
 tail' []      = Nothing
 tail' (x::xs) = Just xs

src/Core/AutoSearch.idr

@@ -524,11 +524,11 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target
 --          Core (Term vars)
 Core.Unify.search fc rigc defaults depth def top env
     = do defs <- get Ctxt
-         logTermNF 2 "Initial target: " env top
-         log 2 $ "Running search with defaults " ++ show defaults
+         logTermNF 3 "Initial target: " env top
+         log 3 $ "Running search with defaults " ++ show defaults
          tm <- searchType fc rigc defaults [] depth def
                           True (abstractEnvType fc env top) env
                           top
-         logTermNF 2 "Result" env tm
+         logTermNF 3 "Result" env tm
          defs <- get Ctxt
          pure tm

src/Idris/Desugar.idr

@@ -329,8 +329,8 @@ mutual
                 desugarB side ps (PApp fc (PRef fc (UN "rangeFrom")) start)
              Just n =>
                 desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
-  desugarB side ps (PUnifyLog fc tm)
-      = pure $ IUnifyLog fc !(desugarB side ps tm)
+  desugarB side ps (PUnifyLog fc lvl tm)
+      = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
 
   desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                   {auto b : Ref Bang BangData} ->

src/Idris/Parser.idr

@@ -358,10 +358,11 @@ mutual
            end <- location
            pure (PIdiom (MkFC fname start end) e)
     <|> do start <- location
-           symbol "%"; exactIdent "unifyLog"
+           symbol "%"; exactIdent "logging"
+           lvl <- intLit
            e <- expr pdef fname indents
            end <- location
-           pure (PUnifyLog (MkFC fname start end) e)
+           pure (PUnifyLog (MkFC fname start end) (cast lvl) e)
 
   multiplicity : EmptyRule (Maybe Integer)
   multiplicity

src/Idris/Resugar.idr

@@ -230,7 +230,7 @@ mutual
   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
   toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))
 
-  toPTerm p (IUnifyLog fc tm) = toPTerm p tm
+  toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm
   toPTerm p (Implicit fc True) = pure (PImplicit fc)
   toPTerm p (Implicit fc False) = pure (PInfer fc)
 

src/Idris/Syntax.idr

@@ -92,7 +92,7 @@ mutual
        PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
 
        -- Debugging
-       PUnifyLog : FC -> PTerm -> PTerm
+       PUnifyLog : FC -> Nat -> PTerm -> PTerm
 
        -- TODO: 'with' disambiguation
 
@@ -485,7 +485,7 @@ mutual
         = "[" ++ showPrec d start ++ " .. ]"
     showPrec d (PRangeStream _ start (Just next))
         = "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]"
-    showPrec d (PUnifyLog _ tm) = showPrec d tm
+    showPrec d (PUnifyLog _ lvl tm) = showPrec d tm
 
 public export
 record IFaceInfo where

src/TTImp/Elab/Term.idr

@@ -5,6 +5,7 @@ import Core.Core
 import Core.Env
 import Core.Metadata
 import Core.Normalise
+import Core.Options
 -- import Core.Reflect
 import Core.Unify
 import Core.TT
@@ -186,11 +187,12 @@ checkTerm rig elabinfo nest env (IType fc) exp
 
 checkTerm rig elabinfo nest env (IHole fc str) exp
     = checkHole rig elabinfo nest env fc str exp
-checkTerm rig elabinfo nest env (IUnifyLog fc tm) exp
-    = do ust <- get UST
-         put UST (record { logging = True } ust)
+checkTerm rig elabinfo nest env (IUnifyLog fc n tm) exp
+    = do opts <- getSession
+         let lvl = logLevel opts
+         setLogLevel n
          r <- check rig elabinfo nest env tm exp
-         put UST ust
+         setLogLevel lvl
          pure r
 checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
     = do nm <- genName "_"

src/TTImp/TTImp.idr

@@ -97,7 +97,7 @@ mutual
        IType : FC -> RawImp
        IHole : FC -> String -> RawImp
 
-       IUnifyLog : FC -> RawImp -> RawImp
+       IUnifyLog : FC -> Nat -> RawImp -> RawImp
        -- An implicit value, solved by unification, but which will also be
        -- bound (either as a pattern variable or a type variable) if unsolved
        -- at the end of elaborator
@@ -164,7 +164,7 @@ mutual
       show (IRunElab fc tm) = "(%runelab " ++ show tm ++ ")"
       show (IPrimVal fc c) = show c
       show (IHole _ x) = "?" ++ x
-      show (IUnifyLog _ x) = "(%unifyLog " ++ show x ++ ")"
+      show (IUnifyLog _ lvl x) = "(%logging " ++ show lvl ++ " " ++ show x ++ ")"
       show (IType fc) = "%type"
       show (Implicit fc True) = "_"
       show (Implicit fc False) = "?"
@@ -542,7 +542,7 @@ getFC (IRewrite x _ _) = x
 getFC (ICoerced x _) = x
 getFC (IPrimVal x _) = x
 getFC (IHole x _) = x
-getFC (IUnifyLog x _) = x
+getFC (IUnifyLog x _ _) = x
 getFC (IType x) = x
 getFC (IBindVar x _) = x
 getFC (IBindHere x _ _) = x
@@ -641,7 +641,7 @@ mutual
         = do tag 26; toBuf b fc
     toBuf b (IHole fc y)
         = do tag 27; toBuf b fc; toBuf b y
-    toBuf b (IUnifyLog fc x) = toBuf b x
+    toBuf b (IUnifyLog fc lvl x) = toBuf b x
 
     toBuf b (Implicit fc i)
         = do tag 28; toBuf b fc; toBuf b i