From 8774df88006fb4a2c982a0c52c365dff6b79b2a8 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 5 Jul 2020 20:01:06 +0100 Subject: [PATCH] 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 | 4 ++-- src/Core/Binary.idr | 2 +- src/Core/Context.idr | 6 ++---- src/Core/Name.idr | 8 ++++---- src/Core/UnifyState.idr | 4 ++-- src/TTImp/Elab/Case.idr | 2 +- src/TTImp/ProcessDef.idr | 2 +- tests/idris2/coverage008/expected | 2 +- tests/idris2/coverage010/expected | 2 +- 9 files changed, 15 insertions(+), 17 deletions(-) diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index b98199d35..c35c7cca8 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 30d0f54ff..1e03b9b71 100644 --- a/src/Core/Binary.idr +++ b/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 () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 60d5c27ed..ca05fa5f8 100644 --- a/src/Core/Context.idr +++ b/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) diff --git a/src/Core/Name.idr b/src/Core/Name.idr index 057ccd664..7ebee3ac2 100644 --- a/src/Core/Name.idr +++ b/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 diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 445d27aca..de2493f10 100644 --- a/src/Core/UnifyState.idr +++ b/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) diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 7290b9903..12a99fa3d 100644 --- a/src/TTImp/Elab/Case.idr +++ b/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 diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index e0bbc34a8..a7bd8d837 100644 --- a/src/TTImp/ProcessDef.idr +++ b/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) diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 0ac963019..1c65917ff 100644 --- a/tests/idris2/coverage008/expected +++ b/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! diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index baf0047af..d56cb07e6 100644 --- a/tests/idris2/coverage010/expected +++ b/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