Don't curry (via eta expansion) a one-argument function

This commit is contained in:
2025-01-25 21:38:59 -08:00
parent 7d218a4b94
commit afc6146050
2 changed files with 94 additions and 91 deletions

View File

@@ -111,7 +111,10 @@ compileTerm t@(Ref fc nm) = do
let (Just (MkEntry _ _ type _)) = lookup nm top
| Nothing => error fc "Undefined name \{show nm}"
arity <- arityForName fc nm
apply (CRef (show nm)) Nil Lin arity type
case arity of
-- we don't need tu curry functions that take one argument
(S Z) => pure $ CRef (show nm)
_ => apply (CRef (show nm)) Nil Lin arity type
compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
compileTerm (Lam _ nm _ _ t) = CLam nm <$> compileTerm t