diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs index ee619d89..993b10e8 100644 --- a/src/Agda2Hs/Compile/ClassInstance.hs +++ b/src/Agda2Hs/Compile/ClassInstance.hs @@ -333,7 +333,7 @@ resolveStringName s = do lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition] lookupDefaultImplementations recName fields = do let modName = qnameToMName recName - isField f _ = (`elem` fields) . unQual <$> compileQName f + isField f _ = (`elem` fields) <$> compileName (qnameName f) findDefinitions isField modName classMemberNames :: Definition -> C [Hs.Name ()] diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index ed42dcbb..0e1f7cf0 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -31,8 +31,10 @@ import qualified Agda.Syntax.Common.Pretty as P import Agda.TypeChecking.Datatypes ( isDataOrRecordType ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records ( isRecordConstructor ) +import Agda.TypeChecking.Warnings ( warning ) import qualified Agda.Utils.List1 as List1 +import Agda.Utils.Monad import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM ) import Agda.Utils.Monad ( whenM ) @@ -102,11 +104,28 @@ compileQName f Just (r, def) | not (_recNamedCon def) -> r -- use record name for unnamed constructors _ -> f hf0 <- compileName (qnameName f) - (hf, mimpBuiltin) <- fromMaybe (hf0, Nothing) <$> isSpecialName f + special <- isSpecialName f + let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) special + parent <- parentName f par <- traverse (compileName . qnameName) parent let mod0 = qnameModule $ fromMaybe f parent mod <- compileModuleName mod0 + + existsInHaskell <- orM + [ pure $ isJust special + , pure $ isPrimModule mod + , hasCompilePragma f + , isClassFunction f + , isWhereFunction f + , maybe (pure False) hasCompilePragma parent + ] + + unless existsInHaskell $ do + reportSDoc "agda2hs.name" 20 $ text "DOES NOT EXIST IN HASKELL" + typeError $ CustomBackendError "agda2hs" $ P.text $ + "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule" + currMod <- hsTopLevelModuleName <$> asks currModule let skipModule = mod == currMod || isJust mimpBuiltin @@ -185,7 +204,7 @@ compileQName f mkImport mod qual par hf maybeIsType -- make sure the Prelude is properly qualified - | any (`isPrefixOf` pp mod) primModules + | isPrimModule mod = if isQualified qual then let mod' = hsModuleName "Prelude" in (mod', Just (Import mod' qual Nothing hf maybeIsType)) @@ -193,6 +212,11 @@ compileQName f | otherwise = (mod, Just (Import mod qual par hf maybeIsType)) +isWhereFunction :: QName -> C Bool +isWhereFunction f = do + whereMods <- asks whereModules + return $ any (qnameModule f `isLeChildModuleOf`) whereMods + hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName () hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack . List1.toList . moduleNameParts diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs index b82b0f4a..b7f6c180 100644 --- a/src/Agda2Hs/Compile/Record.hs +++ b/src/Agda2Hs/Compile/Record.hs @@ -16,7 +16,7 @@ import Agda.Syntax.Common ( Arg(unArg), defaultArg ) import Agda.Syntax.Internal import Agda.Syntax.Common.Pretty ( prettyShow ) -import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM ) +import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM, pretty, prettyList_ ) import Agda.TypeChecking.Substitute ( TelV(TelV), Apply(apply) ) import Agda.TypeChecking.Telescope @@ -38,7 +38,10 @@ withMinRecord :: QName -> C a -> C a withMinRecord m = local $ \ e -> e { minRecordName = Just (qnameToMName m) } compileMinRecord :: [Hs.Name ()] -> QName -> C MinRecord -compileMinRecord fieldNames m = do +compileMinRecord fieldNames m = withMinRecord m $ do + reportSDoc "agda2hs.record.min" 20 $ + text "Compiling minimal record" <+> pretty m <+> + text "with field names" <+> prettyList_ (map (text . pp) fieldNames) rdef <- getConstInfo m definedFields <- classMemberNames rdef let Record{recPars = npars, recTel = tel} = theDef rdef @@ -48,9 +51,12 @@ compileMinRecord fieldNames m = do -- We can't simply compileFun here for two reasons: -- * it has an explicit dictionary argument -- * it's using the fields and definitions from the minimal record and not the parent record - compiled <- withMinRecord m $ addContext (defaultDom rtype) $ compileLocal $ + compiled <- addContext (defaultDom rtype) $ compileLocal $ fmap concat $ traverse (compileFun False) defaults let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ] + reportSDoc "agda2hs.record.min" 20 $ + text "Done compiling minimal record" <+> pretty m <+> + text "defined fields: " <+> prettyList_ (map (text . pp) definedFields) return (definedFields, declMap) diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 2892a8ea..473c34c6 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -22,6 +22,7 @@ import qualified Language.Haskell.Exts.Comments as Hs import Agda.Compiler.Backend import Agda.Syntax.Position ( Range ) import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName ) +import Agda.TypeChecking.Warnings ( MonadWarning ) import Agda.Utils.Null import Agda.Utils.Impossible @@ -174,6 +175,7 @@ instance MonadStConcreteNames C where runStConcreteNames m = rwsT $ \r s -> runStConcreteNames $ StateT $ \ns -> do ((x, ns'), s', w) <- runRWST (runStateT m ns) r s pure ((x, s', w), ns') +instance MonadWarning C where instance IsString a => IsString (C a) where fromString = pure . fromString instance PureTCM C where instance Null a => Null (C a) where diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index a8bb62c7..6d8ef53f 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -9,6 +9,7 @@ import Control.Monad.State ( put, modify ) import Data.Maybe ( isJust ) import qualified Data.Map as M +import Data.List ( isPrefixOf ) import qualified Language.Haskell.Exts as Hs @@ -60,6 +61,8 @@ primModules = , "Haskell.Law" ] +isPrimModule :: Hs.ModuleName () -> Bool +isPrimModule mod = any (`isPrefixOf` pp mod) primModules concatUnzip :: [([a], [b])] -> ([a], [b]) concatUnzip = (concat *** concat) . unzip @@ -152,6 +155,18 @@ isErasedBaseType x = orM ] where b = El __DUMMY_SORT__ x +hasCompilePragma :: QName -> C Bool +hasCompilePragma q = processPragma q <&> \case + NoPragma{} -> False + InlinePragma{} -> True + DefaultPragma{} -> True + ClassPragma{} -> True + ExistingClassPragma{} -> True + UnboxPragma{} -> True + TransparentPragma{} -> True + NewTypePragma{} -> True + DerivePragma{} -> True + -- Exploits the fact that the name of the record type and the name of the record module are the -- same, including the unique name ids. isClassFunction :: QName -> C Bool diff --git a/test/Delay.agda b/test/Delay.agda index b74ec943..3f07763f 100644 --- a/test/Delay.agda +++ b/test/Delay.agda @@ -8,16 +8,21 @@ open import Haskell.Extra.Delay open import Agda.Builtin.Size postulate - div : Int → Int → Int - mod : Int → Int → Int + div' : Int → Int → Int + mod' : Int → Int → Int -even : Int → Bool -even x = mod x 2 == 0 +{-# COMPILE AGDA2HS div' #-} +{-# COMPILE AGDA2HS mod' #-} + +even' : Int → Bool +even' x = mod' x 2 == 0 + +{-# COMPILE AGDA2HS even' #-} collatz : ∀ {@0 j} → Int → Delay Int j -collatz x = +collatz x = if x == 0 then now 0 - else if even x then later (λ where .force → collatz (div x 2)) + else if even' x then later (λ where .force → collatz (div' x 2)) else later λ where .force → collatz (3 * x + 1) {-# COMPILE AGDA2HS collatz #-} diff --git a/test/Fail/Issue119.agda b/test/Fail/Issue119.agda new file mode 100644 index 00000000..70737ecc --- /dev/null +++ b/test/Fail/Issue119.agda @@ -0,0 +1,13 @@ +module Fail.Issue119 where + +open import Haskell.Prelude + +aaa : Int +aaa = 21 + +-- Oops, forgot compile pragma for aaa + +bbb : Int +bbb = aaa + aaa + +{-# COMPILE AGDA2HS bbb #-} diff --git a/test/TypeOperatorImport.agda b/test/TypeOperatorImport.agda index 42520d1a..0b6c5a70 100644 --- a/test/TypeOperatorImport.agda +++ b/test/TypeOperatorImport.agda @@ -2,15 +2,9 @@ module TypeOperatorImport where {-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-} -open import Agda.Builtin.Unit -open import Agda.Builtin.Bool -open import Haskell.Prelude using (_∘_) +open import Haskell.Prelude hiding (_<_) open import TypeOperatorExport -not : Bool → Bool -not true = false -not false = true - test1 : ⊤ < Bool test1 = tt {-# COMPILE AGDA2HS test1 #-} diff --git a/test/golden/Delay.hs b/test/golden/Delay.hs index 6eeaad90..88b21d48 100644 --- a/test/golden/Delay.hs +++ b/test/golden/Delay.hs @@ -1,7 +1,16 @@ module Delay where +div' :: Int -> Int -> Int +div' = error "postulate: Int -> Int -> Int" + +mod' :: Int -> Int -> Int +mod' = error "postulate: Int -> Int -> Int" + +even' :: Int -> Bool +even' x = mod' x 2 == 0 + collatz :: Int -> Int collatz x = if x == 0 then 0 else - if even x then collatz (div x 2) else collatz (3 * x + 1) + if even' x then collatz (div' x 2) else collatz (3 * x + 1) diff --git a/test/golden/Issue119.err b/test/golden/Issue119.err new file mode 100644 index 00000000..3e956c4c --- /dev/null +++ b/test/golden/Issue119.err @@ -0,0 +1,2 @@ +test/Fail/Issue119.agda:10,1-4 +agda2hs: Symbol aaa is missing a COMPILE pragma or rewrite rule