[ #155 ] Add COMPILE ... to pragmas for data types and functions

src/Agda2Hs/AgdaUtils.hs

@@ -4,16 +4,19 @@ import Data.Data
 import Data.Monoid ( Any(..) )
 import qualified Data.Map as Map
 import Data.Maybe ( fromMaybe, isJust )
+import Data.String ( fromString )
 
 import Agda.Compiler.Backend hiding ( Args )
 
+import Agda.Interaction.BasicOps ( parseName )
 import Agda.Interaction.FindFile ( findFile' )
 
 import Agda.Syntax.Common ( Arg, defaultArg )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import qualified Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal
 import Agda.Syntax.Internal.Names
+import Agda.Syntax.Position ( noRange )
 import Agda.Syntax.Scope.Base
 import Agda.Syntax.Scope.Monad
 import Agda.Syntax.TopLevelModuleName
@@ -160,3 +163,10 @@ infoFlags =
     , Option []     ["print-options"] (NoArg ()) ""
     , Option []     ["setup"] (NoArg ()) ""
     ]
+
+resolveStringName :: MonadTCM m => String -> m QName
+resolveStringName s = do
+  rname  <- liftTCM $ resolveName =<< parseName noRange s
+  case rname of
+    DefinedName _ aname _ -> return $ anameName aname
+    _ -> liftTCM $ typeError $ CustomBackendError "agda2hs" $ fromString $ "Couldn't find " ++ s

src/Agda2Hs/Compile.hs

@@ -2,10 +2,12 @@ module Agda2Hs.Compile where
 
 import Prelude hiding (null)
 
+import Control.Monad.IO.Class
 import Control.Monad.Trans.RWS.CPS ( evalRWST )
 import Control.Monad.State ( gets, liftIO )
 import Control.Arrow ((>>>))
 import Data.Functor
+import Data.IORef
 import Data.List ( isPrefixOf, group, sort )
 
 import qualified Data.Map as M
@@ -23,20 +25,28 @@ import Agda.Utils.Null
 import Agda.Utils.Monad ( whenM, anyM, when, unless )
 
 import Agda2Hs.Compile.ClassInstance ( compileInstance )
-import Agda2Hs.Compile.Data ( compileData )
-import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
+import Agda2Hs.Compile.Data ( compileData, checkCompileToDataPragma )
+import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma, checkCompileToFunctionPragma )
 import Agda2Hs.Compile.Name ( hsTopLevelModuleName )
 import Agda2Hs.Compile.Postulate ( compilePostulate )
 import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
+import Agda2Hs.Config
 import Agda2Hs.Pragma
 
 import qualified Agda2Hs.Language.Haskell as Hs
 
-initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv
-initCompileEnv tlm rewrites = CompileEnv
-  { currModule        = tlm
+globalSetup :: Options -> TCM GlobalEnv
+globalSetup opts = do
+  opts <- checkConfig opts
+  ctMap <- liftIO $ newIORef M.empty
+  return $ GlobalEnv opts ctMap
+
+initCompileEnv :: GlobalEnv -> TopLevelModuleName -> SpecialRules -> CompileEnv
+initCompileEnv genv tlm rewrites = CompileEnv
+  { globalEnv         = genv
+  , currModule        = tlm
   , minRecordName     = Nothing
   , isNestedInType    = False
   , locals            = []
@@ -45,16 +55,18 @@ initCompileEnv tlm rewrites = CompileEnv
   , copatternsEnabled = False
   , rewrites          = rewrites
   , writeImports      = True
+  , checkNames        = True
   }
 
 initCompileState :: CompileState
 initCompileState = CompileState { lcaseUsed = 0 }
 
-runC :: TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput)
-runC tlm rewrites c = evalRWST c (initCompileEnv tlm rewrites) initCompileState
+runC :: GlobalEnv -> TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput)
+runC genv tlm rewrites c = evalRWST c (initCompileEnv genv tlm rewrites) initCompileState
 
-moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes)
-moduleSetup opts _ m mifile = do
+moduleSetup :: GlobalEnv -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes)
+moduleSetup genv _ m mifile = do
+  let opts = globalOptions genv
   -- we never compile primitive modules
   if any (`isPrefixOf` prettyShow m) primModules then pure $ Skip ()
   else do
@@ -75,14 +87,15 @@ moduleSetup opts _ m mifile = do
 ------------------------
 
 compile
-  :: Options -> ModuleEnv -> IsMain -> Definition
+  :: GlobalEnv -> ModuleEnv -> IsMain -> Definition
   -> TCM (CompiledDef, CompileOutput)
-compile opts tlm _ def =
+compile genv tlm _ def =
   withCurrentModule (qnameModule qname)
-    $ runC tlm (optRewrites opts)
+    $ runC genv tlm (optRewrites opts)
     $ setCurrentRangeQ qname
     $ compileAndTag <* postCompile
   where
+    opts = globalOptions genv
     qname = defName def
 
     tag []   = []
@@ -94,7 +107,7 @@ compile opts tlm _ def =
 
       reportSDoc "agda2hs.compile" 5  $ text "Compiling definition:" <+> prettyTCM qname
       reportSDoc "agda2hs.compile" 45 $ text "Pragma:" <+> text (show p)
-      reportSDoc "agda2hs.compile" 45 $ text "Compiling definition:" <+> pretty (theDef def)
+      reportSDoc "agda2hs.compile" 65 $ text "Compiling definition:" <+> pretty (theDef def)
 
       isInstance <- anyM (isClassName . instanceClass) $ defInstance def
 
@@ -107,6 +120,8 @@ compile opts tlm _ def =
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
         (TuplePragma b       , Record{}  ) -> return []
+        (CompileToPragma s   , Datatype{}) -> [] <$ checkCompileToDataPragma def s
+        (CompileToPragma s   , Function{}) -> [] <$ checkCompileToFunctionPragma def s
 
         (ClassPragma ms      , Record{}  ) -> pure <$> compileRecord (ToClass ms) def
         (NewTypePragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord True ds) def
@@ -125,7 +140,7 @@ compile opts tlm _ def =
     postCompile = whenM (gets $ lcaseUsed >>> (> 0)) $ tellExtension Hs.LambdaCase
 
 verifyOutput ::
-  Options -> ModuleEnv -> IsMain -> TopLevelModuleName
+  GlobalEnv -> ModuleEnv -> IsMain -> TopLevelModuleName
   -> [(CompiledDef, CompileOutput)] -> TCM ()
 verifyOutput _ _ _ m ls = do
   reportSDoc "agda2hs.compile" 5 $ text "Checking generated output before rendering: " <+> prettyTCM m

src/Agda2Hs/Compile/ClassInstance.hs

@@ -11,12 +11,9 @@ import qualified Data.HashMap.Strict as HMap
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( curDefs, sortDefs )
 
-import Agda.Interaction.BasicOps ( parseName )
-
 import Agda.Syntax.Common hiding ( Ranged )
 import Agda.Syntax.Internal
 import Agda.Syntax.Internal.Pattern ( patternToTerm )
-import Agda.Syntax.Position ( noRange )
 import Agda.Syntax.Scope.Base
 import Agda.Syntax.Scope.Monad ( resolveName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
@@ -326,16 +323,6 @@ findDefinitions p m = do
       inMod = [ (x, def) | (x, def) <- HMap.toList allDefs, isInModule x m ]
   map snd <$> filterM (uncurry p) inMod
 
-
-resolveStringName :: String -> C QName
-resolveStringName s = do
-  cqname <- liftTCM $ parseName noRange s
-  rname  <- liftTCM $ resolveName cqname
-  case rname of
-    DefinedName _ aname _ -> return $ anameName aname
-    _ -> agda2hsStringError $ "Couldn't find " ++ s
-
-
 lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]
 lookupDefaultImplementations recName fields = do
   let modName = qnameToMName recName

src/Agda2Hs/Compile/Data.hs

@@ -1,25 +1,32 @@
 module Agda2Hs.Compile.Data where
 
