diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs index cfc55462..9a9e4385 100644 --- a/src/Agda2Hs/Compile/Function.hs +++ b/src/Agda2Hs/Compile/Function.hs @@ -133,11 +133,18 @@ compileClause' curModule x c@Clause{..} = do reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c addContext (KeepNames clauseTel) $ do ps <- compilePats namedClausePats - body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody let isWhereDecl = not . isExtendedLambdaName /\ (curModule `isFatherModuleOf`) . qnameModule 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 + (c:_) -> withCurrentModule $ qnameModule c + body <- inWhereModule $ compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody let rhs = Hs.UnGuardedRhs () body whereBinds | null whereDecls = Nothing | otherwise = Just $ Hs.BDecls () (concat whereDecls) diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs index ba787c90..3d264a38 100644 --- a/src/Agda2Hs/Compile/Term.hs +++ b/src/Agda2Hs/Compile/Term.hs @@ -240,12 +240,9 @@ compileTerm v = do False -> do reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function" -- Drop module parameters of local `where` functions - xs <- asks locals - reportSDoc "agda2hs.compile.term" 15 $ text "Locals: " <+> (prettyTCM xs) - n <- if - | f `elem` xs -> size <$> lookupSection (qnameModule f) - | otherwise -> return 0 - (`app` drop n es) . Hs.Var () =<< compileQName f + moduleArgs <- getDefFreeVars f + reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs + (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f Con h i es | Just semantics <- isSpecialCon (conName h) -> semantics h i es Con h i es -> isUnboxConstructor (conName h) >>= \case diff --git a/test/AllTests.agda b/test/AllTests.agda index 39cfa870..dc741c3d 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -59,6 +59,7 @@ import IOFile import IOInput import Issue200 import Issue169 +import Issue210 {-# FOREIGN AGDA2HS import Issue14 @@ -118,4 +119,5 @@ import IOFile import IOInput import Issue200 import Issue169 +import Issue210 #-} diff --git a/test/Issue210.agda b/test/Issue210.agda new file mode 100644 index 00000000..bd742958 --- /dev/null +++ b/test/Issue210.agda @@ -0,0 +1,35 @@ +open import Haskell.Prelude hiding (f) + +record Test (a : Set) : Set₁ where + field + f : a -> a +open Test {{...}} public +{-# COMPILE AGDA2HS Test class #-} + +instance + testNat : Test Nat + Test.f testNat n = h + where + g : Nat + g = 3 + n + h : Nat + h = n + g + {-# COMPILE AGDA2HS testNat #-} + +f1 : Nat -> Nat +f1 n = h1 + where + g1 : Nat + g1 = 3 + n + h1 : Nat + h1 = n + g1 +{-# COMPILE AGDA2HS f1 #-} + +f2 : Nat -> Nat +f2 n = h2 n + where + g2 : Nat + g2 = 3 + n + h2 : Nat -> Nat + h2 m = n + g2 + m +{-# COMPILE AGDA2HS f2 #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 13995e87..23cf3e71 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -57,4 +57,5 @@ import IOFile import IOInput import Issue200 import Issue169 +import Issue210 diff --git a/test/golden/Issue210.hs b/test/golden/Issue210.hs new file mode 100644 index 00000000..6c874c21 --- /dev/null +++ b/test/golden/Issue210.hs @@ -0,0 +1,31 @@ +module Issue210 where + +import Numeric.Natural (Natural) + +class Test a where + f :: a -> a + +instance Test Natural where + f n = h + where + g :: Natural + g = 3 + n + h :: Natural + h = n + g + +f1 :: Natural -> Natural +f1 n = h1 + where + g1 :: Natural + g1 = 3 + n + h1 :: Natural + h1 = n + g1 + +f2 :: Natural -> Natural +f2 n = h2 n + where + g2 :: Natural + g2 = 3 + n + h2 :: Natural -> Natural + h2 m = n + g2 + m +