Type-based compilation of everything + fix for #264

src/Agda2Hs/AgdaUtils.hs

@@ -20,7 +20,9 @@ import Agda.Syntax.TopLevelModuleName
 
 import Agda.TypeChecking.Monad ( topLevelModuleName )
 import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Sort
 import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Reduce ( reduceDefCopy )
 
 import Agda.Utils.Either ( isRight )
@@ -136,3 +138,8 @@ isForcedPat = \case
   ProjP{}       -> False
   IApplyP{}     -> False
   DefP{}        -> False
+
+endsInSort :: (PureTCM m, MonadBlock m) => Type -> m Bool
+endsInSort t = do
+  TelV tel b <- telView t
+  addContext tel $ ifIsSort b (\_ -> return True) (return False)

src/Agda2Hs/Compile.hs

@@ -34,8 +34,8 @@ initCompileEnv tlm rewrites = CompileEnv
   { currModule        = tlm
   , minRecordName     = Nothing
   , locals            = []
+  , compilingLocal    = False
   , copatternsEnabled = False
-  , checkVar          = False
   , rewrites          = rewrites
   }
 
@@ -85,7 +85,7 @@ compile opts tlm _ def =
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
         (ExistingClassPragma , _         ) -> return []
-        (UnboxPragma s       , defn      ) -> [] <$ checkUnboxPragma defn
+        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
 

src/Agda2Hs/Compile/ClassInstance.hs

@@ -30,6 +30,7 @@ import Agda.TypeChecking.Records
 import Agda.TypeChecking.Telescope ( mustBePi )
 
 import Agda.Utils.Lens
+import Agda.Utils.Monad ( ifNotM )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
 import Agda2Hs.AgdaUtils
@@ -84,7 +85,8 @@ compileInstance ToDefinition def@Defn{..} =
 compileInstRule :: [Hs.Asst ()] -> Term -> C (Hs.InstRule ())
 compileInstRule cs ty = case unSpine1 ty of
   Def f es | Just args <- allApplyElims es -> do
-    vs <- mapM (compileType . unArg) $ filter keepArg args
+    fty <- defType <$> getConstInfo f
+    vs <- compileTypeArgs fty args
     f <- compileQName f
     return $
       Hs.IRule () Nothing (ctx cs) $ foldl (Hs.IHApp ()) (Hs.IHCon () f) (map pars vs)
@@ -100,6 +102,7 @@ compileInstRule cs ty = case unSpine1 ty of
     DomConstraint hsA ->
       underAbstraction a b (compileInstRule (cs ++ [hsA]) . unEl)
     DomType _ t -> __IMPOSSIBLE__
+    DomForall _ -> __IMPOSSIBLE__
   _ -> __IMPOSSIBLE__
 
 
@@ -131,7 +134,8 @@ etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do
 
 
 compileInstanceClause :: ModuleName -> Type -> Clause -> C ([Hs.InstDecl ()], [QName])
-compileInstanceClause curModule ty c = do
+compileInstanceClause curModule ty c = ifNotM (keepClause c) (return ([], [])) $ do
+
   let naps = namedClausePats c
 
   -- there are no projection patterns: we need to eta-expand the clause
@@ -162,7 +166,11 @@ compileInstanceClause' curModule ty (p:ps) c
 
     -- retrieve the type of the projection
     Just (unEl -> Pi a b) <- getDefType q ty
-    let ty' = absBody b
+    -- We don't really have the information available to reconstruct the instance
+    -- head. However, all dependencies on the instance head are in erased positions, 
+    -- so we can just use a dummy term instead
+    let instanceHead = __DUMMY_TERM__ 
+        ty' = b `absApp` instanceHead
 
     reportSDoc "agda2hs.compile.instance" 15 $
       text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q [])
@@ -193,14 +201,15 @@ compileInstanceClause' curModule ty (p:ps) c
           _ -> return d
 
     if
-      | isInstance arg, usableModality arg -> do
+      -- Instance field: check canonicity.
+      | isInstance arg -> do
           unless (null ps) $ genericDocError =<< text "not allowed: explicitly giving superclass"
           body <- case clauseBody c' of
             Nothing -> genericDocError =<< text "not allowed: absurd clause for superclass"
             Just b  -> return b
           checkInstance body
           return ([], [])
-      | not (keepArg arg) -> return ([], [])
+
       -- Projection of a primitive field: chase down definition and inline as instance clause.
       | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
       , [(_, f)] <- mapMaybe isProjElim es
@@ -210,7 +219,7 @@ compileInstanceClause' curModule ty (p:ps) c
         reportSDoc "agda2hs.compile.instance" 20 $
           text $ "raw projection:" ++ prettyShow (Def n [])
         d <- chaseDef n
