fix projection-like compilation

src/Agda2Hs/Compile/ClassInstance.hs

@@ -235,7 +235,7 @@ compileInstanceClause' curModule ty (p:ps) c
       -- No minimal dictionary used, proceed with compiling as a regular clause.
       | otherwise -> do
         reportSDoc "agda2hs.compile.instance" 20 $ text "Compiling instance clause" <+> prettyTCM c'
-        ms <- disableCopatterns $ compileClause curModule uf ty' c'
+        ms <- disableCopatterns $ compileClause curModule Nothing uf ty' c'
         return ([Hs.InsDecl () (Hs.FunBind () (toList ms))], [])
 
 -- finding a pattern other than a projection: we skip

src/Agda2Hs/Compile/Function.hs

@@ -36,6 +36,7 @@ import Agda.Utils.Lens ((^.))
 import Agda.Utils.List
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
+import Agda.Utils.Size ( Sized(size) )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
@@ -144,12 +145,7 @@ compileFun' withSig def@Defn{..} = do
 
         typ <- if weAreOnTop then pure defType else piApplyM defType pars
 
-
-        -- TODO(flupe):
-        -- for projection-like functions, patterns only start at the record argument
-        -- so it is incorrect to use defType as a way to discard patterns, as they are not aligned
-
-        cs  <- mapMaybeM (compileClause (qnameModule 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."
@@ -167,12 +163,14 @@ compileFun' withSig def@Defn{..} = do
     err = "Not supported: type definition with `where` clauses"
 
 
-compileClause :: ModuleName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause mod x t c = withClauseLocals mod c $ compileClause' mod x t c
+compileClause :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause curModule mproj x t c =
+  withClauseLocals curModule c $ do
+    compileClause' curModule mproj x t c
 
-compileClause' :: ModuleName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause' curModule x _  c@Clause{clauseBody = Nothing} = pure Nothing
-compileClause' curModule x ty c@Clause{..} = do
+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
@@ -182,19 +180,32 @@ compileClause' curModule x ty c@Clause{..} = do
 
   addContext (KeepNames clauseTel) $ do
 
+    toDrop <- case projName of
+      Nothing -> pure 0
+      Just q  -> maybe 0 (pred . projIndex) <$> isProjection q
+
+    reportSDoc "agda2hs.compile" 17 $ "Args to drop (proj-like): " <+> prettyTCM toDrop
+
+    -- NOTE(flupe: for projection-like definitions, we drop the first parameters)
+    let ntel = size clauseTel
+    ty <- ty `piApplyM` [Var (ntel - k - 1) [] | k <- [0.. (toDrop - 1)]]
+
+    reportSDoc "agda2hs.compile" 17 $ "Corrected type: " <+> prettyTCM ty
+
     ps <- compilePats ty namedClausePats
 
     let isWhereDecl = not . isExtendedLambdaName
           /\ (curModule `isFatherModuleOf`) . qnameModule
-    children <- filter isWhereDecl <$> asks locals
+
+    children   <- filter isWhereDecl <$> asks locals
     whereDecls <- 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
     -- that correspond to the pattern variables of this clause from the calls to
     -- the functions defined in the `where` block.
     let inWhereModule = case children of
-          [] -> id
+          []    -> id
           (c:_) -> withCurrentModule $ qnameModule c
 
     let Just body            = clauseBody

src/Agda2Hs/Compile/Function.hs-boot

@@ -1,7 +1,7 @@
 module Agda2Hs.Compile.Function where
 
 import qualified Language.Haskell.Exts.Syntax as Hs ( Match, Name )
-import Agda.Syntax.Internal ( Clause, ModuleName, Type )
+import Agda.Syntax.Internal ( Clause, ModuleName, QName, Type )
 import Agda2Hs.Compile.Types ( C )
 
-compileClause' :: ModuleName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))

src/Agda2Hs/Compile/Term.hs

@@ -26,6 +26,7 @@ import Agda.TypeChecking.Datatypes ( getConType )
 import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, reduce )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM )
