From b4939ab197cfb0028a15c6b61ad9da09a91c2e9a Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Mon, 12 Oct 2020 10:24:15 +0200 Subject: [PATCH] [ fix #4967 ] Treeless simplifier can't handle partially builtin-translated code --- src/full/Agda/Compiler/ToTreeless.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/full/Agda/Compiler/ToTreeless.hs b/src/full/Agda/Compiler/ToTreeless.hs index 758307f6526..1fe64a0a979 100644 --- a/src/full/Agda/Compiler/ToTreeless.hs +++ b/src/full/Agda/Compiler/ToTreeless.hs @@ -127,8 +127,12 @@ compilerPass tag v name code = SinglePass (CompilerPass tag v name code) compilerPipeline :: Int -> QName -> Pipeline compilerPipeline v q = Sequential - [ compilerPass "simpl" (35 + v) "simplification" $ const simplifyTTerm - , compilerPass "builtin" (30 + v) "builtin translation" $ const translateBuiltins + -- Issue #4967: No simplification step before builtin translation! Simplification relies + -- on either all or no builtins being translated. Since we might have inlined + -- functions that have had the builtin translation applied, we need to apply it + -- first. + -- [ compilerPass "simpl" (35 + v) "simplification" $ const simplifyTTerm + [ compilerPass "builtin" (30 + v) "builtin translation" $ const translateBuiltins , FixedPoint 5 $ Sequential [ compilerPass "simpl" (30 + v) "simplification" $ const simplifyTTerm , compilerPass "erase" (30 + v) "erasure" $ eraseTerms q