Use a String, not an Int, for case/with names

The Int represented the resolved name, but this isn't guaranteed to be
up to date after reloading and, worse, it doesn't display helpfully. I'm
bored of updating the tests which fail as a result!

This also fixes #407, which is about displaying the wrong name after
reloading the ttc.

src/Compiler/Scheme/Common.idr

@@ -38,8 +38,8 @@ schName (PV n d) = "pat--" ++ schName n
 schName (DN _ n) = schName n
 schName (RF n) = "rf--" ++ schString n
 schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
-schName (CaseBlock x y) = "case--" ++ show x ++ "-" ++ show y
-schName (WithBlock x y) = "with--" ++ show x ++ "-" ++ show y
+schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
+schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
 schName (Resolved i) = "fn--" ++ show i
 
 export

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 35
+ttcVersion = 36
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Context.idr

@@ -1287,11 +1287,9 @@ prettyName (Nested (i, _) n)
          pure (!(prettyName i') ++ "," ++
                !(prettyName n))
 prettyName (CaseBlock outer idx)
-    = do outer' <- toFullNames (Resolved outer)
-         pure ("case block in " ++ !(prettyName outer'))
+    = pure ("case block in " ++ outer)
 prettyName (WithBlock outer idx)
-    = do outer' <- toFullNames (Resolved outer)
-         pure ("with block in " ++ !(prettyName outer'))
+    = pure ("with block in " ++ outer)
 prettyName (NS ns n) = prettyName n
 prettyName n = pure (show n)
 

src/Core/Name.idr

@@ -14,8 +14,8 @@ data Name : Type where
      DN : String -> Name -> Name -- a name and how to display it
      RF : String -> Name  -- record field name
      Nested : (Int, Int) -> Name -> Name -- nested function name
-     CaseBlock : Int -> Int -> Name -- case block nested in (resolved) name
-     WithBlock : Int -> Int -> Name -- with block nested in (resolved) name
+     CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
+     WithBlock : String -> Int -> Name -- with block nested in (resolved) name
      Resolved : Int -> Name -- resolved, index into context
 
 -- Update a name imported with 'import as', for creating an alias
@@ -88,8 +88,8 @@ Show Name where
   show (RF n) = "." ++ n
   show (Nested (outer, idx) inner)
       = show outer ++ ":" ++ show idx ++ ":" ++ show inner
-  show (CaseBlock outer i) = "case block in " ++ show outer ++ "(" ++ show i ++ ")"
-  show (WithBlock outer i) = "with block in " ++ show outer
+  show (CaseBlock outer i) = "case block in " ++ outer
+  show (WithBlock outer i) = "with block in " ++ outer
   show (Resolved x) = "$resolved" ++ show x
 
 export

src/Core/UnifyState.idr

@@ -145,7 +145,7 @@ genVarName str
 export
 genCaseName : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
-			     		Int -> Core Name
+              String -> Core Name
 genCaseName root
     = do ust <- get UST
          put UST (record { nextName $= (+1) } ust)
@@ -154,7 +154,7 @@ genCaseName root
 export
 genWithName : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
-			     		Int -> Core Name
+              String -> Core Name
 genWithName root
     = do ust <- get UST
          put UST (record { nextName $= (+1) } ust)

src/TTImp/Elab/Case.idr

@@ -178,7 +178,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          log 5 $ "Doing a case under unbound implicits " ++ show fullImps
 
          scrn <- genVarName "scr"
-         casen <- genCaseName (defining est)
+         casen <- genCaseName !(prettyName !(toFullNames (Resolved (defining est))))
 
          -- Update environment so that linear bindings which were used
          -- (esp. in the scrutinee!) are set to 0 in the case type

src/TTImp/ProcessDef.idr

@@ -466,7 +466,7 @@ checkClause {vars} mult vis hashit n opts nest env (WithClause fc lhs_in wval_ra
          logTerm 3 "With function type" wtype
          log 5 $ "Argument names " ++ show wargNames
 
-         wname <- genWithName n
+         wname <- genWithName !(prettyName !(toFullNames (Resolved n)))
          widx <- addDef wname (newDef fc wname (if isErased mult then erased else top)
                                       vars wtype vis None)
          let rhs_in = apply (IVar fc wname)

tests/idris2/coverage008/expected

@@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1395
+Main> Main.wbar is not covering due to call to function Main.with block in wbar
 Main> Main.wbar1 is total
 Main> Bye for now!

tests/idris2/coverage010/expected

@@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
 12	main : IO ()
 13	main = do
 
-	Calls non covering function Main.case block in 2164(630)
+	Calls non covering function Main.case block in main