diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1.0.0 + +Initial version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/dependent-literals-plugin.cabal b/dependent-literals-plugin.cabal new file mode 100644 --- /dev/null +++ b/dependent-literals-plugin.cabal @@ -0,0 +1,237 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: acdf4e8362e54c7dabc311e213378ec098339936e11995a39c08d189594f7ece + +name: dependent-literals-plugin +version: 0.1.0.0 +synopsis: Rewrites integer literals to a pseudo-dependently-typed form. +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 +maintainer: Andrew Pritchard +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 + other-modules: + Paths_dependent_literals_plugin + hs-source-dirs: + src + build-depends: + base >=4.12 && <4.16 + , ghc >=8.6 && <9.1 + , 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + 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.16 + , dependent-literals >=0.1 && <0.2 + , dependent-literals-plugin + , fin-int >=0.1 && <0.2 + , numeric-kinds >=0.1 && <0.2 + , short-vec >=0.1 && <0.2 + , sint >=0.1 && <0.2 + , snumber >=0.1 && <0.2 + if !flag(error_message_tests) + buildable: False + default-language: Haskell2010 diff --git a/src/DependentLiterals/Plugin.hs b/src/DependentLiterals/Plugin.hs new file mode 100644 --- /dev/null +++ b/src/DependentLiterals/Plugin.hs @@ -0,0 +1,398 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +-- | A GHC plugin making numeric literals and patterns pseudo-dependently-typed. + +module DependentLiterals.Plugin (plugin) where + +import Data.Foldable (for_) +import Data.Maybe (fromMaybe, isJust) + +import qualified Data.Generics as SYB + +-- GHC has been overhauling its module hierarchy, but to a significant extent, +-- it's renaming modules entirely and not regrouping exports; most of these we +-- paper over by defining macros for their most-up-to-date name with +-- underscores instead of dots. + +-- This one was renamed twice in the range of supported versions. +#if MIN_VERSION_ghc(9,0,0) +#define GHC_Hs_Type GHC.Hs.Type +#elif MIN_VERSION_ghc(8,10,0) +#define GHC_Hs_Type GHC.Hs.Types +#else +#define GHC_Hs_Type HsTypes +#endif + +-- Renames from 8.10 to 9.0 +#if MIN_VERSION_ghc(9,0,0) +#define GHC_Plugins GHC.Plugins +#define GHC_Types_SourceText GHC.Types.Basic +#define GHC_Types_Name_Occurrence GHC.Types.Name.Occurrence +#define GHC_Types_Name_Reader GHC.Types.Name.Reader +#define GHC_Unit_Module_Name GHC.Unit.Module.Name +#define GHC_Utils_Outputable GHC.Utils.Outputable +#else +#define GHC_Plugins GhcPlugins +#define GHC_Types_SourceText BasicTypes +#define GHC_Types_Name_Occurrence OccName +#define GHC_Types_Name_Reader RdrName +#define GHC_Unit_Module_Name Module +#define GHC_Utils_Outputable Outputable +#endif + +-- Renames from 8.8 to 8.10 +#if MIN_VERSION_ghc(8,10,0) +#define GHC_Hs GHC.Hs +#define GHC_Hs_Expr GHC.Hs.Expr +#define GHC_Hs_Extension GHC.Hs.Extension +#define GHC_Hs_Lit GHC.Hs.Lit +#define GHC_Hs_Pat GHC.Hs.Pat +#define GHC_Hs_Utils GHC.Hs.Utils +#else +#define GHC_Hs HsSyn +#define GHC_Hs_Expr HsExpr +#define GHC_Hs_Extension HsExtension +#define GHC_Hs_Lit HsLit +#define GHC_Hs_Pat HsPat +#define GHC_Hs_Utils HsUtils +#endif + +import GHC_Hs + ( HsModule(..), HsWildCardBndrs(HsWC) + , HsTyLit(HsNumTy) + , ImportDecl(..), IEWrappedName(..), IE(..) + ) +import GHC_Hs_Lit (HsOverLit(..), OverLitVal(HsIntegral)) +import GHC_Hs_Expr (HsExpr(HsAppType, HsOverLit, HsApp, NegApp), LHsExpr) +import GHC_Hs_Extension (GhcPs, GhcPass) +import GHC_Hs_Type + ( HsType(HsAppTy, HsParTy, HsTyLit, HsTyVar) + , LHsType, HsConDetails(PrefixCon) + ) +import GHC_Hs_Pat (LPat, Pat(NPat, ViewPat)) +import GHC_Hs_Utils (nlHsVar, nlHsApp) +import GHC_Plugins + ( Hsc, HsParsedModule(..) + , Plugin(parsedResultAction, pluginRecompile), defaultPlugin + , PluginRecompile(NoForceRecompile) + , CommandLineOption + , DynFlags, Located, GenLocated(L), noSrcSpan + , getDynFlags, liftIO + , gopt_set, GeneralFlag(Opt_SuppressModulePrefixes) + , SrcSpan + ) +import GHC_Types_Name_Occurrence (OccName, mkTcOcc, mkVarOcc, mkDataOcc) +import GHC_Types_Name_Reader (RdrName, mkRdrQual, mkRdrUnqual) +import GHC_Types_SourceText (IntegralLit(IL), SourceText(NoSourceText)) +import GHC_Unit_Module_Name (ModuleName, mkModuleName) +import GHC_Utils_Outputable + ( (<+>), Outputable, nest, pprPrec, sep, showSDoc, text + ) + +-- For semantic changes, we generally try to paper over them by adding +-- compatibility shims, e.g. pattern synonyms, to make the code below look like +-- it's targeting the most-up-to-date version. + +#if MIN_VERSION_ghc(9,0,0) +import GHC_Hs_Pat (Pat(ConPat)) +import GHC.Unit.Types (IsBootInterface(..)) +#else +-- Imports for pre-9.0 compatibily shims. +import GHC_Hs_Pat (Pat(ConPatIn), HsConPatDetails) +import GHC_Hs_Extension (IdP) +#endif + +#if MIN_VERSION_ghc(8,10,0) +import GHC.Hs.Extension (NoExtField(..)) +import GHC.Hs.ImpExp (ImportDeclQualifiedStyle(..)) +import GHC_Plugins (noLoc) +#else +-- Imports for pre-8.10 compatibily shims. +import HsExtension (NoExt(..)) +#endif + +#if MIN_VERSION_ghc(8,8,0) +import GHC_Types_SourceText (PromotionFlag(..)) +#else +-- Imports for pre-8.8 compatibily shims. +import GHC_Plugins (noLoc) +import HsTypes (Promoted(..)) +#endif + +-- Pre-9.0 compatibility shims. +#if !MIN_VERSION_ghc(9,0,0) +pattern ConPat :: a -> Located (IdP p) -> HsConPatDetails p -> Pat p +pattern ConPat ext con args <- (((,) NoExtField) -> (ext, ConPatIn con args)) + where + ConPat _ext con args = ConPatIn con args + +type HsModulePs = HsModule GhcPs + +pattern NotBoot :: Bool +pattern NotBoot = False +#else +type HsModulePs = HsModule +#endif + +-- Pre-8.10 compatibility shims. +#if !MIN_VERSION_ghc(8,10,0) +type NoExtField = NoExt +pattern NoExtField :: NoExt +pattern NoExtField = NoExt + +type ImportDeclQualifiedStyle = Bool +pattern QualifiedPre, NotQualified :: ImportDeclQualifiedStyle +pattern QualifiedPre = True +pattern NotQualified = False +#endif + +-- Pre-8.8 compatibility shims. +#if !MIN_VERSION_ghc(8,8,0) +type PromotionFlag = Promoted +pattern IsPromoted :: PromotionFlag +pattern IsPromoted = Promoted +#endif + +data Config = Config + { _cDoLiterals :: Bool + , _cDoPatterns :: Bool + , _cTraceThings :: Bool + } + +defaultConfig :: Config +defaultConfig = Config True True False + +interpretOpts :: [CommandLineOption] -> Config +interpretOpts opts0 = go opts0 defaultConfig + where + go [] c = c + go ("nolits":opts) c = go opts c { _cDoLiterals = False } + go ("nopats":opts) c = go opts c { _cDoPatterns = False } + go ("trace":opts) c = go opts c { _cTraceThings = True } + go (opt:_) _ = error $ + "Illegal option " ++ show opt ++ + ".\nAll options: " ++ show opts0 + +plugin :: Plugin +plugin = defaultPlugin + { parsedResultAction = \opts _ -> parsedResultPlugin (interpretOpts opts) + , pluginRecompile = \_ -> return NoForceRecompile + } + +parsedResultPlugin :: Config -> HsParsedModule -> Hsc HsParsedModule +parsedResultPlugin cfg m = do + df <- getDynFlags + hpm_module' <- transformParsed cfg df (hpm_module m) + return $ m { hpm_module = hpm_module' } + +when_ :: Applicative f => Bool -> (a -> f a) -> a -> f a +when_ True f = f +when_ False _ = pure + +pattern LPat :: Pat (GhcPass p) -> LPat (GhcPass p) +#if !MIN_VERSION_ghc(8,8,0) || MIN_VERSION_ghc(8,10,0) +pattern LPat pat <- L _ pat +#else +pattern LPat pat <- pat +#endif + +nlPat :: Pat (GhcPass p) -> LPat (GhcPass p) +nlPat = id +#if !MIN_VERSION_ghc(8,8,0) || MIN_VERSION_ghc(8,10,0) + . noLoc +#endif + +transformParsed + :: Config + -> DynFlags + -> Located HsModulePs + -> Hsc (Located HsModulePs) +transformParsed Config{..} df' (L modLoc HsModule{..}) = do + decls <- + pure hsmodDecls + >>= when_ _cDoLiterals + ( SYB.everywhereM (SYB.mkM (wrapDebug "expression" transformExp)) + . SYB.everywhere (SYB.mkT foldNegation) + ) + >>= when_ _cDoPatterns + (SYB.everywhereM (SYB.mkM (wrapDebug "pattern" transformPat))) + + return $ L modLoc $ HsModule + { hsmodDecls = decls + , hsmodImports = + mkModImport litMod Nothing QualifiedPre Nothing : + unqualLitModImport : + qualIntModImport : + hsmodImports + , .. + } + where + df = gopt_set df' Opt_SuppressModulePrefixes + + nl :: a -> Located a + nl = L noSrcSpan + + litMod, intMod :: ModuleName + litMod = mkModuleName "DependentLiterals.Int" + intMod = mkModuleName "Kinds.Integer" + + -- import qualified DependentLiterals.Int + mkModImport nm as q imports = nl $ ImportDecl + NoExtField + NoSourceText + (nl nm) + Nothing -- no package qualifier + NotBoot + False -- not marked safe + q -- qualified + True -- implicit + as -- "as" rename + ((False,) . nl . map nl <$> imports) -- no "hiding" + + -- Import a few things unqualified implicitly. This way, when they appear in + -- error messages, they won't have bulky module names attached. All of these + -- have -XMagicHash names so that they can't conflict with the subset of the + -- namespace used by reasonable Haskell programmers, and most people can't + -- ever tell that they're imported. + -- TODO can we move this plugin post-renamer and do this by generating names + -- that claim to have been originally unqualified? + importVar = IEVar NoExtField . nl . IEName .nl + importAll = IEThingAll NoExtField . nl . IEName . nl + importTyOp = IEThingAbs NoExtField . nl . IEType . nl + unqualLitModImport = mkModImport litMod Nothing NotQualified $ Just + [ importVar litHashName + , importTyOp minusHashName + ] + qualIntModImport = mkModImport intMod Nothing QualifiedPre $ Just + [ importAll integerName + ] + + qual :: OccName -> RdrName + qual = mkRdrQual litMod + + integerName = mkRdrUnqual (mkTcOcc "Integer") + minusHashName = mkRdrUnqual (mkTcOcc "-#") + negName = mkRdrQual intMod (mkDataOcc "Neg") + posName = mkRdrQual intMod (mkDataOcc "Pos") + cjustConName = qual (mkDataOcc "CJust") + litHashName = mkRdrUnqual (mkVarOcc "lit#") + matchHashName = qual (mkVarOcc "match#") + + infixl 4 `mkHsAppType` + mkHsAppType :: LHsExpr GhcPs -> LHsType GhcPs -> HsExpr GhcPs + mkHsAppType expr ty = HsAppType +#if MIN_VERSION_ghc(8,8,0) + NoExtField + expr + (HsWC NoExtField ty) +#else + (HsWC NoExtField ty) + expr +#endif + + infixl 4 `nlHsAppType` + nlHsAppType :: LHsExpr GhcPs -> LHsType GhcPs -> LHsExpr GhcPs + nlHsAppType expr ty = L noSrcSpan $ mkHsAppType expr ty + + infixl 4 `nlHsApp_` + nlHsApp_ = nlHsApp + + litToTyLit :: IntegralLit -> LHsType GhcPs + litToTyLit (IL txt neg val) = nl $ HsParTy NoExtField $ nl $ HsAppTy NoExtField + (nl $ HsTyVar NoExtField IsPromoted $ nl (if neg then negName else posName)) + (nl $ HsTyLit NoExtField (HsNumTy txt (abs val))) + + debug :: String -> Hsc () + debug s + | _cTraceThings = liftIO (putStrLn s) + | otherwise = return () + + wrapDebug :: Outputable a => String -> (a -> Maybe a) -> a -> Hsc a + wrapDebug thing f x = do + let r = f x + for_ r (\x' -> + debug $ showSDoc df $ sep + [ text "Rewrote" <+> text thing <+> pprPrec 11 x <+> text "to" + , nest 2 $ pprPrec 11 x' + ]) + return $ fromMaybe x r + + extractLit :: HsExpr GhcPs -> Maybe (IntegralLit, HsExpr GhcPs) + extractLit (HsOverLit _ (OverLit _ (HsIntegral il) w)) = Just (il, w) + extractLit _ = Nothing + + fuseNegation :: Bool -> IntegralLit -> IntegralLit + fuseNegation negated (IL _txt neg val) = + let -- You can write patterns/exprs that are the negation of a neg literal. + -- We'll just sweep those under the rug by making them into a positive + -- literal. If there's more than one negation, too bad. Those will + -- try to call into a Num instance. + neg' = neg /= negated + + -- If the thing described in the previous comment happened, we have + -- e.g. "-4" as the source text. Just drop the source text always. + txt' = NoSourceText + + -- Set the sign of the resulting literal according to 'neg''. + val' = (if neg' then negate else id) (abs val) + + -- Refabricated literal. + in IL txt' neg' val' + + buildReprLit :: SrcSpan -> IntegralLit -> HsExpr GhcPs -> LHsExpr GhcPs + buildReprLit l il witness = + L l $ HsOverLit NoExtField $ OverLit NoExtField (HsIntegral il) witness + + rewriteLit :: SrcSpan -> Bool -> IntegralLit -> HsExpr GhcPs -> LHsExpr GhcPs + rewriteLit l negated il witness = + let il' = fuseNegation negated il + wrapper = nlHsVar litHashName `nlHsAppType` litToTyLit il' + lit = buildReprLit l il' witness + in L l $ HsApp NoExtField (nlHsApp wrapper lit) lit + + foldNegation :: LHsExpr GhcPs -> LHsExpr GhcPs + foldNegation (L l (NegApp _ (L _ (extractLit -> Just (il, witness))) _)) = + buildReprLit l (fuseNegation True il) witness + foldNegation e = e + + transformExp :: LHsExpr GhcPs -> Maybe (LHsExpr GhcPs) + transformExp (L l (extractLit -> Just (lit, witness))) = + Just $ rewriteLit l False lit witness + transformExp _ = Nothing + + transformPat :: LPat GhcPs -> Maybe (LPat GhcPs) + transformPat (LPat (NPat _ (L l (OverLit _ (HsIntegral il) witness)) negation _)) = + let il' = fuseNegation (isJust negation) il + + -- Wrapper application of match# to the LitRepr. + wrappedLit = + nlHsVar matchHashName + `nlHsAppType` litToTyLit il' + `nlHsApp_` buildReprLit l il' witness + `nlHsApp_` buildReprLit l il' witness + + in Just $ nlPat $ ViewPat NoExtField + wrappedLit + (nlPat $ ConPat NoExtField (nl cjustConName) (PrefixCon [])) + transformPat _ = Nothing diff --git a/tests/Deriving.hs b/tests/Deriving.hs new file mode 100644 --- /dev/null +++ b/tests/Deriving.hs @@ -0,0 +1,72 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Deriving where + +import Data.Int (Int8) +import Data.SNumber (SNumber) +import DependentLiterals (HasIntLiterals, StockLit(..)) +import GHC.TypeNats (type (*)) +import Kinds.Integer (Integer(..)) +import Data.Fin.Int (Fin) + +newtype MyType = MyType Int +#if !defined(__HLINT__) + deriving HasIntLiterals via StockLit Int +#endif + +x0 :: MyType +x0 = 0 + +-- TODO(awpr): it'd be nice to have this trigger -Woverflowed-literals; +-- currently the plugin passes this number as @Num MyType => MyType@, which +-- doesn't trigger it. Sadly I think if we tried to use type family machinery +-- to pass it as Int, it still wouldn't trigger, because the warning checks +-- whether the type /is/ the unique identifier Int, not whether it evaluates to +-- Int. +x1 :: MyType +x1 = 9223372036854775808 + +newtype MyType2 = MyType2 Int + deriving HasIntLiterals + +x2 :: MyType2 +x2 = 0 + +newtype MyType3 = MyType3 (Fin 4) + deriving HasIntLiterals + +x3 :: MyType3 +x3 = 2 + +newtype MyType4 n = MyType4 (SNumber Int ('Pos (2 * n))) + deriving HasIntLiterals + +x4 :: MyType4 77 +x4 = 154 + +newtype MyInt8 = MyInt8 Int8 + deriving HasIntLiterals + +x5 :: MyInt8 +x5 = 42 + +x6 :: MyInt8 +x6 = -7 diff --git a/tests/DoubleNegation.hs b/tests/DoubleNegation.hs new file mode 100644 --- /dev/null +++ b/tests/DoubleNegation.hs @@ -0,0 +1,53 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE CPP #-} +{-# LANGUAGE NegativeLiterals #-} +{-# LANGUAGE TypeOperators #-} + +module DoubleNegation where + +-- HLint doesn't parse the thing we're trying to test here, so shut it up. +#if !defined(__HLINT__) +import Data.Fin.Int (Fin) +import Data.Word (Word8) +import Data.Type.Equality ((:~:)(Refl)) +import Data.SInt (SInt) + +-- Turns out you can have both syntactic negation and a negative literal in the +-- same pattern/expression. We should not have a bug when doing that. + +x0 :: Int -> String +x0 x = case x of + -1 -> "-1" + - -2 -> "2...?" + _ -> "_" + +-- Make sure we in fact get proof for +2 out of matching on @- -2@. +x1 :: SInt n -> Maybe (n :~: 2) +x1 x = case x of + - -2 -> Just Refl + _ -> Nothing + +x2 :: Word8 +x2 = - -8 + +x3 :: Fin 5 +x3 = - -4 + +x4 :: SInt 2 -> SInt 2 +x4 x = case x of + - -2 -> x + _ -> x +#endif diff --git a/tests/FinErrors.hs b/tests/FinErrors.hs new file mode 100644 --- /dev/null +++ b/tests/FinErrors.hs @@ -0,0 +1,63 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# OPTIONS -Wwarn=inaccessible-code #-} + +module FinErrors where + +import Data.Fin.Int (Fin) + +x0 :: Fin 0 +-- Want: out of range. +x0 = 0 + +x1, x2 :: Fin 2 +-- Want: out of range. +x1 = 2 +-- Want: out of range. +x2 = -2 + +x3 :: Fin 2 -> String +x3 x = case x of + 0 -> "hi" + 3 -> "want unreachable code" -- TODO these could have better error messages + -1 -> "want unreachable code" + _ -> "other" + +-- Want: not sure it's in range +x4 :: Fin n +x4 = 42 + +-- Want: illegal -0 +x5 :: Fin 1 +x5 = -0 + +-- Since this literal overflows (LitRepr (Fin n) ~ Int), it's liable to +-- generate proof 18446744073709551618 < n when given any (2 :: Fin n), and +-- then make an ill-formed Fin of that value. We have constraints on the +-- underlying LitRepr precisely to prevent this: because this literal cannot be +-- faithfully represented by LitRepr (Fin n), even if the instance for Fin n +-- thinks it can accept the literal, we must reject it. +x100 :: Fin n -> Fin n +x100 x = case x of + 18446744073709551618 -> 18446744073709551618 + _ -> x + +-- This also needs to be a type error: if it matched (which it would for 2, if +-- we generated code for it), we would be able to create a proof that +-- 18446744073709551618 < n for any n > 2. +x101 :: Fin n -> Fin n +x101 x = case x of + 18446744073709551618 -> x + _ -> x diff --git a/tests/FinLiterals.hs b/tests/FinLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/FinLiterals.hs @@ -0,0 +1,43 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +module FinLiterals where + +import DependentLiterals (AllowsIntLiteral) +import GHC.TypeNats (CmpNat) +import Kinds.Integer (pattern Pos) +import Data.Fin.Int (Fin) + +type m < n = CmpNat m n ~ 'LT + +x0 :: Fin 1 +x0 = 0 + +x1 :: Fin 1024 +x1 = 42 + +x2 :: (4 < n) => Fin n +x2 = 4 + +x3 :: AllowsIntLiteral 4 (Fin n) => Fin n +x3 = 4 + +x4 :: AllowsIntLiteral ('Pos 4) (Fin n) => Fin n +x4 = 4 diff --git a/tests/FinPatterns.hs b/tests/FinPatterns.hs new file mode 100644 --- /dev/null +++ b/tests/FinPatterns.hs @@ -0,0 +1,37 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module FinPatterns where + +import Data.Fin.Int (Fin) + +-- Easy: we know @n@ statically, and don't need the provided constraints. +simpleMatch :: Fin 4 -> String +simpleMatch x = case x of + 0 -> "0" + 1 -> "1" + _ -> "2 or 3" + +-- Harder: we have to compare against 0/1 without knowing it's in range. +polyMatch :: Fin n -> String +polyMatch x = case x of + 0 -> "0" + 1 -> "1" + _ -> "unknown" + +-- Even harder: comparing against 2 has to prove that 2 is in range. +usingEvidence :: Fin n -> Maybe (Fin n) +usingEvidence x = case x of + 2 -> Just 2 + _ -> Nothing diff --git a/tests/FractionalLiterals.hs b/tests/FractionalLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/FractionalLiterals.hs @@ -0,0 +1,24 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module FractionalLiterals where + +x0 :: Float +x0 = 0 + +x1 :: Double +x1 = 0 + +x2 :: Rational +x2 = 0 diff --git a/tests/FractionalPatterns.hs b/tests/FractionalPatterns.hs new file mode 100644 --- /dev/null +++ b/tests/FractionalPatterns.hs @@ -0,0 +1,39 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module FractionalPatterns where + +x0 :: Float -> String +x0 x = case x of + 0 -> "0" + -2 -> "-2" + 2048 -> "2048" + 0.1 -> "0.1" -- Make sure we don't interfere with fractional literals... yet. + _ -> "_" + +x1 :: Double -> String +x1 x = case x of + 0 -> "0" + -2 -> "-2" + 2048 -> "2048" + 0.1 -> "0.1" -- Make sure we don't interfere with fractional literals... yet. + _ -> "_" + +x2 :: Rational -> String +x2 x = case x of + 0 -> "0" + -2 -> "-2" + 2048 -> "2048" + 0.1 -> "0.1" + _ -> "_" diff --git a/tests/IntErrors.hs b/tests/IntErrors.hs new file mode 100644 --- /dev/null +++ b/tests/IntErrors.hs @@ -0,0 +1,39 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module IntErrors where + +import Data.Int (Int8, Int16) + +x0, x1 :: Int8 +-- Want: 128 is too large +x0 = 128 +-- Want: -129 is too small +x1 = -129 + +x2 :: Int8 +-- Want: out of range for Int, for conversion to Int8 +x2 = 9223372036854775808 + +x3, x4 :: Int16 +-- Want: 32768 is too large +x3 = 32768 +-- Want: -32769 is too small +x4 = -32769 + +x5, x6 :: Int +-- Want: too large +x5 = 9223372036854775808 +-- Want: too small +x6 = -9223372036854775809 diff --git a/tests/IntLiterals.hs b/tests/IntLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/IntLiterals.hs @@ -0,0 +1,51 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module IntLiterals where + +import Data.Int (Int8, Int16, Int32, Int64) + +x :: Int +x = 4 + +-- We should be able to use -0 just fine for types with basic literals. +x1 :: Int +x1 = -0 + +x8 :: Int8 +x8 = 4 + +x16 :: Int16 +x16 = 4 + +x32 :: Int32 +x32 = 4 + +x64 :: Int64 +x64 = 4 + +y :: Int +y = -4 + +y8 :: Int8 +y8 = -4 + +y16 :: Int16 +y16 = -4 + +y32 :: Int32 +y32 = -4 + +y64 :: Int64 +y64 = -4 diff --git a/tests/IntPatterns.hs b/tests/IntPatterns.hs new file mode 100644 --- /dev/null +++ b/tests/IntPatterns.hs @@ -0,0 +1,47 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module IntPatterns where + +import Data.Int (Int8, Int16, Int32, Int64) + +x0 :: Int -> String +x0 x = case x of + 1 -> "1" + -2 -> "2" + _ -> "_" + +x1 :: Int8 -> String +x1 x = case x of + 1 -> "1" + -2 -> "2" + _ -> "_" + +x2 :: Int16 -> String +x2 x = case x of + 1 -> "1" + -2 -> "2" + _ -> "_" + +x3 :: Int32 -> String +x3 x = case x of + 1 -> "1" + -2 -> "2" + _ -> "_" + +x4 :: Int64 -> String +x4 x = case x of + 1 -> "1" + -2 -> "2" + _ -> "_" diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,20 @@ +-- Copyright 2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module Main where + +-- This is a shared 'main' function for compilation-only tests. The real tests +-- are in the compilation of the other-modules. +main :: IO () +main = return () diff --git a/tests/PolyErrors.hs b/tests/PolyErrors.hs new file mode 100644 --- /dev/null +++ b/tests/PolyErrors.hs @@ -0,0 +1,56 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +-- Provoking error messages with various amounts of context known about the +-- HasIntLiterals machinery. + +module PolyErrors where + +import DependentLiterals (HasIntLiterals) +import Data.Fin.Int (Fin) +import Data.SInt (SInt) + +-- With absolutely no context. +x1, x2 :: a +-- Want: no instance HasIntLiterals +-- TODO: this generates two errors currently. +x1 = 0 +-- Want: no instance HasIntLiterals +-- TODO: this generates two errors currently. +x2 = -1 + +-- With context that @a@ has an instance, but nothing else. +x3, x4 :: HasIntLiterals a => a +-- Want: something to the effect that we don't know enough about a? +-- TODO: this generates two errors currently. +x3 = 0 +-- Want: something to the effect that we don't know enough about a? +-- TODO: not very good errors +x4 = -1 + +-- With context that @a@ is some @Fin n@. +x5, x6 :: Fin n +-- Want: could not deduce IsLessThanMaxBound +x5 = 0 +-- Want: negative literal for unsigned type. +-- TODO: this generates two errors currently. +x6 = -1 + +-- With context that @a@ is some @SInt n@. +x7, x8 :: SInt n +-- Want: could not match type n with 0 +x7 = 0 +-- Want: negative literal for unsigned type +-- TODO: this generates 3 errors currently. +x8 = -1 diff --git a/tests/PolyLiterals.hs b/tests/PolyLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/PolyLiterals.hs @@ -0,0 +1,77 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} + +module PolyLiterals where + +import DependentLiterals (IntLiteral, HasBasicLiterals) +import Data.Vec.Short (Vec, (!)) +import qualified Data.Vec.Short as V +import GHC.TypeNats (CmpNat) +import Data.Fin.Int (Fin, (+!)) + +-- Will be exported from Fin, later. +type m < n = CmpNat m n ~ 'LT + +xx0 :: Int +xx0 = f (V.fromList [0, 2, 3, 7] :: Vec 4 Int) + where + f v = v ! 2 + +xx1 :: Fin 4 +xx1 = f (0 :: Fin 4) + where + f x = 1 +! x + +x0 :: IntLiteral 4 a => a +x0 = 4 + +x1 :: HasBasicLiterals a => a +x1 = 4 + +x2 :: HasBasicLiterals a => a +x2 = x0 + +x3 :: Fin 4 +x3 = x + where + x = 3 + +theFin :: Fin n -> Fin n +theFin = id + +x4 :: Fin 4 +x4 = x + where + x = theFin 3 + +x5 :: Fin 4 +x5 = x + where + x :: IntLiteral 3 a => a + x = 3 + +x6 :: (3 < n) => Fin n +x6 = x + where + x = 3 + +x7 :: (3 < n) => Fin n +x7 = x + where + x = theFin 3 diff --git a/tests/SIntErrors.hs b/tests/SIntErrors.hs new file mode 100644 --- /dev/null +++ b/tests/SIntErrors.hs @@ -0,0 +1,44 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module SIntErrors where + +import Data.SInt (SInt) + +-- Want: could not match type 3 with 2 +x0 :: SInt 2 +x0 = 3 + +-- Want: negative literal for unsigned type +-- TODO: this generates 3 errors currently. +x1 :: SInt 0 +x1 = -1 + +x2 :: SInt 2 -> String +x2 x = case x of + 0 -> "want inaccessible code error: 0 /= 2" + -1 -> "want inaccessible code error: -1 is negative" + _ -> "_" + +-- Want: could not match +x3 :: SInt n +x3 = 4 + +-- Want: does not match type index. +x4 :: SInt 0 +x4 = -0 + +-- Want: does not match type index. +x5 :: SInt n +x5 = -0 diff --git a/tests/SIntLiterals.hs b/tests/SIntLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/SIntLiterals.hs @@ -0,0 +1,31 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module SIntLiterals where + +import Data.SInt (SInt) + +import TestUtils (theSInt, asFin, showTyped) + +-- Easy: can we use a literal given that we know it matches the type? +x0 :: SInt 24 +x0 = 24 + +-- Can we infer the Nat index from the literal? +x1 :: String +x1 = showTyped (theSInt 24) + +-- Can we use it to pin down the Nat index of a Fin? +x2 :: String +x2 = showTyped (10 `asFin` 24) diff --git a/tests/SIntPatterns.hs b/tests/SIntPatterns.hs new file mode 100644 --- /dev/null +++ b/tests/SIntPatterns.hs @@ -0,0 +1,49 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE ScopedTypeVariables #-} + +module SIntPatterns where + +import Data.Fin.Int (Fin) +import Data.SInt (SInt) +import GHC.TypeNats (KnownNat) + +import TestUtils (showTyped) + +-- Easy: just match on the right value. +x0 :: SInt 2 -> String +x0 x = case x of + 2 -> "2" + _ -> "inconceivable" + +-- We can match on multiple values for unknown SNats. +x1 :: SInt n -> String +x1 x = case x of + 0 -> "0" + 1 -> "1" + _ -> "other" + +-- When matching literals, we get an equality proof. Inside each arm we know +-- @n@ statically and GHC will natively solve KnownNat constraints for it. +x2 :: forall n. SInt n -> String +x2 x = case x of + 0 -> "uninhabited" + 1 -> f 0 + 4 -> f 2 + 16 -> f 7 + _ -> "whatever" + where + f :: KnownNat n => Fin n -> String + f = showTyped diff --git a/tests/SNumberErrors.hs b/tests/SNumberErrors.hs new file mode 100644 --- /dev/null +++ b/tests/SNumberErrors.hs @@ -0,0 +1,61 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# OPTIONS -Wwarn=inaccessible-code #-} + +module SNumberErrors where + +import Data.SNumber (SNumber) +import Kinds.Integer (Integer(..)) + +-- Want: could not match type 3 with 2 +x0 :: SNumber Int ('Pos 2) +x0 = 3 + +-- Want: some form of "out of range" +x1 :: SNumber Int ('Pos 9223372036854775808) +x1 = 9223372036854775808 + +-- Want: could not match type 3 with 2 +x2 :: SNumber Word ('Pos 2) +x2 = 3 + +x3 :: SNumber Word ('Neg 2) +x3 = -2 + +x4 :: SNumber Int ('Pos 2) -> String +x4 x = case x of + 0 -> "want inaccessible code error: 0 /= 2" + -1 -> "want inaccessible code error: -1 is negative" + _ -> "_" + +-- Want: could not match +x5 :: SNumber Int n +x5 = 4 + +-- Want: does not match type index. +x6 :: SNumber Int ('Pos 0) +x6 = -0 + +-- Want: does not match type index. +x7 :: SNumber Int n +x7 = -0 + +-- Want: illegal -0 +x8 :: SNumber Int ('Neg 0) +x8 = -0 + +-- Want: don't know enough about a. +x9 :: SNumber a ('Pos 0) +x9 = 0 diff --git a/tests/SNumberLiterals.hs b/tests/SNumberLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/SNumberLiterals.hs @@ -0,0 +1,49 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE TypeApplications #-} + +module SNumberLiterals where + +import Data.SNumber (SNumber) +import DependentLiterals (valueOf) +import Kinds.Integer (Integer(..)) +import Numeric.Natural (Natural) + +x0 :: SNumber Natural ('Pos 0) +x0 = 0 + +x1 :: SNumber Natural ('Pos 4096) +x1 = 4096 + +x2 :: SNumber Natural ('Pos 77) +x2 = valueOf @77 + +x3 :: SNumber Natural ('Pos 77) +x3 = valueOf @('Pos 77) + +x4 :: SNumber Int ('Pos 0) +x4 = 0 + +x5 :: SNumber Int ('Neg 4) +x5 = -4 + +x6 :: SNumber Int ('Neg 77) +x6 = valueOf @('Neg 77) + +x7 :: SNumber Word ('Pos 7) +x7 = 7 + +x8 :: SNumber Prelude.Integer ('Neg 44) +x8 = -44 diff --git a/tests/TestUtils.hs b/tests/TestUtils.hs new file mode 100644 --- /dev/null +++ b/tests/TestUtils.hs @@ -0,0 +1,49 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} + +module TestUtils + ( type (<), theFin, theSInt + , atNat, asFin, showTyped, showsPrecTyped + ) where + +import Data.Fin.Int (Fin) +import Data.SInt (SInt) +import Data.Typeable (Typeable, typeOf) +import GHC.TypeNats (CmpNat) + +type m < n = CmpNat m n ~ 'LT + +theSInt :: SInt n -> SInt n +theSInt = id + +theFin :: Fin n -> Fin n +theFin = id + +atNat :: SInt n -> p n -> p n +atNat _ = id + +asFin :: Fin n -> SInt n -> Fin n +asFin = const + +showsPrecTyped :: (Show a, Typeable a) => Int -> a -> ShowS +showsPrecTyped p x = showParen (p > 0) $ + shows x . showString " :: " . shows (typeOf x) + +showTyped :: (Show a, Typeable a) => a -> String +showTyped x = showsPrecTyped 0 x "" diff --git a/tests/VecExamples.hs b/tests/VecExamples.hs new file mode 100644 --- /dev/null +++ b/tests/VecExamples.hs @@ -0,0 +1,33 @@ +-- Copyright 2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module VecExamples where + +import Data.Vec.Short.Explicit + +-- Passing a literal to 'mkVec' for the 'SInt' param disambiguates the length. +x1 :: IO () +x1 = print $ mkVec 4 id + +-- This also propagates to the 'Fin' indices: changing 2 to 4 is a type error. +x2 :: IO () +x2 = print $ mkVec 4 id ! 2 + +-- Just driving the point home: 'fromList' works the same way. +x3 :: IO () +x3 = print $ fromList 5 "aoeui" ! 4 + +-- Matching on 'svSize' makes the length index statically-known. +x4 :: Vec n a -> Maybe (Vec 4 a) +x4 v = case svSize v of 4 -> Just v; _ -> Nothing diff --git a/tests/WithNegativeLiterals.hs b/tests/WithNegativeLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/WithNegativeLiterals.hs @@ -0,0 +1,32 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +{-# LANGUAGE NegativeLiterals #-} +{-# LANGUAGE UndecidableInstances #-} + +module WithNegativeLiterals where + +import Data.Int (Int8, Int16, Int32, Int64) + +x0 :: Int8 +x0 = -128 + +x1 :: Int16 +x1 = -32768 + +x2 :: Int32 +x2 = -2147483648 + +x3 :: Int64 +x3 = -9223372036854775808 diff --git a/tests/WordErrors.hs b/tests/WordErrors.hs new file mode 100644 --- /dev/null +++ b/tests/WordErrors.hs @@ -0,0 +1,34 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module WordErrors where + +import Data.Word (Word8, Word16, Word) + +-- Want -Woverflowed-literals warnings for all of these. + +x1, x2, x3 :: Word8 +x1 = -1 +x2 = -256 +x3 = 256 + +x4, x5, x6 :: Word16 +x4 = -1 +x5 = -65536 +x6 = 65536 + +x7, x8, x9 :: Word +x7 = -1 +x8 = -18446744073709551616 +x9 = 18446744073709551616 diff --git a/tests/WordLiterals.hs b/tests/WordLiterals.hs new file mode 100644 --- /dev/null +++ b/tests/WordLiterals.hs @@ -0,0 +1,32 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module WordLiterals where + +import Data.Word (Word8, Word16, Word32, Word64) + +x :: Word +x = 4 + +x8 :: Word8 +x8 = 4 + +x16 :: Word16 +x16 = 4 + +x32 :: Word32 +x32 = 4 + +x64 :: Word64 +x64 = 4 diff --git a/tests/WordPatterns.hs b/tests/WordPatterns.hs new file mode 100644 --- /dev/null +++ b/tests/WordPatterns.hs @@ -0,0 +1,47 @@ +-- Copyright 2020-2021 Google LLC +-- +-- Licensed under the Apache License, Version 2.0 (the "License"); +-- you may not use this file except in compliance with the License. +-- You may obtain a copy of the License at +-- +-- http://www.apache.org/licenses/LICENSE-2.0 +-- +-- Unless required by applicable law or agreed to in writing, software +-- distributed under the License is distributed on an "AS IS" BASIS, +-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +-- See the License for the specific language governing permissions and +-- limitations under the License. + +module WordPatterns where + +import Data.Word (Word8, Word16, Word32, Word64) + +f :: Word -> String +f x = case x of + 1 -> "1" + 2 -> "2" + _ -> "_" + +f8 :: Word8 -> String +f8 x = case x of + 1 -> "1" + 2 -> "2" + _ -> "_" + +f16 :: Word16 -> String +f16 x = case x of + 1 -> "1" + 2 -> "2" + _ -> "_" + +f32 :: Word32 -> String +f32 x = case x of + 1 -> "1" + 2 -> "2" + _ -> "_" + +f64 :: Word64 -> String +f64 x = case x of + 1 -> "1" + 2 -> "2" + _ -> "_"