[ debug ] better information

src/Core/CaseBuilder.idr

@@ -267,8 +267,12 @@ data Partitions : List (PatClause vars todo) -> Type where
      NoClauses : Partitions []
 
 {ps : _} -> Show (Partitions ps) where
-  show (ConClauses cs rest) = "CON " ++ show cs ++ ", " ++ show rest
-  show (VarClauses vs rest) = "VAR " ++ show vs ++ ", " ++ show rest
+  show (ConClauses cs rest)
+    = unlines ("CON" :: map (("  " ++) . show) cs)
+    ++ "\n, " ++ show rest
+  show (VarClauses vs rest)
+    = unlines ("VAR" :: map (("  " ++) . show) vs)
+    ++ "\n, " ++ show rest
   show NoClauses = "NONE"
 
 data ClauseType = ConClause | VarClause
@@ -809,18 +813,19 @@ mutual
   -- has the most distinct constructors (via pickNext)
   match {todo = (_ :: _)} fc fn phase clauses err
       = do (n ** MkNVar next) <- pickNext fc phase fn (map getNPs clauses)
-           log "compile.casetree" 25 $ "Picked " ++ show n ++ " as the next split"
+           log "compile.casetree.pick" 25 $ "Picked " ++ show n ++ " as the next split"
            let clauses' = map (shuffleVars next) clauses
-           log "compile.casetree" 25 $ "Using clauses " ++ show clauses'
+           log "compile.casetree.clauses" 25 $
+             unlines ("Using clauses:" :: map (("  " ++) . show) clauses')
            let ps = partition phase clauses'
-           log "compile.casetree" 25 $ "Got Partition " ++ show ps
+           log "compile.casetree.partition" 25 $ "Got Partition:\n" ++ show ps
            mix <- mixture fc fn phase ps err
            case mix of
              Nothing =>
-               do log "compile.casetree" 25 "match: No clauses"
+               do log "compile.casetree.intermediate" 25 "match: No clauses"
                   pure (Unmatched "No clauses")
              Just m =>
-               do log "compile.casetree" 25 $ "match: new case tree " ++ show m
+               do log "compile.casetree.intermediate" 25 $ "match: new case tree " ++ show m
                   Core.pure m
   match {todo = []} fc fn phase [] err
        = maybe (pure (Unmatched "No patterns"))
@@ -1098,7 +1103,7 @@ getPMDef : {auto c : Ref Ctxt Defs} ->
 -- for the type, which we can use in coverage checking to ensure that one of
 -- the arguments has an empty type
 getPMDef fc phase fn ty []
-    = do log "compile.casetree" 20 "getPMDef: No clauses!"
+    = do log "compile.casetree.getpmdef" 20 "getPMDef: No clauses!"
          defs <- get Ctxt
          pure (!(getArgs 0 !(nf defs [] ty)) ** (Unmatched "No clauses", []))
   where
@@ -1112,7 +1117,7 @@ getPMDef fc phase fn ty clauses
     = do defs <- get Ctxt
          let cs = map (toClosed defs) (labelPat 0 clauses)
          (_ ** t) <- simpleCase fc phase fn ty Nothing cs
-         logC "compile.casetree" 20 $
+         logC "compile.casetree.getpmdef" 20 $
            pure $ "Compiled to: " ++ show !(toFullNames t)
          let reached = findReached t
          pure (_ ** (t, getUnreachable 0 reached clauses))

src/Core/CaseTree.idr

@@ -68,27 +68,38 @@ isPConst : Pat -> Maybe Constant
 isPConst (PConst _ c) = Just c
 isPConst _ = Nothing
 
-mutual
-  export
-  {vars : _} -> Show (CaseTree vars) where
-    show (Case {name} idx prf ty alts)
-        = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of\n { " ++
-                showSep "\n | " (assert_total (map show alts)) ++ "\n }"
-    show (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
-    show (Unmatched msg) = "Error: " ++ show msg
-    show Impossible = "Impossible"
+showCT : {vars : _} -> (indent : String) -> CaseTree vars -> String
+showCA : {vars : _} -> (indent : String) -> CaseAlt vars  -> String
 
-  export
-  {vars : _} -> Show (CaseAlt vars) where
-    show (ConCase n tag args sc)
+showCT indent (Case {name} idx prf ty alts)
+  = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of"
+  ++ "\n" ++ indent ++ " { "
+  ++ showSep ("\n" ++ indent ++ " | ")
+             (assert_total (map (showCA ("  " ++ indent)) alts))
+  ++ "\n" ++ indent ++ " }"
+showCT indent (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
+showCT indent (Unmatched msg) = "Error: " ++ show msg
+showCT indent Impossible = "Impossible"
+
+showCA indent (ConCase n tag args sc)
         = showSep " " (map show (n :: args)) ++ " => " ++
-          show sc
-    show (DelayCase _ arg sc)
-        = "Delay " ++ show arg ++ " => " ++ show sc
-    show (ConstCase c sc)
-        = "Constant " ++ show c ++ " => " ++ show sc
-    show (DefaultCase sc)
-        = "_ => " ++ show sc
+          showCT indent sc
+showCA indent (DelayCase _ arg sc)
+        = "Delay " ++ show arg ++ " => " ++ showCT indent sc
+showCA indent (ConstCase c sc)
+        = "Constant " ++ show c ++ " => " ++ showCT indent sc
+showCA indent (DefaultCase sc)
+        = "_ => " ++ showCT indent sc
+
+export
+{vars : _} -> Show (CaseTree vars) where
+  show = showCT ""
+
+export
+{vars : _} -> Show (CaseAlt vars) where
+  show = showCA ""
+
+
 
 mutual
   export

src/Core/Options/Log.idr

@@ -45,6 +45,11 @@ knownTopics = [
     ("builtin.IntegerToNatural", "some documentation of this option"),
     ("builtin.IntegerToNatural.addTransforms", "some documentation of this option"),
     ("compile.casetree", "some documentation of this option"),
+    ("compile.casetree.clauses", "some documentation of this option"),
+    ("compile.casetree.getpmdef", "some documentation of this option"),
+    ("compile.casetree.intermediate", "some documentation of this option"),
+    ("compile.casetree.pick", "some documentation of this option"),
+    ("compile.casetree.partition", "some documentation of this option"),
     ("compiler.inline.eval", "some documentation of this option"),
     ("compiler.refc", "some documentation of this option"),
     ("compiler.refc.cc", "some documentation of this option"),

src/TTImp/ProcessDef.idr

@@ -984,7 +984,9 @@ processDef opts nest env fc n_in cs_in
                     Core Covering
     checkCoverage n ty mult cs
         = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
-             log "declare.def" 5 $ "Using clauses :" ++ show !(traverse toFullNames covcs')
+             log "declare.def" 5 $ unlines
+               $ "Using clauses :"
+               :: map (("  " ++) . show) !(traverse toFullNames covcs')
              let covcs = mapMaybe id covcs'
              (_ ** (ctree, _)) <-
                  getPMDef fc (CompileTime mult) (Resolved n) ty covcs