[ refactor ] Refactor types for log topic validation (#3503)

src/Compiler/Scheme/Chez.idr

@@ -262,7 +262,7 @@ cCall fc cfn clib args ret collectSafe
                            pure (Just clib)
          argTypes <- traverse (cftySpec fc . snd) args
          retType <- cftySpec fc ret
-         let callConv = if collectSafe then " __collect_safe" else ""
+         let callConv : Builder = if collectSafe then " __collect_safe" else ""
          let call = "((foreign-procedure" ++ callConv ++ " " ++ showB cfn ++ " ("
                       ++ sepBy " " argTypes ++ ") " ++ retType ++ ") "
                       ++ sepBy " " !(traverse buildArg args) ++ ")"

src/Core/Context/Log.idr

@@ -44,21 +44,18 @@ unverifiedLogging str n = do
 %inline
 export
 logging : {auto c : Ref Ctxt Defs} ->
-          (s : String) -> {auto 0 _ : KnownTopic s} ->
-          Nat -> Core Bool
-logging str n = unverifiedLogging str n
+          LogTopic -> Nat -> Core Bool
+logging s n = unverifiedLogging s.topic n
 
 ||| Log message with a term, translating back to human readable names first.
 export
 logTerm : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
-          (s : String) ->
-          {auto 0 _ : KnownTopic s} ->
-          Nat -> Lazy String -> Term vars -> Core ()
-logTerm str n msg tm
-    = when !(logging str n)
+          LogTopic -> Nat -> Lazy String -> Term vars -> Core ()
+logTerm s n msg tm
+    = when !(logging s n)
         $ do tm' <- toFullNames tm
-             logString str n $ msg ++ ": " ++ show tm'
+             logString s.topic n $ msg ++ ": " ++ show tm'
 
 export
 log' : {auto c : Ref Ctxt Defs} ->
@@ -77,17 +74,14 @@ log' lvl msg
 ||| `do` before `pure` in this case ensures the correct bounds.
 export
 log : {auto c : Ref Ctxt Defs} ->
-      (s : String) ->
-      {auto 0 _ : KnownTopic s} ->
-      Nat -> Lazy String -> Core ()
-log str n msg
-    = when !(logging str n)
-        $ logString str n msg
+      LogTopic -> Nat -> Lazy String -> Core ()
+log s n msg
+    = when !(logging s n)
+        $ logString s.topic n msg
 
 export
 unverifiedLogC : {auto c : Ref Ctxt Defs} ->
-                 (s : String) ->
-                 Nat -> Core String -> Core ()
+                 String -> Nat -> Core String -> Core ()
 unverifiedLogC str n cmsg
     = when !(unverifiedLogging str n)
         $ do msg <- cmsg
@@ -96,10 +90,8 @@ unverifiedLogC str n cmsg
 %inline
 export
 logC : {auto c : Ref Ctxt Defs} ->
-       (s : String) ->
-       {auto 0 _ : KnownTopic s} ->
-       Nat -> Core String -> Core ()
-logC str = unverifiedLogC str
+       LogTopic -> Nat -> Core String -> Core ()
+logC s = unverifiedLogC s.topic
 
 nano : Integer
 nano = 1000000000

src/Core/Normalise.idr

@@ -167,87 +167,80 @@ getArity defs env tm = getValArity defs env !(nf defs env tm)
 export
 logNF : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
-        (s : String) ->
-        {auto 0 _ : KnownTopic s} ->
-        Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
-logNF str n msg env tmnf
-    = when !(logging str n) $
+        LogTopic -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
+logNF s n msg env tmnf
+    = when !(logging s n) $
         do defs <- get Ctxt
            tm <- quote defs env tmnf
            tm' <- toFullNames tm
-           logString str n (msg ++ ": " ++ show tm')
+           logString s.topic n (msg ++ ": " ++ show tm')
 
 -- Log message with a term, reducing holes and translating back to human
 -- readable names first
 export
 logTermNF' : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
-             (s : String) ->
-             {auto 0 _ : KnownTopic s} ->
+             LogTopic ->
              Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
-logTermNF' str n msg env tm
+logTermNF' s n msg env tm
     = do defs <- get Ctxt
          tmnf <- normaliseHoles defs env tm
          tm' <- toFullNames tmnf
-         logString str n (msg ++ ": " ++ show tm')
+         logString s.topic n (msg ++ ": " ++ show tm')
 
 export
 logTermNF : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
-            (s : String) ->
-            {auto 0 _ : KnownTopic s} ->
+            LogTopic ->
             Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
-logTermNF str n msg env tm
-    = when !(logging str n) $ logTermNF' str n msg env tm
+logTermNF s n msg env tm
+    = when !(logging s n) $ logTermNF' s n msg env tm
 
 export
 logGlue : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
-          (s : String) ->
-          {auto 0 _ : KnownTopic s} ->
+          LogTopic ->
           Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
-logGlue str n msg env gtm
-    = when !(logging str n) $
+logGlue s n msg env gtm
+    = when !(logging s n) $
         do defs <- get Ctxt
            tm <- getTerm gtm
            tm' <- toFullNames tm
-           logString str n (msg ++ ": " ++ show tm')
+           logString s.topic n (msg ++ ": " ++ show tm')
 
 export
 logGlueNF : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
-            (s : String) ->
-            {auto 0 _ : KnownTopic s} ->
+            LogTopic ->
             Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
-logGlueNF str n msg env gtm
-    = when !(logging str n) $
+logGlueNF s n msg env gtm
+    = when !(logging s n) $
         do defs <- get Ctxt
            tm <- getTerm gtm
            tmnf <- normaliseHoles defs env tm
            tm' <- toFullNames tmnf
-           logString str n (msg ++ ": " ++ show tm')
+           logString s.topic n (msg ++ ": " ++ show tm')
 
 export
 logEnv : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
-         (s : String) ->
-         {auto 0 _ : KnownTopic s} ->
+         LogTopic ->
          Nat -> String -> Env Term vars -> Core ()
-logEnv str n msg env
-    = when !(logging str n) $
-        do logString str n msg
+logEnv s n msg env
+    = when !(logging s n) $
+        do logString s.topic n msg
            dumpEnv env
 
   where
 
     dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
     dumpEnv [] = pure ()
     dumpEnv {vs = x :: _} (Let _ c val ty :: bs)
-        = do logTermNF' str n (msg ++ ": let " ++ show x) bs val
-             logTermNF' str n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty
+        = do logTermNF' s n (msg ++ ": let " ++ show x) bs val
+             logTermNF' s n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty
              dumpEnv bs
     dumpEnv {vs = x :: _} (b :: bs)
-        = do logTermNF' str n (msg ++ ":" ++ show (multiplicity b) ++ " " ++
+        = do logTermNF' s n (msg ++ ":" ++ show (multiplicity b) ++ " " ++
                            show (piInfo b) ++ " " ++
                            show x) bs (binderType b)
              dumpEnv bs

src/Core/Options/Log.idr

@@ -211,8 +211,18 @@ helpTopics = show $ vcat $ map helpTopic knownTopics
       in vcat (title :: blurb)
 
 public export
-KnownTopic : String -> Type
-KnownTopic s = IsJust (lookup s knownTopics)
+data KnownTopic : String -> Type where
+  IsKnownTopic : IsJust (lookup s Log.knownTopics) => KnownTopic s
+
+public export
+record LogTopic where
+  constructor MkLogTopic
+  topic : String
+  {auto 0 known : KnownTopic topic}
+
+export
+fromString : (s : String) -> (0 _ : KnownTopic s) => LogTopic
+fromString = MkLogTopic
 
 ||| An individual log level is a pair of a list of non-empty strings and a number.
 ||| We keep the representation opaque to force users to call the smart constructor
@@ -244,8 +254,8 @@ mkUnverifiedLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
 ||| Like `mkUnverifiedLogLevel` but with a compile time check that
 ||| the passed string is a known topic.
 export
-mkLogLevel : (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
-mkLogLevel s = mkUnverifiedLogLevel s
+mkLogLevel : LogTopic -> Nat -> LogLevel
+mkLogLevel s = mkUnverifiedLogLevel s.topic
 
 ||| The unsafe constructor should only be used in places where the topic has already
 ||| been appropriately processed.

src/Core/UnifyState.idr

@@ -648,44 +648,42 @@ checkNoGuards = checkUserHoles False
 export
 dumpHole : {auto u : Ref UST UState} ->
            {auto c : Ref Ctxt Defs} ->
-           (s : String) ->
-           {auto 0 _ : KnownTopic s} ->
-           Nat -> (hole : Int) -> Core ()
-dumpHole str n hole
+           LogTopic -> Nat -> (hole : Int) -> Core ()
+dumpHole s n hole
     = do ust <- get UST
          defs <- get Ctxt
          case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
           Nothing => pure ()
           Just gdef => case (definition gdef, type gdef) of
              (Guess tm envb constraints, ty) =>
-                  do logString str n $
+                  do logString s.topic n $
                        "!" ++ show !(getFullName (Resolved hole)) ++ " : "
                            ++ show !(toFullNames !(normaliseHoles defs [] ty))
                        ++ "\n\t  = "
                            ++ show !(normaliseHoles defs [] tm)
                            ++ "\n\twhen"
                      traverse_ dumpConstraint constraints
              (Hole _ p, ty) =>
-                  logString str n $
+                  logString s.topic n $
                     "?" ++ show (fullname gdef) ++ " : "
                         ++ show !(normaliseHoles defs [] ty)
                         ++ if implbind p then " (ImplBind)" else ""
                         ++ if invertible gdef then " (Invertible)" else ""
              (BySearch _ _ _, ty) =>
-                  logString str n $
+                  logString s.topic n $
                      "Search " ++ show hole ++ " : " ++
                      show !(toFullNames !(normaliseHoles defs [] ty))
              (PMDef _ args t _ _, ty) =>
-                  log str 4 $
+                  log s 4 $
                      "Solved: " ++ show hole ++ " : " ++
                      show !(normalise defs [] ty) ++
                      " = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
              (ImpBind, ty) =>
-                  log str 4 $
+                  log s 4 $
                       "Bound: " ++ show hole ++ " : " ++
                       show !(normalise defs [] ty)
              (Delayed, ty) =>
-                  log str 4 $
+                  log s 4 $
                      "Delayed elaborator : " ++
                      show !(normalise defs [] ty)
              _ => pure ()
@@ -696,31 +694,27 @@ dumpHole str n hole
              defs <- get Ctxt
              case lookup cid (constraints ust) of
                   Nothing => pure ()
-                  Just Resolved => logString str n "\tResolved"
+                  Just Resolved => logString s.topic n "\tResolved"
                   Just (MkConstraint _ lazy env x y) =>
-                    do logString str n $
+                    do logString s.topic n $
                          "\t  " ++ show !(toFullNames !(quote defs env x))
                                 ++ " =?= " ++ show !(toFullNames !(quote defs env y))
                        empty <- clearDefs defs
-                       log str 5 $
+                       log s 5 $
                          "\t    from " ++ show !(toFullNames !(quote empty env x))
                             ++ " =?= " ++ show !(toFullNames !(quote empty env y))
                             ++ if lazy then "\n\t(lazy allowed)" else ""
 
 export
 dumpConstraints : {auto u : Ref UST UState} ->
                   {auto c : Ref Ctxt Defs} ->
-                  (topics : String) ->
-                  {auto 0 _ : KnownTopic topics} ->
-                  (verbosity : Nat) ->
-                  (all : Bool) ->
-                  Core ()
-dumpConstraints str n all
+                  LogTopic -> (verbosity : Nat) -> (all : Bool) -> Core ()
+dumpConstraints s n all
     = do ust <- get UST
          defs <- get Ctxt
-         when !(logging str n) $ do
+         when !(logging s n) $ do
            let hs = toList (guesses ust) ++
                     toList (if all then holes ust else currentHoles ust)
            unless (isNil hs) $
-             do logString str n "--- CONSTRAINTS AND HOLES ---"
-                traverse_ (dumpHole str n) (map fst hs)
+             do logString s.topic n "--- CONSTRAINTS AND HOLES ---"
+                traverse_ (dumpHole s n) (map fst hs)

src/TTImp/TTImp.idr

@@ -1004,9 +1004,5 @@ getFn f = f
 -- Log message with a RawImp
 export
 logRaw : {auto c : Ref Ctxt Defs} ->
-         (s : String) ->
-         {auto 0 _ : KnownTopic s} ->
-         Nat -> Lazy String -> RawImp -> Core ()
-logRaw str n msg tm
-    = when !(logging str n) $
-        do logString str n (msg ++ ": " ++ show tm)
+         LogTopic -> Nat -> Lazy String -> RawImp -> Core ()
+logRaw s n msg tm = log s n $ msg ++ ": " ++ show tm