diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index ad394b7..441f30c 100644 --- a/libs/base/Data/List.idr +++ b/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 diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index 40747ae..6d23ec4 100644 --- a/src/Core/AutoSearch.idr +++ b/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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 24acfc7..8910367 100644 --- a/src/Idris/Desugar.idr +++ b/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} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 86ab3d5..b87ad9a 100644 --- a/src/Idris/Parser.idr +++ b/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 diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 01e1146..f4b6e04 100644 --- a/src/Idris/Resugar.idr +++ b/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) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 793a1b2..7e4db02 100644 --- a/src/Idris/Syntax.idr +++ b/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 diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index 8aa985a..2912e7f 100644 --- a/src/TTImp/Elab/Term.idr +++ b/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 "_" diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 6ba0170..4c1b12d 100644 --- a/src/TTImp/TTImp.idr +++ b/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