diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,6 @@ +# Changelog + +## 0.1.0 (10/27/2020) + +Initial release. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,19 @@ +Copyright 2020 Matt Superdock + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,155 @@ +# agda-unused + +`agda-unused` checks for unused code in an Agda project, including: + +- variables +- definitions +- postulates +- data & record types +- `import` statements +- `open` statements +- pattern synonyms + +`agda-unused` can be run globally on a full project, or locally on a file and +its dependencies. Running `agda-unused` globally requires an `.agda-roots` file +in the project root directory, which specifies the "roots" of the project. The +"roots" of a project are identifiers that are considered used even if not used +within the project itself. You might think of the `.agda-roots` file as a +specification of the public interface of your project. + +## Example + +File `~/Test.agda`: + +``` +module Test where + +open import Agda.Builtin.Bool + using (Bool; false; true) +open import Agda.Builtin.Unit + +_∧_ + : Bool + → Bool + → Bool +false ∧ x + = false +_ ∧ y + = y +``` + +Command: + +``` +$ agda-unused --local Test.agda +``` + +Output: + +``` +/home/user/Test.agda:4,23-27 + unused imported item ‘true’ +/home/user/Test.agda:5,1-30 + unused import ‘Agda.Builtin.Unit’ +/home/user/Test.agda:11,9-10 + unused variable ‘x’ +``` + +## Roots + +Running `agda-unused` globally requires an `.agda-roots` file in the project +root directory. The `.agda-roots` format consists of: + +- Module names, each followed by a list of (possibly qualified) identifiers. +- Module names in parentheses. + +All given module names not in parentheses are checked, along with their +dependencies. The given identifiers are considered roots; they will not be +marked unused. Qualified identifiers refer to identifiers defined within inner +modules. If no identifiers are given for a module, all publicly accessible +identifiers are considered roots. + +All given module names in parentheses are ignored when checking for unused +files. Such modules may still be checked if imported by another module. + +Example `.agda-roots` file: + +``` +Main +- main + +Pythagorean.Core +- isTriple +- allTriples + +(Pythagorean.Examples) + +Pythagorean.Theorems + +Pythagorean.Utils +- Print.prettyNat +``` + +Spacing and indentation are irrelevant. + +## Usage + +``` +Usage: agda-unused [-r|--root ROOT] [-l|--local FILE] + Check for unused code in project with root directory ROOT + +Available options: + -h,--help Show this help text + -r,--root ROOT Path of project root directory + -l,--local FILE Path of file to check locally + -j,--json Format output as JSON +``` + +The project root directory is determined as follows: + +- If the `--root` option is given, its value is the project root. +- If the `--local` option is given, the nearest ancestor with an `.agda-roots` + file is the project root, if any. +- If the current directory has an `.agda-roots` file, it is the project root. +- Otherwise, the nearest ancestor of the current directory with an `.agda-roots` + file is the project root, if any. +- Otherwise, we take the current directory as the project root. + +## Approach + +We make a single pass through each relevant Agda file: + +- When a new item (variable, definition, etc.) appears, we mark it unused. +- When an existing item appears, we mark it used. + +This means, for example, if we have three definitions (say `f`, `g`, `h`), each +depending on the previous one, where `h` is not a root, then `f` and `g` are +considered used, while `h` is considered unused. If we remove `h` and run +`agda-unsed` again, it will now report that `g` is unused. This behavior is +different from Haskell's built-in tool, which would report that all three +identifiers are unused on the first run. + +For a global check, we check each file appearing in `.agda-roots` and its +dependencies. For a local check, we check just the given file and its +dependencies, ignoring all publicly accessible definitions. + +## JSON + +If the `--json` switch is given, the output is a JSON object with two fields: + +- `type`: One of `"none"`, `"unused"`, `"error"`. +- `message`: A string, the same as the usual output of `agda-unused`. + +The `"none"` type indicates that there is no unused code. + +## Limitations + +We currently do not support the following Agda features: + +- [record module instance applications](https://agda.readthedocs.io/en/v2.6.1.1/language/module-system.html#parameterised-modules) +- [unquoting declarations](https://agda.readthedocs.io/en/v2.6.1.1/language/reflection.html#id3) +- [external libraries](https://agda.readthedocs.io/en/v2.6.1.1/tools/package-system.html) +(other than Agda's built-in libraries) + +`agda-unused` will produce an error if your code uses these language features. + diff --git a/agda-unused.cabal b/agda-unused.cabal new file mode 100644 --- /dev/null +++ b/agda-unused.cabal @@ -0,0 +1,123 @@ +cabal-version: 3.0 + +name: + agda-unused +version: + 0.1.0 +build-type: + Simple +license: + MIT +license-file: + LICENSE +maintainer: + Matt Superdock +synopsis: + Check for unused code in an Agda project. +description: + A tool to check for unused code in an Agda project. +category: + Dependent types +data-files: + data/**/*.agda +extra-source-files: + CHANGELOG.md + README.md + +source-repository head + type: + git + location: + https://github.com/msuperdock/agda-unused.git + +library + hs-source-dirs: + src + exposed-modules: + Agda.Unused + Agda.Unused.Check + Agda.Unused.Monad.Error + Agda.Unused.Monad.Reader + Agda.Unused.Monad.State + Agda.Unused.Parse + Agda.Unused.Print + Agda.Unused.Types.Access + Agda.Unused.Types.Context + Agda.Unused.Types.Name + Agda.Unused.Types.Range + Agda.Unused.Types.Root + Agda.Unused.Utils + other-modules: + Paths_agda_unused + autogen-modules: + Paths_agda_unused + build-depends: + base >= 4.13.0 && < 4.14, + Agda >= 2.6.1 && < 2.6.2, + containers >= 0.6.2 && < 0.7, + directory >= 1.3.6 && < 1.4, + filepath >= 1.4.2 && < 1.5, + megaparsec >= 8.0.0 && < 8.1, + mtl >= 2.2.2 && < 2.3, + text >= 1.2.4 && < 1.3 + default-language: + Haskell2010 + default-extensions: + FlexibleContexts, + FlexibleInstances, + GADTs, + OverloadedStrings + ghc-options: + -Wall + -Wno-orphans + +executable agda-unused + hs-source-dirs: + app + main-is: + Main.hs + build-depends: + agda-unused, + base >= 4.13.0 && < 4.14, + aeson >= 1.4.7 && < 1.5, + directory >= 1.3.6 && < 1.4, + filepath >= 1.4.2 && < 1.5, + mtl >= 2.2.2 && < 2.3, + optparse-applicative >= 0.15.1 && < 0.16, + text >= 1.2.4 && < 1.3 + default-language: + Haskell2010 + default-extensions: + FlexibleContexts, + GADTs, + OverloadedStrings + ghc-options: + -Wall + +test-suite test + type: + exitcode-stdio-1.0 + hs-source-dirs: + test + main-is: + Main.hs + other-modules: + Paths_agda_unused + autogen-modules: + Paths_agda_unused + build-depends: + agda-unused, + base >= 4.13.0 && < 4.14, + containers >= 0.6.2 && < 0.7, + filepath >= 1.4.2 && < 1.5, + hspec >= 2.7.1 && < 2.8, + text >= 1.2.4 && < 1.3 + default-language: + Haskell2010 + default-extensions: + FlexibleInstances, + GADTs, + TypeSynonymInstances + ghc-options: + -Wall + diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,290 @@ +module Main where + +import Agda.Unused.Check + (checkUnused, checkUnusedLocal) +import qualified Agda.Unused.Monad.Error + as E +import Agda.Unused.Parse + (parseConfig) +import qualified Agda.Unused.Print + as P +import Agda.Unused.Types.Name + (Name(..), NamePart(..), QName(..)) +import Agda.Unused.Utils + (liftMaybe, mapLeft) + +import Control.Monad.Except + (MonadError, liftEither, runExceptT, throwError) +import Control.Monad.IO.Class + (MonadIO, liftIO) +import Data.Aeson + (Value(..), (.=), object) +import Data.Aeson.Text + (encodeToLazyText) +import Data.Bool + (bool) +import Data.List + (stripPrefix) +import Data.Text + (Text) +import qualified Data.Text + as T +import qualified Data.Text.IO + as I +import Data.Text.Lazy + (toStrict) +import Options.Applicative + (InfoMod, Parser, ParserInfo, execParser, fullDesc, header, help, helper, + info, long, metavar, optional, progDesc, short, strOption, switch) +import System.Directory + (doesFileExist, getCurrentDirectory, makeAbsolute) +import System.Exit + (exitFailure, exitSuccess) +import System.FilePath + ((), splitDirectories, stripExtension, takeDirectory) +import System.IO + (stderr) + +-- ## Options + +data Options + = Options + { optionsRoot + :: !(Maybe FilePath) + -- ^ The project root path. + , optionsFile + :: !(Maybe FilePath) + -- ^ A file path to check locally. + , optionsJSON + :: !Bool + -- ^ Whether to output JSON. + } deriving Show + +optionsParser + :: Parser Options +optionsParser + = Options + <$> optional (strOption + $ short 'r' + <> long "root" + <> metavar "ROOT" + <> help "Path of project root directory") + <*> optional (strOption + $ short 'l' + <> long "local" + <> metavar "FILE" + <> help "Path of file to check locally") + <*> (switch + $ short 'j' + <> long "json" + <> help "Format output as JSON") + +optionsInfo + :: InfoMod a +optionsInfo + = fullDesc + <> progDesc "Check for unused code in project with root directory ROOT" + <> header "agda-unused - check for unused code in an Agda project" + +options + :: ParserInfo Options +options + = info (helper <*> optionsParser) optionsInfo + +-- ## Errors + +data Error where + + ErrorFile + :: !FilePath + -> Error + + ErrorLocal + :: !FilePath + -> Error + + ErrorParse + :: !Text + -> Error + + deriving Show + +-- ## Check + +check + :: Options + -> IO () +check o@(Options _ _ j) + = runExceptT (check' o) + >>= either (printErrorWith j) (const (pure ())) + +check' + :: MonadError Error m + => MonadIO m + => Options + -> m () + +check' o@(Options _ Nothing j) = do + rootPath + <- liftIO (getRootDirectory o) + configPath + <- pure (rootPath ".agda-roots") + exists + <- liftIO (doesFileExist configPath) + _ + <- bool (throwError (ErrorFile configPath)) (pure ()) exists + contents + <- liftIO (I.readFile configPath) + roots + <- liftEither (mapLeft ErrorParse (parseConfig contents)) + checkResult + <- liftIO (checkUnused rootPath roots) + _ + <- liftIO (printResult j P.printUnused checkResult) + pure () + +check' o@(Options _ (Just f) j) = do + rootPath + <- liftIO (getRootDirectory o) + rootPath' + <- pure (splitDirectories rootPath) + filePath + <- liftIO (makeAbsolute f >>= \f' -> pure (splitDirectories f')) + localModule + <- liftMaybe (ErrorLocal f) (stripPrefix rootPath' filePath >>= pathModule) + checkResult + <- liftIO (checkUnusedLocal rootPath localModule) + _ + <- liftIO (printResult j P.printUnusedItems checkResult) + pure () + +pathModule + :: [FilePath] + -> Maybe QName +pathModule [] + = Nothing +pathModule (p : []) + = QName . name <$> stripExtension "agda" p +pathModule (p : ps@(_ : _)) + = Qual (name p) <$> pathModule ps + +name + :: String + -> Name +name p + = Name [Id p] + +-- ## Print + +printResult + :: Bool + -- ^ Whether to output JSON. + -> (a -> Maybe Text) + -> Either E.Error a + -> IO () +printResult False _ (Left e) + = I.hPutStrLn stderr (P.printError e) >> exitFailure +printResult False p (Right x) + = I.putStrLn (maybe P.printNothing id (p x)) >> exitSuccess +printResult True p x + = I.putStrLn (toStrict (encodeToLazyText (printResultJSON p x))) + +printErrorWith + :: Bool + -- ^ Whether to output JSON. + -> Error + -> IO () +printErrorWith False e + = I.hPutStrLn stderr (printError e) >> exitFailure +printErrorWith True e + = I.putStrLn (toStrict (encodeToLazyText (printErrorJSON e))) + +printError + :: Error + -> Text +printError (ErrorFile p) + = "Error: .agda-roots file not found " <> parens (T.pack p) <> "." +printError (ErrorLocal l) + = "Error: Invalid local path " <> parens (T.pack l) <> "." +printError (ErrorParse t) + = t + +parens + :: Text + -> Text +parens t + = "(" <> t <> ")" + +-- ## JSON + +printErrorJSON + :: Error + -> Value +printErrorJSON e + = encodeMessage "error" (printError e) + +printResultJSON + :: (a -> Maybe Text) + -> Either E.Error a + -> Value +printResultJSON _ (Left e) + = encodeMessage "error" (P.printError e) +printResultJSON p (Right u) + = maybe (encodeMessage "none" P.printNothing) (encodeMessage "unused") (p u) + +encodeMessage + :: Text + -- ^ Type of message. + -> Text + -- ^ Contents of message. + -> Value +encodeMessage t m + = object ["type" .= t, "message" .= m] + +-- ## Root + +getRootDirectory + :: Options + -> IO FilePath +getRootDirectory (Options Nothing Nothing _) + = getCurrentDirectory + >>= \p -> getRootDirectoryFrom p p +getRootDirectory (Options Nothing (Just p) _) + = makeAbsolute p + >>= \p' -> getRootDirectoryFrom (takeDirectory p') (takeDirectory p') +getRootDirectory (Options (Just p) _ _) + = makeAbsolute p + +-- Search recursively upwards for project root directory. +getRootDirectoryFrom + :: FilePath + -- ^ Default directory. + -> FilePath + -- ^ Starting directory. + -> IO FilePath +getRootDirectoryFrom d p + = doesFileExist (p ".agda-roots") >>= getRootDirectoryWith d p + +getRootDirectoryWith + :: FilePath + -- ^ Default directory. + -> FilePath + -- ^ Starting directory. + -> Bool + -- ^ Whether the starting directory contains an .agda-roots file. + -> IO FilePath +getRootDirectoryWith _ p True + = pure p +getRootDirectoryWith d p False | takeDirectory p == p + = pure d +getRootDirectoryWith d p False + = getRootDirectoryFrom d (takeDirectory p) + +-- ## Main + +main + :: IO () +main + = execParser options + >>= check + diff --git a/data/Agda/Builtin/Bool.agda b/data/Agda/Builtin/Bool.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Bool.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism + --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Bool where + +data Bool : Set where + false true : Bool + +{-# BUILTIN BOOL Bool #-} +{-# BUILTIN FALSE false #-} +{-# BUILTIN TRUE true #-} + +{-# COMPILE UHC Bool = data __BOOL__ (__FALSE__ | __TRUE__) #-} + +{-# COMPILE JS Bool = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-} +{-# COMPILE JS false = false #-} +{-# COMPILE JS true = true #-} diff --git a/data/Agda/Builtin/Char.agda b/data/Agda/Builtin/Char.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Char.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism + --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Char where + +open import Agda.Builtin.Nat +open import Agda.Builtin.Bool + +postulate Char : Set +{-# BUILTIN CHAR Char #-} + +primitive + primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii + primIsLatin1 primIsPrint primIsHexDigit : Char → Bool + primToUpper primToLower : Char → Char + primCharToNat : Char → Nat + primNatToChar : Nat → Char + primCharEquality : Char → Char → Bool diff --git a/data/Agda/Builtin/Char/Properties.agda b/data/Agda/Builtin/Char/Properties.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Char/Properties.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Char.Properties where + +open import Agda.Builtin.Char +open import Agda.Builtin.Equality + +primitive + + primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b diff --git a/data/Agda/Builtin/Coinduction.agda b/data/Agda/Builtin/Coinduction.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Coinduction.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --without-K --safe --universe-polymorphism --no-sized-types + --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Coinduction where + +infix 1000 ♯_ + +postulate + ∞ : ∀ {a} (A : Set a) → Set a + ♯_ : ∀ {a} {A : Set a} → A → ∞ A + ♭ : ∀ {a} {A : Set a} → ∞ A → A + +{-# BUILTIN INFINITY ∞ #-} +{-# BUILTIN SHARP ♯_ #-} +{-# BUILTIN FLAT ♭ #-} diff --git a/data/Agda/Builtin/Cubical/Glue.agda b/data/Agda/Builtin/Cubical/Glue.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Cubical/Glue.agda @@ -0,0 +1,123 @@ +{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Cubical.Glue where + +open import Agda.Primitive +open import Agda.Builtin.Sigma +open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_; + primHComp to hcomp; primTransp to transp; primComp to comp; + itIsOne to 1=1) +open import Agda.Builtin.Cubical.Path +open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc) +import Agda.Builtin.Cubical.HCompU as HCompU + +module Helpers = HCompU.Helpers + +open Helpers + + +-- We make this a record so that isEquiv can be proved using +-- copatterns. This is good because copatterns don't get unfolded +-- unless a projection is applied so it should be more efficient. +record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where + no-eta-equality + field + equiv-proof : (y : B) → isContr (fiber f y) + +open isEquiv public + +infix 4 _≃_ + + +_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ') +A ≃ B = Σ (A → B) \ f → (isEquiv f) + +equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B +equivFun e = fst e + +-- Improved version of equivProof compared to Lemma 5 in CCHM. We put +-- the (φ = i0) face in contr' making it be definitionally c in this +-- case. This makes the computational behavior better, in particular +-- for transp in Glue. +equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A) + → ∀ ψ → (Partial ψ (fiber (w .fst) a)) → fiber (w .fst) a +equivProof A B w a ψ fb = contr' {A = fiber (w .fst) a} (w .snd .equiv-proof a) ψ fb + where + contr' : ∀ {ℓ} {A : Set ℓ} → isContr A → (φ : I) → (u : Partial φ A) → A + contr' {A = A} (c , p) φ u = hcomp (λ i → λ { (φ = i1) → p (u 1=1) i + ; (φ = i0) → c }) c + + +{-# BUILTIN EQUIV _≃_ #-} +{-# BUILTIN EQUIVFUN equivFun #-} +{-# BUILTIN EQUIVPROOF equivProof #-} + +primitive + primGlue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I} + → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A)) + → Set ℓ' + prim^glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I} + → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)} + → (t : PartialP φ T) → (a : A) → primGlue A T e + prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I} + → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)} + → primGlue A T e → A + + -- Needed for transp in Glue. + primFaceForall : (I → I) → I + + +module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where + private + E : (i : I) → Set (ℓ i) + E = λ i → P i + ~E : (i : I) → Set (ℓ (~ i)) + ~E = λ i → P (~ i) + + A = P i0 + B = P i1 + + f : A → B + f x = transp E i0 x + + g : B → A + g y = transp ~E i0 y + + u : ∀ i → A → E i + u i x = transp (λ j → E (i ∧ j)) (~ i) x + + v : ∀ i → B → E i + v i y = transp (λ j → ~E ( ~ i ∧ j)) i y + + fiberPath : (y : B) → (xβ0 xβ1 : fiber f y) → xβ0 ≡ xβ1 + fiberPath y (x0 , β0) (x1 , β1) k = ω , λ j → δ (~ j) where + module _ (j : I) where + private + sys : A → ∀ i → PartialP (~ j ∨ j) (λ _ → E (~ i)) + sys x i (j = i0) = v (~ i) y + sys x i (j = i1) = u (~ i) x + ω0 = comp ~E (sys x0) ((β0 (~ j))) + ω1 = comp ~E (sys x1) ((β1 (~ j))) + θ0 = fill ~E (sys x0) (inc (β0 (~ j))) + θ1 = fill ~E (sys x1) (inc (β1 (~ j))) + sys = λ {j (k = i0) → ω0 j ; j (k = i1) → ω1 j} + ω = hcomp sys (g y) + θ = hfill sys (inc (g y)) + δ = λ (j : I) → comp E + (λ i → λ { (j = i0) → v i y ; (k = i0) → θ0 j (~ i) + ; (j = i1) → u i ω ; (k = i1) → θ1 j (~ i) }) + (θ j) + + γ : (y : B) → y ≡ f (g y) + γ y j = comp E (λ i → λ { (j = i0) → v i y + ; (j = i1) → u i (g y) }) (g y) + + pathToisEquiv : isEquiv f + pathToisEquiv .equiv-proof y .fst .fst = g y + pathToisEquiv .equiv-proof y .fst .snd = sym (γ y) + pathToisEquiv .equiv-proof y .snd = fiberPath y _ + + pathToEquiv : A ≃ B + pathToEquiv .fst = f + pathToEquiv .snd = pathToisEquiv diff --git a/data/Agda/Builtin/Cubical/HCompU.agda b/data/Agda/Builtin/Cubical/HCompU.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Cubical/HCompU.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Cubical.HCompU where + +open import Agda.Primitive +open import Agda.Builtin.Sigma +open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_; + primHComp to hcomp; primTransp to transp; primComp to comp; + itIsOne to 1=1) +open import Agda.Builtin.Cubical.Path +open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS; inc to inS) + +module Helpers where + -- Homogeneous filling + hfill : ∀ {ℓ} {A : Set ℓ} {φ : I} + (u : ∀ i → Partial φ A) + (u0 : A [ φ ↦ u i0 ]) (i : I) → A + hfill {φ = φ} u u0 i = + hcomp (λ j → \ { (φ = i1) → u (i ∧ j) 1=1 + ; (i = i0) → outS u0 }) + (outS u0) + + -- Heterogeneous filling defined using comp + fill : ∀ {ℓ : I → Level} (A : ∀ i → Set (ℓ i)) {φ : I} + (u : ∀ i → Partial φ (A i)) + (u0 : A i0 [ φ ↦ u i0 ]) → + ∀ i → A i + fill A {φ = φ} u u0 i = + comp (λ j → A (i ∧ j)) + (λ j → \ { (φ = i1) → u (i ∧ j) 1=1 + ; (i = i0) → outS u0 }) + (outS {φ = φ} u0) + + module _ {ℓ} {A : Set ℓ} where + refl : {x : A} → x ≡ x + refl {x = x} = λ _ → x + + sym : {x y : A} → x ≡ y → y ≡ x + sym p = λ i → p (~ i) + + cong : ∀ {ℓ'} {B : A → Set ℓ'} {x y : A} + (f : (a : A) → B a) (p : x ≡ y) + → PathP (λ i → B (p i)) (f x) (f y) + cong f p = λ i → f (p i) + + isContr : ∀ {ℓ} → Set ℓ → Set ℓ + isContr A = Σ A \ x → (∀ y → x ≡ y) + + fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ') + fiber {A = A} f y = Σ A \ x → f x ≡ y + +open Helpers + + +primitive + prim^glueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)} + {A : Set la [ φ ↦ T i0 ]} → + PartialP φ (T i1) → outS A → hcomp T (outS A) + prim^unglueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)} + {A : Set la [ φ ↦ T i0 ]} → + hcomp T (outS A) → outS A + +transpProof : ∀ {l} → (e : I → Set l) → (φ : I) → (a : Partial φ (e i0)) → (b : e i1 [ φ ↦ (\ o → transp e i0 (a o)) ] ) → fiber (transp e i0) (outS b) +transpProof e φ a b = f , \ j → comp e (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ i)) (~ i) (a 1=1) + ; (j = i0) → transp (\ j → e (j ∧ i)) (~ i) f + ; (j = i1) → g (~ i) }) + f + where + g = fill (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1); (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) (outS b) }) (inS (outS b)) + f = comp (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1); (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) (outS b) }) (outS b) + +{-# BUILTIN TRANSPPROOF transpProof #-} diff --git a/data/Agda/Builtin/Cubical/Id.agda b/data/Agda/Builtin/Cubical/Id.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Cubical/Id.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Cubical.Id where + + open import Agda.Primitive.Cubical + open import Agda.Builtin.Cubical.Path + open import Agda.Builtin.Cubical.Sub renaming (primSubOut to ouc; Sub to _[_↦_]) + + postulate + Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ + + {-# BUILTIN ID Id #-} + {-# BUILTIN CONID conid #-} + + primitive + primDepIMin : _ + primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I + primIdPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → x ≡ y + + primitive + primIdJ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ') → + P x (conid i1 (λ i → x)) → ∀ {y} (p : Id x y) → P y p + + + primitive + primIdElim : ∀ {a c} {A : Set a} {x : A} + (C : (y : A) → Id x y → Set c) → + ((φ : I) (y : A [ φ ↦ (λ _ → x) ]) + (w : (x ≡ ouc y) [ φ ↦ (λ { (φ = i1) → \ _ → x}) ]) → + C (ouc y) (conid φ (ouc w))) → + {y : A} (p : Id x y) → C y p diff --git a/data/Agda/Builtin/Cubical/Path.agda b/data/Agda/Builtin/Cubical/Path.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Cubical/Path.agda @@ -0,0 +1,20 @@ +{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Cubical.Path where + + open import Agda.Primitive.Cubical + + postulate + PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ + + {-# BUILTIN PATHP PathP #-} + + infix 4 _≡_ + + -- We have a variable name in `(λ i → A)` as a hint for case + -- splitting. + _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ + _≡_ {A = A} = PathP (λ i → A) + + {-# BUILTIN PATH _≡_ #-} diff --git a/data/Agda/Builtin/Cubical/Sub.agda b/data/Agda/Builtin/Cubical/Sub.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Cubical/Sub.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Cubical.Sub where + + open import Agda.Primitive.Cubical + + {-# BUILTIN SUB Sub #-} + + postulate + inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x) + + {-# BUILTIN SUBIN inc #-} + + primitive + primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A diff --git a/data/Agda/Builtin/Equality.agda b/data/Agda/Builtin/Equality.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Equality.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Equality where + +infix 4 _≡_ +data _≡_ {a} {A : Set a} (x : A) : A → Set a where + instance refl : x ≡ x + +{-# BUILTIN EQUALITY _≡_ #-} diff --git a/data/Agda/Builtin/Equality/Erase.agda b/data/Agda/Builtin/Equality/Erase.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Equality/Erase.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --with-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Equality.Erase where + +open import Agda.Builtin.Equality + +primitive primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y diff --git a/data/Agda/Builtin/Equality/Rewrite.agda b/data/Agda/Builtin/Equality/Rewrite.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Equality/Rewrite.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Equality.Rewrite where + +open import Agda.Builtin.Equality + +{-# BUILTIN REWRITE _≡_ #-} diff --git a/data/Agda/Builtin/Float.agda b/data/Agda/Builtin/Float.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Float.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Float where + +open import Agda.Builtin.Bool +open import Agda.Builtin.Nat +open import Agda.Builtin.Int +open import Agda.Builtin.Word +open import Agda.Builtin.String + +postulate Float : Set +{-# BUILTIN FLOAT Float #-} + +primitive + primFloatToWord64 : Float → Word64 + primFloatEquality : Float → Float → Bool + primFloatLess : Float → Float → Bool + primFloatNumericalEquality : Float → Float → Bool + primFloatNumericalLess : Float → Float → Bool + primNatToFloat : Nat → Float + primFloatPlus : Float → Float → Float + primFloatMinus : Float → Float → Float + primFloatTimes : Float → Float → Float + primFloatNegate : Float → Float + primFloatDiv : Float → Float → Float + primFloatSqrt : Float → Float + primRound : Float → Int + primFloor : Float → Int + primCeiling : Float → Int + primExp : Float → Float + primLog : Float → Float + primSin : Float → Float + primCos : Float → Float + primTan : Float → Float + primASin : Float → Float + primACos : Float → Float + primATan : Float → Float + primATan2 : Float → Float → Float + primShowFloat : Float → String diff --git a/data/Agda/Builtin/Float/Properties.agda b/data/Agda/Builtin/Float/Properties.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Float/Properties.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Float.Properties where + +open import Agda.Builtin.Float +open import Agda.Builtin.Equality + +primitive + + primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b diff --git a/data/Agda/Builtin/FromNat.agda b/data/Agda/Builtin/FromNat.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/FromNat.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.FromNat where + +open import Agda.Primitive +open import Agda.Builtin.Nat + +record Number {a} (A : Set a) : Set (lsuc a) where + field + Constraint : Nat → Set a + fromNat : ∀ n → {{_ : Constraint n}} → A + +open Number {{...}} public using (fromNat) + +{-# BUILTIN FROMNAT fromNat #-} +{-# DISPLAY Number.fromNat _ n = fromNat n #-} diff --git a/data/Agda/Builtin/FromNeg.agda b/data/Agda/Builtin/FromNeg.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/FromNeg.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.FromNeg where + +open import Agda.Primitive +open import Agda.Builtin.Nat + +record Negative {a} (A : Set a) : Set (lsuc a) where + field + Constraint : Nat → Set a + fromNeg : ∀ n → {{_ : Constraint n}} → A + +open Negative {{...}} public using (fromNeg) + +{-# BUILTIN FROMNEG fromNeg #-} +{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-} diff --git a/data/Agda/Builtin/FromString.agda b/data/Agda/Builtin/FromString.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/FromString.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.FromString where + +open import Agda.Primitive +open import Agda.Builtin.String + +record IsString {a} (A : Set a) : Set (lsuc a) where + field + Constraint : String → Set a + fromString : (s : String) {{_ : Constraint s}} → A + +open IsString {{...}} public using (fromString) + +{-# BUILTIN FROMSTRING fromString #-} +{-# DISPLAY IsString.fromString _ s = fromString s #-} diff --git a/data/Agda/Builtin/IO.agda b/data/Agda/Builtin/IO.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/IO.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.IO where + +postulate IO : ∀ {a} → Set a → Set a +{-# POLARITY IO ++ ++ #-} +{-# BUILTIN IO IO #-} + +{-# FOREIGN GHC type AgdaIO a b = IO b #-} +{-# COMPILE GHC IO = type AgdaIO #-} diff --git a/data/Agda/Builtin/Int.agda b/data/Agda/Builtin/Int.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Int.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Int where + +open import Agda.Builtin.Nat +open import Agda.Builtin.String + +infix 8 pos -- Standard library uses this as +_ + +data Int : Set where + pos : (n : Nat) → Int + negsuc : (n : Nat) → Int + +{-# BUILTIN INTEGER Int #-} +{-# BUILTIN INTEGERPOS pos #-} +{-# BUILTIN INTEGERNEGSUC negsuc #-} + +primitive primShowInteger : Int → String diff --git a/data/Agda/Builtin/List.agda b/data/Agda/Builtin/List.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/List.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.List where + +infixr 5 _∷_ +data List {a} (A : Set a) : Set a where + [] : List A + _∷_ : (x : A) (xs : List A) → List A + +{-# BUILTIN LIST List #-} + +{-# COMPILE UHC List = data __LIST__ (__NIL__ | __CONS__) #-} +{-# COMPILE JS List = function(x,v) { + if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); } +} #-} +{-# COMPILE JS [] = Array() #-} +{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-} diff --git a/data/Agda/Builtin/Nat.agda b/data/Agda/Builtin/Nat.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Nat.agda @@ -0,0 +1,134 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism + --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Nat where + +open import Agda.Builtin.Bool + +data Nat : Set where + zero : Nat + suc : (n : Nat) → Nat + +{-# BUILTIN NATURAL Nat #-} + +infix 4 _==_ _<_ +infixl 6 _+_ _-_ +infixl 7 _*_ + +_+_ : Nat → Nat → Nat +zero + m = m +suc n + m = suc (n + m) + +{-# BUILTIN NATPLUS _+_ #-} + +_-_ : Nat → Nat → Nat +n - zero = n +zero - suc m = zero +suc n - suc m = n - m + +{-# BUILTIN NATMINUS _-_ #-} + +_*_ : Nat → Nat → Nat +zero * m = zero +suc n * m = m + n * m + +{-# BUILTIN NATTIMES _*_ #-} + +_==_ : Nat → Nat → Bool +zero == zero = true +suc n == suc m = n == m +_ == _ = false + +{-# BUILTIN NATEQUALS _==_ #-} + +_<_ : Nat → Nat → Bool +_ < zero = false +zero < suc _ = true +suc n < suc m = n < m + +{-# BUILTIN NATLESS _<_ #-} + +-- Helper function div-helper for Euclidean division. +--------------------------------------------------------------------------- +-- +-- div-helper computes n / 1+m via iteration on n. +-- +-- n div (suc m) = div-helper 0 m n m +-- +-- The state of the iterator has two accumulator variables: +-- +-- k: The quotient, returned once n=0. Initialized to 0. +-- +-- j: A counter, initialized to the divisor m, decreased on each iteration step. +-- Once it reaches 0, the quotient k is increased and j reset to m, +-- starting the next countdown. +-- +-- Under the precondition j ≤ m, the invariant is +-- +-- div-helper k m n j = k + (n + m - j) div (1 + m) + +div-helper : (k m n j : Nat) → Nat +div-helper k m zero j = k +div-helper k m (suc n) zero = div-helper (suc k) m n m +div-helper k m (suc n) (suc j) = div-helper k m n j + +{-# BUILTIN NATDIVSUCAUX div-helper #-} + +-- Proof of the invariant by induction on n. +-- +-- clause 1: div-helper k m 0 j +-- = k by definition +-- = k + (0 + m - j) div (1 + m) since m - j < 1 + m +-- +-- clause 2: div-helper k m (1 + n) 0 +-- = div-helper (1 + k) m n m by definition +-- = 1 + k + (n + m - m) div (1 + m) by induction hypothesis +-- = 1 + k + n div (1 + m) by simplification +-- = k + (n + (1 + m)) div (1 + m) by expansion +-- = k + (1 + n + m - 0) div (1 + m) by expansion +-- +-- clause 3: div-helper k m (1 + n) (1 + j) +-- = div-helper k m n j by definition +-- = k + (n + m - j) div (1 + m) by induction hypothesis +-- = k + ((1 + n) + m - (1 + j)) div (1 + m) by expansion +-- +-- Q.e.d. + +-- Helper function mod-helper for the remainder computation. +--------------------------------------------------------------------------- +-- +-- (Analogous to div-helper.) +-- +-- mod-helper computes n % 1+m via iteration on n. +-- +-- n mod (suc m) = mod-helper 0 m n m +-- +-- The invariant is: +-- +-- m = k + j ==> mod-helper k m n j = (n + k) mod (1 + m). + +mod-helper : (k m n j : Nat) → Nat +mod-helper k m zero j = k +mod-helper k m (suc n) zero = mod-helper 0 m n m +mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j + +{-# BUILTIN NATMODSUCAUX mod-helper #-} + +-- Proof of the invariant by induction on n. +-- +-- clause 1: mod-helper k m 0 j +-- = k by definition +-- = (0 + k) mod (1 + m) since m = k + j, thus k < m +-- +-- clause 2: mod-helper k m (1 + n) 0 +-- = mod-helper 0 m n m by definition +-- = (n + 0) mod (1 + m) by induction hypothesis +-- = (n + (1 + m)) mod (1 + m) by expansion +-- = (1 + n) + k) mod (1 + m) since k = m (as l = 0) +-- +-- clause 3: mod-helper k m (1 + n) (1 + j) +-- = mod-helper (1 + k) m n j by definition +-- = (n + (1 + k)) mod (1 + m) by induction hypothesis +-- = ((1 + n) + k) mod (1 + m) by commutativity +-- +-- Q.e.d. diff --git a/data/Agda/Builtin/Reflection.agda b/data/Agda/Builtin/Reflection.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Reflection.agda @@ -0,0 +1,314 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Reflection where + +open import Agda.Builtin.Unit +open import Agda.Builtin.Bool +open import Agda.Builtin.Nat +open import Agda.Builtin.Word +open import Agda.Builtin.List +open import Agda.Builtin.String +open import Agda.Builtin.Char +open import Agda.Builtin.Float +open import Agda.Builtin.Int +open import Agda.Builtin.Sigma + +-- Names -- + +postulate Name : Set +{-# BUILTIN QNAME Name #-} + +primitive + primQNameEquality : Name → Name → Bool + primQNameLess : Name → Name → Bool + primShowQName : Name → String + +-- Fixity -- + +data Associativity : Set where + left-assoc : Associativity + right-assoc : Associativity + non-assoc : Associativity + +data Precedence : Set where + related : Float → Precedence + unrelated : Precedence + +data Fixity : Set where + fixity : Associativity → Precedence → Fixity + +{-# BUILTIN ASSOC Associativity #-} +{-# BUILTIN ASSOCLEFT left-assoc #-} +{-# BUILTIN ASSOCRIGHT right-assoc #-} +{-# BUILTIN ASSOCNON non-assoc #-} + +{-# BUILTIN PRECEDENCE Precedence #-} +{-# BUILTIN PRECRELATED related #-} +{-# BUILTIN PRECUNRELATED unrelated #-} + +{-# BUILTIN FIXITY Fixity #-} +{-# BUILTIN FIXITYFIXITY fixity #-} + +{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-} +{-# COMPILE GHC Precedence = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-} +{-# COMPILE GHC Fixity = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-} + +{-# COMPILE JS Associativity = function (x,v) { return v[x](); } #-} +{-# COMPILE JS left-assoc = "left-assoc" #-} +{-# COMPILE JS right-assoc = "right-assoc" #-} +{-# COMPILE JS non-assoc = "non-assoc" #-} + +{-# COMPILE JS Precedence = + function (x,v) { + if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-} +{-# COMPILE JS related = function(x) { return x; } #-} +{-# COMPILE JS unrelated = "unrelated" #-} + +{-# COMPILE JS Fixity = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-} +{-# COMPILE JS fixity = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-} + +primitive + primQNameFixity : Name → Fixity + primQNameToWord64s : Name → Σ Word64 (λ _ → Word64) + +-- Metavariables -- + +postulate Meta : Set +{-# BUILTIN AGDAMETA Meta #-} + +primitive + primMetaEquality : Meta → Meta → Bool + primMetaLess : Meta → Meta → Bool + primShowMeta : Meta → String + primMetaToNat : Meta → Nat + +-- Arguments -- + +-- Arguments can be (visible), {hidden}, or {{instance}}. +data Visibility : Set where + visible hidden instance′ : Visibility + +{-# BUILTIN HIDING Visibility #-} +{-# BUILTIN VISIBLE visible #-} +{-# BUILTIN HIDDEN hidden #-} +{-# BUILTIN INSTANCE instance′ #-} + +-- Arguments can be relevant or irrelevant. +data Relevance : Set where + relevant irrelevant : Relevance + +{-# BUILTIN RELEVANCE Relevance #-} +{-# BUILTIN RELEVANT relevant #-} +{-# BUILTIN IRRELEVANT irrelevant #-} + +data ArgInfo : Set where + arg-info : (v : Visibility) (r : Relevance) → ArgInfo + +data Arg {a} (A : Set a) : Set a where + arg : (i : ArgInfo) (x : A) → Arg A + +{-# BUILTIN ARGINFO ArgInfo #-} +{-# BUILTIN ARGARGINFO arg-info #-} +{-# BUILTIN ARG Arg #-} +{-# BUILTIN ARGARG arg #-} + +-- Name abstraction -- + +data Abs {a} (A : Set a) : Set a where + abs : (s : String) (x : A) → Abs A + +{-# BUILTIN ABS Abs #-} +{-# BUILTIN ABSABS abs #-} + +-- Literals -- + +data Literal : Set where + nat : (n : Nat) → Literal + word64 : (n : Word64) → Literal + float : (x : Float) → Literal + char : (c : Char) → Literal + string : (s : String) → Literal + name : (x : Name) → Literal + meta : (x : Meta) → Literal + +{-# BUILTIN AGDALITERAL Literal #-} +{-# BUILTIN AGDALITNAT nat #-} +{-# BUILTIN AGDALITWORD64 word64 #-} +{-# BUILTIN AGDALITFLOAT float #-} +{-# BUILTIN AGDALITCHAR char #-} +{-# BUILTIN AGDALITSTRING string #-} +{-# BUILTIN AGDALITQNAME name #-} +{-# BUILTIN AGDALITMETA meta #-} + +-- Patterns -- + +data Pattern : Set where + con : (c : Name) (ps : List (Arg Pattern)) → Pattern + dot : Pattern + var : (s : String) → Pattern + lit : (l : Literal) → Pattern + proj : (f : Name) → Pattern + absurd : Pattern + +{-# BUILTIN AGDAPATTERN Pattern #-} +{-# BUILTIN AGDAPATCON con #-} +{-# BUILTIN AGDAPATDOT dot #-} +{-# BUILTIN AGDAPATVAR var #-} +{-# BUILTIN AGDAPATLIT lit #-} +{-# BUILTIN AGDAPATPROJ proj #-} +{-# BUILTIN AGDAPATABSURD absurd #-} + +-- Terms -- + +data Sort : Set +data Clause : Set +data Term : Set +Type = Term + +data Term where + var : (x : Nat) (args : List (Arg Term)) → Term + con : (c : Name) (args : List (Arg Term)) → Term + def : (f : Name) (args : List (Arg Term)) → Term + lam : (v : Visibility) (t : Abs Term) → Term + pat-lam : (cs : List Clause) (args : List (Arg Term)) → Term + pi : (a : Arg Type) (b : Abs Type) → Term + agda-sort : (s : Sort) → Term + lit : (l : Literal) → Term + meta : (x : Meta) → List (Arg Term) → Term + unknown : Term + +data Sort where + set : (t : Term) → Sort + lit : (n : Nat) → Sort + unknown : Sort + +data Clause where + clause : (ps : List (Arg Pattern)) (t : Term) → Clause + absurd-clause : (ps : List (Arg Pattern)) → Clause + +{-# BUILTIN AGDASORT Sort #-} +{-# BUILTIN AGDATERM Term #-} +{-# BUILTIN AGDACLAUSE Clause #-} + +{-# BUILTIN AGDATERMVAR var #-} +{-# BUILTIN AGDATERMCON con #-} +{-# BUILTIN AGDATERMDEF def #-} +{-# BUILTIN AGDATERMMETA meta #-} +{-# BUILTIN AGDATERMLAM lam #-} +{-# BUILTIN AGDATERMEXTLAM pat-lam #-} +{-# BUILTIN AGDATERMPI pi #-} +{-# BUILTIN AGDATERMSORT agda-sort #-} +{-# BUILTIN AGDATERMLIT lit #-} +{-# BUILTIN AGDATERMUNSUPPORTED unknown #-} + +{-# BUILTIN AGDASORTSET set #-} +{-# BUILTIN AGDASORTLIT lit #-} +{-# BUILTIN AGDASORTUNSUPPORTED unknown #-} + +{-# BUILTIN AGDACLAUSECLAUSE clause #-} +{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-} + +-- Definitions -- + +data Definition : Set where + function : (cs : List Clause) → Definition + data-type : (pars : Nat) (cs : List Name) → Definition + record-type : (c : Name) (fs : List (Arg Name)) → Definition + data-cons : (d : Name) → Definition + axiom : Definition + prim-fun : Definition + +{-# BUILTIN AGDADEFINITION Definition #-} +{-# BUILTIN AGDADEFINITIONFUNDEF function #-} +{-# BUILTIN AGDADEFINITIONDATADEF data-type #-} +{-# BUILTIN AGDADEFINITIONRECORDDEF record-type #-} +{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons #-} +{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-} +{-# BUILTIN AGDADEFINITIONPRIMITIVE prim-fun #-} + +-- Errors -- + +data ErrorPart : Set where + strErr : String → ErrorPart + termErr : Term → ErrorPart + nameErr : Name → ErrorPart + +{-# BUILTIN AGDAERRORPART ErrorPart #-} +{-# BUILTIN AGDAERRORPARTSTRING strErr #-} +{-# BUILTIN AGDAERRORPARTTERM termErr #-} +{-# BUILTIN AGDAERRORPARTNAME nameErr #-} + +-- TC monad -- + +postulate + TC : ∀ {a} → Set a → Set a + returnTC : ∀ {a} {A : Set a} → A → TC A + bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B + unify : Term → Term → TC ⊤ + typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A + inferType : Term → TC Type + checkType : Term → Type → TC Term + normalise : Term → TC Term + reduce : Term → TC Term + catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A + quoteTC : ∀ {a} {A : Set a} → A → TC Term + unquoteTC : ∀ {a} {A : Set a} → Term → TC A + getContext : TC (List (Arg Type)) + extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A + inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A + freshName : String → TC Name + declareDef : Arg Name → Type → TC ⊤ + declarePostulate : Arg Name → Type → TC ⊤ + defineFun : Name → List Clause → TC ⊤ + getType : Name → TC Type + getDefinition : Name → TC Definition + blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A + commitTC : TC ⊤ + isMacro : Name → TC Bool + + -- If the argument is 'true' makes the following primitives also normalise + -- their results: inferType, checkType, quoteTC, getType, and getContext + withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A + + -- Prints the third argument if the corresponding verbosity level is turned + -- on (with the -v flag to Agda). + debugPrint : String → Nat → List ErrorPart → TC ⊤ + + -- Fail if the given computation gives rise to new, unsolved + -- "blocking" constraints. + noConstraints : ∀ {a} {A : Set a} → TC A → TC A + + -- Run the given TC action and return the first component. Resets to + -- the old TC state if the second component is 'false', or keep the + -- new TC state if it is 'true'. + runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A + +{-# BUILTIN AGDATCM TC #-} +{-# BUILTIN AGDATCMRETURN returnTC #-} +{-# BUILTIN AGDATCMBIND bindTC #-} +{-# BUILTIN AGDATCMUNIFY unify #-} +{-# BUILTIN AGDATCMTYPEERROR typeError #-} +{-# BUILTIN AGDATCMINFERTYPE inferType #-} +{-# BUILTIN AGDATCMCHECKTYPE checkType #-} +{-# BUILTIN AGDATCMNORMALISE normalise #-} +{-# BUILTIN AGDATCMREDUCE reduce #-} +{-# BUILTIN AGDATCMCATCHERROR catchTC #-} +{-# BUILTIN AGDATCMQUOTETERM quoteTC #-} +{-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-} +{-# BUILTIN AGDATCMGETCONTEXT getContext #-} +{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-} +{-# BUILTIN AGDATCMINCONTEXT inContext #-} +{-# BUILTIN AGDATCMFRESHNAME freshName #-} +{-# BUILTIN AGDATCMDECLAREDEF declareDef #-} +{-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-} +{-# BUILTIN AGDATCMDEFINEFUN defineFun #-} +{-# BUILTIN AGDATCMGETTYPE getType #-} +{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-} +{-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-} +{-# BUILTIN AGDATCMCOMMIT commitTC #-} +{-# BUILTIN AGDATCMISMACRO isMacro #-} +{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-} +{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-} +{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-} +{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-} diff --git a/data/Agda/Builtin/Reflection/Properties.agda b/data/Agda/Builtin/Reflection/Properties.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Reflection/Properties.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Reflection.Properties where + +open import Agda.Builtin.Reflection +open import Agda.Builtin.Equality + +primitive + + primMetaToNatInjective : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b + primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b diff --git a/data/Agda/Builtin/Sigma.agda b/data/Agda/Builtin/Sigma.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Sigma.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Sigma where + +open import Agda.Primitive + +record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where + constructor _,_ + field + fst : A + snd : B fst + +open Σ public + +infixr 4 _,_ + +{-# BUILTIN SIGMA Σ #-} diff --git a/data/Agda/Builtin/Size.agda b/data/Agda/Builtin/Size.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Size.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism --sized-types + --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Size where + +{-# BUILTIN SIZEUNIV SizeU #-} +{-# BUILTIN SIZE Size #-} +{-# BUILTIN SIZELT Size<_ #-} +{-# BUILTIN SIZESUC ↑_ #-} +{-# BUILTIN SIZEINF ∞ #-} +{-# BUILTIN SIZEMAX _⊔ˢ_ #-} + +{-# FOREIGN GHC + type SizeLT i = () + #-} + +{-# COMPILE GHC Size = type () #-} +{-# COMPILE GHC Size<_ = type SizeLT #-} +{-# COMPILE GHC ↑_ = \_ -> () #-} +{-# COMPILE GHC ∞ = () #-} +{-# COMPILE GHC _⊔ˢ_ = \_ _ -> () #-} diff --git a/data/Agda/Builtin/Strict.agda b/data/Agda/Builtin/Strict.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Strict.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Strict where + +open import Agda.Builtin.Equality + +primitive + primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x + primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x diff --git a/data/Agda/Builtin/String.agda b/data/Agda/Builtin/String.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/String.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.String where + +open import Agda.Builtin.Bool +open import Agda.Builtin.List +open import Agda.Builtin.Char +open import Agda.Builtin.Nat using (Nat) + +postulate String : Set +{-# BUILTIN STRING String #-} + +primitive + primStringToList : String → List Char + primStringFromList : List Char → String + primStringAppend : String → String → String + primStringEquality : String → String → Bool + primShowChar : Char → String + primShowString : String → String + primShowNat : Nat → String + +{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-} +{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-} +{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-} +{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-} +{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-} +{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-} diff --git a/data/Agda/Builtin/String/Properties.agda b/data/Agda/Builtin/String/Properties.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/String/Properties.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.String.Properties where + +open import Agda.Builtin.String +open import Agda.Builtin.Equality + +primitive + + primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b diff --git a/data/Agda/Builtin/TrustMe.agda b/data/Agda/Builtin/TrustMe.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/TrustMe.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.TrustMe where + +open import Agda.Builtin.Equality +open import Agda.Builtin.Equality.Erase + +private + postulate + unsafePrimTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y + +primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y +primTrustMe = primEraseEquality unsafePrimTrustMe + +{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-} diff --git a/data/Agda/Builtin/Unit.agda b/data/Agda/Builtin/Unit.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Unit.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism + --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Unit where + +record ⊤ : Set where + instance constructor tt + +{-# BUILTIN UNIT ⊤ #-} +{-# COMPILE GHC ⊤ = data () (()) #-} diff --git a/data/Agda/Builtin/Word.agda b/data/Agda/Builtin/Word.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Word.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --without-K --safe --no-universe-polymorphism + --no-sized-types --no-guardedness --no-subtyping #-} + +module Agda.Builtin.Word where + +open import Agda.Builtin.Nat + +postulate Word64 : Set +{-# BUILTIN WORD64 Word64 #-} + +primitive + primWord64ToNat : Word64 → Nat + primWord64FromNat : Nat → Word64 diff --git a/data/Agda/Builtin/Word/Properties.agda b/data/Agda/Builtin/Word/Properties.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Builtin/Word/Properties.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness + --no-subtyping #-} + +module Agda.Builtin.Word.Properties where + +open import Agda.Builtin.Word +open import Agda.Builtin.Equality + +primitive + + primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b diff --git a/data/Agda/Primitive.agda b/data/Agda/Primitive.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Primitive.agda @@ -0,0 +1,33 @@ +-- The Agda primitives (preloaded). + +{-# OPTIONS --without-K --no-subtyping #-} + +module Agda.Primitive where + +------------------------------------------------------------------------ +-- Universe levels +------------------------------------------------------------------------ + +infixl 6 _⊔_ + +-- Level is the first thing we need to define. +-- The other postulates can only be checked if built-in Level is known. + +postulate + Level : Set + +-- MAlonzo compiles Level to (). This should be safe, because it is +-- not possible to pattern match on levels. + +{-# BUILTIN LEVEL Level #-} + +postulate + lzero : Level + lsuc : (ℓ : Level) → Level + _⊔_ : (ℓ₁ ℓ₂ : Level) → Level + +{-# BUILTIN LEVELZERO lzero #-} +{-# BUILTIN LEVELSUC lsuc #-} +{-# BUILTIN LEVELMAX _⊔_ #-} + +{-# BUILTIN SETOMEGA Setω #-} diff --git a/data/Agda/Primitive/Cubical.agda b/data/Agda/Primitive/Cubical.agda new file mode 100644 --- /dev/null +++ b/data/Agda/Primitive/Cubical.agda @@ -0,0 +1,53 @@ +{-# OPTIONS --cubical --no-subtyping #-} + +module Agda.Primitive.Cubical where + +{-# BUILTIN INTERVAL I #-} -- I : Setω + +{-# BUILTIN IZERO i0 #-} +{-# BUILTIN IONE i1 #-} + +infix 30 primINeg +infixr 20 primIMin primIMax + +primitive + primIMin : I → I → I + primIMax : I → I → I + primINeg : I → I + +{-# BUILTIN ISONE IsOne #-} -- IsOne : I → Setω + +postulate + itIsOne : IsOne i1 + IsOne1 : ∀ i j → IsOne i → IsOne (primIMax i j) + IsOne2 : ∀ i j → IsOne j → IsOne (primIMax i j) + +{-# BUILTIN ITISONE itIsOne #-} +{-# BUILTIN ISONE1 IsOne1 #-} +{-# BUILTIN ISONE2 IsOne2 #-} + +-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ +-- Partial i A = IsOne i → A + +{-# BUILTIN PARTIAL Partial #-} +{-# BUILTIN PARTIALP PartialP #-} + +postulate + isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A + +{-# BUILTIN ISONEEMPTY isOneEmpty #-} + +primitive + primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)} + → (u : PartialP i (λ z → A (IsOne1 i j z))) + → (v : PartialP j (λ z → A (IsOne2 i j z))) + → PartialP (primIMax i j) A + + -- Computes in terms of primHComp and primTransp + primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1 + +syntax primPOr p q u t = [ p ↦ u , q ↦ t ] + +primitive + primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1 + primHComp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A diff --git a/data/test/declaration/Abstract.agda b/data/test/declaration/Abstract.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Abstract.agda @@ -0,0 +1,32 @@ +module Abstract where + +abstract + + f + : {A : Set} + → A + → A + f x + = x + + g + : {A : Set} + → A + → A + g x + = x + + h + : {A : Set} + → A + → A + h x + = f x + + _ + : {A : Set} + → A + → A + _ + = λ x → x + diff --git a/data/test/declaration/Data.agda b/data/test/declaration/Data.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Data.agda @@ -0,0 +1,12 @@ +module Data where + +data D + (A : Set) + : Set + +data D A + where + + c + : D A + diff --git a/data/test/declaration/FunClause.agda b/data/test/declaration/FunClause.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/FunClause.agda @@ -0,0 +1,35 @@ +module FunClause where + +f + : {A : Set} + → A + → A +f x + = y + where + y = x + z = x + +data List + (A : Set) + : Set + where + + nil + : List A + + cons + : A + → List A + → List A + +snoc + : {A : Set} + → List A + → A + → List A +snoc nil y + = cons y nil +snoc (cons x xs) y + = cons x (snoc xs y) + diff --git a/data/test/declaration/Import.agda b/data/test/declaration/Import.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Import.agda @@ -0,0 +1,11 @@ +module Import where + +import Agda.Builtin.Unit + using (⊤; tt) +import Agda.Builtin.Bool + +A + : Set +A + = Agda.Builtin.Unit.⊤ + diff --git a/data/test/declaration/Module.agda b/data/test/declaration/Module.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Module.agda @@ -0,0 +1,25 @@ +module Module where + +record R + : Set + where + +module M where + +module N where + +module O where + + postulate + + A + : Set + +x + : R +x + = record {M} + +module P + = N + diff --git a/data/test/declaration/ModuleMacro.agda b/data/test/declaration/ModuleMacro.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/ModuleMacro.agda @@ -0,0 +1,57 @@ +module ModuleMacro where + +record ⊤ + : Set + where + +module M where + +module N where + + postulate + + A + : Set + + B + : Set + +module O + = M + +module P + = M + +module Q + = P + +module R + (x : ⊤) + = N + using (A) + +module S + = N + renaming + ( A + to A' + ; B + to B' + ) + +y + : ⊤ +y + = record {O} + +C + : ⊤ + → Set +C + = R.A + +D + : Set +D + = S.B' + diff --git a/data/test/declaration/Mutual1.agda b/data/test/declaration/Mutual1.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Mutual1.agda @@ -0,0 +1,41 @@ +module Mutual1 where + +data Bool + : Set + where + + false + : Bool + + true + : Bool + +data ℕ + : Set + where + + zero + : ℕ + + suc + : ℕ + → ℕ + +is-even + : ℕ + → Bool + +is-odd + : ℕ + → Bool + +is-even zero + = true +is-even (suc n) + = is-odd n + +is-odd zero + = false +is-odd (suc n) + = is-even n + diff --git a/data/test/declaration/Mutual2.agda b/data/test/declaration/Mutual2.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Mutual2.agda @@ -0,0 +1,47 @@ +module Mutual2 where + +data Bool + : Set + where + + false + : Bool + + true + : Bool + +data ℕ + : Set + where + + zero + : ℕ + + suc + : ℕ + → ℕ + +is-even + : ℕ + → Bool + +is-odd + : ℕ + → Bool + +is-even zero + = true +is-even (suc n) + = is-odd n + +is-odd zero + = false +is-odd (suc n) + = is-even n + +is-even' + : ℕ + → Bool +is-even' + = is-even + diff --git a/data/test/declaration/Open.agda b/data/test/declaration/Open.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Open.agda @@ -0,0 +1,59 @@ +module Open where + +module M where + + data ⊤ + : Set + where + + tt + : ⊤ + +module N where + + open M + + v + : ⊤ + v + = tt + +open M +open N + +module O where + + w + : ⊤ + w + = tt + + x + : ⊤ + x + = tt + +module P where + + open O + using (w) + renaming (x to x') + + y + : ⊤ + y + = w + +open P + +module Q where + + open O + hiding (w) + renaming (x to x'') + + z + : ⊤ + z + = x'' + diff --git a/data/test/declaration/PatternSyn.agda b/data/test/declaration/PatternSyn.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/PatternSyn.agda @@ -0,0 +1,41 @@ +module PatternSyn where + +data ⊤ + : Set + where + + tt + : ⊤ + +data D + (A : Set) + : Set + where + + d + : A + → A + → D A + +pattern p + = tt + +pattern q + = tt + +pattern _,_ x y + = d x y + +f + : ⊤ + → ⊤ +f p + = tt + +g + : {A : Set} + → D A + → A +g (x , _) + = x + diff --git a/data/test/declaration/Postulate.agda b/data/test/declaration/Postulate.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Postulate.agda @@ -0,0 +1,21 @@ +module Postulate where + +postulate + + f + : {A : Set} + → A + → A + + g + : {A : Set} + → A + → A + +h + : {A : Set} + → A + → A +h x + = f x + diff --git a/data/test/declaration/Private.agda b/data/test/declaration/Private.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Private.agda @@ -0,0 +1,32 @@ +module Private where + +private + + f + : {A : Set} + → A + → A + f x + = x + + g + : {A : Set} + → A + → A + g x + = x + + h + : {A : Set} + → A + → A + h x + = f x + + _ + : {A : Set} + → A + → A + _ + = λ x → x + diff --git a/data/test/declaration/Record.agda b/data/test/declaration/Record.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Record.agda @@ -0,0 +1,36 @@ +module Record where + +module M where + + record A + : Set + where + + constructor + + a + +open M + +record B + : Set + where + +record C + : Set + where + + constructor + + c + +x + : A +x + = a + +y + : C +y + = record {} + diff --git a/data/test/declaration/Syntax.agda b/data/test/declaration/Syntax.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/Syntax.agda @@ -0,0 +1,49 @@ +module Syntax where + +data S + (A₁ : Set) + (A₂ : A₁ → Set) + : Set + where + + _,_ + : (x₁ : A₁) + → A₂ x₁ + → S A₁ A₂ + +syntax S A₁ (λ x → A₂) + = x ∈ A₁ × A₂ + +module M where + + data S' + (A₁ : Set) + (A₂ : A₁ → Set) + : Set + where + + _,'_ + : (x₁ : A₁) + → A₂ x₁ + → S' A₁ A₂ + + syntax S' A₁ (λ x → A₂) + = x ∈' A₁ ×' A₂ + +open M + using (S') + +postulate + + p1 + : {A₁ : Set} + → {A₂ : A₁ → Set} + → x₁ ∈ A₁ × A₂ x₁ + → A₁ + + p1' + : {A₁ : Set} + → {A₂ : A₁ → Set} + → x₁ ∈' A₁ ×' A₂ x₁ + → A₁ + diff --git a/data/test/declaration/TypeSig.agda b/data/test/declaration/TypeSig.agda new file mode 100644 --- /dev/null +++ b/data/test/declaration/TypeSig.agda @@ -0,0 +1,30 @@ +module Definition where + +f + : {A : Set} + → A + → A +f x + = x + +g + : {A : Set} + → A + → A +g x + = x + +h + : {A : Set} + → A + → A +h x + = f x + +_ + : {A : Set} + → A + → A +_ + = λ x → x + diff --git a/data/test/example/Test.agda b/data/test/example/Test.agda new file mode 100644 --- /dev/null +++ b/data/test/example/Test.agda @@ -0,0 +1,14 @@ +module Test where + +open import Agda.Builtin.Bool + using (Bool; false; true) +open import Agda.Builtin.Unit + +_∧_ + : Bool + → Bool + → Bool +false ∧ x + = false +_ ∧ y + = y diff --git a/data/test/expression/DoBlock1.agda b/data/test/expression/DoBlock1.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/DoBlock1.agda @@ -0,0 +1,38 @@ +module DoBlock1 where + +data Id + (A : Set) + : Set + where + + id + : A + → Id A + +_>>=_ + : {A B : Set} + → Id A + → (A → Id B) + → Id B +id x >>= f + = f x + +_>>_ + : {A B : Set} + → Id A + → Id B + → Id B +_ >> y + = y + +f + : {A : Set} + → A + → Id A +f x + = do + y <- id x + z <- id x + id y + id y + diff --git a/data/test/expression/DoBlock2.agda b/data/test/expression/DoBlock2.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/DoBlock2.agda @@ -0,0 +1,36 @@ +module DoBlock2 where + +data Id + (A : Set) + : Set + where + + id + : A + → Id A + +_>>=_ + : {A B : Set} + → Id A + → (A → Id B) + → Id B +id x >>= f + = f x + +_>>_ + : {A B : Set} + → Id A + → Id B + → Id B +_ >> y + = y + +f + : {A : Set} + → A + → Id A +f x + = do + y <- id x + id y + diff --git a/data/test/expression/DoBlock3.agda b/data/test/expression/DoBlock3.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/DoBlock3.agda @@ -0,0 +1,36 @@ +module DoBlock3 where + +data Id + (A : Set) + : Set + where + + id + : A + → Id A + +_>>=_ + : {A B : Set} + → Id A + → (A → Id B) + → Id B +id x >>= f + = f x + +_>>_ + : {A B : Set} + → Id A + → Id B + → Id B +_ >> y + = y + +f + : {A : Set} + → A + → Id A +f x + = do + id x + id x + diff --git a/data/test/expression/DoBlock4.agda b/data/test/expression/DoBlock4.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/DoBlock4.agda @@ -0,0 +1,35 @@ +module DoBlock4 where + +data Id + (A : Set) + : Set + where + + id + : A + → Id A + +_>>=_ + : {A B : Set} + → Id A + → (A → Id B) + → Id B +id x >>= f + = f x + +_>>_ + : {A B : Set} + → Id A + → Id B + → Id B +_ >> y + = y + +f + : {A : Set} + → A + → Id A +f x + = do + id x + diff --git a/data/test/expression/ExtendedLam.agda b/data/test/expression/ExtendedLam.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/ExtendedLam.agda @@ -0,0 +1,23 @@ +module ExtendedLam where + +data Bool + : Set + where + + false + : Bool + true + : Bool + +f + : Bool + → Bool + → Bool +f + = λ + { x false + → true + ; y true + → y + } + diff --git a/data/test/expression/Lam.agda b/data/test/expression/Lam.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/Lam.agda @@ -0,0 +1,16 @@ +module Lam where + +f + : {A : Set} + → A + → A +f x + = (λ y z → z) x x + +g + : {A : Set} + → A + → A +g {A = A} x + = (λ (y' : A) (z : A) → z) x x + diff --git a/data/test/expression/Let.agda b/data/test/expression/Let.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/Let.agda @@ -0,0 +1,12 @@ +module Let where + +f + : {A : Set} + → A + → A +f x + = let + y = x + z = x + in y + diff --git a/data/test/expression/Pi.agda b/data/test/expression/Pi.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/Pi.agda @@ -0,0 +1,14 @@ +module Pi where + +open import Agda.Builtin.Equality + using (_≡_; refl) + +f + : {A : Set} + → {x y : A} + → (z w : A) + → x ≡ z + → z ≡ x +f _ _ refl + = refl + diff --git a/data/test/expression/WithApp.agda b/data/test/expression/WithApp.agda new file mode 100644 --- /dev/null +++ b/data/test/expression/WithApp.agda @@ -0,0 +1,23 @@ +module WithApp where + +f + : {A : Set} + → A + → A +f x + with x +... | y + = y + +g + : {A : Set} + → A + → A + → A +g x y + with x +... | _ + with y +... | _ + = x + diff --git a/data/test/pattern/AsP.agda b/data/test/pattern/AsP.agda new file mode 100644 --- /dev/null +++ b/data/test/pattern/AsP.agda @@ -0,0 +1,20 @@ +module AsP where + +f + : {A : Set} + → A + → A + → A +f x@y z@w + = x + +g + : {A : Set} + → A + → A + → A +g x@y z'@w' + with y +... | _ + = x + diff --git a/data/test/pattern/IdentP.agda b/data/test/pattern/IdentP.agda new file mode 100644 --- /dev/null +++ b/data/test/pattern/IdentP.agda @@ -0,0 +1,28 @@ +module IdentP where + +data Bool + : Set + where + + false + : Bool + + true + : Bool + +f + : {A : Set} + → A + → A + → A +f x y + = x + +g + : Bool + → Bool +g false + = true +g true + = true + diff --git a/data/test/pattern/OpAppP.agda b/data/test/pattern/OpAppP.agda new file mode 100644 --- /dev/null +++ b/data/test/pattern/OpAppP.agda @@ -0,0 +1,21 @@ +module OpAppP where + +data Bool + : Set + where + + false + : Bool + + true + : Bool + +_&&_ + : Bool + → Bool + → Bool +false && _ + = false +true && b + = b + diff --git a/src/Agda/Unused.hs b/src/Agda/Unused.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused.hs @@ -0,0 +1,32 @@ +{- | +Module: Agda.Unused + +Definitions and interface for the 'Unused' type, which represents a collection +of unused Agda code structures. +-} +module Agda.Unused + ( Unused(..) + , UnusedItems(..) + ) where + +import Agda.Unused.Types.Range + (Range, RangeInfo) + +-- ## Types + +-- | A collection of unused items and files. +data Unused + = Unused + { unusedItems + :: UnusedItems + , unusedPaths + :: [FilePath] + } deriving Show + +-- | A collection of unused items. +newtype UnusedItems + = UnusedItems + { unusedItemsList + :: [(Range, RangeInfo)] + } deriving Show + diff --git a/src/Agda/Unused/Check.hs b/src/Agda/Unused/Check.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Check.hs @@ -0,0 +1,1901 @@ +{- | +Module: Agda.Unused + +Check an Agda project for unused code. +-} +module Agda.Unused.Check + ( checkUnused + , checkUnusedLocal + ) where + +import Agda.Unused + (Unused(..), UnusedItems(..)) +import Agda.Unused.Monad.Error + (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..), + liftLookup) +import Agda.Unused.Monad.Reader + (Environment(..), askLocal, askRoot, askSkip, localSkip) +import Agda.Unused.Monad.State + (ModuleState(..), State, modifyDelete, modifyInsert, stateBlock, + stateCheck, stateEmpty, stateItems, stateLookup, stateModules) +import Agda.Unused.Types.Access + (Access(..), fromAccess) +import Agda.Unused.Types.Context + (AccessContext, AccessModule(..), Context, LookupError(..), + accessContextDefine, accessContextImport, accessContextItem, + accessContextLookup, accessContextLookupDefining, accessContextLookupModule, + accessContextLookupSpecial, accessContextMatch, accessContextModule, + accessContextModule', accessContextUnion, contextDelete, + contextDeleteModule, contextItem, contextLookup, contextLookupItem, + contextLookupModule, contextModule, contextRanges, fromContext, item, + itemConstructor, itemPattern, moduleRanges, toContext) +import qualified Agda.Unused.Types.Context + as C +import Agda.Unused.Types.Name + (Name(..), QName(..), isBuiltin, fromAsName, fromName, fromNameRange, + fromQName, fromQNameRange, nameIds, pathQName, qNamePath) +import Agda.Unused.Types.Range + (Range'(..), RangeInfo(..), RangeType(..)) +import Agda.Unused.Types.Root + (Root(..), Roots(..)) +import Agda.Unused.Utils + (liftMaybe, mapLeft) + +import Agda.Syntax.Common + (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..), + Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..), Using'(..), + namedThing, unArg, whThing) +import qualified Agda.Syntax.Common + as Common +import Agda.Syntax.Concrete + (Binder, Binder'(..), BoundName(..), Declaration, DoStmt(..), Expr(..), + FieldAssignment, FieldAssignment'(..), ImportDirective, ImportedName, + LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module, + ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..), + RecordAssignment, Renaming, RewriteEqn, RHS, RHS'(..), TypedBinding, + TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA) +import Agda.Syntax.Concrete.Definitions + (Clause(..), NiceDeclaration(..), niceDeclarations, runNice) +import Agda.Syntax.Concrete.Fixity + (DoWarn(..), Fixities, fixitiesAndPolarities) +import Agda.Syntax.Concrete.Name + (NameInScope(..), NamePart(..)) +import qualified Agda.Syntax.Concrete.Name + as N +import Agda.Syntax.Parser + (moduleParser, parseFile, runPMIO) +import Agda.Syntax.Position + (Range, getRange) +import Agda.Utils.FileName + (AbsolutePath(..)) +import Control.Monad + (foldM, void) +import Control.Monad.Except + (MonadError, liftEither, runExceptT, throwError) +import Control.Monad.IO.Class + (MonadIO, liftIO) +import Control.Monad.Reader + (MonadReader, ReaderT, runReaderT) +import Control.Monad.State + (MonadState, StateT, gets, modify, runStateT) +import Data.Bool + (bool) +import qualified Data.Map.Strict + as Map +import Data.Maybe + (catMaybes) +import qualified Data.Text + as T +import System.Directory + (doesDirectoryExist, doesFileExist, listDirectory) +import System.FilePath + (()) + +import Paths_agda_unused + (getDataFileName) + +-- ## Context + +-- Do nothing if `askSkip` returns true. +contextInsertRange + :: MonadReader Environment m + => Name + -> Range + -> Context + -> m Context +contextInsertRange n r c + = askSkip >>= pure . bool (C.contextInsertRange n r c) c + +-- Do nothing if `askSkip` returns true. +contextInsertRangeModule + :: MonadReader Environment m + => Name + -> Range + -> Context + -> m Context +contextInsertRangeModule n r c + = askSkip >>= pure . bool (C.contextInsertRangeModule n r c) c + +-- Do nothing if `askSkip` returns true. +contextInsertRangeAll + :: MonadReader Environment m + => Range + -> Context + -> m Context +contextInsertRangeAll r c + = askSkip >>= pure . bool (C.contextInsertRangeAll r c) c + +-- Do nothing if `askSkip` returns true. +accessContextInsertRangeAll + :: MonadReader Environment m + => Range + -> AccessContext + -> m AccessContext +accessContextInsertRangeAll r c + = askSkip >>= pure . bool (C.accessContextInsertRangeAll r c) c + +-- Also insert range unless `askSkip` returns true. +contextRename + :: MonadReader Environment m + => Name + -> Name + -> Range + -> Context + -> m Context +contextRename n t r c + = contextInsertRange n r c + >>= pure . C.contextRename n t + +-- Also insert range unless `askSkip` returns true. +contextRenameModule + :: MonadReader Environment m + => Name + -> Name + -> Range + -> Context + -> m Context +contextRenameModule n t r c + = contextInsertRangeModule n r c + >>= pure . C.contextRenameModule n t + +-- ## Syntax + +syntax + :: Fixities + -> Name + -> Maybe Name +syntax fs (Name ps) + = Map.lookup (N.Name NoRange InScope ps) fs >>= fromFixity + +fromFixity + :: Fixity' + -> Maybe Name +fromFixity (Fixity' _ [] _) + = Nothing +fromFixity (Fixity' _ ps@(_ : _) _) + = Just (Name (fromGenPart <$> ps)) + +fromGenPart + :: GenPart + -> NamePart +fromGenPart (BindHole _ _) + = Hole +fromGenPart (NormalHole _ _) + = Hole +fromGenPart (WildHole _) + = Hole +fromGenPart (IdPart (Ranged _ s)) + = Id s + +-- ## Lists + +checkSequence + :: Monad m + => Monoid c + => (a -> b -> m c) + -> a + -> [b] + -> m c +checkSequence f x ys + = mconcat <$> sequence (f x <$> ys) + +checkSequence_ + :: Monad m + => (a -> b -> m ()) + -> a + -> [b] + -> m () +checkSequence_ f x ys + = void (sequence (f x <$> ys)) + +checkFold + :: Monad m + => Monoid a + => (a -> b -> m a) + -> a + -> [b] + -> m a +checkFold + = checkFoldWith mempty (<>) + +checkFoldUnion + :: Monad m + => (AccessContext -> b -> m AccessContext) + -> AccessContext + -> [b] + -> m AccessContext +checkFoldUnion + = checkFoldWith mempty accessContextUnion + +checkFoldWith + :: Monad m + => a + -> (a -> a -> a) + -> (a -> b -> m a) + -> a + -> [b] + -> m a +checkFoldWith x f g x' ys + = foldM (\x'' y -> f x'' <$> g (f x' x'') y) x ys + +-- ## Names + +checkName + :: MonadReader Environment m + => MonadState State m + => Bool + -- ^ Whether to treat names as pattern synonyms. + -> Fixities + -> Access + -> RangeType + -> Range + -> Name + -> m AccessContext +checkName _ _ _ _ NoRange _ + = pure mempty +checkName _ _ _ _ _ (Name [Hole]) + = pure mempty +checkName p fs a t r@(Range _ _) n + = modifyInsert r (RangeNamed t (QName n)) + >> pure (accessContextItem n a (bool item itemPattern p [r] (syntax fs n))) + +checkName' + :: MonadReader Environment m + => MonadState State m + => Bool + -- ^ Whether to treat names as pattern synonyms. + -> Fixities + -> Access + -> RangeType + -> N.Name + -> m AccessContext +checkName' p fs a t n + = maybe (pure mempty) (uncurry (checkName p fs a t)) (fromNameRange n) + +checkNames' + :: MonadReader Environment m + => MonadState State m + => Bool + -- ^ Whether to treat names as pattern synonyms. + -> Access + -> RangeType + -> [N.Name] + -> m AccessContext +checkNames' p a + = checkSequence (checkName' p mempty a) + +checkQNameP + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => AccessContext + -> Range + -> QName + -> m AccessContext +checkQNameP c r n + = checkQNamePWith (accessContextLookupSpecial n c) c r n + +checkQNamePWith + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => Maybe Bool + -> AccessContext + -> Range + -> QName + -> m AccessContext +checkQNamePWith Nothing _ r n + = checkQName Public RangeVariable r n +checkQNamePWith (Just False) _ _ _ + = pure mempty +checkQNamePWith (Just True) c r n + = touchQName c r n >> pure mempty + +checkQNameP' + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => AccessContext + -> N.QName + -> m AccessContext +checkQNameP' c n + = maybe (pure mempty) (uncurry (checkQNameP c)) (fromQNameRange n) + +checkQName + :: MonadReader Environment m + => MonadState State m + => Access + -> RangeType + -> Range + -> QName + -> m AccessContext +checkQName a t r (QName n) + = checkName False mempty a t r n +checkQName _ _ _ (Qual _ _) + = pure mempty + +checkModuleName + :: MonadReader Environment m + => MonadState State m + => Context + -> Access + -> Range + -> Name + -> m AccessContext +checkModuleName c a r n + = modifyInsert r (RangeNamed RangeModule (QName n)) + >> contextInsertRangeAll r c + >>= \c' -> pure (accessContextModule n (AccessModule a [r] c')) + +touchName + :: MonadReader Environment m + => MonadState State m + => AccessContext + -> Name + -> m () +touchName c n + = askSkip >>= touchNameWith (accessContextLookupDefining (QName n) c) + +touchNameWith + :: MonadReader Environment m + => MonadState State m + => Either LookupError (Bool, [Range]) + -> Bool + -> m () +touchNameWith (Right (False, rs)) False + = modifyDelete rs +touchNameWith _ _ + = pure () + +touchNames + :: MonadReader Environment m + => MonadState State m + => AccessContext + -> [Name] + -> m () +touchNames + = checkSequence_ touchName + +touchQName + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => AccessContext + -> Range + -> QName + -> m () +touchQName c r n + = askSkip >>= touchQNameWith r n (accessContextLookupDefining n c) + +touchQNameWith + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => Range + -> QName + -> Either LookupError (Bool, [Range]) + -> Bool + -> m () +touchQNameWith r n (Left LookupAmbiguous) False + = throwError (ErrorAmbiguous r n) +touchQNameWith _ _ rs b + = touchNameWith rs b + +touchQNameContext + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => Context + -> QName + -> QName + -> m () +touchQNameContext c m n + = maybe (throwError (ErrorRoot m n)) modifyDelete (contextLookup n c) + +touchQNamesContext + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => Context + -> QName + -> [QName] + -> m () +touchQNamesContext m p + = void . traverse (touchQNameContext m p) + +touchQName' + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => AccessContext + -> N.QName + -> m () +touchQName' c n + = maybe (pure ()) (uncurry (touchQName c)) (fromQNameRange n) + +-- ## Bindings + +checkBinder + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> Binder + -> m AccessContext +checkBinder b c (Binder p (BName n _ _)) + = bool localSkip id b (checkName' False mempty Public RangeVariable n) + >>= \c' -> checkPatternMay c p + >>= \c'' -> pure (c' <> c'') + +checkBinders + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> [Binder] + -> m AccessContext +checkBinders b + = checkSequence (checkBinder b) + +checkLamBinding + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> LamBinding + -> m AccessContext +checkLamBinding b c (DomainFree (Arg _ (Named _ b'))) + = checkBinder b c b' +checkLamBinding b c (DomainFull b') + = checkTypedBinding b c b' + +checkLamBindings + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> [LamBinding] + -> m AccessContext +checkLamBindings b + = checkFold (checkLamBinding b) + +checkTypedBinding + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> TypedBinding + -> m AccessContext +checkTypedBinding b c (TBind _ bs e) + = checkExpr c e >> checkBinders b c (namedThing . unArg <$> bs) +checkTypedBinding _ c (TLet _ ds) + = checkDeclarations c ds + +checkTypedBindings + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Bool + -- ^ Whether to check bound names. + -> AccessContext + -> [TypedBinding] + -> m AccessContext +checkTypedBindings b + = checkFold (checkTypedBinding b) + +-- ## Patterns + +checkPattern + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> Pattern + -> m AccessContext +checkPattern c (IdentP n) + = checkQNameP' c n +checkPattern _ (QuoteP _) + = pure mempty +checkPattern c (RawAppP _ ps) + = checkRawAppP c ps +checkPattern _ (OpAppP r _ _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpAppP) r) +checkPattern c (HiddenP _ (Named _ p)) + = checkPattern c p +checkPattern c (InstanceP _ (Named _ p)) + = checkPattern c p +checkPattern c (ParenP _ p) + = checkPattern c p +checkPattern _ (WildP _) + = pure mempty +checkPattern _ (AbsurdP _) + = pure mempty +checkPattern c (DotP _ e) + = checkExpr c e >> pure mempty +checkPattern _ (LitP _) + = pure mempty +checkPattern c (RecP _ as) + = checkPatterns c (_exprFieldA <$> as) +checkPattern c (EqualP _ es) + = checkExprPairs c es >> pure mempty +checkPattern _ (EllipsisP _) + = pure mempty +checkPattern c (WithP _ p) + = checkPattern c p + +checkPattern c (AppP p (Arg _ (Named _ p'))) + = (<>) + <$> checkPattern c p + <*> checkPattern c p' + +checkPattern c (AsP _ n p) + = (<>) + <$> checkName' False mempty Public RangeVariable n + <*> checkPattern c p + +checkPatternMay + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> Maybe Pattern + -> m AccessContext +checkPatternMay _ Nothing + = pure mempty +checkPatternMay c (Just p) + = checkPattern c p + +checkPatterns + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Pattern] + -> m AccessContext +checkPatterns + = checkSequence checkPattern + +checkRawAppP + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Pattern] + -> m AccessContext +checkRawAppP c ps + = pure (accessContextMatch (patternNames ps) c) + >>= \ns -> touchNames c ns + >> checkPatterns c (patternDelete ns ps) + +patternMatch + :: [Name] + -> Pattern + -> Bool +patternMatch ns p + = maybe False (flip elem (concat (nameIds <$> ns))) (patternName p) + +patternDelete + :: [Name] + -> [Pattern] + -> [Pattern] +patternDelete ns + = filter (not . patternMatch ns) + +patternName + :: Pattern + -> Maybe String +patternName (IdentP (N.QName (N.Name _ _ [Id n]))) + = Just n +patternName _ + = Nothing + +patternNames + :: [Pattern] + -> [String] +patternNames + = catMaybes + . fmap patternName + +-- ## Expressions + +checkExpr + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> Expr + -> m () +checkExpr c (Ident n) + = touchQName' c n +checkExpr _ (Lit _) + = pure () +checkExpr _ (QuestionMark _ _) + = pure () +checkExpr _ (Underscore _ _) + = pure () +checkExpr c (RawApp _ es) + = checkRawApp c es +checkExpr c (App _ e (Arg _ (Named _ e'))) + = checkExpr c e >> checkExpr c e' +checkExpr _ (OpApp r _ _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedOpApp) r) +checkExpr c (WithApp _ e es) + = checkExpr c e >> checkExprs c es +checkExpr c (HiddenArg _ (Named _ e)) + = checkExpr c e +checkExpr c (InstanceArg _ (Named _ e)) + = checkExpr c e +checkExpr c (Lam _ bs e) + = checkLamBindings True c bs >>= \c' -> checkExpr (c <> c') e +checkExpr _ (AbsurdLam _ _) + = pure () +checkExpr c (ExtendedLam _ ls) + = checkLamClauses_ c ls +checkExpr c (Fun _ (Arg _ e) e') + = checkExpr c e >> checkExpr c e' +checkExpr c (Pi bs e) + = checkTypedBindings True c bs >>= \c' -> checkExpr (c <> c') e +checkExpr _ (Set _) + = pure () +checkExpr _ (Prop _) + = pure () +checkExpr _ (SetN _ _) + = pure () +checkExpr _ (PropN _ _) + = pure () +checkExpr c (Rec _ rs) + = checkRecordAssignments c rs +checkExpr c (RecUpdate _ e fs) + = checkExpr c e >> checkFieldAssignments c fs +checkExpr c (Paren _ e) + = checkExpr c e +checkExpr c (IdiomBrackets _ es) + = checkExprs c es +checkExpr c (DoBlock _ ss) + = void (checkDoStmts c ss) +checkExpr _ (Absurd r) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedAbsurd) r) +checkExpr _ (As r _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedAs) r) +checkExpr c (Dot _ e) + = checkExpr c e +checkExpr c (DoubleDot _ e) + = checkExpr c e +checkExpr _ e@(ETel _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedETel) (getRange e)) +checkExpr _ (Quote _) + = pure () +checkExpr _ (QuoteTerm _) + = pure () +checkExpr c (Tactic _ e) + = checkExpr c e +checkExpr _ (Unquote _) + = pure () +checkExpr _ e@(DontCare _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedDontCare) (getRange e)) +checkExpr _ (Equal r _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedEqual) r) +checkExpr _ (Ellipsis r) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedEllipsis) r) +checkExpr c (Generalized e) + = checkExpr c e + +checkExpr c (Let _ ds e) + = checkDeclarations c ds + >>= \c' -> maybe (pure ()) (checkExpr (c <> c')) e + +checkExprs + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Expr] + -> m () +checkExprs + = checkSequence_ checkExpr + +checkExprPair + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> (Expr, Expr) + -> m () +checkExprPair c (e1, e2) + = checkExpr c e1 >> checkExpr c e2 + +checkExprPairs + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [(Expr, Expr)] + -> m () +checkExprPairs + = checkSequence_ checkExprPair + +checkRawApp + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Expr] + -> m () +checkRawApp c es + = touchNames c (accessContextMatch (exprNames es) c) + >> checkExprs c es + +exprName + :: Expr + -> Maybe String +exprName (Ident (N.QName (N.Name _ _ [Id n]))) + = Just n +exprName _ + = Nothing + +exprNames + :: [Expr] + -> [String] +exprNames + = catMaybes + . fmap exprName + +-- ## Assignments + +checkRecordAssignment + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> RecordAssignment + -> m () +checkRecordAssignment c (Left f) + = checkFieldAssignment c f +checkRecordAssignment c (Right m) + = checkModuleAssignment c m + +checkRecordAssignments + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [RecordAssignment] + -> m () +checkRecordAssignments + = checkSequence_ checkRecordAssignment + +checkFieldAssignment + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> FieldAssignment + -> m () +checkFieldAssignment c (FieldAssignment _ e) + = checkExpr c e + +checkFieldAssignments + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [FieldAssignment] + -> m () +checkFieldAssignments + = checkSequence_ checkFieldAssignment + +checkModuleAssignment + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> ModuleAssignment + -> m () +checkModuleAssignment c a@(ModuleAssignment n es _) + = checkExprs c es + >> maybe (pure ()) (touchModule c (getRange a)) (fromQName n) + +-- ## Definitions + +checkLHS + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> LHS + -> m AccessContext +checkLHS c (LHS p rs ws _) + = checkPattern c p + >>= \c' -> checkRewriteEqns (c <> c') rs + >>= \c'' -> checkExprs (c <> c' <> c'') (whThing <$> ws) + >> pure (c' <> c'') + +checkRHS + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> RHS + -> m () +checkRHS _ AbsurdRHS + = pure () +checkRHS c (RHS e) + = checkExpr c e + +checkClause + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> Clause + -> m AccessContext +checkClause c (Clause n _ l r w cs) + = pure (maybe id accessContextDefine (fromName n) c) + >>= \c' -> checkLHS c' l + >>= \c'' -> checkWhereClause (c' <> c'') w + >>= \(m, c''') -> checkRHS (c' <> c'' <> c''') r + >> checkClauses (c' <> c'' <> c''') cs + >>= \m' -> pure (m <> m') + +checkClauses + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Clause] + -> m AccessContext +checkClauses + = checkSequence checkClause + +checkLamClause + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> LamClause + -> m AccessContext +checkLamClause c (LamClause l r _ _) + = checkLHS c l + >>= \c' -> checkRHS (c <> c') r + >> pure c' + +checkLamClauses + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [LamClause] + -> m AccessContext +checkLamClauses + = checkFold checkLamClause + +checkLamClause_ + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> LamClause + -> m () +checkLamClause_ c ls + = void (checkLamClause c ls) + +-- Do not propogate context from one clause to the next. +checkLamClauses_ + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [LamClause] + -> m () +checkLamClauses_ + = checkSequence_ checkLamClause_ + +checkWhereClause + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> WhereClause + -> m (AccessContext, AccessContext) + -- ^ A context for the named where block, then the full context. +checkWhereClause _ NoWhere + = pure (mempty, mempty) +checkWhereClause c (AnyWhere ds) + = checkDeclarations c ds + >>= \c' -> pure (mempty, c') +checkWhereClause c (SomeWhere n a ds) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> checkDeclarations c ds + >>= \c' -> checkModuleName (toContext c') (fromAccess a) (getRange n) n' + >>= \c'' -> pure (c'' , c') + +checkRewriteEqn + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> RewriteEqn + -> m AccessContext +checkRewriteEqn c (Rewrite rs) + = checkExprs c (snd <$> rs) >> pure mempty +checkRewriteEqn c (Invert _ ws) + = checkIrrefutableWiths c ws + +checkRewriteEqns + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [RewriteEqn] + -> m AccessContext +checkRewriteEqns + = checkFold checkRewriteEqn + +checkIrrefutableWith + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> (Pattern, Expr) + -> m AccessContext +checkIrrefutableWith c (p, e) + = checkExpr c e >> checkPattern c p + +checkIrrefutableWiths + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [(Pattern, Expr)] + -> m AccessContext +checkIrrefutableWiths + = checkFold checkIrrefutableWith + +checkDoStmt + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> DoStmt + -> m AccessContext +checkDoStmt c (DoBind _ p e cs) + = checkLamClauses c cs + >>= \c' -> checkExpr (c <> c') e + >> checkPattern (c <> c') p + >>= \c'' -> pure (c' <> c'') +checkDoStmt c (DoThen e) + = checkExpr c e >> pure mempty +checkDoStmt c (DoLet _ ds) + = checkDeclarations c ds + +checkDoStmts + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [DoStmt] + -> m AccessContext +checkDoStmts c ss + = bool (pure ()) (touchName c bind) (hasBind ss) + >> bool (pure ()) (touchName c bind_) (hasBind_ ss) + >> checkFold checkDoStmt c ss + +hasBind + :: [DoStmt] + -> Bool +hasBind [] + = False +hasBind (_ : []) + = False +hasBind (DoBind _ _ _ _ : _ : _) + = True +hasBind (_ : ss) + = hasBind ss + +hasBind_ + :: [DoStmt] + -> Bool +hasBind_ [] + = False +hasBind_ (_ : []) + = False +hasBind_ (DoThen _ : _ : _) + = True +hasBind_ (_ : ss) + = hasBind_ ss + +bind + :: Name +bind + = Name + [ Hole + , Id ">>=" + , Hole + ] + +bind_ + :: Name +bind_ + = Name + [ Hole + , Id ">>" + , Hole + ] + +-- ## Declarations + +checkDeclarations + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Declaration] + -> m AccessContext +checkDeclarations + = checkDeclarationsWith checkNiceDeclarations + +checkDeclarationsRecord + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Name + -> [Range] + -- ^ Ranges associated with parent record. + -> AccessContext + -> [Declaration] + -> m AccessContext +checkDeclarationsRecord n rs + = checkDeclarationsWith (checkNiceDeclarationsRecord n rs) + +checkDeclarationsTop + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> [Declaration] + -> m AccessContext +checkDeclarationsTop + = checkDeclarationsWith checkNiceDeclarationsTop + +checkDeclarationsWith + :: MonadError Error m + => (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext) + -> AccessContext + -> [Declaration] + -> m AccessContext +checkDeclarationsWith f c ds = do + (fixities, _) + <- fixitiesAndPolarities NoWarn ds + (niceDeclsEither, _) + <- pure (runNice (niceDeclarations fixities ds)) + niceDecls + <- liftEither (mapLeft ErrorDeclaration niceDeclsEither) + f fixities c niceDecls + +checkNiceDeclaration + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> AccessContext + -> NiceDeclaration + -> m AccessContext + +checkNiceDeclaration fs c (Axiom _ a _ _ _ n e) + = checkExpr c e >> checkName' False fs (fromAccess a) RangePostulate n +checkNiceDeclaration _ _ (NiceField r _ _ _ _ _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedField) r) +checkNiceDeclaration fs c (PrimitiveFunction _ a _ n e) + = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n +checkNiceDeclaration _ c (NiceModule r a _ (N.QName n) bs ds) + = checkNiceModule c (fromAccess a) r (fromName n) bs ds +checkNiceDeclaration _ _ (NiceModule _ _ _ n@(N.Qual _ _) _ _) + = throwError (ErrorInternal ErrorName (getRange n)) +checkNiceDeclaration _ _ (NicePragma _ _) + = pure mempty +checkNiceDeclaration fs c (NiceRecSig _ a _ _ _ n bs e) + = checkNiceSig fs c a RangeRecord n bs e +checkNiceDeclaration fs c (NiceDataSig _ a _ _ _ n bs e) + = checkNiceSig fs c a RangeData n bs e +checkNiceDeclaration _ _ (NiceFunClause r _ _ _ _ _ _) + = throwError (ErrorInternal (ErrorUnexpected UnexpectedNiceFunClause) r) +checkNiceDeclaration fs c (FunSig _ a _ _ _ _ _ _ n e) + = checkExpr c e >> checkName' False fs (fromAccess a) RangeDefinition n +checkNiceDeclaration _ c (FunDef _ _ _ _ _ _ _ cs) + = checkClauses c cs >> pure mempty +checkNiceDeclaration _ c (NiceGeneralize _ _ _ _ _ e) + = checkExpr c e >> pure mempty +checkNiceDeclaration _ _ (NiceUnquoteDecl r _ _ _ _ _ _ _) + = throwError (ErrorUnsupported UnsupportedUnquote r) +checkNiceDeclaration _ _ (NiceUnquoteDef r _ _ _ _ _ _) + = throwError (ErrorUnsupported UnsupportedUnquote r) + +checkNiceDeclaration fs c + (NiceMutual _ _ _ _ + ds@(NiceRecSig _ _ _ _ _ _ _ _ : NiceRecDef _ _ _ _ _ _ _ _ _ _ _ : _)) + = checkNiceDeclarations fs c ds +checkNiceDeclaration fs c + (NiceMutual _ _ _ _ + ds@(NiceDataSig _ _ _ _ _ _ _ _ : NiceDataDef _ _ _ _ _ _ _ _ : _)) + = checkNiceDeclarations fs c ds +checkNiceDeclaration fs c + (NiceMutual _ _ _ _ + ds@(FunSig _ _ _ _ _ _ _ _ _ _ : FunDef _ _ _ _ _ _ _ _ : _)) + = checkNiceDeclarations fs c ds +checkNiceDeclaration fs c (NiceMutual r _ _ _ ds) + = checkNiceDeclarations fs c ds + >>= \c' -> modifyInsert r RangeMutual + >> accessContextInsertRangeAll r c' + +checkNiceDeclaration _ c + (NiceModuleMacro r _ (N.NoName _ _) + (SectionApp _ [] (RawApp _ (Ident n : es))) DoOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftLookup r n' (accessContextLookupModule n' c) + >>= \(C.Module rs c') -> modifyDelete rs + >> checkExprs c es + >> checkImportDirective Open r n' c' i + >>= pure . fromContext (importDirectiveAccess i) +checkNiceDeclaration _ c + (NiceModuleMacro r a a' + (SectionApp _ bs (RawApp _ (Ident n : es))) DontOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a')) (fromName a') + >>= \a'' -> liftLookup r n' (accessContextLookupModule n' c) + >>= \(C.Module rs c') -> modifyDelete rs + >> checkTypedBindings True c bs + >>= \c'' -> checkExprs (c <> c'') es + >> checkImportDirective Module r (QName a'') c' i + >>= \c''' -> checkModuleName c''' (fromAccess a) r a'' +checkNiceDeclaration _ c + (NiceModuleMacro r a a' + (SectionApp _ bs (RawApp _ (Ident n : es))) DoOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a')) (fromName a') + >>= \a'' -> liftLookup r n' (accessContextLookupModule n' c) + >>= \(C.Module rs c') -> modifyDelete rs + >> checkTypedBindings True c bs + >>= \c'' -> checkExprs (c <> c'') es + >> checkImportDirective Module r (QName a'') c' i + >>= \c''' -> checkModuleName c''' (fromAccess a) r a'' + >>= \c'''' -> pure (c'''' <> fromContext (importDirectiveAccess i) c''') +checkNiceDeclaration _ _ + (NiceModuleMacro _ _ _ + (SectionApp r _ _) _ _) + = throwError (ErrorInternal ErrorMacro r) +checkNiceDeclaration _ _ + (NiceModuleMacro r _ _ + (RecordModuleInstance _ _) _ _) + = throwError (ErrorUnsupported UnsupportedMacro r) + +checkNiceDeclaration _ c (NiceOpen r n i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftLookup r n' (accessContextLookupModule n' c) + >>= \(C.Module rs c') -> modifyDelete rs + >> checkImportDirective Open r n' c' i + >>= \c'' -> pure (fromContext (importDirectiveAccess i) c'') + +checkNiceDeclaration _ _ (NiceImport r n Nothing DontOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> checkFile (Just r) n' + >>= \c' -> checkImportDirective Import r n' c' i + >>= \c'' -> pure (accessContextImport n' c'') +checkNiceDeclaration _ _ (NiceImport r n Nothing DoOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> checkFile (Just r) n' + >>= \c' -> checkImportDirective Import r n' c' i + >>= \c'' -> pure (accessContextImport n' c' + <> fromContext (importDirectiveAccess i) c'') +checkNiceDeclaration _ _ (NiceImport r n (Just a) DontOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a)) (fromAsName a) + >>= \a' -> checkFile (Just r) n' + >>= \c' -> checkImportDirective Import r n' c' i + >>= \c'' -> checkModuleName c'' Public (getRange a) a' +checkNiceDeclaration _ _ (NiceImport r n (Just a) DoOpen i) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromQName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange a)) (fromAsName a) + >>= \a' -> checkFile (Just r) n' + >>= \c' -> checkImportDirective Import r n' c' i + >>= \c'' -> checkModuleName c' Public (getRange a) a' + >>= \c''' -> pure (c''' <> fromContext (importDirectiveAccess i) c'') + +checkNiceDeclaration fs c (NiceDataDef _ _ _ _ _ n bs cs) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> pure (either (const []) id (accessContextLookup (QName n') c)) + >>= \rs -> checkLamBindings False c bs + >>= \c' -> checkNiceConstructors fs rs (accessContextDefine n' c <> c') cs + >>= \c'' -> pure (accessContextModule' n' Public rs c'' <> c'') + +checkNiceDeclaration fs c (NiceRecDef _ _ _ _ _ n _ _ m bs ds) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> pure (either (const []) id (accessContextLookup (QName n') c)) + >>= \rs -> checkLamBindings False c bs + >>= \c' -> checkNiceConstructorRecordMay fs rs (m >>= fromNameRange . fst) + >>= \c'' -> checkDeclarationsRecord n' rs (c <> c') ds + >>= \c''' -> pure (accessContextModule' n' Public rs (c'' <> c''') <> c'') + +checkNiceDeclaration fs c (NicePatternSyn _ a n ns p) + = localSkip (checkNames' False Public RangeVariable (unArg <$> ns)) + >>= \c' -> checkPattern (c <> c') p + >> checkName' True fs (fromAccess a) RangePatternSynonym n + +checkNiceDeclarationRecord + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Name + -> [Range] + -- ^ Ranges associated with parent record. + -> Fixities + -> AccessContext + -> NiceDeclaration + -> m AccessContext +checkNiceDeclarationRecord _ rs fs c d@(Axiom _ _ _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ rs fs c d@(PrimitiveFunction _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord n rs fs c (NiceMutual _ _ _ _ ds) + = checkNiceDeclarationsRecord n rs fs c ds +checkNiceDeclarationRecord _ rs fs c d@(NiceModule _ _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceModuleMacro _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceOpen _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceImport _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NicePragma _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ rs fs c d@(NiceRecSig _ _ _ _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ rs fs c d@(NiceDataSig _ _ _ _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceFunClause _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ rs fs c d@(FunSig _ _ _ _ _ _ _ _ _ _) + = modifyDelete rs >> checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(FunDef _ _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceDataDef _ _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceRecDef _ _ _ _ _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NicePatternSyn _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceGeneralize _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceUnquoteDecl _ _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d +checkNiceDeclarationRecord _ _ fs c d@(NiceUnquoteDef _ _ _ _ _ _ _) + = checkNiceDeclaration fs c d + +checkNiceDeclarationRecord n rs fs c (NiceField _ a _ _ _ n' (Arg _ e)) + = checkExpr (accessContextDefine n c) e + >> maybe + (pure mempty) + (\n'' -> pure (accessContextItem n'' (fromAccess a) + (item rs (syntax fs n'')))) + (fromName n') + +checkNiceDeclarations + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> AccessContext + -> [NiceDeclaration] + -> m AccessContext +checkNiceDeclarations fs + = checkFoldUnion (checkNiceDeclaration fs) + +checkNiceDeclarationsRecord + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Name + -> [Range] + -- ^ Ranges associated with parent record. + -> Fixities + -> AccessContext + -> [NiceDeclaration] + -> m AccessContext +checkNiceDeclarationsRecord n rs fs + = checkFoldUnion (checkNiceDeclarationRecord n rs fs) + +checkNiceDeclarationsTop + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> AccessContext + -> [NiceDeclaration] + -> m AccessContext +checkNiceDeclarationsTop _ _ [] + = pure mempty +checkNiceDeclarationsTop _ c (NiceModule r a _ _ bs ds : _) + = checkNiceModule c (fromAccess a) r Nothing bs ds +checkNiceDeclarationsTop fs c (d : ds) + = checkNiceDeclaration fs c d + >>= \c' -> checkNiceDeclarations fs (c <> c') ds + +checkNiceSig + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> AccessContext + -> Common.Access + -> RangeType + -> N.Name + -> [LamBinding] + -> Expr + -> m AccessContext +checkNiceSig fs c a t n bs e + = checkLamBindings False c bs + >>= \c' -> checkExpr (c <> c') e + >> checkName' False fs (fromAccess a) t n + +checkNiceConstructor + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> [Range] + -- ^ Ranges associated with parent type. + -> AccessContext + -> NiceDeclaration + -> m AccessContext +checkNiceConstructor fs rs c (Axiom _ a _ _ _ n e) + = checkExpr c e + >> maybe + (pure mempty) + (\n'' -> pure (accessContextItem n'' (fromAccess a) + (itemConstructor rs (syntax fs n'')))) + (fromName n) +checkNiceConstructor _ _ _ d + = throwError (ErrorInternal ErrorConstructor (getRange d)) + +checkNiceConstructors + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Fixities + -> [Range] + -- ^ Ranges associated with parent type. + -> AccessContext + -> [NiceDeclaration] + -> m AccessContext +checkNiceConstructors fs rs + = checkSequence (checkNiceConstructor fs rs) + +checkNiceConstructorRecord + :: MonadReader Environment m + => MonadState State m + => Fixities + -> [Range] + -- ^ Ranges associated with record type. + -> Range + -> Name + -> m AccessContext +checkNiceConstructorRecord fs rs r n + = modifyInsert r (RangeNamed RangeRecordConstructor (QName n)) + >> pure (accessContextItem n Public (itemConstructor (r : rs) (syntax fs n))) + +checkNiceConstructorRecordMay + :: MonadReader Environment m + => MonadState State m + => Fixities + -> [Range] + -- ^ Ranges associated with record type. + -> Maybe (Range, Name) + -> m AccessContext +checkNiceConstructorRecordMay _ _ Nothing + = pure mempty +checkNiceConstructorRecordMay fs rs (Just (r, n)) + = checkNiceConstructorRecord fs rs r n + +checkNiceModule + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => AccessContext + -> Access + -> Range + -> Maybe Name + -- ^ If `Nothing`, the module is anonymous. + -> [TypedBinding] + -> [Declaration] + -> m AccessContext +checkNiceModule c a r n bs ds + = checkTypedBindings True c bs + >>= \c' -> checkDeclarations (c <> c') ds + >>= \c'' -> pure (toContext c'') + >>= \c''' -> maybe (pure (fromContext a c''')) (checkModuleName c''' a r) n + +-- ## Imports + +data DirectiveType where + + Import + :: DirectiveType + + Module + :: DirectiveType + + Open + :: DirectiveType + + deriving Show + +directiveStatement + :: DirectiveType + -> Maybe RangeType +directiveStatement Import + = Just RangeImport +directiveStatement Module + = Nothing +directiveStatement Open + = Just RangeOpen + +directiveItem + :: DirectiveType + -> RangeType +directiveItem Import + = RangeImportItem +directiveItem Module + = RangeModuleItem +directiveItem Open + = RangeOpenItem + +checkImportDirective + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Range + -> QName + -> Context + -> ImportDirective + -> m Context +checkImportDirective dt r n c (ImportDirective _ UseEverything hs rs _) + = maybe (pure ()) (\t -> modifyInsert r (RangeNamed t n)) + (directiveStatement dt) + >> modifyHidings c hs + >>= flip (modifyRenamings dt) rs + >>= contextInsertRangeAll r +checkImportDirective dt r n c (ImportDirective _ (Using ns) _ rs _) + = maybe (pure ()) (\t -> modifyInsert r (RangeNamed t n)) + (directiveStatement dt) + >> checkImportedNames dt c ns + >>= \c' -> checkRenamings dt c rs + >>= \c'' -> contextInsertRangeAll r (c' <> c'') + +checkRenaming + :: MonadReader Environment m + => MonadState State m + => MonadError Error m + => DirectiveType + -> Context + -> Renaming + -> m Context +checkRenaming dt c r@(Renaming n t _ _) + = checkImportedNamePair dt c (getRange r, n, t) + +checkRenamings + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> [Renaming] + -> m Context +checkRenamings dt + = checkSequence (checkRenaming dt) + +checkImportedName + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> ImportedName + -> m Context +checkImportedName dt c n + = checkImportedNamePair dt c (getRange n, n, n) + +checkImportedNamePair + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> (Range, ImportedName, ImportedName) + -> m Context +checkImportedNamePair dt c (_, ImportedName n, ImportedName t) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t) + >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t')) + >> pure (maybe mempty (contextItem t') (contextLookupItem (QName n') c) + <> maybe mempty (contextModule t') (contextLookupModule (QName n') c)) + >>= contextInsertRangeAll r +checkImportedNamePair dt c (_, ImportedModule n, ImportedModule t) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t) + >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t')) + >> pure (maybe mempty (contextModule t') (contextLookupModule (QName n') c)) + >>= contextInsertRangeAll r +checkImportedNamePair _ _ (r, _, _) + = throwError (ErrorInternal ErrorRenaming r) + +checkImportedNames + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> [ImportedName] + -> m Context +checkImportedNames dt + = checkSequence (checkImportedName dt) + +modifyHiding + :: MonadError Error m + => Context + -> ImportedName + -> m Context +modifyHiding c (ImportedName n) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= pure . flip contextDelete c +modifyHiding c (ImportedModule n) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= pure . flip contextDeleteModule c + +modifyHidings + :: MonadError Error m + => Context + -> [ImportedName] + -> m Context +modifyHidings + = foldM modifyHiding + +modifyRenaming + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> Renaming + -> m Context +modifyRenaming dt c (Renaming (ImportedName n) (ImportedName t) _ _) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t) + >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t')) + >> contextRename n' t' r c + >>= contextRenameModule n' t' r +modifyRenaming dt c (Renaming (ImportedModule n) (ImportedModule t) _ _) + = liftMaybe (ErrorInternal ErrorName (getRange n)) (fromName n) + >>= \n' -> liftMaybe (ErrorInternal ErrorName (getRange t)) (fromNameRange t) + >>= \(r, t') -> modifyInsert r (RangeNamed (directiveItem dt) (QName t')) + >> contextRenameModule n' t' r c +modifyRenaming _ _ r + = throwError (ErrorInternal ErrorRenaming (getRange r)) + +modifyRenamings + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => DirectiveType + -> Context + -> [Renaming] + -> m Context +modifyRenamings dt + = foldM (modifyRenaming dt) + +touchModule + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => AccessContext + -> Range + -> QName + -> m () +touchModule c r n + = touchModuleWith (accessContextLookupModule n c) r n + +touchModuleWith + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => Either LookupError C.Module + -> Range + -> QName + -> m () +touchModuleWith (Left LookupNotFound) _ _ + = pure () +touchModuleWith (Left LookupAmbiguous) r n + = throwError (ErrorAmbiguous r n) +touchModuleWith (Right m) _ _ + = modifyDelete (moduleRanges m) + +touchContext + :: MonadReader Environment m + => MonadState State m + => Context + -> m () +touchContext c + = modifyDelete (contextRanges c) + +importDirectiveAccess + :: ImportDirective + -> Access +importDirectiveAccess (ImportDirective _ _ _ _ Nothing) + = Private +importDirectiveAccess (ImportDirective _ _ _ _ (Just _)) + = Public + +-- ## Modules + +checkModule + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Module + -> m Context +checkModule (_, ds) + = toContext <$> checkDeclarationsTop mempty ds + +-- ## Files + +checkFile + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Maybe Range + -> QName + -> m Context +checkFile r n + = gets (stateLookup n) >>= \s -> checkFileWith s r n + +checkFileWith + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Maybe ModuleState + -> Maybe Range + -> QName + -> m Context + +checkFileWith Nothing r n | isBuiltin n + = liftIO (getDataFileName ("data" qNamePath n)) + >>= \p -> localSkip (checkFilePath r n p) + +checkFileWith Nothing r n = do + local + <- askLocal + rootPath + <- askRoot + context + <- checkFilePath r n (rootPath qNamePath n) + _ + <- bool (pure ()) (touchContext context) local + pure context + +checkFileWith (Just Blocked) r n + = throwError (ErrorCyclic r n) +checkFileWith (Just (Checked c)) _ _ + = pure c + +checkFilePath + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Maybe Range + -> QName + -> FilePath + -> m Context +checkFilePath r n p = do + _ + <- modify (stateBlock n) + absolutePath + <- pure (AbsolutePath (T.pack p)) + exists + <- liftIO (doesFileExist p) + _ + <- bool (throwError (ErrorFile r n p)) (pure ()) exists + contents + <- liftIO (readFile p) + (parseResult, _) + <- liftIO (runPMIO (parseFile moduleParser absolutePath contents)) + (module', _) + <- liftEither (mapLeft ErrorParse parseResult) + context + <- checkModule module' + _ + <- modify (stateCheck n context) + pure context + +-- ## Paths + +-- Look for unvisited modules at the given path. +checkPath + :: MonadIO m + => [QName] + -- ^ Visited or ignored modules. + -> FilePath + -- ^ The project root path. + -> FilePath + -- ^ The path at which to look. + -> m [FilePath] +checkPath ms p p' + = liftIO (doesDirectoryExist p') + >>= bool (pure (checkPathFile ms p p')) (checkPathDirectory ms p p') + +checkPathFile + :: [QName] + -> FilePath + -> FilePath + -> [FilePath] +checkPathFile ms p p' + = maybe [] (bool [p'] [] . flip elem ms) (pathQName p p') + +checkPathDirectory + :: MonadIO m + => [QName] + -> FilePath + -> FilePath + -> m [FilePath] +checkPathDirectory ms p p' + = fmap (p' ) <$> liftIO (listDirectory p') + >>= traverse (checkPath ms p) + >>= pure . concat + +-- ## Roots + +checkRoot + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => Root + -> m () +checkRoot (Root p Nothing) + = checkFile Nothing p + >>= touchContext +checkRoot (Root p (Just ns)) + = checkFile Nothing p + >>= \c -> touchQNamesContext c p ns + +checkRoots + :: MonadError Error m + => MonadReader Environment m + => MonadState State m + => MonadIO m + => [Root] + -> m () +checkRoots + = void . traverse checkRoot + +-- ## Main + +-- | Check an Agda file and its dependencies for unused code. +checkUnused + :: FilePath + -- ^ The project root path. + -> Roots + -- ^ The public entry points for the project. + -> IO (Either Error Unused) +checkUnused p (Roots rs is) + = runExceptT + $ checkUnusedItems False p (checkRoots rs) + >>= \s -> checkPath (is <> stateModules s) p p + >>= \fs -> pure (Unused (UnusedItems (stateItems s)) fs) + +-- | Check an Agda file for unused code. +checkUnusedLocal + :: FilePath + -- ^ The project root path. + -> QName + -- ^ The module to check. + -> IO (Either Error UnusedItems) +checkUnusedLocal p + = runExceptT + . fmap UnusedItems + . fmap stateItems + . checkUnusedItems True p + . checkFile Nothing + +checkUnusedItems + :: MonadError Error m + => MonadIO m + => Bool + -- ^ Whether to use local mode. + -> FilePath + -> ReaderT Environment (StateT State m) a + -> m State +checkUnusedItems l p + = fmap snd + . flip runStateT stateEmpty + . flip runReaderT (Environment False l p) + diff --git a/src/Agda/Unused/Monad/Error.hs b/src/Agda/Unused/Monad/Error.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Monad/Error.hs @@ -0,0 +1,220 @@ +{-# LANGUAGE UndecidableInstances #-} + +{- | +Module: Agda.Unused.Monad.Error + +An error monad for determining unused code. +-} +module Agda.Unused.Monad.Error + + ( -- * Definitions + + Error(..) + , InternalError(..) + , UnexpectedError(..) + , UnsupportedError(..) + + -- * Lift + + , liftLookup + + ) where + +import Agda.Unused.Types.Context + (LookupError(..)) +import Agda.Unused.Types.Name + (QName) +import Agda.Unused.Types.Range + (Range, getRange) + +import Agda.Syntax.Concrete.Definitions + (DeclarationException) +import Agda.Syntax.Concrete.Fixity + (MonadFixityError(..)) +import Agda.Syntax.Parser + (ParseError) +import Control.Monad.Except + (MonadError, throwError) + +-- ## Definitions + +-- | An error encountered while checking for unused code. +data Error where + + -- | Ambiguous lookup. + ErrorAmbiguous + :: !Range + -> !QName + -> Error + + -- | Cyclic module dependency. + ErrorCyclic + :: !(Maybe Range) + -> !QName + -> Error + + -- | Agda declaration exception. + ErrorDeclaration + :: !DeclarationException + -> Error + + -- | File not found. + ErrorFile + :: !(Maybe Range) + -> !QName + -> !FilePath + -> Error + + -- | Agda fixity exception. + ErrorFixity + :: !(Maybe Range) + -> Error + + -- | Internal error; should be reported. + ErrorInternal + :: !InternalError + -> !Range + -> Error + + -- | Module not found in open statement. + ErrorOpen + :: !Range + -> !QName + -> Error + + -- | Agda parse error. + ErrorParse + :: !ParseError + -> Error + + -- | Agda polarity error. + ErrorPolarity + :: !(Maybe Range) + -> Error + + -- | Root not found. + ErrorRoot + :: !QName + -> !QName + -> Error + + -- | Unsupported language feature. + ErrorUnsupported + :: !UnsupportedError + -> !Range + -> Error + + deriving Show + +-- | An internal error, indicating a bug in our code. This type of error should +-- be reported by filing an issue. +data InternalError where + + -- | Unexpected declaration type for constructor. + ErrorConstructor + :: InternalError + + -- | Unexpected arguments to SectionApp constructor. + ErrorMacro + :: InternalError + + -- | Unexpected underscore as name. + ErrorName + :: InternalError + + -- | Unexpected name-module mismatch in renaming statement. + ErrorRenaming + :: InternalError + + -- | Unexpected data type constructor. + ErrorUnexpected + :: !UnexpectedError + -> InternalError + + deriving Show + +-- | An error indicating that a constructor for a data type is used where it +-- should not be used. +data UnexpectedError where + + UnexpectedAbsurd + :: UnexpectedError + + UnexpectedAs + :: UnexpectedError + + UnexpectedDontCare + :: UnexpectedError + + UnexpectedETel + :: UnexpectedError + + UnexpectedEllipsis + :: UnexpectedError + + UnexpectedEqual + :: UnexpectedError + + UnexpectedField + :: UnexpectedError + + UnexpectedNiceFunClause + :: UnexpectedError + + UnexpectedOpApp + :: UnexpectedError + + UnexpectedOpAppP + :: UnexpectedError + + deriving Show + +-- | An error indicating that an unsupported language was found. +data UnsupportedError where + + -- | Record module instance applications. + UnsupportedMacro + :: UnsupportedError + + -- | Unquoting primitives. + UnsupportedUnquote + :: UnsupportedError + + deriving Show + +-- ## Fixity + +instance (Monad m, MonadError Error m) => MonadFixityError m where + throwMultipleFixityDecls [] + = throwError (ErrorFixity Nothing) + throwMultipleFixityDecls ((n, _) : _) + = throwError (ErrorFixity (Just (getRange n))) + throwMultiplePolarityPragmas [] + = throwError (ErrorPolarity Nothing) + throwMultiplePolarityPragmas (n : _) + = throwError (ErrorPolarity (Just (getRange n))) + warnUnknownNamesInFixityDecl _ + = pure () + warnUnknownNamesInPolarityPragmas _ + = pure () + warnUnknownFixityInMixfixDecl _ + = pure () + warnPolarityPragmasButNotPostulates _ + = pure () + +-- ## Lookup + +-- | Lift a lookup result to our error monad. +liftLookup + :: MonadError Error m + => Range + -> QName + -> Either LookupError a + -> m a +liftLookup r n (Left LookupNotFound) + = throwError (ErrorOpen r n) +liftLookup r n (Left LookupAmbiguous) + = throwError (ErrorAmbiguous r n) +liftLookup _ _ (Right x) + = pure x + diff --git a/src/Agda/Unused/Monad/Reader.hs b/src/Agda/Unused/Monad/Reader.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Monad/Reader.hs @@ -0,0 +1,69 @@ +{- | +Module: Agda.Unused.Monad.Reader + +A reader monad for determining unused code. +-} +module Agda.Unused.Monad.Reader + + ( -- * Definition + + Environment(..) + + -- * Ask + + , askSkip + , askLocal + , askRoot + + -- * Local + + , localSkip + + ) where + +import Control.Monad.Reader + (MonadReader, ask, local) + +-- | An environment type for use in a reader monad. +data Environment + = Environment + { environmentSkip + :: !Bool + -- ^ Whether to skip all names. + , environmentLocal + :: !Bool + -- ^ Whether to skip public names. + , environmentRoot + :: !FilePath + -- ^ The project root path. + } deriving Show + +-- | Ask whether to skip checking names. +askSkip + :: MonadReader Environment m + => m Bool +askSkip + = environmentSkip <$> ask + +-- | Ask whether to skip checking public names. +askLocal + :: MonadReader Environment m + => m Bool +askLocal + = environmentLocal <$> ask + +-- | Ask for the project root path. +askRoot + :: MonadReader Environment m + => m FilePath +askRoot + = environmentRoot <$> ask + +-- | Skip checking names in a local computation. +localSkip + :: MonadReader Environment m + => m a + -> m a +localSkip + = local (\e -> e {environmentSkip = True}) + diff --git a/src/Agda/Unused/Monad/State.hs b/src/Agda/Unused/Monad/State.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Monad/State.hs @@ -0,0 +1,174 @@ +{- | +Module: Agda.Unused.Monad.State + +A state monad for determining unused code. +-} +module Agda.Unused.Monad.State + + ( -- * Definitions + + ModuleState(..) + , State + + -- * Interface + + , stateEmpty + , stateItems + , stateModules + , stateBlock + , stateCheck + , stateLookup + + -- * Modify + + , modifyDelete + , modifyInsert + + ) where + +import Agda.Unused.Monad.Reader + (Environment, askSkip) +import Agda.Unused.Types.Context + (Context) +import Agda.Unused.Types.Name + (QName) +import Agda.Unused.Types.Range + (Range, Range'(..), RangeInfo, rangeContains) +import Agda.Unused.Utils + (mapDeletes) + +import Control.Monad.Reader + (MonadReader) +import Control.Monad.State + (MonadState, modify) +import Data.Bool + (bool) +import Data.Map.Strict + (Map) +import qualified Data.Map.Strict + as Map + +-- | Cache the results of checking modules. This allows us to: +-- +-- - Avoid duplicate computations. +-- - Handle cyclic module dependencies without nontermination. +data ModuleState where + + Blocked + :: ModuleState + + Checked + :: !Context + -> ModuleState + + deriving Show + +-- | The current computation state. +data State + = State + { stateItems' + :: !(Map Range RangeInfo) + -- ^ Ranges for each unused item. + , stateModules' + :: !(Map QName ModuleState) + -- ^ States for each module dependency. + } deriving Show + +-- | Construct an empty state. +stateEmpty + :: State +stateEmpty + = State mempty mempty + +-- | Get a sorted list of state items. +-- +-- If one state item contains another (e.g., an @open@ statement containing +-- @using@ directives), then keep only the containing item. +stateItems + :: State + -> [(Range, RangeInfo)] +stateItems + = stateItemsFilter + . Map.toAscList + . stateItems' + +-- | Get a list of visited modules. +stateModules + :: State + -> [QName] +stateModules + = Map.keys + . stateModules' + +-- Remove nested items. +stateItemsFilter + :: [(Range, RangeInfo)] + -> [(Range, RangeInfo)] +stateItemsFilter [] + = [] +stateItemsFilter (i : i' : is) | rangeContains (fst i) (fst i') + = stateItemsFilter (i : is) +stateItemsFilter (i : is) + = i : stateItemsFilter is + +stateInsert + :: Range + -> RangeInfo + -> State + -> State +stateInsert NoRange _ s + = s +stateInsert r@(Range _ _) i (State rs ms) + = State (Map.insert r i rs) ms + +stateDelete + :: [Range] + -> State + -> State +stateDelete rs (State rs' ms) + = State (mapDeletes rs rs') ms + +-- | Lookup the state of a module. +stateLookup + :: QName + -> State + -> Maybe ModuleState +stateLookup m (State _ ms) + = Map.lookup m ms + +-- | Mark that we are beginning to check a module. +stateBlock + :: QName + -> State + -> State +stateBlock m (State rs ms) + = State rs (Map.insert m Blocked ms) + +-- | Record the results of checking a module. +stateCheck + :: QName + -> Context + -> State + -> State +stateCheck m c (State rs ms) + = State rs (Map.insert m (Checked c) ms) + +-- | Record a new unused item. +modifyInsert + :: MonadReader Environment m + => MonadState State m + => Range + -> RangeInfo + -> m () +modifyInsert r i + = askSkip >>= bool (modify (stateInsert r i)) (pure ()) + +-- | Mark a list of items as used. +modifyDelete + :: MonadReader Environment m + => MonadState State m + => [Range] + -> m () +modifyDelete rs + = askSkip >>= bool (modify (stateDelete rs)) (pure ()) + diff --git a/src/Agda/Unused/Parse.hs b/src/Agda/Unused/Parse.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Parse.hs @@ -0,0 +1,150 @@ +{- | +Module: Agda.Unused.Parse + +Parsers for roots. +-} +module Agda.Unused.Parse + ( parseConfig + ) where + +import Agda.Unused.Types.Name + (Name(..), NamePart(..), QName(..)) +import Agda.Unused.Types.Root + (Root(..), Roots, fromList) +import Agda.Unused.Utils + (mapLeft) + +import Control.Monad + (void) +import Data.Char + (isSpace) +import Data.Text + (Text) +import qualified Data.Text + as T +import Data.Void + (Void) +import Text.Megaparsec + (Parsec, (<|>), between, many, parse, satisfy, some, try) +import Text.Megaparsec.Char + (char, space1) +import qualified Text.Megaparsec.Char.Lexer + as L +import Text.Megaparsec.Error + (errorBundlePretty) + +-- ## Utilities + +isNameChar + :: Char + -> Bool +isNameChar '.' + = False +isNameChar '(' + = False +isNameChar ')' + = False +isNameChar c | isSpace c + = False +isNameChar _ + = True + +listMaybe + :: [a] + -> Maybe [a] +listMaybe [] + = Nothing +listMaybe xs@(_ : _) + = Just xs + +-- ## Parsers + +type Parser + = Parsec Void Text + +parseSpace + :: Parser () +parseSpace + = L.space space1 + (L.skipLineComment "--") + (L.skipBlockComment "{-" "-}") + +parseDot + :: Parser () +parseDot + = void (char '.') + +parseHyphen + :: Parser () +parseHyphen + = void (char '-') + +parseParens + :: Parser a + -> Parser a +parseParens + = between (char '(') (char ')') + +parseNamePart + :: Parser NamePart +parseNamePart + = Id <$> some (satisfy isNameChar) + +parseName + :: Parser Name +parseName + = Name <$> some parseNamePart + +parseQName + :: Parser QName +parseQName + = try (Qual <$> parseName <* parseDot <*> parseQName) + <|> QName <$> parseName + +parseIgnore + :: Parser QName +parseIgnore + = parseParens (between parseSpace parseSpace parseQName) + <* parseSpace + +parseRootName + :: Parser QName +parseRootName + = parseHyphen + *> parseSpace + *> parseQName + <* parseSpace + +parseRootNames + :: Parser (Maybe [QName]) +parseRootNames + = listMaybe <$> many parseRootName + +parseRoot + :: Parser Root +parseRoot + = Root + <$> parseQName + <* parseSpace + <*> parseRootNames + +parseRootEither + :: Parser (Either QName Root) +parseRootEither + = Left <$> parseIgnore + <|> Right <$> parseRoot + +parseRoots + :: Parser Roots +parseRoots + = fromList <$> many parseRootEither + +-- | Parse configuration, producing either an error or a collection of roots. +parseConfig + :: Text + -> Either Text Roots +parseConfig + = mapLeft T.pack + . mapLeft errorBundlePretty + . parse (parseSpace *> parseRoots) ".agda-roots" + diff --git a/src/Agda/Unused/Print.hs b/src/Agda/Unused/Print.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Print.hs @@ -0,0 +1,285 @@ +{- | +Module: Agda.Unused.Print + +Printing functions for unused items and errors. +-} +module Agda.Unused.Print + ( printError + , printUnused + , printUnusedItems + , printNothing + ) where + +import Agda.Unused + (Unused(..), UnusedItems(..)) +import Agda.Unused.Monad.Error + (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..)) +import Agda.Unused.Types.Name + (Name(..), NamePart(..), QName(..)) +import Agda.Unused.Types.Range + (Range, Range'(..), RangeInfo(..), RangeType(..), getRange) + +import Agda.Utils.Pretty + (prettyShow) +import Data.Text + (Text) +import qualified Data.Text + as T + +-- ## Utilities + +quote + :: Text + -> Text +quote t + = "‘" <> t <> "’" + +parens + :: Text + -> Text +parens t + = "(" <> t <> ")" + +indent + :: Text + -> Text +indent t + = " " <> t + +-- ## Names + +printNamePart + :: NamePart + -> Text +printNamePart + = T.pack . show + +printName + :: Name + -> Text +printName (Name ps) + = mconcat (printNamePart <$> ps) + +printQName + :: QName + -> Text +printQName (QName n) + = printName n +printQName (Qual n ns) + = printName n <> "." <> printQName ns + +-- ## Ranges + +printRange + :: Range + -> Text +printRange NoRange + = "unknown location" +printRange r@(Range _ _) + = T.pack (show r) + +-- ## Messages + +printMessage + :: Text + -> Text + -> Text +printMessage t1 t2 + = T.unlines [t1, t2] + +printMessageIndent + :: Text + -> Text + -> Text +printMessageIndent t1 t2 + = T.unlines [t1, indent t2] + +-- ## Errors + +-- | Print an error. +printError + :: Error + -> Text + +printError (ErrorAmbiguous r n) + = printMessage (printRange r) + $ "Error: Ambiguous name " <> parens (quote (printQName n)) <> "." +printError (ErrorCyclic r n) + = printMessage (maybe (printQName n) printRange r) + $ "Error: Cyclic module dependency " <> parens (printQName n) <> "." +printError (ErrorFile r n p) + = printMessage (maybe (printQName n) printRange r) + $ "Error: File not found " <> parens (T.pack p) <> "." +printError (ErrorFixity (Just r)) + = printMessage (printRange r) + $ "Error: Multiple fixity declarations." +printError (ErrorInternal e r) + = printMessage (printRange r) + $ "Internal error: " <> printInternalError e +printError (ErrorOpen r n) + = printMessage (printRange r) + $ "Error: Module not found " <> parens (printQName n) <> "." +printError (ErrorPolarity (Just r)) + = printMessage (printRange r) + $ "Error: Multiple polarity declarations." +printError (ErrorRoot m n) + = printMessage (printQName m) + $ "Error: Root not found " <> parens (quote (printQName n)) <> "." +printError (ErrorUnsupported e r) + = printMessage (printRange r) + $ "Error: " <> printUnsupportedError e <> " not supported." + +printError (ErrorFixity Nothing) + = "Error: Multiple fixity declarations." +printError (ErrorPolarity Nothing) + = "Error: Multiple polarity declarations." + +printError (ErrorDeclaration e) + = printRange (getRange e) <> "\n" <> T.pack (prettyShow e) +printError (ErrorParse e) + = T.pack (show e) + +printInternalError + :: InternalError + -> Text +printInternalError ErrorConstructor + = "Invalid data constructor." +printInternalError ErrorMacro + = "Invalid module application." +printInternalError ErrorName + = "Invalid name." +printInternalError ErrorRenaming + = "Invalid renaming directive." +printInternalError (ErrorUnexpected e) + = "Unexpected constructor " <> quote (printUnexpectedError e) <> "." + +printUnexpectedError + :: UnexpectedError + -> Text +printUnexpectedError UnexpectedAbsurd + = "Absurd" +printUnexpectedError UnexpectedAs + = "As" +printUnexpectedError UnexpectedDontCare + = "DontCare" +printUnexpectedError UnexpectedETel + = "ETel" +printUnexpectedError UnexpectedEllipsis + = "Ellipsis" +printUnexpectedError UnexpectedEqual + = "Equal" +printUnexpectedError UnexpectedField + = "Field" +printUnexpectedError UnexpectedNiceFunClause + = "NiceFunClause" +printUnexpectedError UnexpectedOpApp + = "OpApp" +printUnexpectedError UnexpectedOpAppP + = "OpAppP" + +printUnsupportedError + :: UnsupportedError + -> Text +printUnsupportedError UnsupportedMacro + = "Record module instance applications" +printUnsupportedError UnsupportedUnquote + = "Unquoting primitives" + +-- ## Unused + +-- | Print a collection of unused items and files. +printUnused + :: Unused + -> Maybe Text +printUnused (Unused is ps) + = printUnusedWith + (printUnusedItems is) + (printUnusedPaths ps) + +printUnusedWith + :: Maybe Text + -> Maybe Text + -> Maybe Text +printUnusedWith Nothing Nothing + = Nothing +printUnusedWith Nothing (Just t2) + = Just t2 +printUnusedWith (Just t1) Nothing + = Just t1 +printUnusedWith (Just t1) (Just t2) + = Just (t2 <> t1) + +printUnusedPaths + :: [FilePath] + -> Maybe Text +printUnusedPaths [] + = Nothing +printUnusedPaths ps@(_ : _) + = Just (mconcat (printUnusedPath <$> ps)) + +printUnusedPath + :: FilePath + -> Text +printUnusedPath p + = printMessageIndent (T.pack p) "unused file" + +-- | Print a collection of unused items. +printUnusedItems + :: UnusedItems + -> Maybe Text +printUnusedItems (UnusedItems []) + = Nothing +printUnusedItems (UnusedItems rs@(_ : _)) + = Just (foldMap (uncurry printRangeInfoWith) rs) + +-- | Print a message indicating that no unused code was found. +printNothing + :: Text +printNothing + = T.unlines ["No unused code."] + +printRangeInfoWith + :: Range + -> RangeInfo + -> Text +printRangeInfoWith r i + = printMessageIndent (printRange r) (printRangeInfo i) + +printRangeInfo + :: RangeInfo + -> Text +printRangeInfo (RangeNamed t n) + = T.unwords ["unused", printRangeType t, quote (printQName n)] +printRangeInfo RangeMutual + = "unused mutually recursive definition" + +printRangeType + :: RangeType + -> Text +printRangeType RangeData + = "data type" +printRangeType RangeDefinition + = "definition" +printRangeType RangeImport + = "import" +printRangeType RangeImportItem + = "imported item" +printRangeType RangeModule + = "module" +printRangeType RangeModuleItem + = "module assignment item" +printRangeType RangeOpen + = "open" +printRangeType RangeOpenItem + = "opened item" +printRangeType RangePatternSynonym + = "pattern synonym" +printRangeType RangePostulate + = "postulate" +printRangeType RangeRecord + = "record" +printRangeType RangeRecordConstructor + = "record constructor" +printRangeType RangeVariable + = "variable" + diff --git a/src/Agda/Unused/Types/Access.hs b/src/Agda/Unused/Types/Access.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Types/Access.hs @@ -0,0 +1,55 @@ +{- | +Module: Agda.Unused.Types.Access + +Access modifiers indicating whether an item is public or private. +-} +module Agda.Unused.Types.Access + + ( -- * Definition + + Access(..) + + -- * Interface + + , access + + -- * Conversion + + , fromAccess + + ) where + +import qualified Agda.Syntax.Common + as C + +-- | An access modifier. +data Access where + + Private + :: Access + + Public + :: Access + + deriving Show + +-- | Elimination rule for 'Access'. +access + :: a + -> a + -> Access + -> a +access x _ Private + = x +access _ y Public + = y + +-- | Conversion from Agda access type. +fromAccess + :: C.Access + -> Access +fromAccess (C.PrivateAccess _) + = Private +fromAccess C.PublicAccess + = Public + diff --git a/src/Agda/Unused/Types/Context.hs b/src/Agda/Unused/Types/Context.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Types/Context.hs @@ -0,0 +1,789 @@ +{- | +Module: Agda.Unused.Types.Context + +Definitions and interface for the 'Context' and 'AccessContext' types, which +represent namespaces of definitions. +-} +module Agda.Unused.Types.Context + + ( -- * Definitions + + Item + , Module(Module) + , AccessModule(AccessModule) + , Context + , AccessContext + , accessContextUnion + + -- * Interface + + -- ** Lookup + + , LookupError(..) + , contextLookup + , contextLookupItem + , contextLookupModule + , accessContextLookup + , accessContextLookupModule + , accessContextLookupDefining + , accessContextLookupSpecial + + -- ** Insert + + , contextInsertRange + , contextInsertRangeModule + , contextInsertRangeAll + , accessContextInsertRangeAll + + -- ** Delete + + , contextDelete + , contextDeleteModule + + -- ** Rename + + , contextRename + , contextRenameModule + + -- ** Define + + , accessContextDefine + + -- ** Ranges + + , moduleRanges + , contextRanges + + -- ** Match + + , accessContextMatch + + -- * Construction + + , item + , itemPattern + , itemConstructor + , contextItem + , contextModule + , accessContextItem + , accessContextModule + , accessContextModule' + , accessContextImport + + -- * Conversion + + , fromContext + , toContext + + ) where + +import Agda.Unused.Types.Access + (Access(..)) +import Agda.Unused.Types.Name + (Name, QName(..), matchOperators, stripPrefix) +import Agda.Unused.Types.Range + (Range) +import Agda.Unused.Utils + (mapUpdateKey) + +import Data.Map.Strict + (Map) +import qualified Data.Map.Strict + as Map +import Data.Maybe + (catMaybes) + +-- ## Definitions + +-- | The data associated with a name in context. This includes: +-- +-- - Whether the name is a constructor, pattern synonym, or ordinary definition. +-- - A list of ranges associated with the name, which includes the site of the +-- original definition, as well as any relevant @import@ or @open@ statements. +-- - Alternative syntax for the name, if any. +data Item where + + ItemConstructor + :: ![Range] + -> ![Name] + -> Item + + ItemPattern + :: ![Range] + -> !(Maybe Name) + -> Item + + Item + :: ![Range] + -> !(Maybe Name) + -> Item + + deriving Show + +-- Like 'Item', but with some additional data: +-- +-- - Whether the name is public or private. +-- - Whether the name is currently being defined. +-- +-- Since constructors may be overloaded, a constructor AccessItem may +-- represent multiple constructors, some public and some private. +data AccessItem where + + AccessItemConstructor + -- Private ranges. + :: ![Range] + -- Public ranges. + -> ![Range] + -- Private syntax. + -> ![Name] + -- Public syntax. + -> ![Name] + -> AccessItem + + AccessItemPattern + :: !Access + -> ![Range] + -> !(Maybe Name) + -> AccessItem + + AccessItemSyntax + -- Whether the item is special. + :: !Bool + -> ![Range] + -> AccessItem + + AccessItem + -- Whether we are currently defining this item. + :: !Bool + -> !Access + -> ![Range] + -> !(Maybe Name) + -> AccessItem + + deriving Show + +-- | The data associated with a module in context. This includes: +-- +-- - A list of ranges associated with the module, which includes the site of the +-- original definition, as well as any relevant @import@ or @open@ statements. +-- - The inner context of the module. +data Module + = Module + { moduleRanges' + :: ![Range] + , moduleContext + :: !Context + } deriving Show + +-- | Like 'Module', but also recording whether the module is public or private. +data AccessModule + = AccessModule + { accessModuleAccess + :: !Access + , accessModuleRanges + :: ![Range] + , accessModuleContext + :: !Context + } deriving Show + +-- | A namespace of definitions. Any Agda module produces a 'Context'. +data Context + = Context + { contextItems + :: !(Map Name Item) + , contextModules + :: !(Map Name Module) + } deriving Show + +-- | A namespace of definitions, which may be public or private. Any collection +-- of Agda declarations produces an 'AccessContext', for example. +data AccessContext + = AccessContext + { accessContextItems + :: !(Map Name AccessItem) + , accessContextModules + :: !(Map Name AccessModule) + , accessContextImports + :: !(Map QName Context) + } deriving Show + +-- | If both items are constructors, collect the private and public ranges for +-- both. Otherwise, return the second item. +instance Semigroup AccessItem where + AccessItemConstructor rs1 ss1 ts1 us1 <> AccessItemConstructor rs2 ss2 ts2 us2 + = AccessItemConstructor (rs1 <> rs2) (ss1 <> ss2) (ts1 <> ts2) (us1 <> us2) + _ <> i + = i + +-- | Prefer values from second context. +instance Semigroup Context where + Context is1 ms1 <> Context is2 ms2 + = Context (is2 <> is1) (ms2 <> ms1) + +-- | Prefer values from second access context. +instance Semigroup AccessContext where + AccessContext is1 ms1 js1 <> AccessContext is2 ms2 js2 + = AccessContext (Map.unionWith (<>) is1 is2) (ms2 <> ms1) (js2 <> js1) + +instance Monoid Context where + mempty + = Context mempty mempty + +instance Monoid AccessContext where + mempty + = AccessContext mempty mempty mempty + +-- Ensure public names are not shadowed by private names. +accessItemUnion + :: AccessItem + -> AccessItem + -> AccessItem +accessItemUnion i@(AccessItem _ Public _ _) (AccessItemConstructor _ [] _ _) + = i +accessItemUnion i@(AccessItem _ Public _ _) (AccessItem _ Private _ _) + = i +accessItemUnion i1 i2 + = i1 <> i2 + +-- Ensure public names are not shadowed by private names. +accessModuleUnion + :: AccessModule + -> AccessModule + -> AccessModule +accessModuleUnion m1@(AccessModule Public _ _) (AccessModule Private _ _) + = m1 +accessModuleUnion _ m2 + = m2 + +-- | Like '(<>)', but public items take precedence over private items. This is +-- important when combining contexts from successive declarations; for example: +-- +-- @ +-- module M where +-- +-- postulate +-- A : Set +-- +-- module N where +-- +-- postulate +-- A : Set +-- +-- open M +-- +-- x : N.A +-- x = ? +-- @ +-- +-- This code type-checks, and the identifier @N.A@ refers to the postulate +-- declared in the definition of @N@, not the definition opened from @M@. +accessContextUnion + :: AccessContext + -> AccessContext + -> AccessContext +accessContextUnion (AccessContext is1 ms1 js1) (AccessContext is2 ms2 js2) + = AccessContext + { accessContextItems + = Map.unionWith accessItemUnion is1 is2 + , accessContextModules + = Map.unionWith accessModuleUnion ms1 ms2 + , accessContextImports + = js2 <> js1 + } + +-- ## Interface + +-- ### Lookup + +-- | A description of failure for an 'AccessContext' lookup. +data LookupError where + + LookupNotFound + :: LookupError + + LookupAmbiguous + :: LookupError + + deriving Show + +-- | Get the ranges for the given name, or 'Nothing' if not in context. +contextLookup + :: QName + -> Context + -> Maybe [Range] +contextLookup n c + = itemRanges <$> contextLookupItem n c + +-- | Get the inner module for the given name, or 'Nothing' if not in context. +contextLookupModule + :: QName + -> Context + -> Maybe Module +contextLookupModule (QName n) (Context _ ms) + = Map.lookup n ms +contextLookupModule (Qual n ns) (Context _ ms) + = Map.lookup n ms >>= contextLookupModule ns . moduleContext + +-- | Get the item for the given name, or 'Nothing' if not in context. +contextLookupItem + :: QName + -> Context + -> Maybe Item +contextLookupItem (QName n) (Context is _) + = Map.lookup n is +contextLookupItem (Qual n ns) (Context _ ms) + = Map.lookup n ms >>= contextLookupItem ns . moduleContext + +-- | Get the ranges for the given name, or produce a 'LookupError'. +accessContextLookup + :: QName + -> AccessContext + -> Either LookupError [Range] +accessContextLookup n c@(AccessContext _ _ is) + = contextLookup n (toContext' c) + <|> Map.mapWithKey (accessContextLookupImport n) is + +-- | Get the inner module for the given name, or produce a 'LookupError'. +accessContextLookupModule + :: QName + -> AccessContext + -> Either LookupError Module +accessContextLookupModule n c@(AccessContext _ _ is) + = contextLookupModule n (toContext' c) + <|> Map.mapWithKey (accessContextLookupModuleImport n) is + +accessContextLookupImport + :: QName + -> QName + -> Context + -> Maybe [Range] +accessContextLookupImport n i c + = stripPrefix i n >>= flip contextLookup c + +accessContextLookupModuleImport + :: QName + -> QName + -> Context + -> Maybe Module +accessContextLookupModuleImport n i c | n == i + = Just (Module [] c) +accessContextLookupModuleImport n i c + = stripPrefix i n >>= flip contextLookupModule c + +(<|>) + :: Maybe a + -> Map k (Maybe a) + -> Either LookupError a +x <|> xs + = resolve (catMaybes (x : Map.elems xs)) + +resolve + :: [a] + -> Either LookupError a +resolve [] + = Left LookupNotFound +resolve (x : []) + = Right x +resolve (_ : _ : _) + = Left LookupAmbiguous + +accessItemDefining + :: AccessItem + -> Bool +accessItemDefining (AccessItem b _ _ _) + = b +accessItemDefining _ + = False + +-- | Like 'accessContextLookup', but also return a boolean indicating whether we +-- are currently defining the referenced item. +accessContextLookupDefining + :: QName + -> AccessContext + -> Either LookupError (Bool, [Range]) +accessContextLookupDefining (QName n) (AccessContext is _ _) + = maybe + (Left LookupNotFound) + (\i -> Right (accessItemDefining i, accessItemRanges i)) + (Map.lookup n is) +accessContextLookupDefining n@(Qual _ _) c + = (,) False <$> accessContextLookup n c + +itemSpecial + :: Item + -> Bool +itemSpecial (ItemConstructor _ _) + = True +itemSpecial (ItemPattern _ _) + = True +itemSpecial (Item _ _) + = False + +-- | Determine whether a name represents a constructor or pattern synonym. +-- Return 'Nothing' if the name is not in context. +accessContextLookupSpecial + :: QName + -> AccessContext + -> Maybe Bool +accessContextLookupSpecial n c + = itemSpecial <$> contextLookupItem n (toContext' c) + +-- ### Insert + +itemInsertRange + :: Range + -> Item + -> Item +itemInsertRange r (ItemConstructor rs ss) + = ItemConstructor (r : rs) ss +itemInsertRange r (ItemPattern rs s) + = ItemPattern (r : rs) s +itemInsertRange r (Item rs s) + = Item (r : rs) s + +accessItemInsertRange + :: Range + -> AccessItem + -> AccessItem +accessItemInsertRange r (AccessItemConstructor rs1 rs2 ns1 ns2) + = AccessItemConstructor (r : rs1) (r : rs2) ns1 ns2 +accessItemInsertRange r (AccessItemPattern a rs n) + = AccessItemPattern a (r : rs) n +accessItemInsertRange r (AccessItemSyntax b rs) + = AccessItemSyntax b (r : rs) +accessItemInsertRange r (AccessItem b a rs n) + = AccessItem b a (r : rs) n + +-- | Insert a range for the given name, if present. +contextInsertRange + :: Name + -> Range + -> Context + -> Context +contextInsertRange n r (Context is ms) + = Context (Map.adjust (itemInsertRange r) n is) ms + +-- | Insert a range for all names in the given module, if present. +contextInsertRangeModule + :: Name + -> Range + -> Context + -> Context +contextInsertRangeModule n r (Context is ms) + = Context is (Map.adjust (moduleInsertRangeAll r) n ms) + +moduleInsertRangeAll + :: Range + -> Module + -> Module +moduleInsertRangeAll r (Module rs c) + = Module (r : rs) (contextInsertRangeAll r c) + +accessModuleInsertRangeAll + :: Range + -> AccessModule + -> AccessModule +accessModuleInsertRangeAll r (AccessModule a rs c) + = AccessModule a (r : rs) (contextInsertRangeAll r c) + +-- | Insert a range for all names in a context. +contextInsertRangeAll + :: Range + -> Context + -> Context +contextInsertRangeAll r (Context is ms) + = Context + (itemInsertRange r <$> is) + (moduleInsertRangeAll r <$> ms) + +-- | Insert a range for all names in an access context. +accessContextInsertRangeAll + :: Range + -> AccessContext + -> AccessContext +accessContextInsertRangeAll r (AccessContext is ms js) + = AccessContext + (accessItemInsertRange r <$> is) + (accessModuleInsertRangeAll r <$> ms) js + +-- ### Delete + +-- | Delete an item from the context. +contextDelete + :: Name + -> Context + -> Context +contextDelete n (Context is ms) + = Context (Map.delete n is) ms + +-- | Delete a module from the context. +contextDeleteModule + :: Name + -> Context + -> Context +contextDeleteModule n (Context is ms) + = Context is (Map.delete n ms) + +-- ### Rename + +-- | Rename an item, if present. +contextRename + :: Name + -> Name + -> Context + -> Context +contextRename n n' (Context is ms) + = Context (mapUpdateKey n n' is) ms + +-- | Rename a module, if present. +contextRenameModule + :: Name + -> Name + -> Context + -> Context +contextRenameModule n n' (Context is ms) + = Context is (mapUpdateKey n n' ms) + +-- ### Define + +accessItemDefine + :: AccessItem + -> AccessItem +accessItemDefine (AccessItem _ a rs s) + = AccessItem True a rs s +accessItemDefine i + = i + +-- | Mark an existing name as in process of being defined. +accessContextDefine + :: Name + -> AccessContext + -> AccessContext +accessContextDefine n (AccessContext is ms js) + = AccessContext (Map.adjust accessItemDefine n is) ms js + +-- ### Ranges + +itemRanges + :: Item + -> [Range] +itemRanges (ItemConstructor rs _) + = rs +itemRanges (ItemPattern rs _) + = rs +itemRanges (Item rs _) + = rs + +accessItemRanges + :: AccessItem + -> [Range] +accessItemRanges + = itemRanges . toItem' + +-- | Get all ranges associated with names in the given module, including ranges +-- associated with the module itself. +moduleRanges + :: Module + -> [Range] +moduleRanges (Module rs c) + = rs <> contextRanges c + +-- | Get all ranges associated with names in the given context. +contextRanges + :: Context + -> [Range] +contextRanges (Context is ms) + = concat (itemRanges <$> Map.elems is) + <> concat (moduleRanges <$> Map.elems ms) + +-- ### Match + +-- | Find all operators matching the given list of tokens. +accessContextMatch + :: [String] + -> AccessContext + -> [Name] +accessContextMatch ss (AccessContext is _ _) + = matchOperators ss (Map.keys is) + +-- ## Construction + +-- | Construct an 'Item' representing an ordinary definition. +item + :: [Range] + -> Maybe Name + -> Item +item + = Item + +-- | Construct an 'Item' representing a pattern synonym. +itemPattern + :: [Range] + -> Maybe Name + -> Item +itemPattern + = ItemPattern + +-- | Construct an 'Item' representing a constructor. +itemConstructor + :: [Range] + -> Maybe Name + -> Item +itemConstructor rs Nothing + = ItemConstructor rs [] +itemConstructor rs (Just s) + = ItemConstructor rs [s] + +-- | Construct a 'Context' with a single item. +contextItem + :: Name + -> Item + -> Context +contextItem n i + = Context (Map.singleton n i) mempty + +-- | Construct a 'Context' with a single module. +contextModule + :: Name + -> Module + -> Context +contextModule n m + = Context mempty (Map.singleton n m) + +-- | Construct an 'AccessContext' with a single item, along with the relevant +-- syntax item if applicable. +accessContextItem + :: Name + -> Access + -> Item + -> AccessContext +accessContextItem n a i + = fromContext a (contextItem n i) + +-- | Construct an 'AccessContext' with a single access module. +accessContextModule + :: Name + -> AccessModule + -> AccessContext +accessContextModule n m + = AccessContext mempty (Map.singleton n m) mempty + +-- | Like 'accessContextModule', but taking an access context. We convert the +-- given access context to an ordinary context using 'toContext': +-- +-- @ +-- accessContextModule' n a rs c +-- = accessContextModule n (AccessModule a rs (toContext c)) +-- @ +accessContextModule' + :: Name + -> Access + -> [Range] + -> AccessContext + -> AccessContext +accessContextModule' n a rs c + = accessContextModule n (AccessModule a rs (toContext c)) + +-- | Construct an access context with a single import. +accessContextImport + :: QName + -> Context + -> AccessContext +accessContextImport n c + = AccessContext mempty mempty (Map.singleton n c) + +-- ## Conversion + +fromItem + :: Access + -> Item + -> AccessItem +fromItem Private (ItemConstructor rs ss) + = AccessItemConstructor rs [] ss [] +fromItem Public (ItemConstructor rs ss) + = AccessItemConstructor [] rs [] ss +fromItem a (ItemPattern rs s) + = AccessItemPattern a rs s +fromItem a (Item rs s) + = AccessItem False a rs s + +fromItemSyntax + :: Item + -> [(Name, AccessItem)] +fromItemSyntax (ItemConstructor rs ss) + = flip (,) (AccessItemSyntax True rs) <$> ss +fromItemSyntax (ItemPattern rs s) + = flip (,) (AccessItemSyntax True rs) <$> maybe [] (: []) s +fromItemSyntax (Item rs s) + = flip (,) (AccessItemSyntax False rs) <$> maybe [] (: []) s + +toItem + :: AccessItem + -> Maybe Item +toItem (AccessItemConstructor _ rs@(_ : _) _ ss) + = Just (ItemConstructor rs ss) +toItem (AccessItemPattern Public rs s) + = Just (ItemPattern rs s) +toItem (AccessItem _ Public rs s) + = Just (Item rs s) +toItem _ + = Nothing + +toItem' + :: AccessItem + -> Item +toItem' (AccessItemConstructor rs1 rs2 ss1 ss2) + = ItemConstructor (rs1 <> rs2) (ss1 <> ss2) +toItem' (AccessItemPattern _ rs s) + = ItemPattern rs s +toItem' (AccessItemSyntax _ rs) + = Item rs Nothing +toItem' (AccessItem _ _ rs s) + = Item rs s + +fromModule + :: Access + -> Module + -> AccessModule +fromModule a (Module rs c) + = AccessModule a rs c + +toModule + :: AccessModule + -> Maybe Module +toModule (AccessModule Private _ _) + = Nothing +toModule (AccessModule Public rs c) + = Just (Module rs c) + +toModule' + :: AccessModule + -> Module +toModule' (AccessModule _ rs c) + = Module rs c + +-- | Convert a 'Context' to 'AccessContext'. Give all items the given access. +fromContext + :: Access + -> Context + -> AccessContext +fromContext a (Context is ms) + = AccessContext + (Map.map (fromItem a) is <> Map.fromList (Map.elems is >>= fromItemSyntax)) + (Map.map (fromModule a) ms) + mempty + +-- | Convert an 'AccessContext' to 'Context'. Discard private items and imports. +toContext + :: AccessContext + -> Context +toContext (AccessContext is ms _) + = Context (Map.mapMaybe toItem is) (Map.mapMaybe toModule ms) + +-- Like 'toContext`, but keep private items. +toContext' + :: AccessContext + -> Context +toContext' (AccessContext is ms _) + = Context (Map.map toItem' is) (Map.map toModule' ms) + diff --git a/src/Agda/Unused/Types/Name.hs b/src/Agda/Unused/Types/Name.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Types/Name.hs @@ -0,0 +1,235 @@ +{- | +Module: Agda.Unused.Types.Name + +Names and qualified names. +-} +module Agda.Unused.Types.Name + + ( -- * Definitions + + NamePart(..) + , Name(..) + , QName(..) + + -- * Interface + + , nameIds + , isBuiltin + , stripPrefix + + -- * Conversion + + , fromName + , fromNameRange + , fromQName + , fromQNameRange + , fromAsName + + -- * Paths + + , qNamePath + , pathQName + + -- * Match + + , matchOperators + + ) where + +import Agda.Unused.Utils + (stripSuffix) + +import Agda.Syntax.Concrete + (AsName, AsName'(..)) +import Agda.Syntax.Concrete.Name + (NamePart(..)) +import qualified Agda.Syntax.Concrete.Name + as N +import Agda.Syntax.Position + (Range) +import Data.List + (isSubsequenceOf) +import qualified Data.List + as List +import Data.Maybe + (mapMaybe) +import System.FilePath + ((), (<.>), splitDirectories) + +-- ## Definitions + +-- | An unqualified name, represented as a list of name parts. +newtype Name + = Name + { nameParts + :: [NamePart] + } deriving (Eq, Ord, Show) + +-- | A qualified name. +data QName where + + QName + :: !Name + -> QName + + Qual + :: !Name + -> !QName + -> QName + + deriving (Eq, Ord, Show) + +-- ## Interface + +-- | Get the non-hole parts of a 'Name'. +nameIds + :: Name + -> [String] +nameIds (Name ps) + = mapMaybe namePartId ps + +namePartId + :: NamePart + -> Maybe String +namePartId Hole + = Nothing +namePartId (Id s) + = Just s + +isOperator + :: Name + -> Bool +isOperator (Name []) + = False +isOperator (Name (_ : [])) + = False +isOperator (Name (_ : _ : _)) + = True + +-- | Determine if a module name represents a builtin module. +isBuiltin + :: QName + -> Bool +isBuiltin (Qual (Name [Id "Agda"]) _) + = True +isBuiltin _ + = False + +-- | If the first module name is a prefix of the second module name, then strip +-- the prefix, otherwise return 'Nothing'. +stripPrefix + :: QName + -- ^ The prefix to strip + -> QName + -> Maybe QName +stripPrefix (QName m) (Qual n ns) | m == n + = Just ns +stripPrefix (Qual m ms) (Qual n ns) | m == n + = stripPrefix ms ns +stripPrefix _ _ + = Nothing + +-- ## Conversion + +-- | Conversion from Agda name type. +fromName + :: N.Name + -> Maybe Name +fromName (N.NoName _ _) + = Nothing +fromName (N.Name _ _ n) + = Just (Name n) + +-- | Like 'fromName', but also return a 'Range'. +fromNameRange + :: N.Name + -> Maybe (Range, Name) +fromNameRange (N.NoName _ _) + = Nothing +fromNameRange (N.Name r _ n) + = Just (r, Name n) + +-- | Conversion from Agda qualified name type. +fromQName + :: N.QName + -> Maybe QName +fromQName (N.QName n) + = QName <$> fromName n +fromQName (N.Qual n ns) + = Qual <$> fromName n <*> fromQName ns + +-- | Like 'fromQName', but also return a 'Range'. +fromQNameRange + :: N.QName + -> Maybe (Range, QName) +fromQNameRange (N.QName n) + = fmap QName <$> fromNameRange n +fromQNameRange (N.Qual n ns) + = fmap . Qual <$> fromName n <*> fromQNameRange ns + +-- | Conversion from Agda as-name type. +fromAsName + :: AsName + -> Maybe Name +fromAsName (AsName (Left _) _) + = Nothing +fromAsName (AsName (Right n) _) + = fromName n + +-- ## Paths + +namePath + :: Name + -> String +namePath (Name ps) + = mconcat (show <$> ps) + +-- | Convert a module name to a 'FilePath'. +qNamePath + :: QName + -> FilePath +qNamePath (QName n) + = namePath n <.> "agda" +qNamePath (Qual n ns) + = namePath n qNamePath ns + +-- | Convert a 'FilePath' to a module name. +pathQName + :: FilePath + -- ^ The project root directory. + -> FilePath + -- ^ The path to the module. + -> Maybe QName +pathQName p p' + = List.stripPrefix (splitDirectories p) (splitDirectories p') + >>= pathQNameRelative + +pathQNameRelative + :: [String] + -> Maybe QName +pathQNameRelative [] + = Nothing +pathQNameRelative [n] + = QName <$> pathName n +pathQNameRelative (n : ns@(_ : _)) + = Qual (Name [Id n]) <$> pathQNameRelative ns + +pathName + :: String + -> Maybe Name +pathName n + = Name . (: []) . Id <$> stripSuffix ".agda" n + +-- ## Match + +-- | Given a string of tokens found in a raw application, filter the given list +-- of names by whether each name's identifiers appear in order. +matchOperators + :: [String] + -- ^ A string of tokens found in a raw application. + -> [Name] + -- ^ A list of names to consider. + -> [Name] +matchOperators ss + = filter (\n -> isOperator n && isSubsequenceOf (nameIds n) ss) + diff --git a/src/Agda/Unused/Types/Range.hs b/src/Agda/Unused/Types/Range.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Types/Range.hs @@ -0,0 +1,107 @@ +{- | +Module: Agda.Unused.Types.Range + +Location ranges of Agda code files. +-} +module Agda.Unused.Types.Range + + ( -- * Definitions + + Range + , Range'(..) + , RangeType(..) + , RangeInfo(..) + + -- * Interface + + , getRange + , rangeContains + + ) where + +import Agda.Unused.Types.Name + (QName) + +import Agda.Syntax.Position + (PositionWithoutFile, Range, Range'(..), getRange, rEnd', rStart') + +-- ## Definitions + +-- | The type of item found at a named range. +data RangeType where + + RangeData + :: RangeType + + RangeDefinition + :: RangeType + + RangeImport + :: RangeType + + RangeImportItem + :: RangeType + + RangeModule + :: RangeType + + RangeModuleItem + :: RangeType + + RangeOpen + :: RangeType + + RangeOpenItem + :: RangeType + + RangePatternSynonym + :: RangeType + + RangePostulate + :: RangeType + + RangeRecord + :: RangeType + + RangeRecordConstructor + :: RangeType + + RangeVariable + :: RangeType + + deriving (Eq, Ord, Show) + +-- | Information associated with an item found at a certain range. +data RangeInfo where + + RangeNamed + :: !RangeType + -> !QName + -> RangeInfo + + RangeMutual + :: RangeInfo + + deriving (Eq, Ord, Show) + +-- ## Interface + +-- | Determine whether the first range contains the second. +rangeContains + :: Range + -> Range + -> Bool +rangeContains r1 r2 + = rangeContains' (rStart' r1) (rEnd' r1) (rStart' r2) (rEnd' r2) + +rangeContains' + :: Maybe PositionWithoutFile + -> Maybe PositionWithoutFile + -> Maybe PositionWithoutFile + -> Maybe PositionWithoutFile + -> Bool +rangeContains' (Just s1) (Just e1) (Just s2) (Just e2) + = s1 <= s2 && e1 >= e2 +rangeContains' _ _ _ _ + = False + diff --git a/src/Agda/Unused/Types/Root.hs b/src/Agda/Unused/Types/Root.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Types/Root.hs @@ -0,0 +1,53 @@ +{- | +Module: Agda.Unused.Types.Root + +Data types representing public entry points for an Agda project. +-} +module Agda.Unused.Types.Root + + ( -- * Types + + Root(..) + , Roots(..) + + -- * Construction + + , fromList + + ) where + +import Agda.Unused.Types.Name + (QName) + +import Data.Either + (lefts, rights) + +-- | A public entry point for an Agda project. +data Root + = Root + { rootFile + :: QName + -- ^ A module name. + , rootNames + :: Maybe [QName] + -- ^ Identifier names. An value of 'Nothing' represents all names in scope. + } deriving Show + +-- | A collection of public entry points for an Agda project. +data Roots + = Roots + { rootsCheck + :: [Root] + -- ^ Modules to check. + , rootsIgnore + :: [QName] + -- ^ Modules to ignore. + } deriving Show + +-- | Construct a collection of roots from a list of elements. +fromList + :: [Either QName Root] + -> Roots +fromList rs + = Roots (rights rs) (lefts rs) + diff --git a/src/Agda/Unused/Utils.hs b/src/Agda/Unused/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Agda/Unused/Utils.hs @@ -0,0 +1,95 @@ +{- | +Module: Agda.Unused.Utils + +Utility functions for 'Maybe', 'Either', and 'Map' types. +-} +module Agda.Unused.Utils + + ( -- * Maybe + + liftMaybe + + -- * Either + + , mapLeft + + -- * List + + , stripSuffix + + -- * Map + + , mapDeletes + , mapUpdateKey + + ) where + +import Control.Monad.Except + (MonadError, throwError) +import Data.List + (stripPrefix) +import Data.Map.Strict + (Map) +import qualified Data.Map.Strict + as Map + +-- ## Maybe + +-- | Lift a 'Maybe' type to an error monad by throwing a fixed error. +liftMaybe + :: MonadError e m + => e + -> Maybe a + -> m a +liftMaybe e Nothing + = throwError e +liftMaybe _ (Just x) + = pure x + +-- ## Either + +-- | Map the left component of an 'Either' type. +mapLeft + :: (e -> f) + -> Either e a + -> Either f a +mapLeft f (Left e) + = Left (f e) +mapLeft _ (Right x) + = Right x + +-- ## List + +-- | Drop the given suffix from a list. +stripSuffix + :: Eq a + => [a] + -> [a] + -> Maybe [a] +stripSuffix xs ys + = reverse <$> stripPrefix (reverse xs) (reverse ys) + +-- ## Map + +-- | Delete a list of keys from a map. +mapDeletes + :: Ord k + => [k] + -> Map k a + -> Map k a +mapDeletes ks xs + = foldr Map.delete xs ks + +-- | Modify a key of a map. +-- +-- - If the source key is not present, do nothing. +-- - If the target key is already present, overwrite it. +mapUpdateKey + :: Ord k + => k + -> k + -> Map k a + -> Map k a +mapUpdateKey k k' m + = maybe m (\x -> Map.insert k' x (Map.delete k m)) (Map.lookup k m) + diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,766 @@ +module Main where + +import Agda.Unused + (Unused(..), UnusedItems(..)) +import Agda.Unused.Check + (checkUnused, checkUnusedLocal) +import Agda.Unused.Monad.Error + (Error) +import Agda.Unused.Print + (printUnusedItems) +import Agda.Unused.Types.Access + (Access(..)) +import Agda.Unused.Types.Name + (Name(..), NamePart(..), QName(..)) +import Agda.Unused.Types.Range + (RangeInfo(..)) +import qualified Agda.Unused.Types.Range + as R +import Agda.Unused.Types.Root + (Root(..), Roots(..)) + +import Data.Maybe + (mapMaybe) +import qualified Data.Set + as Set +import Data.Text + (Text) +import qualified Data.Text + as T +import System.FilePath + (()) +import Test.Hspec + (Expectation, Spec, describe, expectationFailure, hspec, it, shouldBe, + shouldSatisfy) + +import Paths_agda_unused + (getDataFileName) + +-- ## Names + +newtype PrivateName + = PrivateName + { privateQName + :: QName + } deriving Show + +class IsName a where + + name + :: a + -> QName + + access + :: a + -> Access + +instance IsName QName where + + name + = id + + access _ + = Public + +instance IsName String where + + name n + = QName (Name [Id n]) + + access _ + = Public + +instance IsName PrivateName where + + name + = privateQName + + access _ + = Private + +private + :: IsName a + => a + -> PrivateName +private n + = PrivateName (name n) + +land + :: QName +land + = QName (Name [Hole, Id "&&", Hole]) + +bind + :: QName +bind + = QName (Name [Hole, Id ">>=", Hole]) + +bind_ + :: QName +bind_ + = QName (Name [Hole, Id ">>", Hole]) + +agdaBuiltinBool + :: QName +agdaBuiltinBool + = Qual (Name [Id "Agda"]) + $ Qual (Name [Id "Builtin"]) + $ QName (Name [Id "Bool"]) + +-- ## Ranges + +data RangeType where + + Data + :: RangeType + + Definition + :: RangeType + + Import + :: RangeType + + ImportItem + :: RangeType + + Module + :: RangeType + + ModuleItem + :: RangeType + + Mutual + :: RangeType + + Open + :: RangeType + + OpenItem + :: RangeType + + PatternSynonym + :: RangeType + + Postulate + :: RangeType + + Record + :: RangeType + + RecordConstructor + :: RangeType + + Variable + :: RangeType + + deriving Show + +(~:) + :: IsName a + => a + -> RangeType + -> (Access, RangeInfo) +n ~: Data + = (access n, RangeNamed R.RangeData (name n)) +n ~: Definition + = (access n, RangeNamed R.RangeDefinition (name n)) +n ~: Import + = (access n, RangeNamed R.RangeImport (name n)) +n ~: ImportItem + = (access n, RangeNamed R.RangeImportItem (name n)) +n ~: Module + = (access n, RangeNamed R.RangeModule (name n)) +n ~: ModuleItem + = (access n, RangeNamed R.RangeModuleItem (name n)) +n ~: Mutual + = (access n, RangeMutual) +n ~: Open + = (access n, RangeNamed R.RangeOpen (name n)) +n ~: OpenItem + = (access n, RangeNamed R.RangeOpenItem (name n)) +n ~: PatternSynonym + = (access n, RangeNamed R.RangePatternSynonym (name n)) +n ~: Postulate + = (access n, RangeNamed R.RangePostulate (name n)) +n ~: Record + = (access n, RangeNamed R.RangeRecord (name n)) +n ~: RecordConstructor + = (access n, RangeNamed R.RangeRecordConstructor (name n)) +n ~: Variable + = (access n, RangeNamed R.RangeVariable (name n)) + +-- ## Expectations + +testCheck + :: Test + -> Expectation +testCheck n = do + path + <- testPath n + unused + <- checkUnused path (Roots [Root (name (testModule n)) (Just [])] []) + unusedLocal + <- checkUnusedLocal path (name (testModule n)) + _ + <- testUnused (unusedItems <$> unused) (snd <$> testResult n) + _ + <- testUnused unusedLocal (mapMaybe privateMay (testResult n)) + pure () + +testCheckExample + :: Expectation +testCheckExample = do + path + <- getDataFileName "data/test/example" + unusedLocal + <- checkUnusedLocal path (name "Test") + _ + <- testUnusedExample unusedLocal + pure () + +testUnused + :: Either Error UnusedItems + -> [RangeInfo] + -> Expectation +testUnused (Left _) _ + = expectationFailure "" +testUnused (Right (UnusedItems is)) rs + = Set.fromList (snd <$> is) `shouldBe` Set.fromList rs + +testUnusedExample + :: Either Error UnusedItems + -> Expectation +testUnusedExample (Left _) + = expectationFailure "" +testUnusedExample (Right is) + = testUnusedOutput (T.lines <$> printUnusedItems is) + +testUnusedOutput + :: Maybe [Text] + -> Expectation +testUnusedOutput (Just [t0, t1, t2, t3, t4, t5]) + = (t0 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:4,23-27")) + >> (t1 `shouldBe` T.pack " unused imported item ‘true’") + >> (t2 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:5,1-30")) + >> (t3 `shouldBe` T.pack " unused import ‘Agda.Builtin.Unit’") + >> (t4 `shouldSatisfy` T.isSuffixOf (T.pack "/Test.agda:11,9-10")) + >> (t5 `shouldBe` T.pack " unused variable ‘x’") +testUnusedOutput _ + = expectationFailure "" + +privateMay + :: (Access, a) + -> Maybe a +privateMay (Private, x) + = Just x +privateMay (Public, _) + = Nothing + +-- ## Tests + +data Test where + + Pattern + :: !PatternTest + -> Test + + Expression + :: !ExpressionTest + -> Test + + Declaration + :: !DeclarationTest + -> Test + + deriving Show + +data PatternTest where + + IdentP + :: PatternTest + + OpAppP + :: PatternTest + + AsP + :: PatternTest + + deriving Show + +data ExpressionTest where + + WithApp + :: ExpressionTest + + Lam + :: ExpressionTest + + ExtendedLam + :: ExpressionTest + + Pi + :: ExpressionTest + + Let + :: ExpressionTest + + DoBlock1 + :: ExpressionTest + + DoBlock2 + :: ExpressionTest + + DoBlock3 + :: ExpressionTest + + DoBlock4 + :: ExpressionTest + + deriving Show + +data DeclarationTest where + + TypeSig + :: DeclarationTest + + FunClause + :: DeclarationTest + + Data' + :: DeclarationTest + + Record' + :: DeclarationTest + + Syntax + :: DeclarationTest + + PatternSyn + :: DeclarationTest + + Mutual1 + :: DeclarationTest + + Mutual2 + :: DeclarationTest + + Abstract + :: DeclarationTest + + Private' + :: DeclarationTest + + Postulate' + :: DeclarationTest + + Open' + :: DeclarationTest + + Import' + :: DeclarationTest + + ModuleMacro + :: DeclarationTest + + Module' + :: DeclarationTest + + deriving Show + +testDir + :: Test + -> FilePath +testDir (Pattern _) + = "pattern" +testDir (Expression _) + = "expression" +testDir (Declaration _) + = "declaration" + +testPath + :: Test + -> IO FilePath +testPath n + = getDataFileName ("data/test" testDir n) + +testModule + :: Test + -> String +testModule (Pattern IdentP) + = "IdentP" +testModule (Pattern OpAppP) + = "OpAppP" +testModule (Pattern AsP) + = "AsP" +testModule (Expression WithApp) + = "WithApp" +testModule (Expression Lam) + = "Lam" +testModule (Expression ExtendedLam) + = "ExtendedLam" +testModule (Expression Pi) + = "Pi" +testModule (Expression Let) + = "Let" +testModule (Expression DoBlock1) + = "DoBlock1" +testModule (Expression DoBlock2) + = "DoBlock2" +testModule (Expression DoBlock3) + = "DoBlock3" +testModule (Expression DoBlock4) + = "DoBlock4" +testModule (Declaration TypeSig) + = "TypeSig" +testModule (Declaration FunClause) + = "FunClause" +testModule (Declaration Data') + = "Data" +testModule (Declaration Record') + = "Record" +testModule (Declaration Syntax) + = "Syntax" +testModule (Declaration PatternSyn) + = "PatternSyn" +testModule (Declaration Mutual1) + = "Mutual1" +testModule (Declaration Mutual2) + = "Mutual2" +testModule (Declaration Abstract) + = "Abstract" +testModule (Declaration Private') + = "Private" +testModule (Declaration Postulate') + = "Postulate" +testModule (Declaration Open') + = "Open" +testModule (Declaration Import') + = "Import" +testModule (Declaration ModuleMacro) + = "ModuleMacro" +testModule (Declaration Module') + = "Module" + +testResult + :: Test + -> [(Access, RangeInfo)] +testResult n + = case n of + + Pattern IdentP -> + [ private "y" + ~: Variable + , "f" + ~: Definition + , "g" + ~: Definition + ] + + Pattern OpAppP -> + [ land + ~: Definition + ] + + Pattern AsP -> + [ private "y" + ~: Variable + , private "z" + ~: Variable + , private "w" + ~: Variable + , private "z'" + ~: Variable + , private "w'" + ~: Variable + , "f" + ~: Definition + , "g" + ~: Definition + ] + + Expression WithApp -> + [ "f" + ~: Definition + , "g" + ~: Definition + ] + + Expression Lam -> + [ private "y" + ~: Variable + , private "y'" + ~: Variable + , "f" + ~: Definition + , "g" + ~: Definition + ] + + Expression ExtendedLam -> + [ private "x" + ~: Variable + , "f" + ~: Definition + ] + + Expression Pi -> + [ private "y" + ~: Variable + , private "w" + ~: Variable + , "f" + ~: Definition + ] + + Expression Let -> + [ private "z" + ~: Definition + , "f" + ~: Definition + ] + + Expression DoBlock1 -> + [ private "z" + ~: Variable + , "f" + ~: Definition + ] + + Expression DoBlock2 -> + [ bind_ + ~: Definition + , "f" + ~: Definition + ] + + Expression DoBlock3 -> + [ bind + ~: Definition + , "f" + ~: Definition + ] + + Expression DoBlock4 -> + [ bind + ~: Definition + , bind_ + ~: Definition + , "f" + ~: Definition + ] + + Declaration TypeSig -> + [ "g" + ~: Definition + , "h" + ~: Definition + ] + + Declaration FunClause -> + [ private "z" + ~: Definition + , "f" + ~: Definition + , "snoc" + ~: Definition + ] + + Declaration Data' -> + [ "D" + ~: Data + ] + + Declaration Record' -> + [ "B" + ~: Record + , "c" + ~: RecordConstructor + , "x" + ~: Definition + , "y" + ~: Definition + ] + + Declaration Syntax -> + [ "p1" + ~: Postulate + , "p1'" + ~: Postulate + ] + + Declaration PatternSyn -> + [ "q" + ~: PatternSynonym + , "f" + ~: Definition + , "g" + ~: Definition + ] + + Declaration Mutual1 -> + [ "_" + ~: Mutual + ] + + Declaration Mutual2 -> + [ "is-even'" + ~: Definition + ] + + Declaration Abstract -> + [ "g" + ~: Definition + , "h" + ~: Definition + ] + + Declaration Private' -> + [ private "g" + ~: Definition + , private "h" + ~: Definition + ] + + Declaration Postulate' -> + [ "g" + ~: Postulate + , "h" + ~: Definition + ] + + Declaration Open' -> + [ private "N" + ~: Open + , private "P" + ~: Open + , "Q" + ~: Module + , private "x'" + ~: OpenItem + , "v" + ~: Definition + , "y" + ~: Definition + ] + + Declaration Import' -> + [ private agdaBuiltinBool + ~: Import + , private "tt" + ~: ImportItem + , "A" + ~: Definition + ] + + Declaration ModuleMacro -> + [ private "x" + ~: Variable + , "Q" + ~: Module + , "A'" + ~: ModuleItem + , "C" + ~: Definition + , "D" + ~: Definition + , "y" + ~: Definition + ] + + Declaration Module' -> + [ "O" + ~: Module + , "P" + ~: Module + , "x" + ~: Definition + ] + +-- ## Main + +main + :: IO () +main + = hspec testAll + +testAll + :: Spec +testAll + = describe "checkUnused" + $ testPattern + >> testExpression + >> testDeclaration + >> testExample + +testPattern + :: Spec +testPattern + = describe "patterns" + $ it "checks identifiers (IdentP)" + (testCheck (Pattern IdentP)) + >> it "checks operator applications (OpAppP)" + (testCheck (Pattern OpAppP)) + >> it "checks as-patterns (AsP)" + (testCheck (Pattern AsP)) + +testExpression + :: Spec +testExpression + = describe "expressions" + $ it "checks with-applications (WithApp)" + (testCheck (Expression WithApp)) + >> it "checks lambdas (Lam)" + (testCheck (Expression Lam)) + >> it "checks extended lambdas (ExtendedLam)" + (testCheck (Expression ExtendedLam)) + >> it "checks pi-types (Pi)" + (testCheck (Expression Pi)) + >> it "checks let-blocks (Let)" + (testCheck (Expression Let)) + >> it "checks do-blocks (DoBlock)" + (testCheck (Expression DoBlock1) + >> testCheck (Expression DoBlock2) + >> testCheck (Expression DoBlock3) + >> testCheck (Expression DoBlock4)) + +testDeclaration + :: Spec +testDeclaration + = describe "declarations" + $ it "checks type signatures (TypeSig)" + (testCheck (Declaration TypeSig)) + >> it "checks function clauses (FunClause)" + (testCheck (Declaration FunClause)) + >> it "checks data declarations (Data)" + (testCheck (Declaration Data')) + >> it "checks record declarations (Record)" + (testCheck (Declaration Record')) + >> it "checks syntax declarations (Syntax)" + (testCheck (Declaration Syntax)) + >> it "checks pattern synonyms (PatternSyn)" + (testCheck (Declaration PatternSyn)) + >> it "checks mutual blocks (Mutual)" + (testCheck (Declaration Mutual1) + >> testCheck (Declaration Mutual2)) + >> it "checks abstract blocks (Abstract)" + (testCheck (Declaration Abstract)) + >> it "checks private blocks (Private)" + (testCheck (Declaration Private')) + >> it "checks postulates (Postulate)" + (testCheck (Declaration Postulate')) + >> it "checks open statements (Open)" + (testCheck (Declaration Open')) + >> it "checks import statements (Import)" + (testCheck (Declaration Import')) + >> it "checks module macros (ModuleMacro)" + (testCheck (Declaration ModuleMacro)) + >> it "checks module definitions (Module)" + (testCheck (Declaration Module')) + +testExample + :: Spec +testExample + = describe "example" + $ it "outputs the text in README.md" + $ testCheckExample +