Cabal revisions of dependent-literals-plugin-0.1.0.2
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-cabal-version: 1.12---- This file has been generated from package.yaml by hpack version 0.34.4.------ see: https://github.com/sol/hpack--name: dependent-literals-plugin-version: 0.1.0.2-synopsis: Dependent integer literals-description: This plugin implements pseudo-dependently-typed integer literals.- .- This means the value of an integer literal is available at the type level,- and can be used for things like validation or type inference. For example,- the 'SInt' instance refines unknown type-level 'Nat' variables to the- particular literal value, and the 'Fin' instance emits compile-time errors- for out-of-range values. So, given- @mkVec :: SInt n -> (Fin n -> a) -> Vec n a@, @mkVec 4@ will have type- @(Fin 4 -> a) -> Vec 4 a@, and trying to type-check @4 :: Fin 4@ will report- a type error saying that @4@ is out of range.- .- Patterns get a similar treatment, too, so- @case (x :: SInt n) of { 1 -> Just Refl; _ -> Nothing } :: Maybe (n :~: 1)@- can type-check: the act of matching against 1 proved that the type-level @n@- was equal to 1, so 'Refl' can type-check as @n :~: 1@.- .- To use this, enable the extensions @DataKinds@, @FlexibleContexts@,- @ViewPatterns@, and @TypeApplications@, add @dependent-literals@ and- @dependent-literals-plugin@ to your package's dependencies, and add- @-fplugin=DependentLiterals.Plugin@ to @ghc-options@ to enable the plugin- globally, or use @OPTIONS_GHC@ pragmas to enable the plugin on a per-module- basis. \"Normal\" integral types should still behave as normal, but literals- and numeric patterns will become supported for 'SInt' and 'Fin', and will- provide additional information to the type checker automatically.-category: Constraints-homepage: https://github.com/google/hs-dependent-literals#readme-bug-reports: https://github.com/google/hs-dependent-literals/issues-author: Andrew Pritchard <awpr@google.com>-maintainer: Andrew Pritchard <awpr@google.com>-copyright: 2019-2021 Google LLC-license: Apache-2.0-license-file: LICENSE-build-type: Simple-extra-source-files:- CHANGELOG.md--source-repository head- type: git- location: https://github.com/google/hs-dependent-literals- subdir: dependent-literals-plugin--flag error_message_tests- description: Enable tests that emit error messages for inspection.- manual: True- default: False--library- exposed-modules:- DependentLiterals.Plugin- hs-source-dirs:- src- build-depends:- base >=4.12 && <4.17- , ghc >=8.6 && <9.3- , syb >=0.1 && <0.8- default-language: Haskell2010--test-suite FinErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- FinErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010--test-suite IntErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- IntErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010--test-suite Plugin-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- Deriving- DoubleNegation- FinLiterals- FinPatterns- FractionalLiterals- FractionalPatterns- IntLiterals- IntPatterns- PolyLiterals- SIntLiterals- SIntPatterns- TestUtils- SNumberLiterals- WithNegativeLiterals- WordLiterals- WordPatterns- VecExamples- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- default-language: Haskell2010--test-suite PolyErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- PolyErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010--test-suite SIntErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- SIntErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010--test-suite SNumberErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- SNumberErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010--test-suite WordErrors-test- type: exitcode-stdio-1.0- main-is: Main.hs- other-modules:- WordErrors- hs-source-dirs:- tests- default-extensions:- NoStarIsType- DataKinds- FlexibleContexts- ViewPatterns- TypeApplications- ghc-options: -fplugin=DependentLiterals.Plugin- build-depends:- base >=4.12 && <4.17- , dependent-literals >=0.1.1 && <0.3- , dependent-literals-plugin- , fin-int >=0.1 && <0.3- , numeric-kinds >=0.1 && <0.3- , short-vec ==0.1.*- , sint >=0.1 && <0.3- , snumber >=0.1 && <0.4- , wrapped ==0.1.*- if !flag(error_message_tests)- buildable: False- default-language: Haskell2010+cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.34.4. +-- +-- see: https://github.com/sol/hpack + +name: dependent-literals-plugin +version: 0.1.0.2 +x-revision: 1 +synopsis: Dependent integer literals +description: This plugin implements pseudo-dependently-typed integer literals. + . + This means the value of an integer literal is available at the type level, + and can be used for things like validation or type inference. For example, + the 'SInt' instance refines unknown type-level 'Nat' variables to the + particular literal value, and the 'Fin' instance emits compile-time errors + for out-of-range values. So, given + @mkVec :: SInt n -> (Fin n -> a) -> Vec n a@, @mkVec 4@ will have type + @(Fin 4 -> a) -> Vec 4 a@, and trying to type-check @4 :: Fin 4@ will report + a type error saying that @4@ is out of range. + . + Patterns get a similar treatment, too, so + @case (x :: SInt n) of { 1 -> Just Refl; _ -> Nothing } :: Maybe (n :~: 1)@ + can type-check: the act of matching against 1 proved that the type-level @n@ + was equal to 1, so 'Refl' can type-check as @n :~: 1@. + . + To use this, enable the extensions @DataKinds@, @FlexibleContexts@, + @ViewPatterns@, and @TypeApplications@, add @dependent-literals@ and + @dependent-literals-plugin@ to your package's dependencies, and add + @-fplugin=DependentLiterals.Plugin@ to @ghc-options@ to enable the plugin + globally, or use @OPTIONS_GHC@ pragmas to enable the plugin on a per-module + basis. \"Normal\" integral types should still behave as normal, but literals + and numeric patterns will become supported for 'SInt' and 'Fin', and will + provide additional information to the type checker automatically. +category: Constraints +homepage: https://github.com/google/hs-dependent-literals#readme +bug-reports: https://github.com/google/hs-dependent-literals/issues +author: Andrew Pritchard <awpritchard@gmail.com> +maintainer: Andrew Pritchard <awpritchard@gmail.com> +copyright: 2019-2021 Google LLC +license: Apache-2.0 +license-file: LICENSE +build-type: Simple +extra-source-files: + CHANGELOG.md + +source-repository head + type: git + location: https://github.com/google/hs-dependent-literals + subdir: dependent-literals-plugin + +flag error_message_tests + description: Enable tests that emit error messages for inspection. + manual: True + default: False + +library + exposed-modules: + DependentLiterals.Plugin + hs-source-dirs: + src + build-depends: + base >=4.12 && <4.17 + , ghc >=8.6 && <9.3 + , syb >=0.1 && <0.8 + default-language: Haskell2010 + +test-suite FinErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + FinErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 + +test-suite IntErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + IntErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 + +test-suite Plugin-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + Deriving + DoubleNegation + FinLiterals + FinPatterns + FractionalLiterals + FractionalPatterns + IntLiterals + IntPatterns + PolyLiterals + SIntLiterals + SIntPatterns + TestUtils + SNumberLiterals + WithNegativeLiterals + WordLiterals + WordPatterns + VecExamples + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + default-language: Haskell2010 + +test-suite PolyErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + PolyErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 + +test-suite SIntErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + SIntErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 + +test-suite SNumberErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + SNumberErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 + +test-suite WordErrors-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + WordErrors + hs-source-dirs: + tests + default-extensions: + NoStarIsType + DataKinds + FlexibleContexts + ViewPatterns + TypeApplications + ghc-options: -fplugin=DependentLiterals.Plugin + build-depends: + base >=4.12 && <4.17 + , dependent-literals >=0.1.1 && <0.3 + , dependent-literals-plugin + , fin-int >=0.1 && <0.3 + , numeric-kinds >=0.1 && <0.3 + , short-vec ==0.1.* + , sint >=0.1 && <0.3 + , snumber >=0.1 && <0.4 + , wrapped ==0.1.* + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010