Skip to content

Commit

Permalink
Simplify check for when to drop arguments
Browse files Browse the repository at this point in the history
If a function is from a where-module or is from the current minimal class record, we know that
it's a module we're in, so that check is redundant
  • Loading branch information
anka-213 authored and jespercockx committed Sep 20, 2024
1 parent fd8f271 commit 22f37f5
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/Agda2Hs/Compile/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -168,10 +168,9 @@ compileDef f ty args =
ifM (isInlinedFunction f) (compileInlineFunctionApp f ty args) $ do
reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function:" <+> prettyTCM f

currentMod <- currentModule
let defMod = qnameModule f

defIsClass <- isClassModule defMod
minRecord <- asks minRecordName
-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
outerWhereModules <- asks whereModules

Expand All @@ -180,7 +179,7 @@ compileDef f ty args =
-- if the function comes from a where-clause
-- or is a class-method for the class we are currently defining,
-- we drop the module parameters
if defMod `elem` outerWhereModules || defIsClass && (mnameToList defMod `isPrefixOf` mnameToList currentMod) then do
if defMod `elem` outerWhereModules || Just defMod == minRecord then do
npars <- size <$> lookupSection defMod
let (pars, rest) = splitAt npars args
ty' <- piApplyM ty pars
Expand Down

0 comments on commit 22f37f5

Please sign in to comment.