-import Control.Monad ( when )
 import Agda.Compiler.Backend
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
+import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Reduce
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
+import Agda.Utils.Maybe
+import Agda.Utils.Monad
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
+import Agda2Hs.AgdaUtils
+
+import Agda2Hs.Compile.Name
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 
 import qualified Agda2Hs.Language.Haskell as Hs
 import Agda2Hs.Language.Haskell.Utils ( hsName )
 
+import Agda2Hs.Pragma
+
 checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do
   checkSingleElement name cs "Newtype must have exactly one constructor in definition"
@@ -36,8 +43,9 @@ compileData newtyp ds def = do
   reportSDoc "agda2hs.data" 10 $ text "Datatype telescope:" <+> prettyTCM tel
   allIndicesErased t
   let params = teleArgs tel
+  binds <- compileTeleBinds False tel -- TODO: add kind annotations?
   addContext tel $ do
-    binds <- compileTeleBinds tel
+    -- TODO: filter out erased constructors
     cs <- mapM (compileConstructor params) cs
     let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds
 
@@ -46,21 +54,23 @@ compileData newtyp ds def = do
     when newtyp (checkNewtype d cs)
 
     return [Hs.DataDecl () target Nothing hd cs ds]
-  where
-    allIndicesErased :: Type -> C ()
-    allIndicesErased t = reduce (unEl t) >>= \case
-      Pi dom t -> compileDomType (absName t) dom >>= \case
-        DomDropped      -> allIndicesErased (unAbs t)
-        DomType{}       -> agda2hsError "Not supported: indexed datatypes"
-        DomConstraint{} -> agda2hsError "Not supported: constraints in types"
-        DomForall{}     -> agda2hsError "Not supported: indexed datatypes"
-      _ -> return ()
+
+allIndicesErased :: Type -> C ()
+allIndicesErased t = reduce (unEl t) >>= \case
+  Pi dom t -> compileDomType (absName t) dom >>= \case
+    DomDropped      -> allIndicesErased (unAbs t)
+    DomType{}       -> agda2hsError "Not supported: indexed datatypes"
+    DomConstraint{} -> agda2hsError "Not supported: constraints in types"
+    DomForall{}     -> agda2hsError "Not supported: indexed datatypes"
+  _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
 compileConstructor params c = do
   reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c
   reportSDoc "agda2hs.data.con" 20 $ text "  params = " <+> prettyTCM params
-  ty <- (`piApplyM` params) . defType =<< getConstInfo c
+  ty <- defType <$> getConstInfo c
+  reportSDoc "agda2hs.data.con" 30 $ text "  ty (before piApply) = " <+> prettyTCM ty
+  ty <- ty `piApplyM` params
   reportSDoc "agda2hs.data.con" 20 $ text "  ty = " <+> prettyTCM ty
   TelV tel _ <- telView ty
   let conName = hsName $ prettyShow $ qnameName c
@@ -77,3 +87,92 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
   DomConstraint hsA -> agda2hsError "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
   DomForall{}       -> __IMPOSSIBLE__
