[ fix #119 ] Raise a warning when an unknown name appears in generate…

…d Haskell code

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 ()]

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 Agda2Hs.AgdaUtils
@@ -98,11 +100,27 @@ compileQName f
       Just (r, Record{recNamedCon = False}) -> 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
+      , maybe (pure False) hasCompilePragma parent
+      ]
+
+    unless existsInHaskell $ do
+      reportSDoc "agda2hs.name" 20 $ text "DOES NOT EXIST IN HASKELL"
+      warning $ GenericWarning $ P.text $
+        "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule"
+
     currMod <- hsTopLevelModuleName <$> asks currModule
     let skipModule = mod == currMod
                   || isJust mimpBuiltin
@@ -180,7 +198,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))

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)
 
 

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
 
@@ -168,6 +169,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

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
 
@@ -58,6 +59,8 @@ primModules =
   , "Haskell.Law"
   ]
 
+isPrimModule :: Hs.ModuleName () -> Bool
+isPrimModule mod = any (`isPrefixOf` pp mod) primModules
 
 concatUnzip :: [([a], [b])] -> ([a], [b])
 concatUnzip = (concat *** concat) . unzip
@@ -143,6 +146,18 @@ canErase a = do
     , isPropSort (getSort b)              -- _ : Prop
     ]
 
+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

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 #-}

test/golden/Issue119.err

@@ -0,0 +1 @@
+UNEXPECTED SUCCESS