Add simple where-provenance to agda2hs

By keeping track of which where-clause modules we have in scope, we can determine if a function if from a where-clause

Fixes #353

src/Agda2Hs/Compile.hs

@@ -37,6 +37,7 @@ initCompileEnv tlm rewrites = CompileEnv
   , minRecordName     = Nothing
   , locals            = []
   , compilingLocal    = False
+  , whereModules      = []
   , copatternsEnabled = False
   , rewrites          = rewrites
   , writeImports      = True

src/Agda2Hs/Compile/Function.hs

@@ -222,20 +222,16 @@ compileClause' curModule projName x ty c@Clause{..} = do
           /\ (curModule `isFatherModuleOf`) . qnameModule
 
     children   <- filter isWhereDecl <$> asks locals
-    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
-    -- 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
+    -- TODO: remove this when Agda exposes where-provenance in 'Internal' syntax
+    let withWhereModule = case children of
+          []    -> id
+          (c:_) -> addWhereModule $ qnameModule c
+    whereDecls <- withWhereModule $ compileLocal $ mapM (getConstInfo >=> compileFun' True) children
 
     let Just body            = clauseBody
         Just (unArg -> typ)  = clauseType
 
-    hsBody <- compileTerm typ body
+    hsBody <- withWhereModule $ compileTerm typ body
 
     let rhs = Hs.UnGuardedRhs () hsBody
         whereBinds | null whereDecls = Nothing

src/Agda2Hs/Compile/Term.hs

@@ -170,17 +170,17 @@ compileDef f ty args =
 
     currentMod <- currentModule
     let defMod = qnameModule f
+
     defIsClass <- isClassModule defMod
     -- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
-    isLocal <- asks compilingLocal
-    localDefs <- asks locals -- If we're calling into a where-clause
+    outerWhereModules <- asks whereModules -- W
 
     (ty', args') <-
 
       -- if the function is called from the same module it's defined in,
       -- we drop the module parameters
       -- NOTE(flupe): in the future we're not always gonna be erasing module parameters
-      if f `elem` localDefs || (isLocal || defIsClass) && (mnameToList defMod `isPrefixOf` mnameToList currentMod) then do
+      if defMod `elem` outerWhereModules || defIsClass && (mnameToList defMod `isPrefixOf` mnameToList currentMod) then do
         npars <- size <$> lookupSection defMod
         let (pars, rest) = splitAt npars args
         ty' <- piApplyM ty pars

src/Agda2Hs/Compile/Types.hs

@@ -82,6 +82,8 @@ data CompileEnv = CompileEnv
   -- ^ keeps track of the current clause's where declarations
   , compilingLocal :: Bool
   -- ^ whether we are currently compiling a where clause or pattern-matching lambda
+  , whereModules :: [ModuleName]
+  -- ^ the where-blocks currently in scope. Hack until Agda adds where-prominence
   , copatternsEnabled :: Bool
   -- ^ whether copatterns should be allowed when compiling patterns
   , rewrites :: SpecialRules

src/Agda2Hs/Compile/Utils.hs

@@ -278,6 +278,9 @@ checkInstance u = do
 compileLocal :: C a -> C a
 compileLocal = local $ \e -> e { compilingLocal = True }
 
+addWhereModule :: ModuleName  -> C a -> C a
+addWhereModule mName = local $ \e -> e { whereModules = mName : whereModules e }
+
 modifyLCase :: (Int -> Int) -> CompileState -> CompileState
 modifyLCase f (CompileState {lcaseUsed = n}) = CompileState {lcaseUsed = f n}
 

test/Issue353.agda

@@ -31,15 +31,13 @@ module _ (b : Bool) where
     bar = foo True 0
     {-# COMPILE AGDA2HS bar #-}
 
-    -- Still broken, since they are actually the same module here
-    -- would generate baz = bar in haskell
     baz : Bool
     baz = bar
     {-# COMPILE AGDA2HS baz #-}
 
-    -- Still broken, because we cant differentiate this from where-blocks
     callFromNested : Bool
     callFromNested = nested
       where nested = bar
-    -- {-# COMPILE AGDA2HS callFromNested #-}
+    {-# COMPILE AGDA2HS callFromNested #-}
+
 -- The check is needed both for instance declarations and where-clauses

test/golden/Issue353.hs

@@ -18,3 +18,9 @@ bar b = foo True 0
 baz :: Bool -> Bool
 baz b = bar b
 
+callFromNested :: Bool -> Bool
+callFromNested b = nested
+  where
+    nested :: Bool
+    nested = bar b
+