+
+checkCompileToDataPragma :: Definition -> String -> C ()
+checkCompileToDataPragma def s = noCheckNames $ do
+  r <- resolveStringName s
+  let ppd = prettyTCM (defName def)
+      ppr = prettyTCM r
+  let fail reason = agda2hsErrorM $
+        "Cannot compile datatype" <+> liftTCM ppd <+>
+        "to" <+> liftTCM ppr <+> "because" <+> reason
+  -- Start by adding compile-to rule because it makes the check
+  -- for constructor types easier
+  addCompileToName (defName def) r
+  -- Check that target is a datatype with a regular COMPILE pragma
+  reportSDoc "agda2hs.compileto" 20 $ "Checking that" <+> ppr <+> "is a datatype"
+  unlessM (liftTCM $ isDatatype r) $ fail "it is not a datatype"
+  (rdef, rpragma) <- getDefAndPragma r
+  whenNothing (isSpecialCon r) $ case rpragma of
+    DefaultPragma{} -> return ()
+    NewTypePragma{} -> return ()
+    NoPragma{} -> fail "it is missing a COMPILE pragma"
+    _ -> fail "it has an unsupported COMPILE pragma"
+  -- Check that parameters match
+  reportSDoc "agda2hs.compileto" 20 $ "Checking that parameters of" <+> ppd <+> "match those of" <+> ppr
+  TelV dtel dtarget <- telViewUpTo (dataPars $ theDef def) (defType def)
+  rtel <- theTel <$> telViewUpTo (dataPars $ theDef rdef) (defType rdef)
+  dpars <- compileTeleBinds True dtel
+  rpars <- compileTeleBinds True rtel
+  unless (length rpars == length dpars) $ fail
+    "they have a different number of parameters"
+  forM_ (zip dpars rpars) $ \(Hs.KindedVar _ a ak, Hs.KindedVar _ b bk) ->
+    unless (ak == bk) $ fail $
+      "parameter" <+> text (Hs.pp a) <+> "of kind" <+> text (Hs.pp ak) <+>
+      "does not match" <+> text (Hs.pp b) <+> "of kind" <+> text (Hs.pp bk)
+  -- Check that d has no non-erased indices
+  addContext dtel $ allIndicesErased dtarget
+  -- Check that constructors match
+  -- TODO: filter out erased constructors
+  reportSDoc "agda2hs.compileto" 20 $ "Checking that constructors of" <+> ppd <+> "match those of" <+> ppr
+  let dcons = dataCons $ theDef def
+      rcons = dataCons $ theDef rdef
+  unless (length rcons == length dcons) $ fail
+    "they have a different number of constructors"
+  forM_ (zip dcons rcons) $ \(c1, c2) -> do
+    Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC1 args1) <-
+      addContext dtel $ compileConstructor (teleArgs dtel) c1
+    -- rename parameters of r to match those of d
+    rtel' <- renameParameters dtel rtel
+    Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC2 args2) <-
+      addContext rtel' $ compileConstructor (teleArgs rtel') c2
+    unless (hsC1 == hsC2) $ fail $
+      "name of constructor" <+> text (Hs.pp hsC1) <+>
+      "does not match" <+> text (Hs.pp hsC2)
+    unless (length args1 == length args2) $ fail $
+      "number of arguments to" <+> text (Hs.pp hsC1) <+>
+      "does not match with" <+> text (Hs.pp hsC2)
+    forM_ (zip args1 args2) $ \(b1, b2) ->
+      unless (b1 == b2) $ fail $
+        "constructor argument type" <+> text (Hs.pp b1) <+>
+        "does not match with" <+> text (Hs.pp b2)
+    addCompileToName c1 c2
+
+  where
+    -- Use the names of the non-erased variables in the first telescope
+    -- as the names of the non-erased variables in the second telescope.
+    renameParameters :: Telescope -> Telescope -> C Telescope
+    renameParameters tel1 tel2 = flip loop tel2 =<< nonErasedNames tel1
+      where
+        loop :: [ArgName] -> Telescope -> C Telescope
+        loop _ EmptyTel = pure EmptyTel
+        loop [] tel = pure tel
+        loop (x:xs) (ExtendTel dom tel) = compileDom dom >>= \case
+          DOType -> ExtendTel dom . Abs x <$>
+            underAbstraction dom tel (loop xs)
+          DODropped -> ExtendTel dom . Abs (absName tel) <$>
+            underAbstraction dom tel (loop (x:xs))
+          DOTerm -> __IMPOSSIBLE__
+          DOInstance -> __IMPOSSIBLE__
+
+    nonErasedNames :: Telescope -> C [ArgName]
+    nonErasedNames EmptyTel = pure []
+    nonErasedNames (ExtendTel dom tel) = do
+      cd <- compileDom dom
+      let mx = case cd of
+            DOType -> (absName tel :)
+            DODropped -> id
+            DOTerm -> __IMPOSSIBLE__
+            DOInstance -> __IMPOSSIBLE__
+      mx <$> underAbstraction dom tel nonErasedNames
+