Merge pull request #416 from edwinb/with-name

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

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