From 66b61a316b8723127af388d199fbe05a83b4a513 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 24 Feb 2025 16:35:13 -0800 Subject: [PATCH] Improve error messages, which mention module parameters. Fixes #1560 --- CHANGES.md | 3 ++ src/Cryptol/TypeCheck/Error.hs | 21 ++++---- src/Cryptol/TypeCheck/InferTypes.hs | 70 +++++++++++++++++++++--- src/Cryptol/Utils/Ident.hs | 9 ++++ src/Cryptol/Utils/PP.hs | 4 +- tests/docstrings/T02.icry.stdout | 2 +- tests/docstrings/T07.icry.stdout | 2 +- tests/docstrings/T08.icry.stdout | 2 +- tests/docstrings/T10.icry.stdout | 2 +- tests/issues/issue058.icry.stdout | 2 +- tests/issues/issue1560.icry | 4 ++ tests/issues/issue1560.icry.stdout | 82 +++++++++++++++++++++++++++++ tests/issues/issue1560/T1.cry | 7 +++ tests/issues/issue1560/T2.cry | 16 ++++++ tests/issues/issue1560/T3.cry | 26 +++++++++ tests/issues/issue1560/T4.cry | 27 ++++++++++ tests/issues/issue582.icry.stdout | 4 +- 17 files changed, 255 insertions(+), 28 deletions(-) create mode 100644 tests/issues/issue1560.icry create mode 100644 tests/issues/issue1560.icry.stdout create mode 100644 tests/issues/issue1560/T1.cry create mode 100644 tests/issues/issue1560/T2.cry create mode 100644 tests/issues/issue1560/T3.cry create mode 100644 tests/issues/issue1560/T4.cry diff --git a/CHANGES.md b/CHANGES.md index cf8755b39..11c488238 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -24,6 +24,9 @@ ## New features +* Improved error messages mentioning module parameters + ([#1560](https://github.com/GaloisInc/cryptol/issues/1560)) + * Improved the naming convention for anonymous modules generated by the module system ([#1810](https://github.com/GaloisInc/cryptol/issues/1810)) diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 8b6a94cd1..b9c2094d6 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -819,6 +819,7 @@ explainUnsolvable names gs = computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap computeFreeVarNames warns errs = mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars + `IntMap.union` mpNames {- XXX: Currently we pick the names based on the unique of the variable: smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`) @@ -831,20 +832,16 @@ computeFreeVarNames warns errs = mkName x v = (tvUnique x, v) mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots)) - (numVaras,otherVars) = partition ((== KNum) . kindOf) - $ Set.toList - $ Set.filter isFreeTV - $ fvs (map snd warns, map snd errs) + (uvars,non_uvars) = partition isFreeTV + $ Set.toList + $ fvs (map snd warns, map snd errs) + + mpNames = computeModParamNames [ tp | TVBound tp <- non_uvars ] mempty + + (numVaras,otherVars) = partition ((== KNum) . kindOf) uvars otherRoots = [ "a", "b", "c", "d" ] numRoots = [ "m", "n", "u", "v" ] - useUnicode = True + variants roots = [ nameVariant n r | n <- [ 0 .. ], r <- roots ] - suff n - | n < 10 && useUnicode = [toEnum (0x2080 + n)] - | otherwise = show n - - variant n x = if n == 0 then x else x ++ suff n - - variants roots = [ variant n r | n <- [ 0 .. ], r <- roots ] diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 171d4f431..4507ebcab 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -21,7 +21,7 @@ module Cryptol.TypeCheck.InferTypes where import Control.Monad(guard) import Cryptol.Parser.Position -import Cryptol.ModuleSystem.Name (asPrim,nameLoc) +import Cryptol.ModuleSystem.Name (asPrim,nameLoc,nameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Subst @@ -31,10 +31,13 @@ import Cryptol.Utils.Ident (PrimIdent(..), preludeName) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Misc(anyJust) +import Data.List(mapAccumL,partition) +import Data.Maybe(mapMaybe) import Data.Set ( Set ) import qualified Data.Set as Set import Data.Map ( Map ) import qualified Data.Map as Map +import qualified Data.IntMap as IntMap import GHC.Generics (Generic) import Control.DeepSeq @@ -323,14 +326,17 @@ cppKind ki = _ -> pp ki addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc -addTVarsDescsAfter nm t d +addTVarsDescsAfter nm t = addTVarsDescsAfterFVS nm (fvs t) + +addTVarsDescsAfterFVS :: NameMap -> Set TVar -> Doc -> Doc +addTVarsDescsAfterFVS nm vs d | Set.null vs = d -- TODO? use `hang` here instead to indent things after "where" | otherwise = d $$ text "where" $$ vcat (map desc (Set.toList vs)) where - vs = fvs t desc v = ppWithNames nm v <+> text "is" <+> pp (tvInfo v) + addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc addTVarsDescsBefore nm t d = vcat (frontMsg ++ [d] ++ backMsg) where @@ -393,13 +399,16 @@ instance PP (WithNames DelayedCt) where ppPrec _ (WithNames d names) = sig $$ hang "we need to show that" - 2 (vcat ( vars ++ asmps ++ + + 2 (explain (vcat ( vars ++ asmps ++ [ hang "the following constraints hold:" 2 (vcat $ bullets $ map (ppWithNames ns1) - $ dctGoals d )])) + $ dctGoals d )]))) where + + bullets xs = [ "•" <+> x | x <- xs ] sig = case name of @@ -408,7 +417,7 @@ instance PP (WithNames DelayedCt) where Nothing -> "when checking the module's parameters," name = dctSource d - vars = case dctForall d of + vars = case otherTPs of [] -> [] xs -> ["for any type" <+> commaSep (map (ppWithNames ns1) xs)] asmps = case dctAsmps d of @@ -416,4 +425,51 @@ instance PP (WithNames DelayedCt) where xs -> [hang "assuming" 2 (vcat (bullets (map (ppWithNames ns1) xs)))] - ns1 = addTNames (dctForall d) names + tvars = fvs (dctAsmps d, dctGoals d) + used = filter ((`Set.member` tvars) . TVBound) (dctForall d) + isModP tp = + case tpFlav tp of + TPModParam {} -> True + _ -> False + (mpTPs,otherTPs) = partition isModP used + explain = addTVarsDescsAfterFVS ns1 (Set.fromList (map TVBound mpTPs)) + + mps = computeModParamNames mpTPs names + ns1 = addTNames otherTPs mps + + + +-- | Add a suffix to a name to make a different label. +nameVariant :: Int -> String -> String +nameVariant n x = if n == 0 then x else x ++ suff + where + useUnicode = True + + suff + | n < 10 && useUnicode = [toEnum (0x2080 + n)] + | otherwise = show n + + + +-- | Pick names for the type parameters that correspond to module parameters, +-- avoiding strings that already appear in the given name map. +-- Returns and extended name map. +computeModParamNames :: [TParam] -> NameMap -> NameMap +computeModParamNames tps names = IntMap.fromList newNames `IntMap.union` names + where + newNames = snd (mapAccumL pickName used0 (mapMaybe isModP tps)) + + used0 = Set.fromList (IntMap.elems names) + + pickName used (u,i) = + let ns = filter (not . (`Set.member` used)) + $ map (`nameVariant` i) [0..] + name = case ns of + x : _ -> x + [] -> panic "computeModParamNames" ["Out of names!"] + in (Set.insert name used, (u,name)) + + isModP tp = + case tpFlav tp of + TPModParam x -> Just (tpUnique tp, show (pp (nameIdent x))) + _ -> Nothing diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index ad7e523fe..0f7b0aa1b 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -53,6 +53,7 @@ module Cryptol.Utils.Ident , mkInfix , isInfixIdent , isUpperIdent + , isAnonIfaceModIdnet , nullIdent , identText , identAnonArg @@ -354,6 +355,14 @@ isUpperIdent (Ident _ mb t) = NormalName | Just (c,_) <- T.uncons t -> isUpper c _ -> False +-- | Is this an ident for an anonymous module interface +-- (i.e., a `parameter` block) +isAnonIfaceModIdnet :: Ident -> Bool +isAnonIfaceModIdnet (Ident _ ty _) = + case ty of + AnonIfaceModName -> True + _ -> False + nullIdent :: Ident -> Bool nullIdent = T.null . identText diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index baaf40643..17b1b0ece 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -415,8 +415,8 @@ instance PP OrigName where Qualified m -> ppQual (TopModule m) (pp (ogName og)) NotInScope -> ppQual (ogModule og) case ogFromParam og of - Just x -> pp x <.> "::" <.> pp (ogName og) - Nothing -> pp (ogName og) + Just x | not (isAnonIfaceModIdnet x) -> pp x <.> "::" <.> pp (ogName og) + _ -> pp (ogName og) where ppQual mo x = case mo of diff --git a/tests/docstrings/T02.icry.stdout b/tests/docstrings/T02.icry.stdout index 97015a386..d24d4c040 100644 --- a/tests/docstrings/T02.icry.stdout +++ b/tests/docstrings/T02.icry.stdout @@ -4,7 +4,7 @@ Loading module T02 Checking module T02 Docstrings on T02 Docstrings on T02::where_at__27_11::n - Docstrings on T02::F7::F__parameter::n + Docstrings on T02::F7::n Docstrings on T02::F7::c :check c == 1 Using exhaustive testing. diff --git a/tests/docstrings/T07.icry.stdout b/tests/docstrings/T07.icry.stdout index b41a85a2a..2247b4bed 100644 --- a/tests/docstrings/T07.icry.stdout +++ b/tests/docstrings/T07.icry.stdout @@ -8,5 +8,5 @@ Checking module T07 Docstrings on T07 42 : [N] 0x2a - Docstrings on T07::T07F__parameter::N + Docstrings on T07::N Successes: 1, No fences: 1, Failures: 0 diff --git a/tests/docstrings/T08.icry.stdout b/tests/docstrings/T08.icry.stdout index d0012b252..a8b34b789 100644 --- a/tests/docstrings/T08.icry.stdout +++ b/tests/docstrings/T08.icry.stdout @@ -4,7 +4,7 @@ Loading module Main Checking module Main Docstrings on Main Docstrings on Main::where_at__16_11::n - Docstrings on Main::M::F__parameter::n + Docstrings on Main::M::n Docstrings on submodule Main::where_at__16_11 Docstrings on submodule Main::M "M" diff --git a/tests/docstrings/T10.icry.stdout b/tests/docstrings/T10.icry.stdout index 1a815b1dc..77c72b2e6 100644 --- a/tests/docstrings/T10.icry.stdout +++ b/tests/docstrings/T10.icry.stdout @@ -20,7 +20,7 @@ Checking module T10 Testing... Passed 1 tests. Q.E.D. Docstrings on T10::where_at__30_11::N - Docstrings on T10::F1::F__parameter::N + Docstrings on T10::F1::N Docstrings on T10::M::q Docstrings on T10::M::r Docstrings on T10::F1::s diff --git a/tests/issues/issue058.icry.stdout b/tests/issues/issue058.icry.stdout index cd2df137a..5a46ec210 100644 --- a/tests/issues/issue058.icry.stdout +++ b/tests/issues/issue058.icry.stdout @@ -16,7 +16,7 @@ Loading module Main Failed to validate user-specified signature. in the definition of 'Main::last', at issue058.cry:7:1--7:5, we need to show that - for any type n, a + for any type n assuming • n >= 1 the following constraints hold: diff --git a/tests/issues/issue1560.icry b/tests/issues/issue1560.icry new file mode 100644 index 000000000..e49d8580c --- /dev/null +++ b/tests/issues/issue1560.icry @@ -0,0 +1,4 @@ +:load issue1560/T1.cry +:load issue1560/T2.cry +:load issue1560/T3.cry +:load issue1560/T4.cry diff --git a/tests/issues/issue1560.icry.stdout b/tests/issues/issue1560.icry.stdout new file mode 100644 index 000000000..0443cec39 --- /dev/null +++ b/tests/issues/issue1560.icry.stdout @@ -0,0 +1,82 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module T1__parameter +Loading module T1 + +[error] at issue1560/T1.cry:7:5--7:6: + Unsolved constraints: + • fin n + arising from + use of literal or demoted expression + at issue1560/T1.cry:7:5--7:6 + where + n is module parameter T1::n at issue1560/T1.cry:1:8--1:10 +[error] at issue1560/T1.cry:7:5--7:6: + Unsolved constraints: + • n >= 1 + arising from + use of literal or demoted expression + at issue1560/T1.cry:7:5--7:6 + where + n is module parameter T1::n at issue1560/T1.cry:1:8--1:10 +Loading module Cryptol +Loading interface module T2__parameter +Loading module T2 + +[error] at issue1560/T2.cry:15:3--15:10: + Failed to validate user-specified signature. + in the definition of 'T2::F::b', at issue1560/T2.cry:15:3--15:4, + we need to show that + for any type m + assuming + • fin n + the following constraints hold: + • m == n + arising from + matching types + at issue1560/T2.cry:15:9--15:10 + where + n is module parameter T2::n at issue1560/T2.cry:1:8--1:10 +Loading module Cryptol +Loading module T3 + +[error] at issue1560/T3.cry:1:1--23:13: + Failed to validate user-specified signature. + when checking the module's parameters, + we need to show that + assuming + • x₁ >= 1 + • x₁ <= 4 + • x >= 1 + • x <= 3 + the following constraints hold: + • x₁ == x + arising from + matching types + at issue1560/T3.cry:23:12--23:13 + where + x is module parameter T3::F::I::x at issue1560/T3.cry:14:30--14:32 + x₁ is module parameter T3::F::G::I::x at issue1560/T3.cry:20:32--20:34 +Loading module Cryptol +Loading module T3 + +[error] at issue1560/T4.cry:1:1--24:13: + Failed to validate user-specified signature. + when checking the module's parameters, + we need to show that + assuming + • x₂ >= 1 + • x₂ <= 4 + • x₁ >= 1 + • x₁ <= 4 + • x >= 1 + • x <= 3 + the following constraints hold: + • x₁ == x + arising from + matching types + at issue1560/T4.cry:24:12--24:13 + where + x is module parameter T3::F::I::x at issue1560/T4.cry:14:30--14:32 + x₁ is module parameter T3::F::G::I::x at issue1560/T4.cry:20:32--20:34 + x₂ is module parameter T3::F::G::J::x at issue1560/T4.cry:21:32--21:34 diff --git a/tests/issues/issue1560/T1.cry b/tests/issues/issue1560/T1.cry new file mode 100644 index 000000000..d0e0b4f75 --- /dev/null +++ b/tests/issues/issue1560/T1.cry @@ -0,0 +1,7 @@ +module T1 where + +parameter + type n: # + +y: [n] +y = 1 diff --git a/tests/issues/issue1560/T2.cry b/tests/issues/issue1560/T2.cry new file mode 100644 index 000000000..d9469caa9 --- /dev/null +++ b/tests/issues/issue1560/T2.cry @@ -0,0 +1,16 @@ +module T2 where + +parameter + type n: # + type constraint (fin n) + +a:[n] +a = a + +submodule F where + parameter + type n: # + + b: {m} [n] -> [m] + b _ = a + diff --git a/tests/issues/issue1560/T3.cry b/tests/issues/issue1560/T3.cry new file mode 100644 index 000000000..2602de38c --- /dev/null +++ b/tests/issues/issue1560/T3.cry @@ -0,0 +1,26 @@ +module T3 where + +interface submodule I1 where + type x: # + type constraint (x >= 1, x <= 3) + +interface submodule I2 where + type x: # + type constraint (x >= 1, x <= 4) + + + +submodule F where + import interface submodule I1 as I + + y: [I::x] + y = 1 + + submodule G where + import interface submodule I2 as I + + csum : [I::x] + csum = y + + + diff --git a/tests/issues/issue1560/T4.cry b/tests/issues/issue1560/T4.cry new file mode 100644 index 000000000..09d9ba729 --- /dev/null +++ b/tests/issues/issue1560/T4.cry @@ -0,0 +1,27 @@ +module T3 where + +interface submodule I1 where + type x: # + type constraint (x >= 1, x <= 3) + +interface submodule I2 where + type x: # + type constraint (x >= 1, x <= 4) + + + +submodule F where + import interface submodule I1 as I + + y: [I::x] + y = 1 + + submodule G where + import interface submodule I2 as I + import interface submodule I2 as J + + csum : [I::x] + csum = y + + + diff --git a/tests/issues/issue582.icry.stdout b/tests/issues/issue582.icry.stdout index 07de82fc5..2b3085073 100644 --- a/tests/issues/issue582.icry.stdout +++ b/tests/issues/issue582.icry.stdout @@ -36,7 +36,7 @@ Loading module Main Failed to validate user-specified signature. in the definition of 'Main::foo', at issue582.cry:2:1--2:4, we need to show that - for any type i, j + for any type j the following constraints hold: • fin j arising from @@ -50,7 +50,7 @@ Loading module Main Failed to validate user-specified signature. in the definition of 'Main::bar', at issue582.cry:5:1--5:4, we need to show that - for any type i, j + for any type j the following constraints hold: • fin j arising from