From d38c99f78ef89b203a4d3e01918d9d93f2da6bf8 Mon Sep 17 00:00:00 2001 From: Ben Orchard Date: Sun, 14 Jul 2024 19:05:17 +0100 Subject: [PATCH] use new Data.Text.Builder.Linear.fromUnboundedDec --- flake.lock | 17 +++++++++++++++++ flake.nix | 5 +++++ package.yaml | 2 +- src/Strongweak/Strengthen.hs | 15 ++++++++------- strongweak.cabal | 4 ++-- 5 files changed, 33 insertions(+), 10 deletions(-) diff --git a/flake.lock b/flake.lock index 7ee959b..8efcece 100644 --- a/flake.lock +++ b/flake.lock @@ -33,6 +33,22 @@ "type": "github" } }, + "linear-builder": { + "flake": false, + "locked": { + "lastModified": 1720637713, + "narHash": "sha256-utDoofUwo4rlkMefgrzB47TBemVhVj6FoJwRgpTHq3o=", + "owner": "Bodigrim", + "repo": "linear-builder", + "rev": "23a07e4d070cc55a45231c2f9b5659692d2fcdc0", + "type": "github" + }, + "original": { + "owner": "Bodigrim", + "repo": "linear-builder", + "type": "github" + } + }, "nixpkgs": { "locked": { "lastModified": 1715037484, @@ -81,6 +97,7 @@ "inputs": { "flake-parts": "flake-parts", "haskell-flake": "haskell-flake", + "linear-builder": "linear-builder", "nixpkgs": "nixpkgs", "rerefined": "rerefined", "singleraeh": "singleraeh", diff --git a/flake.nix b/flake.nix index 886ce41..284b108 100644 --- a/flake.nix +++ b/flake.nix @@ -14,6 +14,8 @@ type-level-show.flake = false; singleraeh.url = "github:raehik/singleraeh"; singleraeh.flake = false; + linear-builder.url = "github:Bodigrim/linear-builder"; + linear-builder.flake = false; }; outputs = inputs: let @@ -39,6 +41,7 @@ packages.rerefined.source = inputs.rerefined; packages.type-level-show.source = inputs.type-level-show; packages.singleraeh.source = inputs.singleraeh; + packages.text-builder-linear.source = inputs.linear-builder; devShell = nondevDevShell "ghc98"; }; haskellProjects.ghc96 = { @@ -46,6 +49,7 @@ packages.rerefined.source = inputs.rerefined; packages.type-level-show.source = inputs.type-level-show; packages.singleraeh.source = inputs.singleraeh; + packages.text-builder-linear.source = inputs.linear-builder; devShell.mkShellArgs.name = "ghc96-strongweak"; }; haskellProjects.ghc94 = { @@ -53,6 +57,7 @@ packages.rerefined.source = inputs.rerefined; packages.type-level-show.source = inputs.type-level-show; packages.singleraeh.source = inputs.singleraeh; + packages.text-builder-linear.source = inputs.linear-builder; devShell = nondevDevShell "ghc94"; }; }; diff --git a/package.yaml b/package.yaml index 181271a..4d9566c 100644 --- a/package.yaml +++ b/package.yaml @@ -63,7 +63,7 @@ dependencies: # strengthening - text >= 2.0 && < 2.2 -- text-builder-linear ^>= 0.1.2 +- text-builder-linear ^>= 0.1.3 # instances - rerefined ^>= 0.5.0 diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs index 693a8f3..d7dcb76 100644 --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -128,12 +128,15 @@ instance Strengthen (NonEmpty a) where -- | Strengthen a plain list into a sized vector by asserting length. instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where - -- TODO another case of TBL not supporting unbounded integrals + -- as of text-linear-builder-0.1.3, we can use 'fromUnboundedDec' for the + -- phantom vector size + -- I don't believe you can actually ever construct a vector with size + -- greater than @'maxBound' \@'Int'@. but still! strengthen as = case VGS.fromList as of Just va -> Right va Nothing -> failStrengthen1 $ - [ "type: [a] -> Vector v "<>fromString (show n)<>" a" + [ "type: [a] -> Vector v "<>TBL.fromUnboundedDec n<>" a" , "fail: wrong length (got "<>TBL.fromDec (length as)<>")" ] where n = natVal'' @n @@ -168,12 +171,10 @@ instance Strengthen Int64 where strengthen = strengthenBounded -- -- @n@ must be "wider" than @m@. -- --- @'FiniteBits' m@ and @'Show' n@ are for error printing. We're forced to --- @'Show' n@ because linear-text-builder can't print unbounded integrals. PR: --- https://github.com/Bodigrim/linear-builder/pull/20 +-- @'FiniteBits' m@ is for error printing. strengthenBounded :: forall m n - . ( Typeable n, Integral n, Show n + . ( Typeable n, Integral n , Typeable m, Integral m, Bounded m, FiniteBits m ) => n -> Either StrengthenFailure' m strengthenBounded n @@ -182,7 +183,7 @@ strengthenBounded n [ "numeric strengthen: "<>fromString (show (typeRep' @n)) <>" -> "<>fromString (show (typeRep' @m)) , "bounds check does not hold: " - <>TBL.fromDec minBm<>" <= "<>fromString (show n) + <>TBL.fromDec minBm<>" <= "<>TBL.fromUnboundedDec n <>" <= "<>TBL.fromDec maxBm ] where diff --git a/strongweak.cabal b/strongweak.cabal index 1b37907..418385e 100644 --- a/strongweak.cabal +++ b/strongweak.cabal @@ -57,7 +57,7 @@ library base >=4.18 && <5 , rerefined >=0.5.0 && <0.6 , text >=2.0 && <2.2 - , text-builder-linear >=0.1.2 && <0.2 + , text-builder-linear >=0.1.3 && <0.2 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.7 default-language: GHC2021 @@ -94,7 +94,7 @@ test-suite spec , rerefined >=0.5.0 && <0.6 , strongweak , text >=2.0 && <2.2 - , text-builder-linear >=0.1.2 && <0.2 + , text-builder-linear >=0.1.3 && <0.2 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.7 default-language: GHC2021