+import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
 
 import Agda.Utils.Lens
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
@@ -74,11 +75,11 @@ lambdaCase q ty args = setCurrentRangeQ q $ do
 
   ty' <- piApplyM ty pars
 
-  cs <- mapMaybeM (compileClause' (qnameModule q) (hsName "(lambdaCase)") ty') cs
+  cs <- mapMaybeM (compileClause' (qnameModule q) (Just q) (hsName "(lambdaCase)") ty') cs
 
   case cs of
     -- If there is a single clause and all patterns got erased, we
-    -- simply return the body.
+    -- simply return the body. do
     [Hs.Match _ _ [] (Hs.UnGuardedRhs _ rhs) _] -> return rhs
     _ -> do
       lcase <- hsLCase =<< mapM clauseToAlt cs -- Pattern lambdas cannot have where blocks
@@ -131,7 +132,7 @@ compileSpined :: Type -> Term -> Maybe (C (Hs.Exp ()))
 compileSpined ty tm =
   case tm of
 
-    Def f es     -> Just $ do
+    Def f es -> Just $ do
       ty <- defType <$> getConstInfo f
       aux (compileDef f ty) (Def f) ty es
 
@@ -165,7 +166,6 @@ compileSpined ty tm =
 
 
 -- TODO(flupe):
--- maybeUnfoldCopy f es compileTerm $ \f es ->
 
 -- | Compile a definition.
 compileDef :: QName -> Type -> [Term] -> C (Hs.Exp ())
@@ -185,15 +185,15 @@ compileDef f ty args =
 
       -- if the function is called from the same module it's defined in,
       -- we drop the module parameters
-      -- TODO: in the future we're not always gonna be erasing module parameters
+      -- NOTE(flupe): in the future we're not always gonna be erasing module parameters
       if prettyShow currentMod `isPrefixOf` prettyShow defMod then do
         npars <- size <$> (lookupSection =<< currentModule)
         let (pars, rest) = splitAt npars args
         ty' <- piApplyM ty pars
         pure (ty', rest)
       else pure (ty, args)
 
-    reportSDoc "agda2hs.compile.term" 15 $ text " module args" <+> prettyTCM ty'
+    reportSDoc "agda2hs.compile.term" 15 $ text "module args" <+> prettyTCM ty'
     reportSDoc "agda2hs.compile.term" 15 $ text "args to def: " <+> prettyTCM args'
 
     hsName <- compileQName f
@@ -390,7 +390,7 @@ compileTerm ty v = do
 
   reportSDoc "agda2hs.compile" 7  $ text "compiling term:" <+> prettyTCM v
 
-  case compileSpined ty v of
+  reduceProjectionLike v <&> compileSpined ty >>= \case
     Just cont -> cont
     Nothing   -> case v of
       Lit l   -> compileLiteral l

test/Makefile

@@ -10,13 +10,13 @@ clean :
 
 alltests :
 	@echo == Compiling tests ==
-	./agda2hs --no-projection-like AllTests.agda -o build
+	./agda2hs AllTests.agda -o build
 	@echo == Running ghc ==
 	@(cd build; ghc -fno-code AllTests.hs)
 
 cubicaltests :
 	@echo == Compiling tests using cubical ==
-	./agda2hs --no-projection-like CubicalTests.agda -o build
+	./agda2hs CubicalTests.agda -o build
 	@echo == Running ghc ==
 	@(cd build; ghc -fno-code CubicalTests.hs)
 
@@ -31,7 +31,7 @@ print-fail :
 
 build/%.err : Fail/%.agda force-recompile alltests
 	@echo Compiling $<
-	@(./agda2hs --no-projection-like $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@
+	@(./agda2hs $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@
 
 force-recompile :
 

test/ModuleParameters.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --no-projection-like #-}
 open import Haskell.Prelude hiding (a)
 
 module ModuleParameters

test/ModuleParametersImports.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --no-projection-like #-}
 module ModuleParametersImports where
 
 open import Haskell.Prelude