binrep 0.8.0 → 1.0.0

raw patch · 39 files changed

+980/−606 lines, 39 filesdep +ghc-bignumdep +rerefineddep +text-builder-lineardep −refined1dep ~basedep ~bytezapdep ~generic-data-functionsPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-bignum, rerefined, text-builder-linear, type-level-show

Dependencies removed: refined1

Dependency ranges changed: base, bytezap, generic-data-functions, strongweak, text, type-level-bytestrings

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• LICENSE +1/−1
• README.md +17/−7
• binrep.cabal +43/−31
• src/Binrep/BLen.hs +29/−11
• src/Binrep/CBLen.hs +2/−1
• src/Binrep/Example/Sum.hs +16/−0
• src/Binrep/Example/Tga.hs +28/−0
• src/Binrep/Generic.hs +2/−2
• src/Binrep/Get.hs +125/−76
• src/Binrep/Get/Error.hs +49/−81
• src/Binrep/Get/Struct.hs +52/−35
• src/Binrep/Put.hs +17/−10
• src/Binrep/Put/Struct.hs +3/−4
• src/Binrep/Test.hs +0/−26
• src/Binrep/Type/AsciiNat.hs +257/−0
• src/Binrep/Type/Derived/NullTermPadded.hs +2/−1
• src/Binrep/Type/Magic.hs +36/−44
• src/Binrep/Type/NullPadded.hs +18/−18
• src/Binrep/Type/NullTerminated.hs +17/−13
• src/Binrep/Type/Prefix/Count.hs +31/−21
• src/Binrep/Type/Prefix/Internal.hs +65/−0
• src/Binrep/Type/Prefix/Size.hs +23/−18
• src/Binrep/Type/Sized.hs +17/−13
• src/Binrep/Type/Text.hs +3/−3
• src/Binrep/Type/Text/Encoding/Ascii.hs +12/−28
• src/Binrep/Type/Text/Encoding/ShiftJis.hs +3/−2
• src/Binrep/Type/Text/Encoding/Utf16.hs +7/−3
• src/Binrep/Type/Text/Encoding/Utf32.hs +7/−3
• src/Binrep/Type/Text/Encoding/Utf8.hs +3/−2
• src/Binrep/Type/Text/Internal.hs +2/−3
• src/Binrep/Util.hs +0/−31
• src/Binrep/Util/ByteOrder.hs +7/−2
• src/Binrep/Util/Prefix.hs +0/−62
• src/Raehik/Compat/FlatParse/Basic/CutWithPos.hs +15/−0
• src/Util/TypeNats.hs +4/−0
• test/Binrep/GenericSpec.hs +39/−0
• test/Binrep/LawsSpec.hs +0/−54
• test/Binrep/TypesSpec.hs +19/−0

@@ -1,3 +1,12 @@+## 1.0.0 (2024-10-03)+* fix `NullTerminate` check being inverted (OOPS LOL)+* fix `Get [a]` instance (list backwards xd)+* add type-level constructor parsing for generics (!!)+* rewrite `AsciiNat`+* switch from refined to rerefined (my refined rewrite)+* add missing `BLen (GenericallyNonSum a)` instance+* other various cleanup+ ## 0.8.0 (2024-04-13) * add missing `And` predicate combinators instances (`PutC`, `GetC`) * add `Type.Derived.NullTermPadded` (type synonym over `And`)

@@ -1,4 +1,4 @@-Copyright (c) 2022 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>+Copyright (c) 2022-2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the

@@ -7,14 +7,13 @@  # binrep binrep is a Haskell library for *precisely modelling binary schemas*, especially-byte-oriented file formats, and working with them effectively and efficiently.-Here's why it's useful:+low-context byte-oriented file formats e.g. C enums, and working with them+effectively and efficiently. Here's why it's useful:    * **Explicit:** Define Haskell data types with the binary schema "baked in".     Use highly parameterized binary representation primitives including     null-terminated data (e.g. C-style strings), Pascal-style data (length-    prefixed), sized explicit-endian machine integers, null-padded data. Write-    your own primitives if you want (if so, please consider making a PR!).+    prefixed), sized explicit-endian machine integers, null-padded data.   * **Low boilerplate:** Free performant parsers and serializers via generics.     _(See [Generic binary representation](#generic-binary-representation).)_   * **Easy validation:** Use the [strongweak][gh-strongweak] library design@@ -70,12 +69,23 @@ _(Generics are now handled by [generic-data-functions][hackage-gdf]. This info is largely the same, but the code is elsewhere.)_ -binrep's generic deriving makes very few decisions:+binrep includes powerful generics for automatically writing instances.+They all work the same way:    * Constructors are encoded by sequentially encoding every enclosed field.     * Empty constructors thus serialize to 0 bytes.-  * Sum types are encoded via a tag obtained from the constructor names.-    * It's the same approach as aeson, with a bit more flexibility: see below.+  * For sum types, the constructor is disambiguated via a tag obtained from the+    constructor name.+    * Tags may be parsed on the type or term level.++Note that when parsing sum types, we compare tags sequentially. You may design+your tag schema to have a more efficient approach. In such cases, consider using+`Generic.Data.FOnCstr` from [generic-data-functions][hackage-gdf].++As an example, you could encode constructor names as a null-terminated ASCII+bytestring for a tag. (This is provided at `Binrep.Generic.nullTermCstrPfxTag`.)+Alternatively, you may encode each constructor at a unique byte value, stated at+the end of the constructor name.  Sum types (data types with multiple constructors) are handled by first encoding a "tag field", the value of which then indicates which constructor to use. You

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.36.1. -- -- see: https://github.com/sol/hpack  name:           binrep-version:        0.8.0+version:        1.0.0 synopsis:       Encode precise binary representations directly in types description:    Please see README.md. category:       Data, Serialization, Generics@@ -17,7 +17,7 @@ license-file:   LICENSE build-type:     Simple tested-with:-    GHC ==9.4.4+    GHC==9.8 extra-source-files:     README.md     CHANGELOG.md@@ -39,18 +39,21 @@       Binrep.Common.Class.TypeErrors       Binrep.Common.Via.Generically.NonSum       Binrep.Common.Via.Prim+      Binrep.Example.Sum+      Binrep.Example.Tga       Binrep.Generic       Binrep.Get       Binrep.Get.Error       Binrep.Get.Struct       Binrep.Put       Binrep.Put.Struct-      Binrep.Test+      Binrep.Type.AsciiNat       Binrep.Type.Derived.NullTermPadded       Binrep.Type.Magic       Binrep.Type.NullPadded       Binrep.Type.NullTerminated       Binrep.Type.Prefix.Count+      Binrep.Type.Prefix.Internal       Binrep.Type.Prefix.Size       Binrep.Type.Sized       Binrep.Type.Text@@ -61,10 +64,9 @@       Binrep.Type.Text.Encoding.Utf8       Binrep.Type.Text.Internal       Binrep.Type.Thin-      Binrep.Util       Binrep.Util.ByteOrder       Binrep.Util.Generic-      Binrep.Util.Prefix+      Raehik.Compat.FlatParse.Basic.CutWithPos       Raehik.Compat.FlatParse.Basic.Prim       Raehik.Compat.FlatParse.Basic.WithLength       Util.TypeNats@@ -83,22 +85,25 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall+  ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.14 && <5+      base >=4.18 && <5     , bytestring >=0.11 && <0.13-    , bytezap >=1.2.0 && <1.3+    , bytezap >=1.6.0 && <1.7     , deepseq >=1.4.6.1 && <1.6     , defun-core ==0.1.*     , flatparse >=0.5.0.2 && <0.6-    , generic-data-functions >=0.5.0 && <0.6+    , generic-data-functions >=0.6.0 && <0.7     , generic-type-asserts >=0.3.0 && <0.4     , generic-type-functions >=0.1.0 && <0.2+    , ghc-bignum ==1.3.*     , parser-combinators >=1.3.0 && <1.4-    , refined1 ==0.9.*-    , strongweak >=0.6.0 && <0.7-    , text >=1.2.5.0 && <2.1-    , type-level-bytestrings >=0.1.0 && <0.2+    , rerefined >=0.6.0 && <0.7+    , strongweak >=0.9.1 && <0.10+    , text >=2.0 && <2.2+    , text-builder-linear >=0.1.3 && <0.2+    , type-level-bytestrings >=0.1.0 && <0.3+    , type-level-show >=0.3.0 && <0.4   default-language: GHC2021   if flag(icu)     cpp-options: -DHAVE_ICU@@ -110,7 +115,8 @@   main-is: Spec.hs   other-modules:       ArbitraryOrphans-      Binrep.LawsSpec+      Binrep.GenericSpec+      Binrep.TypesSpec       Paths_binrep   hs-source-dirs:       test@@ -125,29 +131,32 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall+  ghc-options: -Wall -Wno-unticked-promoted-constructors   build-tool-depends:       hspec-discover:hspec-discover >=2.7 && <2.12   build-depends:       QuickCheck >=2.14.2 && <2.15-    , base >=4.14 && <5+    , base >=4.18 && <5     , binrep     , bytestring >=0.11 && <0.13-    , bytezap >=1.2.0 && <1.3+    , bytezap >=1.6.0 && <1.7     , deepseq >=1.4.6.1 && <1.6     , defun-core ==0.1.*     , flatparse >=0.5.0.2 && <0.6-    , generic-data-functions >=0.5.0 && <0.6+    , generic-data-functions >=0.6.0 && <0.7     , generic-random >=1.5.0.1 && <1.6     , generic-type-asserts >=0.3.0 && <0.4     , generic-type-functions >=0.1.0 && <0.2+    , ghc-bignum ==1.3.*     , hspec >=2.7 && <2.12     , parser-combinators >=1.3.0 && <1.4     , quickcheck-instances >=0.3.26 && <0.4-    , refined1 ==0.9.*-    , strongweak >=0.6.0 && <0.7-    , text >=1.2.5.0 && <2.1-    , type-level-bytestrings >=0.1.0 && <0.2+    , rerefined >=0.6.0 && <0.7+    , strongweak >=0.9.1 && <0.10+    , text >=2.0 && <2.2+    , text-builder-linear >=0.1.3 && <0.2+    , type-level-bytestrings >=0.1.0 && <0.3+    , type-level-show >=0.3.0 && <0.4   default-language: GHC2021   if flag(icu)     cpp-options: -DHAVE_ICU@@ -172,24 +181,27 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall+  ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.14 && <5+      base >=4.18 && <5     , binrep     , bytestring >=0.11 && <0.13-    , bytezap >=1.2.0 && <1.3+    , bytezap >=1.6.0 && <1.7     , deepseq >=1.4.6.1 && <1.6     , defun-core ==0.1.*     , flatparse >=0.5.0.2 && <0.6     , gauge-    , generic-data-functions >=0.5.0 && <0.6+    , generic-data-functions >=0.6.0 && <0.7     , generic-type-asserts >=0.3.0 && <0.4     , generic-type-functions >=0.1.0 && <0.2+    , ghc-bignum ==1.3.*     , parser-combinators >=1.3.0 && <1.4-    , refined1 ==0.9.*-    , strongweak >=0.6.0 && <0.7-    , text >=1.2.5.0 && <2.1-    , type-level-bytestrings >=0.1.0 && <0.2+    , rerefined >=0.6.0 && <0.7+    , strongweak >=0.9.1 && <0.10+    , text >=2.0 && <2.2+    , text-builder-linear >=0.1.3 && <0.2+    , type-level-bytestrings >=0.1.0 && <0.3+    , type-level-show >=0.3.0 && <0.4   default-language: GHC2021   if flag(icu)     cpp-options: -DHAVE_ICU

