From 22f37f57fe5c17193147d90f548ecf327b5a694c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= Date: Fri, 20 Sep 2024 12:43:30 +0200 Subject: [PATCH] Simplify check for when to drop arguments 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 --- src/Agda2Hs/Compile/Term.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs index b5187dde..e9a85db3 100644 --- a/src/Agda2Hs/Compile/Term.hs +++ b/src/Agda2Hs/Compile/Term.hs @@ -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 @@ -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