-        fc <- compileFun False d
+        fc <- compileLocal $ compileFun False d
         let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d
         let fc' = {- dropPatterns 1 $ -} replaceName hd uf fc
         return (map (Hs.InsDecl ()) fc', [n])
@@ -219,7 +228,21 @@ compileInstanceClause' curModule ty (p:ps) c
        -- same (minimal) dictionary as the primitive fields.
       | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
       , n .~ q -> do
-        case map unArg . filter keepArg <$> allApplyElims es of
+        let err = genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+            filterArgs :: Type -> [Term] -> C [Term]
+            filterArgs ty [] = return []
+            filterArgs ty (v:vs) = do
+              reportSDoc "agda2hs.compile.instance" 25 $ text "filterArgs: v =" <+> prettyTCM v
+              (a,b) <- mustBePi ty
+              reportSDoc "agda2hs.compile.instance" 25 $ text "filterArgs: a =" <+> prettyTCM a
+              let rest = underAbstraction a b $ \b' -> filterArgs b' vs
+              compileDom a >>= \case
+                DODropped -> rest
+                DOType -> rest
+                DOTerm -> (v:) <$> rest
+                DOInstance -> err
+        ty <- defType <$> getConstInfo n
+        traverse (filterArgs ty) (map unArg <$> allApplyElims es) >>= \case
           Just [ Def f _ ] -> do
             reportSDoc "agda2hs.compile.instance" 20 $ vcat
                 [ text "Dropping default instance clause" <+> prettyTCM c'
@@ -228,8 +251,7 @@ compileInstanceClause' curModule ty (p:ps) c
             reportSDoc "agda2hs.compile.instance" 40 $
                 text $ "raw dictionary:" ++ prettyShow f
             return ([], [f])
-
-          _ -> genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+          _ -> err
 
       -- No minimal dictionary used, proceed with compiling as a regular clause.
       | otherwise -> do

src/Agda2Hs/Compile/Data.hs

@@ -52,10 +52,11 @@ compileData newtyp ds def = do
         DomDropped      -> allIndicesErased (unAbs t)
         DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
         DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
+        DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
       _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
-compileConstructor params c = checkingVars $ do
+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
@@ -74,3 +75,4 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
     (ty :) <$> underAbstraction a tel compileConstructorArgs
   DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
+  DomForall{}       -> __IMPOSSIBLE__

src/Agda2Hs/Compile/Function.hs

@@ -2,15 +2,14 @@
 module Agda2Hs.Compile.Function where
 
 import Control.Monad ( (>=>), filterM, forM_ )
-import Control.Monad.Reader ( asks )
+import Control.Monad.Reader ( asks, local )
 
 import Data.Generics
 import Data.List
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Build as Hs
+import qualified Language.Haskell.Exts as Hs
 
 import Agda.Compiler.Backend
 import Agda.Compiler.Common
@@ -41,7 +40,7 @@ import Agda.Utils.Size ( Sized(size) )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 import Agda2Hs.Compile.Term ( compileTerm, usableDom )
-import Agda2Hs.Compile.Type ( compileTopLevelType, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -116,50 +115,50 @@ compileFun withSig def@Defn{..} =
     $ compileFun' withSig def
 
 -- inherit existing (instantiated) locals
-compileFun' withSig def@Defn{..} = do
+compileFun' withSig def@Defn{..} = inTopContext $ do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 
   whenM ((withSig &&) <$> inRecordMod defName) $
     genericDocError =<< text "not supported by agda2hs: functions inside a record module"
 
-  withCurrentModule m $ do
+  -- We add the module parameters to the context
+  -- if we are compiling a local function (e.g. a where declaration or pattern-matching lambda)
+  isLocalFun <- asks compilingLocal
+  tel <- if isLocalFun then lookupSection m else return EmptyTel
+
+  withCurrentModule m $ addContext tel $ do
     ifM (endsInSort defType)
         -- if the function type ends in Sort, it's a type alias!
         (ensureNoLocals err >> compileTypeDef x def) 
         -- otherwise, we have to compile clauses.
         $ do
+
+      pars <- getContextArgs
+      reportSDoc "agda2hs.compile.type" 8 $ "Function module parameters: " <+> prettyTCM pars
 
-      when withSig $ checkValidFunName x
-
-      compileTopLevelType withSig defType $ \ty -> do
-
-        let filtered = filter keepClause funClauses
-        weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)
-        pars <- getContextArgs
+      reportSDoc "agda2hs.compile.type" 8 $ "Function type (before instantiation): " <+> inTopContext (prettyTCM defType)
+      typ <- piApplyM defType pars
+      reportSDoc "agda2hs.compile.type" 8 $ "Function type (after instantiation): " <+> prettyTCM typ 
 
-        -- We only instantiate the clauses to the current module parameters
-        -- if the current module isn't the toplevel module
-        unless weAreOnTop $
-          reportSDoc "agda2hs.compile.type" 8 $ "Applying module parameters to clauses: " <+> prettyTCM pars
-        let clauses = if weAreOnTop then filtered else filtered `apply` pars
+      sig <- if not withSig then return [] else do
+        checkValidFunName x
+        ty <- compileType $ unEl typ
+        reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty) 
+        return [Hs.TypeSig () [x] ty]
 
-        typ <- if weAreOnTop then pure defType else piApplyM defType pars
+      let clauses = funClauses `apply` pars
+      cs  <- mapMaybeM (compileClause m (Just defName) x typ) clauses
 
-        cs  <- mapMaybeM (compileClause m (Just defName) x typ) clauses
+      when (null cs) $ genericDocError
+        =<< text "Functions defined with absurd patterns exclusively are not supported."
+        <+> text "Use function `error` from the Haskell.Prelude instead."
 
-        when (null cs) $ genericDocError
-          =<< text "Functions defined with absurd patterns exclusively are not supported."
-          <+> text "Use function `error` from the Haskell.Prelude instead."
-
-        return $ [Hs.TypeSig () [x] ty | withSig ] ++ [Hs.FunBind () cs]
+      return $ sig ++ [Hs.FunBind () cs]
   where
     Function{..} = theDef
     m = qnameModule defName
     n = qnameName defName
     x = hsName $ prettyShow n
-    endsInSort t = do
-      TelV tel b <- telView t
-      addContext tel $ ifIsSort b (\_ -> return True) (return False)
     err = "Not supported: type definition with `where` clauses"
 
 
@@ -169,16 +168,15 @@ compileClause curModule mproj x t c =
     compileClause' curModule mproj x t c
 
 compileClause' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause' curModule projName x _  c@Clause{clauseBody = Nothing} = pure Nothing
 compileClause' curModule projName x ty c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7  $ "compiling clause: " <+> prettyTCM c
-  reportSDoc "agda2hs.compile" 17 $ "Old context: "      <+> (prettyTCM =<< getContext)
-  reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> prettyTCM clauseTel
-  reportSDoc "agda2hs.compile" 17 $ "Clause type:      " <+> prettyTCM clauseType
-  reportSDoc "agda2hs.compile" 17 $ "Function type:    " <+> prettyTCM ty
-  reportSDoc "agda2hs.compile" 17 $ "Clause patterns:  " <+> text (prettyShow namedClausePats)
 
-  addContext (KeepNames clauseTel) $ do
+  ifNotM (keepClause c) (pure Nothing) $ addContext (KeepNames clauseTel) $ do
+    reportSDoc "agda2hs.compile" 17 $ "Old context: "      <+> (inTopContext . prettyTCM =<< getContext)
+    reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> inTopContext (prettyTCM clauseTel)
+    reportSDoc "agda2hs.compile" 17 $ "Clause type:      " <+> prettyTCM clauseType
+    reportSDoc "agda2hs.compile" 17 $ "Function type:    " <+> prettyTCM ty
+    reportSDoc "agda2hs.compile" 17 $ "Clause patterns:  " <+> text (prettyShow namedClausePats)
 
     toDrop <- case projName of
       Nothing -> pure 0
@@ -198,7 +196,7 @@ compileClause' curModule projName x ty c@Clause{..} = do
           /\ (curModule `isFatherModuleOf`) . qnameModule
 
     children   <- filter isWhereDecl <$> asks locals
-    whereDecls <- mapM (getConstInfo >=> compileFun' True) children
+    whereDecls <- compileLocal $ mapM (getConstInfo >=> compileFun' True) children
 
     -- Jesper, 2023-10-30: We should compile the body in the module of the
     -- `where` declarations (if there are any) in order to drop the arguments
@@ -221,6 +219,16 @@ compileClause' curModule projName x ty c@Clause{..} = do
           _                         -> Hs.Match () x ps rhs whereBinds
     return $ Just match
 
+keepClause :: Clause -> C Bool
+keepClause c@Clause{..} = case (clauseBody, clauseType) of
+  (Nothing, _) -> pure False
+  (_, Nothing) -> pure False
+  (Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
+    DODropped  -> False
+    DOInstance -> False -- not __IMPOSSIBLE__ because of current hacky implementation of `compileInstanceClause`
+    DOType     -> __IMPOSSIBLE__
+    DOTerm     -> True
+
 
 -- TODO(flupe): projection-like definitions are missing the first (variable) patterns
 --             (that are however present in the type)
@@ -241,11 +249,12 @@ compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
+  when (usableDom a) checkForced
   compileDom a >>= \case
     DOInstance -> rest
-    DODropped  -> rest <* when (usableDom a) checkForced
-    DOKept     -> do
-      checkForced
+    DODropped  -> rest
+    DOType     -> rest
+    DOTerm     -> do
       checkNoAsPatterns pat
       (:) <$> compilePat (unDom a) pat <*> rest
   where checkForced  = when (isForcedPat pat) $ genericDocError =<< "not supported by agda2hs: forced (dot) patterns in non-erased positions"