@@ -1,4 +1,5 @@ {-# LANGUAGE UndecidableInstances #-} -- for 'ViaCBLen', 'TypeError'+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling  {- | Byte length as a simple pure function, no bells or whistles. @@ -18,7 +19,7 @@  module Binrep.BLen   ( BLen(blen)-  , blenGenericNonSum, blenGenericSum+  , blenGenericNonSum, blenGenericSum, blenGenericSumRaw   , ViaCBLen(..), cblen   ) where @@ -37,10 +38,12 @@ import Data.Monoid qualified as Monoid import GHC.Generics import Generic.Data.Function.FoldMap+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo ) import Generic.Type.Assert+import Binrep.Common.Via.Generically.NonSum -import Refined-import Refined.Unsafe+import Rerefined.Refine+import Rerefined.Predicate.Logical.And  -- | Class for types with easily-calculated length in bytes. --@@ -65,26 +68,41 @@     ) => a -> Int blenGenericNonSum = Monoid.getSum . genericFoldMapNonSum @BLen +instance+  ( Generic a, GFoldMapNonSum BLen (Rep a)+  , GAssertNotVoid a, GAssertNotSum a+  ) => BLen (GenericallyNonSum a) where+    blen = blenGenericNonSum . unGenericallyNonSum+ -- | Measure the byte length of a term of the sum type @a@ via its 'Generic' --   instance.------ You must provide a function to obtain the byte length for the prefix tag, via--- inspecting the reified constructor names. This is regrettably inefficient.--- Alas. Do write your own instance if you want better performance! blenGenericSum+    :: forall sumtag a+    .  ( Generic a, GFoldMapSum BLen sumtag (Rep a)+       , GAssertNotVoid a, GAssertSum a+    ) => ParseCstrTo sumtag Int -> a -> Int+blenGenericSum f =+    Monoid.getSum . genericFoldMapSum @BLen @sumtag (\p -> Monoid.Sum (f p))++-- TODO perhaps provide some handy wrappers that fill in blen for sumtag type+-- with cblen? how to do this well?++-- | Measure the byte length of a term of the sum type @a@ via its 'Generic'+--   instance.+blenGenericSumRaw     :: forall a-    .  ( Generic a, GFoldMapSum BLen (Rep a)+    .  ( Generic a, GFoldMapSum BLen Raw (Rep a)        , GAssertNotVoid a, GAssertSum a     ) => (String -> Int) -> a -> Int-blenGenericSum f =-    Monoid.getSum . genericFoldMapSum @BLen (Monoid.Sum <$> f)+blenGenericSumRaw f =+    Monoid.getSum . genericFoldMapSumRaw @BLen (Monoid.Sum <$> f)  -- We can't provide a Generically instance because the user must choose between -- sum and non-sum handlers.  instance BLen (Refined pr (Refined pl a))   => BLen (Refined (pl `And` pr) a) where-    blen = blen . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine+    blen = blen . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine  instance TypeError ENoEmpty => BLen Void where blen = undefined instance TypeError ENoSum => BLen (Either a b) where blen = undefined

@@ -13,7 +13,8 @@  import DeFun.Core ( type (~>), type App ) -import Refined+import Rerefined.Refine+import Rerefined.Predicate.Logical.And  import Binrep.Common.Class.TypeErrors ( ENoEmpty ) 

@@ -0,0 +1,16 @@+module Binrep.Example.Sum where++import Binrep+import Data.Word+import GHC.Generics ( type Generic )+import Generic.Data.FOnCstr++data SumType = SumType1 Word8 | SumType2 Word8 Word8+    deriving stock (Generic, Show)++instance Get SumType where+    get = do+        get @Word8 >>= \case+          1 -> genericFOnCstr @Get @"SumType1"+          2 -> genericFOnCstr @Get @"SumType2"+          _ -> error "TODO"

@@ -0,0 +1,28 @@+module Binrep.Example.Tga where++{-+import Binrep+import Binrep.Type.Derived.NullTermPadded+import Binrep.Type.AsciiNat+import Rerefined+-}+import Strongweak+import Data.Word++data Header (s :: Strength) a = Header+  { idLen :: SW s Word8+  , colorMapType :: ColorMapType+  , imageType :: ImageType+  --, colorMapSpec :: +  --, imageSpec+  }++data ColorMapType = NoColorMap {- ^ 0 -} | HasColorMap {- ^ 1 -}+data ImageType+  = NoImageData+  | UncompColorMapped+  | UncompTrueColor+  | UncompBW+  | RLEColorMapped+  | RLETrueColor+  | RLEBW

@@ -4,12 +4,12 @@ import Data.ByteString qualified as B import Data.Text qualified as Text import Data.Text.Encoding qualified as Text-import Refined.Unsafe+import Rerefined.Refine ( unsafeRefine )  -- | Turn a constructor name into a prefix tag by adding a null terminator. -- -- Not common in binary data representations, but safe and useful for debugging. nullTermCstrPfxTag :: String -> NullTerminated B.ByteString-nullTermCstrPfxTag = reallyUnsafeRefine . Text.encodeUtf8 . Text.pack+nullTermCstrPfxTag = unsafeRefine . Text.encodeUtf8 . Text.pack -- ^ reallyUnsafeRefine : safe assuming Haskell constructor names are UTF-8 with -- no null bytes allowed

@@ -1,5 +1,6 @@-{-# LANGUAGE UndecidableInstances #-} -- required below GHC 9.6-{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE UndecidableInstances #-} -- for various stuff+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling+{-# LANGUAGE OverloadedStrings #-} -- for easy error building  module Binrep.Get   ( module Binrep.Get@@ -7,18 +8,20 @@   ) where  import Binrep.Get.Error+import Data.Text.Builder.Linear qualified as TBL import Binrep.Util.ByteOrder import Binrep.Common.Via.Prim ( ViaPrim(..) )-import Raehik.Compat.Data.Primitive.Types ( Prim', sizeOf )+import Raehik.Compat.Data.Primitive.Types ( Prim' ) import Raehik.Compat.Data.Primitive.Types.Endian ( ByteSwap ) -import Binrep.Get.Struct ( GetC(getC) )+import Binrep.Get.Struct ( GetC(getC), GetterC ) import Bytezap.Parser.Struct qualified as BZ import Binrep.CBLen ( IsCBLen(CBLen), cblen ) import GHC.TypeLits ( KnownNat )  import FlatParse.Basic qualified as FP import Raehik.Compat.FlatParse.Basic.Prim qualified as FP+import Raehik.Compat.FlatParse.Basic.CutWithPos qualified as FP  import Data.ByteString qualified as B @@ -27,12 +30,13 @@  import GHC.Generics import Generic.Data.Function.Traverse+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo ) import Generic.Type.Assert  import GHC.Exts ( minusAddr#, Int(I#), Int#, plusAddr#, (+#) ) -import Refined-import Refined.Unsafe+import Rerefined.Refine+import Rerefined.Predicate.Logical.And  import Data.Word import Data.Int@@ -40,33 +44,42 @@ import Data.Functor.Identity import Binrep.Common.Via.Generically.NonSum -type Getter a = FP.Parser E a+import Generic.Data.FOnCstr+import Generic.Data.Function.Traverse.Constructor hiding ( ENoEmpty )+import GHC.Exts ( Proxy# ) +type Getter = FP.Parser (ParseError FP.Pos TBL.Builder)+ class Get a where     -- | Parse from binary.     get :: Getter a -runGet :: Get a => B.ByteString -> Either E (a, B.ByteString)+runGet+    :: Get a+    => B.ByteString+    -> Either (ParseError Int TBL.Builder) (a, B.ByteString) runGet = runGetter get -runGetter :: Getter a -> B.ByteString -> Either E (a, B.ByteString)-runGetter g bs = case FP.runParser g bs of-                   FP.OK a bs' -> Right (a, bs')-                   FP.Fail     -> Left EFail-                   FP.Err e    -> Left e+runGetter+    :: Getter a+    -> B.ByteString+    -> Either (ParseError Int TBL.Builder) (a, B.ByteString)+runGetter p bs =+    case FP.runParser p bs of+      FP.OK   a bs' -> Right (a, bs')+      FP.Err  e     ->+        -- TODO check this is right. might need length of bs' ... ?+        Left $ fmap (mapParseErrorSinglePos (\(FP.Pos pos) -> len - pos)) e+      FP.Fail       -> Left []+  where len = B.length bs  instance GenericTraverse Get where-    type GenericTraverseF Get = FP.Parser E+    type GenericTraverseF Get = Getter     type GenericTraverseC Get a = Get a-    genericTraverseAction cd cc mcs si =-        getWrapGeneric cd $ EGenericField cc mcs si--instance GenericTraverseSum Get where-    genericTraverseSumPfxTagAction cd =-        getWrapGeneric cd $ EGenericSum . EGenericSumTag-    -- TODO proper offset info-    genericTraverseSumNoMatchingCstrAction cd cstrs ptText =-        FP.err $ E 0 $ EGeneric cd $ EGenericSum $ EGenericSumTagNoMatch cstrs ptText+    genericTraverseAction dtName cstrName mFieldName fieldIdx =+        get `cutting1` e+      where+        e = parseErrorTextGenericFieldBld dtName cstrName mFieldName fieldIdx  getGenericNonSum     :: forall a@@ -82,72 +95,111 @@     get = GenericallyNonSum <$> getGenericNonSum  getGenericSum+    :: forall sumtag pt a+    .  ( Generic a, GTraverseSum Get sumtag (Rep a)+       , Get pt+       , GAssertNotVoid a, GAssertSum a+    ) => ParseCstrTo sumtag pt+      -> (pt -> pt -> Bool)+      -> Getter a+getGenericSum parseCstr ptEq =+    genericTraverseSum @Get @sumtag parseCstr ptGet fNoMatch ptEq+  where+      fNoMatch dtName = err1 (parseErrorTextGenericNoCstrMatchBld dtName)+      ptGet dtName = get `cutting1` parseErrorTextGenericSumTagBld dtName++getGenericSumRaw     :: forall pt a-    .  ( Generic a, GTraverseSum Get (Rep a)+    .  ( Generic a, GTraverseSum Get Raw (Rep a)        , Get pt        , GAssertNotVoid a, GAssertSum a-    ) => PfxTagCfg pt -> Getter a-getGenericSum = genericTraverseSum @Get+    ) => (String -> pt)+      -> (pt -> pt -> Bool)+      -> Getter a+getGenericSumRaw parseCstr ptEq =+    genericTraverseSumRaw @Get parseCstr ptGet fNoMatch ptEq+  where+      fNoMatch dtName = err1 (parseErrorTextGenericNoCstrMatchBld dtName)+      ptGet dtName = get `cutting1` parseErrorTextGenericSumTagBld dtName --- We can't provide a Generically instance because the user must choose between--- sum and non-sum handlers.+-- | Emit a single error. Use with flatparse primitives that only 'FP.Fail'.+err1 :: [text] -> FP.ParserT st (ParseError FP.Pos text) a+err1 = FP.err' . parseError1 -eBase :: EBase -> Getter a-eBase eb = FP.ParserT \_fp eob s st ->-    let os = I# (minusAddr# eob s)-     in FP.Err# st (E os $ EBase eb)+-- | Turn a 'FP.Fail' into a single error. (Re-emits existing 'FP.Error's.)+--+-- Use when wrapping flatparse primitives that directly only 'FP.Fail'. (It's+-- fine to use with combinators if the combinator itself doesn't 'FP.Error'.)+cut1+    :: FP.ParserT st (ParseError FP.Pos text) a -> [text]+    -> FP.ParserT st (ParseError FP.Pos text) a+cut1 p texts = p `FP.cut'` parseError1 texts -getEBase :: Getter a -> EBase -> Getter a-getEBase (FP.ParserT f) eb =-    FP.ParserT \fp eob s st ->-        let os = I# (minusAddr# eob s)-         in case f fp eob s st of-              FP.Fail# st'   -> FP.Err# st' (E os $ EBase eb)-              FP.Err#  st' e -> FP.Err# st' (E os $ EAnd e eb)-              x -> x+-- | Turn a 'FP.Fail' into a single error, or prepend it to any existing ones.+--+-- Use when wrapping other 'get'ters.+--+-- We reimplement 'FP.cutting' with a tweak. Otherwise, we'd have to join lists+-- in the error case (instead of simply prepending).+cutting1+    :: FP.ParserT st (ParseError FP.Pos text) a -> [text]+    -> FP.ParserT st (ParseError FP.Pos text) a+cutting1 (FP.ParserT p) texts =+    FP.getPos >>= \pos -> FP.ParserT $ \fp eob s st ->+        case p fp eob s st of+          FP.Fail# st'    -> FP.Err# st' [ParseErrorSingle pos texts]+          FP.Err#  st' e' -> FP.Err# st' (ParseErrorSingle pos texts : e')+          x            -> x --- | Convert a bytezap struct parser to a flatparse parser.-bzToFp-    :: forall a e st. KnownNat (CBLen a)-    => BZ.ParserT st e a -> FP.ParserT st e a-bzToFp (BZ.ParserT p) = FP.ensure (I# len#) >> (FP.ParserT $ \fpc _eob s st0 ->-    case p fpc s 0# st0 of-      BZ.OK#   st1 a -> FP.OK#   st1 a (s `plusAddr#` len#)-      BZ.Fail# st1   -> FP.Fail# st1-      BZ.Err#  st1 e -> FP.Err#  st1 e-    )-  where-    !(I# len#) = cblen @a+-- We can't provide a Generically instance because the user must choose between+-- sum and non-sum handlers. +instance GenericFOnCstr Get where+    type GenericFOnCstrF Get = Getter+    type GenericFOnCstrC Get dtName cstrName gf =+        GTraverseC Get dtName cstrName 0 gf+    genericFOnCstrF (_ :: Proxy# '(dtName, cstrName)) =+        gTraverseC @Get @dtName @cstrName @0++-- TODO this is hard to parse visually. document...? fpToBz-    :: FP.ParserT st e a -> Int#-    -> (a -> Int# -> BZ.ParserT st e r) -> BZ.ParserT st e r+    :: FP.ParserT st (ParseError FP.Pos text) a -> Int#+    -> (a -> Int# -> BZ.ParserT st (ParseError Int text) r)+    -> BZ.ParserT st (ParseError Int text) r fpToBz (FP.ParserT p) len# fp = BZ.ParserT $ \fpc base# os# st0 ->     case p fpc (base# `plusAddr#` (os# +# len#)) (base# `plusAddr#` os#) st0 of       FP.OK#   st1 a s ->         let unconsumed# = s `minusAddr#` (base# `plusAddr#` os#)         in  BZ.runParserT# (fp a unconsumed#) fpc base# (os# +# unconsumed#) st1+      FP.Err#  st1 e   ->+        -- on error, we turn the flatparse 'FP.Pos' indices into actual byte+        -- offsets (which bytezap deals in), then emit+        let e' = fmap (mapParseErrorSinglePos (\(FP.Pos pos) -> I# len# - pos)) e+        in  BZ.Err# st1 e'       FP.Fail# st1     -> BZ.Fail# st1-      FP.Err#  st1 e   -> BZ.Err#  st1 e --- | Parse. On parse error, coat it in a generic context layer.-getWrapGeneric :: Get a => String -> (E -> EGeneric E) -> Getter a-getWrapGeneric = getWrapGeneric' get--getWrapGeneric' :: Getter a -> String -> (E -> EGeneric E) -> Getter a-getWrapGeneric' (FP.ParserT f) cd fe =-    FP.ParserT \fp eob s st ->-        let os = I# (minusAddr# eob s)-         in case f fp eob s st of-              FP.Fail# st'   -> FP.Err# st' (E os $ EGeneric cd $ fe EFail)-              FP.Err#  st' e -> FP.Err# st' (E os $ EGeneric cd $ fe e)-              x -> x- newtype ViaGetC a = ViaGetC { unViaGetC :: a } instance (GetC a, KnownNat (CBLen a)) => Get (ViaGetC a) where     {-# INLINE get #-}     get = ViaGetC <$> bzToFp getC +-- TODO messy ran out of input handling. should be a util for it+-- TODO pos handling seems correct on quick test. need stronger assertion plz+bzToFp :: forall a. KnownNat (CBLen a) => GetterC a -> Getter a+bzToFp (BZ.ParserT p) =+    (FP.ensure (I# len#) `cut1` eRanOut) >> FP.getPos >>= \(FP.Pos pos) ->+        FP.ParserT $ \fpc _eob s st0 ->+            case p fpc s 0# st0 of+              BZ.OK#   st1 a -> FP.OK#   st1 a (s `plusAddr#` len#)+              BZ.Err#  st1 e ->+                let e' = fmap (mapParseErrorSinglePos (\idx -> FP.Pos (pos - idx))) e+                in  FP.Err# st1 e'+              BZ.Fail# st1   -> FP.Fail# st1+  where+    !(I# len#) = cblen @a+    eRanOut = [ "ran out of input while running inner parser"+              , "bytes needed: "<>TBL.fromDec (I# len#) ]+ instance TypeError ENoEmpty => Get Void where get = undefined instance TypeError ENoSum => Get (Either a b) where get = undefined @@ -181,13 +233,10 @@  -- | Parse elements until EOF. Sometimes used at the "top" of binary formats. instance Get a => Get [a] where-    get = go+    -- TODO slow, uses reverse. build a DList instead+    get = go []       where-        go = do-            FP.withOption FP.eof (\() -> pure []) $ do-                a <- get-                as <- go-                pure $ a : as+        go as = FP.branch FP.eof (pure (reverse as)) (get >>= \a -> go (a : as))  -- | Return the rest of the input. --@@ -217,7 +266,7 @@  -- | Parse any 'Prim''. getPrim :: forall a. Prim' a => Getter a-getPrim = getEBase FP.anyPrim (ERanOut (sizeOf (undefined :: a)))+getPrim = FP.anyPrim `FP.cut'` parseError1 ["IDK"]  instance Prim' a => Get (ViaPrim a) where get = ViaPrim <$> getPrim @@ -229,7 +278,7 @@     instance (Prim' a, ByteSwap a) => Get (ByteOrdered    'BigEndian a)  instance Get (Refined pr (Refined pl a)) => Get (Refined (pl `And` pr) a) where-    get = (reallyUnsafeRefine . unrefine @pl . unrefine @pr) <$> get+    get = (unsafeRefine . unrefine @pl . unrefine @pr) <$> get  {- 

@@ -1,92 +1,60 @@--- | Error data type definitions (shared between parsers).+{-# LANGUAGE OverloadedStrings #-} -- for easy error building +-- | Common parser error definitions.+ module Binrep.Get.Error where -import GHC.Generics ( Generic )-import Data.Text ( Text )+import Data.Text.Builder.Linear qualified as TBL+import Data.Text qualified as Text import Numeric.Natural ( Natural )-import Data.Word ( Word8 )-import Data.ByteString ( ByteString ) --- | Structured parse error.-data E-  = E Int EMiddle--  -- | Unhandled parse error.-  ---  -- You get this if you don't change a flatparse fail to an error.-  ---  -- Should not be set except by library code.-  | EFail--    deriving stock (Eq, Show, Generic)--data EMiddle--  -- | Parse error with no further context.-  = EBase EBase--  -- | Somehow, we got two parse errors.-  ---  -- I have a feeling that seeing this indicates a problem in your code.-  | EAnd E EBase--  -- | Parse error decorated with generic info.-  ---  -- Should not be set except by library code.-  | EGeneric String {- ^ data type name -} (EGeneric E)--    deriving stock (Eq, Show, Generic)--data EBase-  = EExpectedByte Word8 Word8-  -- ^ expected first, got second--  | EOverlong Int Int-  -- ^ expected first, got second--  | EExpected ByteString ByteString-  -- ^ expected first, got second--  | EFailNamed String-  -- ^ known fail--  | EFailParse String ByteString Word8-  -- ^ parse fail (where you parse a larger object, then a smaller one in it)+-- | Top-level parse error.+--+-- The final element is the concrete error. Prior elements should "contain" the+-- error (i.e. be the larger part that the error occurred in).+--+-- Really should be non-empty-- but by using List, we can use the empty list for+-- Fail. Bit of a cute cheat.+type ParseError pos text = [ParseErrorSingle pos text] -  | ERanOut Int-  -- ^ ran out of input, needed precisely @n@ bytes for this part (n > 0)-  ---  -- Actually a 'Natural', but we use 'Int' because that's what flatparse uses-  -- internally.+-- | A single indexed parse error.+data ParseErrorSingle pos text = ParseErrorSingle+  { parseErrorSinglePos  :: pos+  , parseErrorSingleText :: [text]+  } deriving stock Show -    deriving stock (Eq, Show, Generic)+-- | Map over the @pos@ index type of a 'ParseErrorSingle'.+mapParseErrorSinglePos+    :: (pos1 -> pos2)+    -> ParseErrorSingle pos1 text+    -> ParseErrorSingle pos2 text+mapParseErrorSinglePos f (ParseErrorSingle pos text) =+    ParseErrorSingle (f pos) text --- | A generic context layer for a parse error of type @e@.------ Recursive: parse errors occurring in fields are wrapped up here. (Those--- errors may also have a generic context layer.)------ Making this explicitly recursive may seem strange, but it clarifies that this--- data type is to be seen as a layer over a top-level type.-data EGeneric e-  -- | Parse error relating to sum types (constructors).-  = EGenericSum (EGenericSum e)+-- | Shorthand for one parse error.+parseError1 :: [text] -> pos -> ParseError pos text+parseError1 texts pos = [ParseErrorSingle pos texts] -  -- | Parse error in a constructor field.-  | EGenericField-        String          -- ^ constructor name-        (Maybe String)  -- ^ field record name (if present)-        Natural         -- ^ field index in constructor-        e               -- ^ field parse error-    deriving stock (Eq, Show, Generic)+-- | Construct a parse error message for a generic field failure.+parseErrorTextGenericFieldBld+    :: String -> String -> Maybe String -> Natural+    -> [TBL.Builder]+parseErrorTextGenericFieldBld dtName cstrName (Just fieldName) _fieldIdx =+  [    "in " <> TBL.fromText (Text.pack dtName)+    <>   "." <> TBL.fromText (Text.pack cstrName)+    <>   "." <> TBL.fromText (Text.pack fieldName) ]+parseErrorTextGenericFieldBld dtName cstrName Nothing           fieldIdx =+  [    "in " <> TBL.fromText (Text.pack dtName)+    <>   "." <> TBL.fromText (Text.pack cstrName)+    <>   "." <> TBL.fromUnboundedDec fieldIdx ] -data EGenericSum e-  -- | Parse error parsing prefix tag.-  = EGenericSumTag e+-- | Construct a parse error message for a generic sum tag no-match.+parseErrorTextGenericNoCstrMatchBld :: String -> [TBL.Builder]+parseErrorTextGenericNoCstrMatchBld dtName =+  [    "sum tag did not match any constructors in "+    <> TBL.fromText (Text.pack dtName) ] -  -- | Unable to match a constructor to the parsed prefix tag.-  | EGenericSumTagNoMatch-        [String] -- ^ constructors tested-        Text     -- ^ prettified prefix tag-    deriving stock (Eq, Show, Generic)+-- | Construct a parse error message for a generic sum tag parse error.+parseErrorTextGenericSumTagBld :: String -> [TBL.Builder]+parseErrorTextGenericSumTagBld dtName =+  [    "while parsing sum tag in " <> TBL.fromText (Text.pack dtName) ]

@@ -1,8 +1,15 @@ {-# LANGUAGE UndecidableInstances #-} -- for Generically instance+{-# LANGUAGE OverloadedStrings #-} -- for easy error building -module Binrep.Get.Struct where+module Binrep.Get.Struct+  ( GetterC, GetC(getC)+  , getGenericStruct+  , runGetCBs+  , unsafeRunGetCPtr+  ) where  import Binrep.Get.Error+import Data.Text.Builder.Linear qualified as TBL import Bytezap.Parser.Struct import Bytezap.Parser.Struct.Generic import Binrep.CBLen@@ -27,46 +34,67 @@  import Binrep.Common.Via.Generically.NonSum -import Refined-import Refined.Unsafe+import Rerefined.Refine+import Rerefined.Predicate.Logical.And -type GetterC = Parser E+type GetterC = Parser (ParseError Int TBL.Builder)  -- | constant size parser class GetC a where getC :: GetterC a +-- | Consume 'Result'.+finishGetterC+    :: Result (ParseError Int TBL.Builder) a+    -> Either (ParseError Int TBL.Builder) a+finishGetterC = \case+  OK  a -> Right a+  Err e -> Left  e+  Fail  -> Left  []+ runGetCBs     :: forall a. (GetC a, KnownNat (CBLen a))-    => B.ByteString -> Either E a+    => B.ByteString -> Either (ParseError Int TBL.Builder) a runGetCBs bs =-    if   cblen @a <= B.length bs-    then unsafeRunGetC' unsafeRunParserBs bs-    else Left $ E 0 $ EBase $ ERanOut 0 -- TODO made up numbers---- | doesn't check len-unsafeRunGetC'-    :: forall a buf. GetC a-    => (forall e. buf -> Parser e a -> Result e a)-    -> buf -> Either E a-unsafeRunGetC' p buf =-    case p buf getC of-      OK   a -> Right a-      Fail   -> Left EFail-      Err  e -> Left e+    if   lenReq <= lenAvail+    then finishGetterC $ unsafeRunParserBs bs getC+    else Left [ParseErrorSingle 0 [errMsg]]+  where+    lenReq   = cblen @a+    lenAvail = B.length bs+    errMsg   =+        "input too short (need "<>TBL.fromDec lenReq+                      <>", got "<>TBL.fromDec lenAvail<>")"  -- | doesn't check len unsafeRunGetCPtr     :: forall a. GetC a-    => Ptr Word8 -> Either E a-unsafeRunGetCPtr = unsafeRunGetC' unsafeRunParserPtr+    => Ptr Word8 -> Either (ParseError Int TBL.Builder) a+unsafeRunGetCPtr ptr = finishGetterC $ unsafeRunParserPtr ptr getC  instance GParseBase GetC where     type GParseBaseSt GetC = Proxy# Void     type GParseBaseC  GetC a = GetC a-    type GParseBaseE  GetC = E-    gParseBase = getC+    type GParseBaseE  GetC = ParseError Int TBL.Builder+    gParseBase dtName cstrName mFieldName fieldIdx = getC `cutting1` e+      where+        e = parseErrorTextGenericFieldBld dtName cstrName mFieldName fieldIdx     type GParseBaseLenTF GetC = CBLenSym +-- | Turn a 'Fail' into a single error, or prepend it to any existing ones.+--+-- Use when wrapping other 'get'ters.+--+-- We reimplement @cutting@ with a tweak. Otherwise, we'd have to join lists in+-- the error case (instead of simply prepending).+cutting1+    :: ParserT st (ParseError Int text) a -> [text]+    -> ParserT st (ParseError Int text) a+cutting1 (ParserT p) texts = ParserT $ \fpc base# os# st ->+    case p fpc base# os# st of+      Fail# st'    -> Err# st' [ParseErrorSingle (I# os#) texts]+      Err#  st' e' -> Err# st' (ParseErrorSingle (I# os#) texts : e')+      x               -> x+ -- | Serialize a term of the struct-like type @a@ via its 'Generic' instance. getGenericStruct     :: forall a@@ -89,7 +117,7 @@  instance GetC (Refined pr (Refined pl a))   => GetC (Refined (pl `And` pr) a) where-    getC = (reallyUnsafeRefine . unrefine @pl . unrefine @pr) <$> getC+    getC = (unsafeRefine . unrefine @pl . unrefine @pr) <$> getC  instance GetC () where     {-# INLINE getC #-}@@ -128,14 +156,3 @@     putC (l, r) = sequencePokes (putC l) (cblen @l) (putC r)  -}--eCBase :: EBase -> GetterC a-eCBase eb = ParserT $ \_fpc _base os# st ->-    Err# st (E (I# os#) $ EBase eb)--getECBase :: GetterC a -> EBase -> GetterC a-getECBase (ParserT p) eb = ParserT $ \fpc base os# st0 ->-    case p fpc base os# st0 of-      Fail# st1   -> Err# st1 (E (I# os#) $ EBase eb)-      Err#  st1 e -> Err# st1 (E (I# os#) $ EAnd e eb)-      x -> x

@@ -1,4 +1,5 @@-{-# LANGUAGE UndecidableInstances #-} -- required below GHC 9.6+{-# LANGUAGE UndecidableInstances #-} -- for various stuff+{-# LANGUAGE AllowAmbiguousTypes #-} -- for type-level sum type handling  module Binrep.Put where @@ -17,14 +18,15 @@  import GHC.Generics import Generic.Data.Function.FoldMap+import Generic.Data.MetaParse.Cstr ( Raw, ParseCstrTo ) import Generic.Type.Assert  import Control.Monad.ST ( RealWorld )  import Binrep.Put.Struct ( PutC(putC) ) -import Refined-import Refined.Unsafe+import Rerefined.Refine+import Rerefined.Predicate.Logical.And  import Data.Word import Data.Int@@ -59,16 +61,21 @@     put = putGenericNonSum . unGenericallyNonSum  -- | Serialize a term of the sum type @a@ via its 'Generic' instance.------ You must provide a serializer for @a@'s constructors. This is regrettably--- inefficient due to having to use 'String's. Alas. Do write your own instance--- if you want better performance! putGenericSum+    :: forall sumtag a+    .  ( Generic a, GFoldMapSum Put sumtag (Rep a)+       , GAssertNotVoid a, GAssertSum a+    ) => ParseCstrTo sumtag Putter -> a -> Putter+putGenericSum = genericFoldMapSum @Put @sumtag++-- | Serialize a term of the sum type @a@ via its 'Generic' instance, without+--   pre-parsing constructor names.+putGenericSumRaw     :: forall a-    .  ( Generic a, GFoldMapSum Put (Rep a)+    .  ( Generic a, GFoldMapSum Put Raw (Rep a)        , GAssertNotVoid a, GAssertSum a     ) => (String -> Putter) -> a -> Putter-putGenericSum = genericFoldMapSum @Put+putGenericSumRaw = genericFoldMapSumRaw @Put  newtype ViaPutC a = ViaPutC { unViaPutC :: a } instance (PutC a, KnownNat (CBLen a)) => Put (ViaPutC a) where@@ -129,4 +136,4 @@ -- | Put types refined with multiple predicates by wrapping the left --   predicate with the right. LOL REALLY? instance Put (Refined pr (Refined pl a)) => Put (Refined (pl `And` pr) a) where-    put = put . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine+    put = put . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine

@@ -26,8 +26,8 @@  import Binrep.Common.Via.Generically.NonSum -import Refined-import Refined.Unsafe+import Rerefined.Refine+import Rerefined.Predicate.Logical.And  type PutterC = Struct.Poke RealWorld @@ -65,8 +65,7 @@  instance PutC (Refined pr (Refined pl a))   => PutC (Refined (pl `And` pr) a) where-    putC =-        putC . reallyUnsafeRefine @_ @pr . reallyUnsafeRefine @_ @pl . unrefine+    putC = putC . unsafeRefine @_ @pr . unsafeRefine @_ @pl . unrefine  instance Prim' a => PutC (ViaPrim a) where     putC = Struct.prim . unViaPrim

@@ -1,26 +0,0 @@-{-# LANGUAGE UndecidableInstances #-} -- for CBLen instances--module Binrep.Test where--import Binrep-import Binrep.Type.Magic-import GHC.Generics ( Generic )-import Data.Word-import Binrep.Util.ByteOrder--import Binrep.Common.Via.Generically.NonSum--data DMagic = DMagic-  { dMagic1_8b :: Magic '[0xFF, 0, 1, 0, 1, 0, 1, 0xFF]-  } deriving stock Generic-    deriving (IsCBLen, PutC) via GenericallyNonSum DMagic--data DMagicSum = DMagicSum1 (Magic '[0]) | DMagicSum2 (Magic '[0xFF])-    deriving stock Generic--data DStruct = DStruct-  { dStruct1 :: Magic '[0xFF, 0, 1, 0xFF]-  , dStruct2 :: ByteOrdered LE Word32-  , dStruct3 :: ()-  } deriving stock (Generic, Show)-    deriving (IsCBLen, PutC, GetC) via GenericallyNonSum DStruct

@@ -0,0 +1,257 @@+{-| Naturals represented via ASCII digits.++A concept which sees occasional use in places where neither speed nor size+efficiency matter. The tar file format uses it, apparently to sidestep making a+decision on byte ordering. Pretty silly.++As with other binrep string-likes, you probably want to wrap this with+'Binrep.Type.Sized.Sized' or 'Binrep.Type.Prefix.Size.SizePrefixed'.++We use a refinement to permit using any numeric type, while ensuring that+negative values are not permitted.+-}++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE OverloadedStrings #-} -- for refined error+{-# LANGUAGE UndecidableInstances #-} -- for deriving predicate instance++module Binrep.Type.AsciiNat where++import Binrep++import GHC.Exts ( Word(W#), Word#, Int(I#), word2Int#, eqWord#, plusWord# )+import Util.TypeNats ( natValWord )+import Data.Semigroup ( sconcat )++import GHC.Num.Primitives ( wordLogBase# )+import GHC.Num.Natural ( naturalSizeInBase# )++import Data.Word+import Data.Int+import Data.List.NonEmpty ( NonEmpty( (:|) ) )++import GHC.TypeNats ( Natural, KnownNat )++import Data.ByteString qualified as B+import Binrep.Type.Thin ( Thin(Thin) )++import Rerefined.Predicate+import Rerefined.Predicate.Via+import Rerefined.Predicate.Relational.Value+import Rerefined.Predicate.Relational+import Rerefined.Refine+import TypeLevelShow.Natural+import TypeLevelShow.Utils++import Data.Text.Builder.Linear qualified as TBL++-- | A natural represented in binary as an ASCII string, where each character is+--   a digit in the given base.+--+-- Only certain bases are supported: 2, 8, 10 and 16.+--+-- Hex parsing permits mixed case digits when parsing (@1-9a-fA-F@), and+-- serializes with lower-case ASCII hex digits.+data AsciiNat (base :: Natural)+--type AsciiNat base = Refined (AsciiNat base)++instance Predicate (AsciiNat base) where+    type PredicateName d (AsciiNat base) = ShowParen (d > 9)+        ("AsciiNat " ++ ShowNatDec base)++instance (KnownPredicateName (AsciiNat base), Num a, Ord a)+  => Refine (AsciiNat base) a where+    validate = validateVia @(CompareValue GTE Pos 0)++-- | Compare two 'AsciiNat's, ignoring base information.+asciiNatCompare+    :: Ord a => Refined (AsciiNat bl) a -> Refined (AsciiNat br) a -> Ordering+asciiNatCompare l r = compare (unrefine l) (unrefine r)++-- | The bytelength of an 'AsciiNat' is the number of digits in the number in+--   the given base. We can calculate this generally with great efficiency+--   using GHC (ghc-bignum) primitives!+instance (HasBaseOps a, KnownNat base) => BLen (Refined (AsciiNat base) a) where+    blen n = I# (word2Int# (sizeInBase# base# (unrefine n)))+      where+        !(W# base#) = natValWord @base++class HasBaseOps a where+    -- | See ghc-bignum internals at @GHC.Num.*@.+    sizeInBase# :: Word# -> a -> Word#++instance HasBaseOps Word    where sizeInBase# = sizeInBaseWordSize+instance HasBaseOps Natural where+    sizeInBase# base = \case+      0 -> 1##+      a -> naturalSizeInBase# base a++instance HasBaseOps Word8  where sizeInBase# = sizeInBaseWordSize+instance HasBaseOps Word16 where sizeInBase# = sizeInBaseWordSize+instance HasBaseOps Word32 where sizeInBase# = sizeInBaseWordSize++-- | TODO unsafe for 32-bit platform+instance HasBaseOps Word64 where sizeInBase# = sizeInBaseWordSize++instance HasBaseOps Int8   where sizeInBase# = sizeInBaseWordSize+instance HasBaseOps Int16  where sizeInBase# = sizeInBaseWordSize+instance HasBaseOps Int32  where sizeInBase# = sizeInBaseWordSize++-- | TODO unsafe for 32-bit platform+instance HasBaseOps Int64  where sizeInBase# = sizeInBaseWordSize++-- | 'Int' can use 'Word' size (but TODO what happens for negatives?)+instance HasBaseOps Int  where sizeInBase# = sizeInBaseWordSize++-- | Safe for types smaller than a 'Word'.+--+-- Uses ghc-bignum internals. Slightly unwrapped for better performance.+--+-- One could perhaps write faster algorithms for smaller primitive types too...+-- but performance increase would be minimal if even present.+sizeInBaseWordSize :: Integral a => Word# -> a -> Word#+sizeInBaseWordSize base a =+    case w# `eqWord#` 0## of+      1# -> 1##+      _  -> 1## `plusWord#` wordLogBase# base w#+  where+    !(W# w#) = fromIntegral a++-- | Serialize any term of an 'Integral' type to binary (base 2) ASCII.+instance Integral a => Put (Refined (AsciiNat  2) a) where+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8  2 . unrefine++-- | Serialize any term of an 'Integral' type to octal (base 8) ASCII.+instance Integral a => Put (Refined (AsciiNat  8) a) where+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8  8 . unrefine++-- | Serialize any term of an 'Integral' type to decimal (base 10) ASCII.+instance Integral a => Put (Refined (AsciiNat 10) a) where+    put = sconcat . fmap (put . (+) 0x30) . unsafeDigits @Word8 10 . unrefine++-- | Serialize any term of an 'Integral' type to hex (base 16) ASCII.+--+-- Uses lower-case ASCII.+instance Integral a => Put (Refined (AsciiNat 16) a) where+    put =+          sconcat . fmap (put . unsafeHexDigitToAsciiLower)+        . unsafeDigits @Word8 16 . unrefine++-- | Parse a  binary  (base 2) ASCII natural to any 'Num' type.+instance (Num a, Ord a) => Get (Refined (AsciiNat  2)  a) where+    get = unsafeRefine <$> getAsciiNatByByte 2  "binary"  parseBinaryAsciiDigit++-- | Parse an octal   (base 8) ASCII natural to any 'Num' type.+instance (Num a, Ord a) => Get (Refined (AsciiNat  8)  a) where+    get = unsafeRefine <$> getAsciiNatByByte 8  "octal"   parseOctalAsciiDigit++-- | Parse a  decimal (base 10) ASCII natural to any 'Num' type.+instance (Num a, Ord a) => Get (Refined (AsciiNat 10) a) where+    get = unsafeRefine <$> getAsciiNatByByte 10 "decimal" parseDecimalAsciiDigit++-- | Parse a  hex     (base 16) ASCII natural to any 'Num' type.+--+-- Parses lower and upper case (mixed permitted).+instance (Num a, Ord a) => Get (Refined (AsciiNat 16) a) where+    get = unsafeRefine <$> getAsciiNatByByte 16 "hex"     parseHexAsciiDigit++-- | Parse an ASCII natural in the given base with the given digit parser.+--+-- Parses byte-by-byte. As such, it only supports bases up to 256.+getAsciiNatByByte :: Num a => a -> TBL.Builder -> (a -> Maybe a) -> Getter a+getAsciiNatByByte base baseStr f = do+    Thin bs <- get -- no need to copy since we consume during parsing!+    if   B.null bs+    then err1 ["ASCII natural cannot be empty"]+    else case asciiBytesToNat f base bs of+          Left  b -> err1 [+            "non-"<>baseStr<>" ASCII digit in "+            <>baseStr<>" ASCII natural: "<>TBL.fromDec b]+          Right n -> pure n++{- | Get the digits in the given number as rendered in the given base.++Digits will be between 0-base. The return type must be sized to support this.++Base must be > 2. This is not checked. (Internal function eh.)++Note the 'NonEmpty' return type. Returns @[0]@ for 0 input. (This does not match+ghc-bignum's @sizeInBase@ primitives!)+-}+unsafeDigits :: forall b a. (Integral a, Integral b) => a -> a -> NonEmpty b+unsafeDigits base = go []+  where+    go s x = loop (head' :| s) tail'+      where+        head' = fromIntegral (x `mod` base)+        tail' = x `div` base+    loop s@(r :| rs) = \case+        0 -> s+        x -> go (r : rs) x++asciiBytesToNat+    :: Num a => (a -> Maybe a) -> a -> B.ByteString -> Either Word8 a+asciiBytesToNat f base bs =+    -- we use Int for exponent because it seems most sensible & gets SPECIALISEd+    case B.foldr go (Right (0, (0 :: Int))) bs of+      Left w -> Left w+      Right (n, _) -> Right n+  where+    go _ (Left w) = Left w+    go w (Right (n, expo)) =+        case f (fromIntegral w) of+          Nothing -> Left w+          Just d  -> Right (n + d * base^expo, expo+1)++parseBinaryAsciiDigit :: (Num a, Ord a) => a -> Maybe a+parseBinaryAsciiDigit = \case+  0x30 -> Just 0 -- 0+  0x31 -> Just 1 -- 1+  _    -> Nothing++parseOctalAsciiDigit :: (Num a, Ord a) => a -> Maybe a+parseOctalAsciiDigit a+  | a >= 0x30 && a <= 0x37 = Just $ a - 0x30 -- 0-7+  | otherwise = Nothing++parseDecimalAsciiDigit :: (Num a, Ord a) => a -> Maybe a+parseDecimalAsciiDigit a+  | a >= 0x30 && a <= 0x39 = Just $ a - 0x30 -- 0-9+  | otherwise = Nothing++parseHexAsciiDigit :: (Num a, Ord a) => a -> Maybe a+parseHexAsciiDigit a+  | a >= 0x30 && a <= 0x39 = Just $ a - 0x30 -- 0-9+  | a >= 0x41 && a <= 0x46 = Just $ a - 0x37 -- A-F (upper case)+  | a >= 0x61 && a <= 0x66 = Just $ a - 0x57 -- a-f (lower case)+  | otherwise = Nothing++-- | May only be called with 0<=n<=15.+unsafeHexDigitToAsciiLower :: (Num a, Ord a) => a -> a+unsafeHexDigitToAsciiLower a+  | a <= 9    = 0x30 + a+  | otherwise = 0x57 + a++{-++-- | Print a binary (base 2) ASCII natural with an @0b@ prefix.+prettyAsciiNat2 :: Integral a => Int -> a -> ShowS+prettyAsciiNat2 _ n = showString "0b" . showBin n++-- | Show binary (base 2) ASCII naturals with an @0b@ prefix.+instance Integral a => Show (AsciiNat 2 a) where+    showsPrec _ n = showString "0b" . showBin (unAsciiNat n)++-- | Show octal (base 8) ASCII naturals with an @0o@ prefix.+instance Integral a => Show (AsciiNat 8  a) where+    showsPrec _ n = showString "0o" . showOct (unAsciiNat n)++-- | Show decimal (base 10) ASCII naturals with no prefix.+instance Integral a => Show (AsciiNat 10 a) where+    showsPrec _ = showInt . unAsciiNat++-- | Show hex (base 16) ASCII naturals with an @0x@ prefix.+instance Integral a => Show (AsciiNat 16 a) where+    showsPrec _ n = showString "0x" . showHex (unAsciiNat n)++-}

@@ -10,7 +10,8 @@ import Binrep.Type.NullTerminated import Binrep.Type.NullPadded -import Refined+import Rerefined.Predicate.Logical.And+import Rerefined.Refine ( Refined )  -- | Predicate for null-terminated, then null-padded data. type NullTermPad n = NullTerminate `And` NullPad n

@@ -1,4 +1,6 @@-{-# LANGUAGE UndecidableInstances #-} -- for weirder type families+{-# LANGUAGE UndecidableInstances #-} -- for tons of stuff+{-# LANGUAGE PatternSynonyms #-} -- TODO wip+{-# LANGUAGE OverloadedStrings #-} -- for easy error building  {- | Magic numbers (also just magic): short constant bytestrings usually      found at the top of a file, often used as an early sanity check.@@ -8,8 +10,8 @@   * byte magics e.g. Zstandard: @28 B5 2F FD@   * printable magics e.g. Ogg: @4F 67 67 53@ -> @OggS@ (in ASCII) -For byte magics, use type-level 'Natural' lists.-For printable magics, use 'Symbol's (type-level strings).+For byte magics, use type-level 'Natural' lists e.g. @'Magic' \@'[0xFF, 0x01]@+For printable (UTF-8) magics, use 'Symbol's e.g. @'Magic' \@"hello"@. -}  module Binrep.Type.Magic@@ -20,7 +22,6 @@  import Data.Type.Symbol.Utf8 ( type SymbolToUtf8 ) -import Util.TypeNats ( natValInt ) import GHC.TypeLits ( type Natural, type Symbol, type KnownNat, type (+) )  import GHC.Generics ( Generic )@@ -32,80 +33,71 @@ import Bytezap.Parser.Struct.TypeLits.Bytes   ( ParseReifyBytesW64(parseReifyBytesW64) ) import Bytezap.Parser.Struct qualified as BZ-import Data.ByteString.Internal qualified as B-import GHC.Exts ( Int(I#), plusAddr#, Ptr(Ptr) )-import Foreign.Marshal.Utils ( copyBytes )+import GHC.Exts ( Int(I#) ) import FlatParse.Basic qualified as FP+import Data.Text.Builder.Linear qualified as TBL --- | A singleton data type representing a "magic number" via a phantom type.------ The phantom type variable unambiguously defines a constant bytestring.--- A handful of types are supported for using magics conveniently, e.g. for pure--- ASCII magics, you may use a 'Symbol' type-level string.-data Magic (a :: k) = Magic deriving stock (Generic, Data, Show, Eq)+{- | A unit data type representing a "magic number" via a phantom type. --- | Weaken a @'Magic' a@ to the unit.+The phantom type unambiguously defines a bytestring at compile time. This+depends on the type's kind. See 'MagicBytes' for details.++This is defined using GADT syntax to permit labelling the phantom type kind as+/inferred/, which effectively means hidden (not available for visible type+applications). That kind is always evident from the type, so it's just nicer.+-}+data Magic a where Magic :: forall {k} (a :: k). Magic a+    deriving stock (Generic, Data, Show, Eq)++-- | Weaken a @'Magic' a@ to the unit '()'. instance Weaken (Magic a) where     type Weak (Magic a) = ()     weaken Magic = () --- | Strengthen the unit to some @'Magic' a@.-instance Strengthen (Magic a) where strengthen () = pure Magic+-- | Strengthen the unit '()' to some @'Magic' a@.+instance Strengthen (Magic a) where strengthen () = Right Magic  -- | The byte length of a magic is known at compile time. instance IsCBLen (Magic a) where type CBLen (Magic a) = Length (MagicBytes a) --- | The byte length of a magic is obtained via reifying. deriving via ViaCBLen (Magic a) instance     KnownNat (Length (MagicBytes a)) => BLen (Magic a) +-- | Efficiently serialize a @'Magic' a@. instance (bs ~ MagicBytes a, ReifyBytesW64 bs) => PutC (Magic a) where     putC Magic = reifyBytesW64 @bs  deriving via (ViaPutC (Magic a)) instance   (bs ~ MagicBytes a, ReifyBytesW64 bs, KnownNat (Length bs)) => Put (Magic a) -{- this works, but is ugly.-* we have to duplicate our error wrapping because errors use parser internals-* we throw the magic into the error, so we need the serializer constraints too-I mean, it's fine. It's correct. It's as fast as possible. But it looks bad :<--}-instance-  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs-  , ReifyBytesW64 bs, KnownNat (Length bs)-  ) => GetC (Magic a) where-    getC = BZ.ParserT $ \fpc base os# st0 ->-        case BZ.runParserT# (parseReifyBytesW64 @bs) fpc base os# st0 of-          BZ.OK#   st1 () -> BZ.OK#  st1 Magic-          BZ.Fail# st1    ->-            let bsActual = B.unsafeCreate len (\buf -> copyBytes buf (Ptr (base `plusAddr#` os#)) len)-                eb = EExpected bsExpected bsActual-            in  BZ.Err# st1 (E (I# os#) $ EBase eb)-          BZ.Err#  st1 e  ->-            let bsActual = B.unsafeCreate len (\buf -> copyBytes buf (Ptr (base `plusAddr#` os#)) len)-                eb = EExpected bsExpected bsActual-            in  BZ.Err# st1 (E (I# os#) $ EAnd e eb)-      where-        len = natValInt @(Length bs)-        bsExpected = runPutC (Magic :: Magic a)+-- | Efficiently parse a @'Magic' a@. Serialization constraints are included as+--   we emit the expected bytestring in errors.+instance (bs ~ MagicBytes a, ParseReifyBytesW64 0 bs) => GetC (Magic a) where+    getC = BZ.ParserT $ \fpc base# os# st0 ->+        case BZ.runParserT# (parseReifyBytesW64 @0 @bs) fpc base# os# st0 of+          BZ.OK#   st1 ()             -> BZ.OK#   st1 Magic+          BZ.Err#  st1 (pos, bActual) -> BZ.Err#  st1 (parseError1+            ["TODO magic parse error: "<>TBL.fromDec bActual]+            (pos + I# os#))+          BZ.Fail# st1                -> BZ.Fail# st1 -- shouldn't occur  deriving via ViaGetC (Magic a) instance-  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs+  ( bs ~ MagicBytes a, ParseReifyBytesW64 0 bs   , ReifyBytesW64 bs, KnownNat (Length bs)   ) => Get (Magic a)  -- | Types which define a magic value. class Magical (a :: k) where-    -- | How to turn the type into a list of bytes.+    -- | How to turn the type into a list of bytes (stored using 'Natural's).     type MagicBytes a :: [Natural]  -- | Type-level naturals go as-is. (Make sure you don't go over 255, though!)-instance Magical (ns :: [Natural]) where type MagicBytes ns = ns+instance Magical (bs :: [Natural]) where type MagicBytes bs = bs  -- | Type-level symbols are converted to UTF-8. instance Magical (sym :: Symbol) where type MagicBytes sym = SymbolToUtf8 sym  -- | The length of a type-level list. type family Length (a :: [k]) :: Natural where-    Length '[]       = 0     Length (a ': as) = 1 + Length as+    Length '[]       = 0

@@ -1,6 +1,7 @@ -- | Data null-padded to a given length. -{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for refine error builder  module Binrep.Type.NullPadded where @@ -11,20 +12,22 @@ import Raehik.Compat.FlatParse.Basic.WithLength qualified as FP import Control.Monad.Combinators ( skipCount ) -import Binrep.Util ( tshow )--import Refined-import Refined.Unsafe+import Rerefined.Predicate.Common+import Rerefined.Refine+import TypeLevelShow.Natural+import TypeLevelShow.Utils+import Data.Text.Builder.Linear qualified as TBL  import GHC.TypeNats import Util.TypeNats ( natValInt ) -import Data.Typeable ( typeRep )- import Bytezap.Parser.Struct qualified as BZG import GHC.Exts ( Int(I#) )  data NullPad (n :: Natural)+instance Predicate (NullPad n) where+    type PredicateName d (NullPad n) = ShowParen (d > 9)+        ("NullPad " ++ ShowNatDec n)  {- | A type which is to be null-padded to a given total length. @@ -48,12 +51,10 @@ deriving via ViaCBLen (NullPadded n a) instance KnownNat n => BLen (NullPadded n a)  -- | Assert that term will fit.-instance (BLen a, KnownNat n) => Predicate (NullPad n) a where-    validate p a-      | len <= n = success-      | otherwise-          = throwRefineOtherException (typeRep p) $-                   "too long: " <> tshow len <> " > " <> tshow n+instance (KnownPredicateName (NullPad n), BLen a, KnownNat n)+  => Refine (NullPad n) a where+    validate p a = validateBool p (len <= n) $+        "too long: " <> TBL.fromDec len <> " > " <> TBL.fromDec n       where         n = natValInt @n         len = blen a@@ -78,7 +79,7 @@ instance (KnownNat n, Get a) => GetC (NullPadded n a) where     getC = fpToBz get len# $ \a _unconsumed# ->         -- TODO consume nulls lol-        BZG.constParse $ reallyUnsafeRefine a+        BZG.constParse $ unsafeRefine a       where         !(I# len#) = natValInt @n @@ -87,7 +88,6 @@         (a, len) <- FP.parseWithLength get         let paddingLen = natValInt @n - len         if   paddingLen < 0-        then eBase $ EFailNamed "TODO used to be EOverlong, cba"-        else do-            skipCount paddingLen (FP.word8 0x00)-            pure $ reallyUnsafeRefine a+        then err1 ["TODO used to be EOverlong, cba"]+        else do skipCount paddingLen (FP.word8 0x00)+                pure $ unsafeRefine a

@@ -13,9 +13,8 @@  import FlatParse.Basic qualified as FP -import Refined-import Refined.Unsafe-import Data.Typeable ( typeRep )+import Rerefined.Predicate.Common+import Rerefined.Refine  import Data.ByteString qualified as B import Data.Word ( Word8 )@@ -23,20 +22,18 @@ -- | Null-terminated data. Arbitrary length terminated with a null byte. --   Permits no null bytes inside the data. data NullTerminate++instance Predicate NullTerminate where+    type PredicateName d NullTerminate = "NullTerminate"+ type NullTerminated = Refined NullTerminate  -- | Null-terminated data may not contain any null bytes.-instance NullCheck a => Predicate NullTerminate a where-    validate p a-     | hasNoNulls a = throwRefineOtherException (typeRep p) $+instance Refine NullTerminate B.ByteString where+    -- TODO is there a faster check we can conjure up here...?+    validate p a = validateBool p (not (B.any (== 0x00) a)) $         "null byte not permitted in null-terminated data"-     | otherwise = success -class NullCheck a where hasNoNulls :: a -> Bool-instance NullCheck B.ByteString where-    {-# INLINE hasNoNulls #-}-    hasNoNulls = B.any (== 0x00)- instance BLen a => BLen (NullTerminated a) where     blen ra = 1 + blen (unrefine ra)     {-# INLINE blen #-}@@ -48,9 +45,16 @@     put a = put (unrefine a) <> put @Word8 0x00  -- | We may parse any null-terminated data using a special flatparse combinator.+--+-- The combinator doesn't permit distinguishing between the two possible+-- failures: either there was no next null, or the inner parser didn't consume+-- up to it. instance Get a => Get (NullTerminated a) where     {-# INLINE get #-}-    get = reallyUnsafeRefine <$> getEBase (FP.isolateToNextNull get) (EFailNamed "cstring")+    get = unsafeRefine <$> cut1 (FP.isolateToNextNull get) e+      where e = [ "while isolating to next null"+                , "either there was no next null in the input,"+                , "or the inner parser didn't fully consume its input" ]  {- I don't know how to do @[a]@. Either I nullterm each element, which is weird

@@ -3,34 +3,44 @@  module Binrep.Type.Prefix.Count where -import Binrep.Util.Prefix+import Binrep.Type.Prefix.Internal import Binrep import Control.Monad.Combinators qualified as Monad  import GHC.TypeNats import Util.TypeNats ( natValInt )-import Refined hiding ( Weaken(..), strengthen )-import Refined.Unsafe ( reallyUnsafeRefine1 ) -import Data.Typeable ( Typeable, typeRep )-import Data.Kind+import Rerefined.Predicate.Common+import Rerefined.Refine+import TypeLevelShow.Utils +import Data.Kind ( type Type )+ import Data.Foldable qualified as Foldable +-- TODO put monofoldable in here, instead of that useless @(f a)@ stuff+ data CountPrefix (pfx :: Type)-type CountPrefixed pfx = Refined1 (CountPrefix pfx) -instance (KnownNat (Max pfx), Foldable f, Typeable pfx)-  => Predicate1 (CountPrefix pfx) f where-    validate1 p fa-      | Foldable.length fa <= natValInt @(Max pfx) = success-      | otherwise = throwRefineOtherException (typeRep p) "TODO bad"+instance Predicate (CountPrefix pfx) where+    type PredicateName d (CountPrefix pfx) = ShowParen (d > 9)+        ("CountPrefix " ++ LenNatName pfx) -instance (KnownNat (Max pfx), Foldable f, Typeable pfx)-  => Predicate (CountPrefix pfx) (f a) where+instance+  ( KnownPredicateName (CountPrefix pfx), KnownNat (LenNatMax pfx), Foldable f+  ) => Refine1 (CountPrefix pfx) f where+    validate1 p fa =+        validateBool p (Foldable.length fa <= natValInt @(LenNatMax pfx)) $+            "TODO too large for count prefix"++instance+  ( KnownPredicateName (CountPrefix pfx), KnownNat (LenNatMax pfx), Foldable f+  ) => Refine (CountPrefix pfx) (f a) where     validate = validate1 --- | We can know byte length at compile time _if_ we know it for the prefix and+type CountPrefixed pfx = Refined1 (CountPrefix pfx)++-- | We can know byte length at compile time /if/ we know it for the prefix and --   the list-like. -- -- This is extremely unlikely, because then what counting are we even@@ -42,22 +52,22 @@ --   (holding the length of the type) plus the length of the type. -- -- Bit confusing. How to explain this? TODO-instance (Prefix pfx, Foldable f, BLen pfx, BLen (f a))+instance (LenNat pfx, Foldable f, BLen pfx, BLen (f a))   => BLen (CountPrefixed pfx f a) where-    blen rfa = blen (lenToPfx @pfx (Foldable.length fa)) + blen fa+    blen rfa = blen (lenToNat @pfx (Foldable.length fa)) + blen fa       where fa = unrefine1 rfa -instance (Prefix pfx, Foldable f, Put pfx, Put (f a))+instance (LenNat pfx, Foldable f, Put pfx, Put (f a))   => Put (CountPrefixed pfx f a) where-    put rfa = put (lenToPfx @pfx (Foldable.length fa)) <> put fa+    put rfa = put (lenToNat @pfx (Foldable.length fa)) <> put fa       where fa = unrefine1 rfa  class GetCount f where getCount :: Get a => Int -> Getter (f a) instance GetCount [] where getCount n = Monad.count n get -instance (Prefix pfx, GetCount f, Get pfx, Get a)+instance (LenNat pfx, GetCount f, Get pfx, Get a)   => Get (CountPrefixed pfx f a) where     get = do         pfx <- get @pfx-        fa <- getCount (pfxToLen pfx)-        pure $ reallyUnsafeRefine1 fa+        fa <- getCount (natToLen pfx)+        pure $ unsafeRefine1 fa

@@ -0,0 +1,65 @@+{-# LANGUAGE UndecidableInstances #-} -- for convenient type level arithmetic++module Binrep.Type.Prefix.Internal where++import Binrep.Util.ByteOrder ( ByteOrdered(ByteOrdered) )+import GHC.TypeNats+import GHC.TypeLits ( type Symbol )+import Data.Word+import Data.Kind ( type Type )++-- | Types which can encode natural (positive integer) lengths.+--+-- Types must provide convert to and from 'Int', which is the most common type+-- used for data lengths.+class LenNat a where+    -- | The maximum value the type can encode.+    type LenNatMax a :: Natural++    -- | The name of the type, to display when used as part of a predicate.+    type LenNatName a :: Symbol++    -- | Turn an 'Int' length into an @a@.+    --+    -- It is guaranteed that the 'Int' fits i.e. @<= 'LenNatMax' a@.+    lenToNat :: Int -> a++    -- | Turn an @a@ into an 'Int' length.+    --+    -- Don't worry if @a@ may encode larger numbers than 'Int'. I think other+    -- things will be breaking at that point. Or perhaps it's our responsibility+    -- to emit the runtime error? TODO.+    natToLen :: a -> Int++-- | The unit can only encode 1 value -> lengths of 0 only.+instance LenNat () where+    type LenNatMax  () = 0+    type LenNatName () = "()"+    lenToNat = \case+      0 -> ()+      _ -> error "you lied to refine and broke everything :("+    natToLen () = 0++-- | Byte ordering doesn't change how prefixes work.+deriving via (a :: Type) instance LenNat a => LenNat (ByteOrdered end a)++instance LenNat Word8  where+    type LenNatMax  Word8  = 2^8  - 1+    type LenNatName Word8 = "Word8"+    lenToNat = fromIntegral+    natToLen = fromIntegral+instance LenNat Word16 where+    type LenNatMax  Word16 = 2^16 - 1+    type LenNatName Word16 = "Word16"+    lenToNat = fromIntegral+    natToLen = fromIntegral+instance LenNat Word32 where+    type LenNatMax  Word32 = 2^32 - 1+    type LenNatName Word32 = "Word32"+    lenToNat = fromIntegral+    natToLen = fromIntegral -- TODO check for overflow?+instance LenNat Word64 where+    type LenNatMax  Word64 = 2^64 - 1+    type LenNatName Word64 = "Word64"+    lenToNat = fromIntegral+    natToLen = fromIntegral -- TODO check for overflow?

@@ -3,7 +3,7 @@  module Binrep.Type.Prefix.Size where -import Binrep.Util.Prefix+import Binrep.Type.Prefix.Internal import Binrep.Type.Thin import Binrep import FlatParse.Basic qualified as FP@@ -11,43 +11,48 @@ import GHC.TypeNats import Util.TypeNats ( natValInt ) import Data.ByteString qualified as B-import Refined hiding ( Weaken(..), strengthen )-import Refined.Unsafe -import Data.Typeable ( Typeable, typeRep )-import Data.Kind+import Rerefined.Predicate.Common+import Rerefined.Refine+import TypeLevelShow.Utils +import Data.Kind ( type Type )+ data SizePrefix (pfx :: Type)++instance Predicate (SizePrefix pfx) where+    type PredicateName d (SizePrefix pfx) = ShowParen (d > 9)+        ("SizePrefix " ++ LenNatName pfx)+ type SizePrefixed pfx = Refined (SizePrefix pfx) -instance (KnownNat (Max pfx), BLen a, Typeable pfx)-  => Predicate (SizePrefix pfx) a where-    validate p a-      | blen a <= natValInt @(Max pfx) = Nothing-      | otherwise = throwRefineOtherException (typeRep p) $-          "thing too big for length prefix type"+instance+  ( KnownPredicateName (SizePrefix pfx), KnownNat (LenNatMax pfx), BLen a+  ) => Refine (SizePrefix pfx) a where+    validate p a = validateBool p (blen a <= natValInt @(LenNatMax pfx)) $+        "thing too big for length prefix type"  -- TODO no idea if this is sensible instance IsCBLen (SizePrefixed pfx a) where     type CBLen (SizePrefixed pfx a) = CBLen pfx + CBLen a -instance (Prefix pfx, BLen a, BLen pfx)+instance (LenNat pfx, BLen a, BLen pfx)   => BLen (SizePrefixed pfx a) where-    blen ra = blen (lenToPfx @pfx (blen a)) + blen a+    blen ra = blen (lenToNat @pfx (blen a)) + blen a       where a = unrefine ra -instance (Prefix pfx, BLen a, Put pfx, Put a)+instance (LenNat pfx, BLen a, Put pfx, Put a)   => Put (SizePrefixed pfx a) where-    put ra = put (lenToPfx @pfx (blen a)) <> put a+    put ra = put (lenToNat @pfx (blen a)) <> put a       where a = unrefine ra  class GetSize a where getSize :: Int -> Getter a instance GetSize       B.ByteString  where getSize = fmap B.copy . FP.take instance GetSize (Thin B.ByteString) where getSize = fmap Thin . FP.take -instance (Prefix pfx, GetSize a, Get pfx)+instance (LenNat pfx, GetSize a, Get pfx)   => Get (SizePrefixed pfx a) where     get = do         pfx <- get @pfx-        a <- getSize (pfxToLen pfx)-        pure $ reallyUnsafeRefine a+        a <- getSize (natToLen pfx)+        pure $ unsafeRefine a

@@ -1,31 +1,35 @@ -- | Constant-size data. -{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName+{-# LANGUAGE OverloadedStrings #-} -- for refine error builder  module Binrep.Type.Sized where  import Binrep import FlatParse.Basic qualified as FP -import Binrep.Util ( tshow )--import Refined-import Refined.Unsafe-import Data.Typeable ( typeRep )+import Rerefined.Predicate.Common+import Rerefined.Refine+import TypeLevelShow.Natural+import TypeLevelShow.Utils+import Data.Text.Builder.Linear qualified as TBL  import GHC.TypeNats import Util.TypeNats ( natValInt )  -- | Essentially runtime reflection of a 'BLen' type to 'CBLen'. data Size (n :: Natural)++instance Predicate (Size n) where+    type PredicateName d (Size n) = ShowParen (d > 9)+        ("Size " ++ ShowNatDec n)+ type Sized n = Refined (Size n) -instance (BLen a, KnownNat n) => Predicate (Size n) a where-    validate p a-     | len /= n-        = throwRefineOtherException (typeRep p) $-            "not correctly sized: "<>tshow len<>" /= "<>tshow n-     | otherwise = success+instance (KnownPredicateName (Size n), BLen a, KnownNat n)+  => Refine (Size n) a where+    validate p a = validateBool p (len == n) $+        "not correctly sized: "<>TBL.fromDec len<>" /= "<>TBL.fromDec n       where         n = natValInt @n         len = blen a@@ -42,6 +46,6 @@ instance (Get a, KnownNat n) => Get (Sized n a) where     get = do         a <- FP.isolate (natValInt @n) get-        pure $ reallyUnsafeRefine a+        pure $ unsafeRefine a         -- ^ REFINE SAFETY: 'FP.isolate' consumes precisely the number of bytes         -- requested when it succeeds

@@ -22,7 +22,7 @@  import Binrep.Type.Text.Internal -import Refined+import Rerefined  import Binrep.Type.Text.Encoding.Utf8 import Binrep.Type.Text.Encoding.Ascii@@ -47,7 +47,7 @@ -- bs :: Refined 'C Bytes encodeToRep     :: forall rep enc-    .  (Encode enc, Predicate rep Bytes)+    .  (Encode enc, Refine rep Bytes)     => AsText enc-    -> Either RefineException (Refined rep Bytes)+    -> Either RefineFailure (Refined rep Bytes) encodeToRep = refine . encode

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-}  module Binrep.Type.Text.Encoding.Ascii where@@ -6,42 +5,27 @@ import Binrep.Type.Text.Internal import Binrep.Type.Text.Encoding.Utf8 -import Refined-import Data.Typeable ( typeRep )+import Rerefined.Predicate.Common+import Rerefined.Refine ( unsafeRefine ) -import Data.Char qualified as Char import Data.Text qualified as Text import Data.Text ( Text )  import Data.Text.Encoding qualified as Text-import Control.Exception qualified-import System.IO.Unsafe qualified  -- | 7-bit data Ascii+instance Predicate Ascii where type PredicateName d Ascii = "ASCII" +-- | 'Text' must be validated if you want to permit 7-bit ASCII only.+instance Refine Ascii Text where+    validate p t = validateBool p (Text.isAscii t) "not valid 7-bit ASCII"+ -- | We reuse UTF-8 encoding for ASCII, since it is a subset of UTF-8. instance Encode Ascii where encode' = encode' @Utf8 --- Pre-@text-2.0@, @decodeASCII@ generated a warning and ran @decodeUtf8@.--- TODO can I give some compile time warning about this instance missing on--- below text-2.0?? would be cool-#if MIN_VERSION_text(2,0,0)--- TODO 2023-01-26 raehik: awful UX by text. hopefully safe lol?? works at least-instance Decode Ascii where decode = decodeText id $ catchErrorCall Text.decodeASCII-#endif--catchErrorCall :: (a -> b) -> a -> Either String b-catchErrorCall f a = System.IO.Unsafe.unsafeDupablePerformIO $ do-    Control.Exception.try @Control.Exception.ErrorCall (Control.Exception.evaluate (f a)) >>= \case-      Right b -> pure $ Right b-      Left  (Control.Exception.ErrorCallWithLocation msg _) -> pure $ Left msg---- | 'Text' must be validated if you want to permit 7-bit ASCII only.------ TODO there should be a MUCH faster check here in text-2.0. text-short has it,--- text doesn't yet. see: https://github.com/haskell/text/issues/496-instance Predicate Ascii Text where-    validate p t = if   Text.all Char.isAscii t-                   then success-                   else throwRefineOtherException (typeRep p) "not valid 7-bit ASCII"+instance Decode Ascii where+    decode bs =+        case Text.decodeASCII' bs of+          Just t  -> Right $ unsafeRefine t+          Nothing -> Left  "not valid 7-bit ASCII"

@@ -2,7 +2,7 @@  module Binrep.Type.Text.Encoding.ShiftJis where -import Refined+import Rerefined.Predicate  import Data.Text ( Text ) @@ -15,9 +15,10 @@ #endif  data ShiftJis+instance Predicate ShiftJis where type PredicateName d ShiftJis = "Shift-JIS"  -- | TODO Unsafely assume all 'Text's are valid Shift-JIS.-instance Predicate ShiftJis Text where validate _ _ = success+instance Refine ShiftJis Text where validate _ _ = Nothing  #ifdef HAVE_ICU instance Encode ShiftJis where encode' = encodeViaTextICU' "Shift-JIS"

@@ -1,15 +1,19 @@+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName+ module Binrep.Type.Text.Encoding.Utf16 where  import Binrep.Type.Text.Internal import Binrep.Util.ByteOrder -import Refined-import Data.Typeable ( Typeable )+import Rerefined.Predicate+import TypeLevelShow.Utils  import Data.Text.Encoding qualified as Text import Data.Text ( Text )  data Utf16 (end :: ByteOrder)+instance Predicate (Utf16 end) where+    type PredicateName d (Utf16 end) = "UTF-16" ++ EndianSuffix end  instance Encode (Utf16 BE) where encode' = Text.encodeUtf16BE instance Encode (Utf16 LE) where encode' = Text.encodeUtf16LE@@ -18,4 +22,4 @@ instance Decode (Utf16 LE) where decode = decodeText show $ wrapUnsafeDecoder Text.decodeUtf16LE  -- | Any 'Text' value is always valid UTF-16.-instance Typeable end => Predicate (Utf16 end) Text where validate _ _ = success+instance Refine (Utf16 end) Text where validate _ _ = Nothing

@@ -1,15 +1,19 @@+{-# LANGUAGE UndecidableInstances #-} -- for PredicateName+ module Binrep.Type.Text.Encoding.Utf32 where  import Binrep.Type.Text.Internal import Binrep.Util.ByteOrder -import Refined-import Data.Typeable ( Typeable )+import Rerefined.Predicate+import TypeLevelShow.Utils  import Data.Text.Encoding qualified as Text import Data.Text ( Text )  data Utf32 (end :: ByteOrder)+instance Predicate (Utf32 end) where+    type PredicateName d (Utf32 end) = "UTF-32" ++ EndianSuffix end  instance Encode (Utf32 BE) where encode' = Text.encodeUtf32BE instance Encode (Utf32 LE) where encode' = Text.encodeUtf32LE@@ -18,4 +22,4 @@ instance Decode (Utf32 LE) where decode = decodeText show $ wrapUnsafeDecoder Text.decodeUtf32LE  -- | Any 'Text' value is always valid UTF-32.-instance Typeable end => Predicate (Utf32 end) Text where validate _ _ = success+instance Refine (Utf32 end) Text where validate _ _ = Nothing

@@ -2,15 +2,16 @@  import Binrep.Type.Text.Internal -import Refined+import Rerefined.Predicate  import Data.Text.Encoding qualified as Text import Data.Text ( Text )  data Utf8+instance Predicate Utf8 where type PredicateName d Utf8 = "UTF-8"  instance Encode Utf8 where encode' = Text.encodeUtf8 instance Decode Utf8 where decode  = decodeText show Text.decodeUtf8'  -- | Any 'Text' value is always valid UTF-8.-instance Predicate Utf8 Text where validate _ _ = success+instance Refine Utf8 Text where validate _ _ = Nothing

@@ -4,8 +4,7 @@  import Data.Text ( Text ) import Data.ByteString qualified as B-import Refined-import Refined.Unsafe ( reallyUnsafeRefine )+import Rerefined.Refine  import System.IO.Unsafe qualified import Control.Exception qualified@@ -40,7 +39,7 @@     :: forall enc e     .  (e -> String) -> (Bytes -> Either e Text) -> Bytes     -> Either String (AsText enc)-decodeText g f = bimap g reallyUnsafeRefine . f+decodeText g f = bimap g unsafeRefine . f  -- | Run an unsafe decoder safely. --

@@ -1,31 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}--module Binrep.Util where---- tshow-import Data.Text qualified as Text-import Data.Text ( Text )---- posIntToNat-import GHC.Exts ( Int(..), int2Word# )-import GHC.Num.Natural ( Natural(..) )---- natVal''-import GHC.TypeNats ( KnownNat, natVal' )-import GHC.Exts ( proxy#, Proxy# )--tshow :: Show a => a -> Text-tshow = Text.pack . show---- | Convert some 'Int' @i@ where @i >= 0@ to a 'Natural'.------ This is intended for wrapping the output of 'length' functions.------ underflows if you call it with a negative 'Int' :)-posIntToNat :: Int -> Natural-posIntToNat (I# i#) = NS (int2Word# i#)-{-# INLINE posIntToNat #-}--natVal'' :: forall a. KnownNat a => Natural-natVal'' = natVal' (proxy# :: Proxy# a)-{-# INLINE natVal'' #-}

@@ -1,14 +1,15 @@ {-# OPTIONS_GHC -fno-warn-orphans #-}  module Binrep.Util.ByteOrder-  ( ByteOrder(..), ByteOrdered(..)+  ( ByteOrder(..), ByteOrdered(..), type EndianSuffix   , type LE, type BE, type Endian   ) where  import Raehik.Compat.Data.Primitive.Types.Endian ( ByteOrdered(..) ) import GHC.ByteOrder ( ByteOrder(..) ) import Strongweak-import Data.Kind ( Type )+import Data.Kind ( type Type )+import GHC.TypeLits ( type Symbol )  deriving via (a :: Type) instance     Weaken a =>     Weaken (ByteOrdered end a) deriving via (a :: Type) instance Strengthen a => Strengthen (ByteOrdered end a)@@ -17,3 +18,7 @@ type LE = 'LittleEndian type BE =    'BigEndian type Endian = ByteOrdered++type family EndianSuffix (end :: ByteOrder) :: Symbol where+    EndianSuffix 'LittleEndian = "LE"+    EndianSuffix    'BigEndian = "BE"

@@ -1,62 +0,0 @@-{-# LANGUAGE UndecidableInstances #-} -- for convenient type level arithmetic--module Binrep.Util.Prefix where--import Binrep.Util.ByteOrder ( ByteOrdered(ByteOrdered) )-import GHC.TypeNats-import Data.Word--import Data.Kind---- | Types which may be used as prefixes.------ Generally, these will be integer types.------ Note that this is separate to binary representation, so endianness is--- irrelevant.------ Note that we are also limited by the host architecture's 'Int' type.--- We don't try to work around this, because most types are indexed with 'Int's,--- so I think other things will break before we do.-class Prefix a where-    type Max a :: Natural--    -- | used by put. guaranteed that it fits from refined. that is, lenToPfx <=-    --   Max.-    lenToPfx :: Int -> a--    -- | used by get. better not lie.-    pfxToLen :: a -> Int---- | Length prefixing with the unit means a length of 0.------ This is the only sensible case. 1 doesn't work because refining checks @<=@.------ I think there are laws here, where using this is the same as doing nothing at--- all.-instance Prefix () where-    type Max () = 0-    lenToPfx = \case-      0 -> ()-      _ -> error "you lied to refine and broke everything :("-    pfxToLen () = 0---- | Byte ordering doesn't change how prefixes work.-deriving via (a :: Type) instance Prefix a => Prefix (ByteOrdered end a)--instance Prefix Word8  where-    type Max Word8  = 2^8  - 1-    lenToPfx = fromIntegral-    pfxToLen = fromIntegral-instance Prefix Word16 where-    type Max Word16 = 2^16 - 1-    lenToPfx = fromIntegral-    pfxToLen = fromIntegral-instance Prefix Word32 where-    type Max Word32 = 2^32 - 1-    lenToPfx = fromIntegral-    pfxToLen = fromIntegral-instance Prefix Word64 where-    type Max Word64 = 2^64 - 1-    lenToPfx = fromIntegral-    pfxToLen = fromIntegral

@@ -0,0 +1,15 @@+module Raehik.Compat.FlatParse.Basic.CutWithPos where++import FlatParse.Basic ( ParserT, Pos, getPos, cut, err )++-- | Convert a parsing failure to an error, which also receives the parser+--   position (as a 'Pos', from the end of input).+cut' :: ParserT st e a -> (Pos -> e) -> ParserT st e a+cut' p e = getPos >>= \pos -> cut p (e pos)+{-# inline cut' #-}++-- | Throw a parsing error, which also receives the parser position (as a 'Pos',+--   from the end of input).+err' :: (Pos -> e) -> ParserT st e a+err' e = getPos >>= \pos -> err (e pos)+{-# inline err' #-}

@@ -15,3 +15,7 @@ natValInt :: forall n. KnownNat n => Int natValInt = fromIntegral $ natVal'' @n {-# INLINE natValInt #-}++natValWord :: forall n. KnownNat n => Word+natValWord = fromIntegral $ natVal'' @n+{-# INLINE natValWord #-}

@@ -0,0 +1,39 @@+{-# LANGUAGE OverloadedStrings #-}++module Binrep.GenericSpec where++import Test.Hspec++spec :: Spec+spec = pure ()+    {-+spec = do+    prop "parse-print roundtrip isomorphism (generic, sum tag via nullterm constructor)" $ do+      \(d :: D) -> runGet (runPut d) `shouldBe` Right (d, "")++--------------------------------------------------------------------------------++type W1   = Word8+type W2LE = ByteOrdered LE Word16+type W8BE = ByteOrdered BE Word64++data D+  = D01Bla     Word8 W1 W8BE+  | D23        W2LE  B.ByteString -- dangerous bytestring, must be last+  | DUnicode例 Word8+  | DSymbols_#+    deriving stock (Generic, Eq, Show)+deriving via (GenericArbitraryU `AndShrinking` D) instance Arbitrary D++instance BLen D where blen = blenGenericSum $ blen . nullTermCstrPfxTag+instance Put  D where put  = putGenericSum  $ put . nullTermCstrPfxTag+instance Get  D where get  = getGenericSum  $ eqShowPfxTagCfg nullTermCstrPfxTag++data DNoSum = DNoSum Word8 W1 W2LE W8BE+    deriving stock (Generic, Eq, Show)+deriving via (GenericArbitraryU `AndShrinking` DNoSum) instance Arbitrary DNoSum++instance BLen DNoSum where blen = blenGenericNonSum+instance Put  DNoSum where put  = putGenericNonSum+instance Get  DNoSum where get  = getGenericNonSum+    -}

@@ -1,54 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--module Binrep.LawsSpec where--import Test.Hspec-import Test.Hspec.QuickCheck-import Test.QuickCheck.Instances.ByteString()-import Generic.Random-import Test.QuickCheck-import ArbitraryOrphans()--import Binrep-import Binrep.Generic ( nullTermCstrPfxTag )-import Binrep.Util.ByteOrder-import Data.Word-import Data.ByteString qualified as B-import GHC.Generics ( Generic )--import Generic.Data.Function.Traverse--spec :: Spec-spec = do-    prop "put is identity on ByteString" $ do-      \(bs :: B.ByteString) -> runPut bs  `shouldBe` bs-    prop "parse-print roundtrip isomorphism (ByteString)" $ do-      \(bs :: B.ByteString) -> runGet (runPut bs) `shouldBe` Right (bs, "")-    prop "parse-print roundtrip isomorphism (generic, sum tag via nullterm constructor)" $ do-      \(d :: D) -> runGet (runPut d) `shouldBe` Right (d, "")------------------------------------------------------------------------------------type W1   = Word8-type W2LE = ByteOrdered LE Word16-type W8BE = ByteOrdered BE Word64--data D-  = D01Bla     Word8 W1 W8BE-  | D23        W2LE  B.ByteString -- dangerous bytestring, must be last-  | DUnicode例 Word8-  | DSymbols_#-    deriving stock (Generic, Eq, Show)-deriving via (GenericArbitraryU `AndShrinking` D) instance Arbitrary D--instance BLen D where blen = blenGenericSum $ blen . nullTermCstrPfxTag-instance Put  D where put  = putGenericSum  $ put . nullTermCstrPfxTag-instance Get  D where get  = getGenericSum  $ eqShowPfxTagCfg nullTermCstrPfxTag--data DNoSum = DNoSum Word8 W1 W2LE W8BE-    deriving stock (Generic, Eq, Show)-deriving via (GenericArbitraryU `AndShrinking` DNoSum) instance Arbitrary DNoSum--instance BLen DNoSum where blen = blenGenericNonSum-instance Put  DNoSum where put  = putGenericNonSum-instance Get  DNoSum where get  = getGenericNonSum

@@ -0,0 +1,19 @@+{-# LANGUAGE OverloadedStrings #-}++module Binrep.TypesSpec where++import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck.Instances.ByteString()++import Binrep+import Data.ByteString qualified as B++spec :: Spec+spec = do+    prop "put is identity on ByteString" $ do+      \(bs :: B.ByteString) -> runPut bs  `shouldBe` bs+    prop "parse-print roundtrip isomorphism (ByteString)" $ do+      \(bs :: B.ByteString) ->+        runGet (runPut bs) `shouldSatisfy`+          (\case Right (bs', "") -> bs == bs'; _ -> False)