Skip to content

Commit cc26686

Browse files
flupeflupe
committed
fix bug in eta-expansion of constructors
1 parent e6df1ef commit cc26686

File tree

7 files changed

+97
-65
lines changed

7 files changed

+97
-65
lines changed

‎agda2lambox.cabal‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,9 @@ executable agda2lambox
1616
hs-source-dirs: src
1717
main-is: Main.hs
1818
other-modules: Agda.Utils,
19-
Agda.Utils.Treeless,
2019
Agda.Utils.EliminateDefaults,
20+
Agda.Utils.EtaExpandConstructors,
21+
Agda.Utils.Treeless,
2122
Agda2Lambox.Compile.Target,
2223
Agda2Lambox.Compile.Utils,
2324
Agda2Lambox.Compile.Monad,

‎src/Agda/Utils.hs‎

Lines changed: 0 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -103,54 +103,6 @@ treeless = CustomTT.toTreeless EagerEvaluation
103103
]
104104
-}
105105

106-
-- ** eta-expansion of constructors
107-
108-
-- NOTE(flupe):
109-
-- We do this because CertiCoq requires fully-applied constructors.
110-
-- In the future, this transformation should be made on the Coq side.
111-
-- (as it would be proven correct).
112-
-- NB: MetaCoq provides eta-expansion of constructors, but only for eprograms.
113-
-- (see : erasure/theories/EConstructorsAsBlocks.v)
114-
115-
-- | Check whether a treeless term is a constructor applied to (many) terms.
116-
unSpineCon :: TTerm -> Maybe (QName, [TTerm])
117-
unSpineCon (TCon q) = Just (q, [])
118-
unSpineCon (TApp u v) = second (++ v) <$> unSpineCon u
119-
unSpineCon _ = Nothing
120-
121-
-- | Return the arity of a constructor. Ignores parameters.
122-
conArity :: ConstructorInfo -> Int
123-
conArity (DataCon a) = a
124-
conArity (RecordCon _ _ a _) = a
125-
126-
-- | Eta-expand treeless constructors.
127-
etaExpandCtor :: TTerm -> TCM TTerm
128-
etaExpandCtor t | Just (q, args) <- unSpineCon t = do
129-
arity <- conArity <$> getConstructorInfo q
130-
let nargs = length args
131-
132-
if nargs >= arity then -- should really be (==), but just in case
133-
TApp (TCon q) <$> mapM etaExpandCtor args
134-
else do
135-
let nlam = arity - nargs
136-
exargs <- mapM (etaExpandCtor . raise nlam) args
137-
let vars = TVar <$> [(nlam - 1) .. 0]
138-
pure $ iterate TLam (TApp (TCon q) $ exargs ++ vars) !! nlam
139-
140-
etaExpandCtor t | otherwise = case t of
141-
TApp u v -> TApp <$> etaExpandCtor u <*> mapM etaExpandCtor v
142-
TLam u -> TLam <$> etaExpandCtor u
143-
TLet u v -> TLet <$> etaExpandCtor u <*> etaExpandCtor v
144-
TCase k ci tdef alts -> TCase k ci <$> etaExpandCtor tdef
145-
<*> mapM etaExpandAlt alts
146-
TCoerce u -> TCoerce <$> etaExpandCtor u
147-
_ -> pure t
148-
149-
etaExpandAlt :: TAlt -> TCM TAlt
150-
etaExpandAlt = \case
151-
TACon q a b -> TACon q a <$> etaExpandCtor b
152-
TAGuard a b -> TAGuard a <$> etaExpandCtor b
153-
TALit l b -> TALit l <$> etaExpandCtor b
154106

155107

156108
-- * projections

‎src/Agda/Utils/EliminateDefaults.hs‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,15 @@
1-
-- NOTE(flupe): Taken straight from Agda source.
2-
-- The difference is that we also add branches for unreachable defaults.
1+
{-
2+
NOTE(flupe):
3+
Taken straight from Agda source.
4+
There are two important differences:
5+
- we also add branches for unreachable defaults (because we need all cases to be exhaustive)
6+
- we sort the case alts according to the order of constructors for the given inductive
7+
8+
Currently, the default branch value is bound in a let binding,
9+
I don't know if this will be problematic for some targets that evaluate
10+
the binding before the case. Will they fail?
11+
12+
-}
313

414
-- | Eliminates case defaults by adding an alternative for all possible
515
-- constructors. Literal cases are preserved as-is.
@@ -9,12 +19,10 @@ import Control.Monad
919
import qualified Data.List as List
1020

1121
import Agda.Syntax.Treeless
12-
1322
import Agda.TypeChecking.Monad
1423
import Agda.TypeChecking.Substitute
15-
1624
import Agda.Compiler.Treeless.Subst () --instance only
17-
import Control.Monad.IO.Class (MonadIO(liftIO))
25+
1826

1927
eliminateCaseDefaults :: TTerm -> TCM TTerm
2028
eliminateCaseDefaults = tr
@@ -32,12 +40,12 @@ eliminateCaseDefaults = tr
3240

3341
alts' <- (++ newAlts) <$> mapM (trAlt . raise 1) alts
3442

35-
-- NOTE(flupe):
36-
-- alts have to respect the order of constructors
43+
-- sort the alts
3744
let alts'' = flip List.sortOn alts' \alt -> List.elemIndex (aCon alt) dtCons
3845

3946
return $ TLet def $ TCase (sc + 1) ct tUnreachable alts''
4047

48+
-- case on non-data are always exhaustive
4149
TCase sc ct def alts -> TCase sc ct <$> tr def <*> mapM trAlt alts
4250

4351
t@TVar{} -> return t
@@ -50,10 +58,10 @@ eliminateCaseDefaults = tr
5058
t@TErased{} -> return t
5159
t@TError{} -> return t
5260

53-
TCoerce a -> TCoerce <$> tr a
54-
TLam b -> TLam <$> tr b
55-
TApp a bs -> TApp <$> tr a <*> mapM tr bs
56-
TLet e b -> TLet <$> tr e <*> tr b
61+
TCoerce a -> TCoerce <$> tr a
62+
TLam b -> TLam <$> tr b
63+
TApp a bs -> TApp <$> tr a <*> mapM tr bs
64+
TLet e b -> TLet <$> tr e <*> tr b
5765

5866
trAlt :: TAlt -> TCM TAlt
5967
trAlt = \case

‎src/Agda/Utils/EtaExpandConstructors.hs‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
-- | Eta-expansion on constructors to fully-apply them, for treeless syntax.
2+
module Agda.Utils.EtaExpandConstructors (etaExpandConstructors) where
3+
4+
import Data.Bifunctor (second)
5+
6+
import Agda.Syntax.Treeless
7+
import Agda.TypeChecking.Monad
8+
import Agda.TypeChecking.Substitute
9+
import Agda.TypeChecking.Datatypes
10+
import Agda.Compiler.Treeless.Subst () --instance only
11+
import Agda.Compiler.Backend
12+
import Control.Monad.IO.Class (MonadIO(liftIO))
13+
14+
15+
-- | Check whether a treeless term is a constructor applied to (many) terms.
16+
unSpineCon :: TTerm -> Maybe (QName, [TTerm])
17+
unSpineCon (TCon q) = Just (q, [])
18+
unSpineCon (TApp u v) = second (++ v) <$> unSpineCon u
19+
unSpineCon _ = Nothing
20+
21+
-- | Return the arity of a constructor
22+
getConArity :: ConstructorInfo -> Int
23+
getConArity (DataCon a) = a
24+
getConArity (RecordCon _ _ a _) = a
25+
26+
-- | Eta-expand treeless constructors.
27+
etaExpandConstructors :: TTerm -> TCM TTerm
28+
etaExpandConstructors t | Just (q, args) <- unSpineCon t = do
29+
arity <- getConArity <$> getConstructorInfo q
30+
let nargs = length args
31+
32+
if nargs >= arity then -- should really be (==), but just in case
33+
TApp (TCon q) <$> mapM etaExpandConstructors args
34+
35+
else do
36+
let nlam = arity - nargs
37+
exargs <- mapM (etaExpandConstructors . raise nlam) args
38+
let vars = TVar <$> reverse [0 .. nlam - 1]
39+
liftIO $ putStrLn $ show vars
40+
pure $ iterate TLam (TApp (TCon q) $ exargs ++ vars) !! nlam
41+
42+
etaExpandConstructors t = case t of
43+
TApp u v -> TApp <$> etaExpandConstructors u <*> mapM etaExpandConstructors v
44+
TLam u -> TLam <$> etaExpandConstructors u
45+
TLet u v -> TLet <$> etaExpandConstructors u <*> etaExpandConstructors v
46+
TCase k ci tdef alts -> TCase k ci <$> etaExpandConstructors tdef
47+
<*> mapM etaExpandAlt alts
48+
TCoerce u -> TCoerce <$> etaExpandConstructors u
49+
_ -> pure t
50+
51+
etaExpandAlt :: TAlt -> TCM TAlt
52+
etaExpandAlt = \case
53+
TACon q a b -> TACon q a <$> etaExpandConstructors b
54+
TAGuard a b -> TAGuard a <$> etaExpandConstructors b
55+
TALit l b -> TALit l <$> etaExpandConstructors b

‎src/Agda/Utils/Treeless.hs‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,6 @@ import Agda.Compiler.Treeless.Identity
4343
import Agda.Compiler.Treeless.Simplify
4444
import Agda.Compiler.Treeless.Uncase
4545
import Agda.Compiler.Treeless.Unused
46-
import Agda.Utils.EliminateDefaults
4746

4847
import Agda.Utils.Function
4948
import Agda.Utils.Functor
@@ -57,6 +56,9 @@ import qualified Agda.Utils.SmallSet as SmallSet
5756

5857
import Agda.Utils.Impossible
5958

59+
import Agda.Utils.EliminateDefaults
60+
import Agda.Utils.EtaExpandConstructors
61+
6062
prettyPure :: P.Pretty a => a -> TCM Doc
6163
prettyPure = return . P.pretty
6264

@@ -185,7 +187,11 @@ compilerPipeline v q =
185187
, compilerPass "uncase" (30 + v) "uncase" $ const caseToSeq
186188
, compilerPass "aspat" (30 + v) "@-pattern recovery" $ const recoverAsPatterns
187189
]
190+
188191
, compilerPass "id" (30 + v) "identity function detection" $ const (detectIdentityFunctions q)
192+
193+
-- NOTE(flupe): those are custom transformations required by the backend
194+
, compilerPass "ctors" (30 + v) "eta-expand constructors" $ const etaExpandConstructors
189195
, compilerPass "defaults" (30 + v) "remove default branches" $ const eliminateCaseDefaults
190196
]
191197

‎src/Agda2Lambox/Compile/Function.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ import Agda.Syntax.Common ( hasQuantityω )
2020
import Agda.Utils.Monad (guardWithError, whenM)
2121
import Agda.Utils.Lens ( (^.) )
2222

23-
import Agda.Utils ( etaExpandCtor, treeless, pp, isRecordProjection )
23+
import Agda.Utils ( treeless, pp, isRecordProjection )
2424
import Agda2Lambox.Compile.Target
2525
import Agda2Lambox.Compile.Utils
2626
import Agda2Lambox.Compile.Monad
@@ -44,10 +44,10 @@ compileFunctionBody :: [QName] -> Definition -> CompileM LBox.Term
4444
compileFunctionBody ms Defn{defName, theDef} = do
4545
Just t <- liftTCM $ treeless defName
4646

47-
reportSDoc "agda2lambox.ocmpile.function" 10 $
47+
reportSDoc "agda2lambox.compile.function" 10 $
4848
"treeless body:" <+> pretty t
49-
50-
compileTerm ms =<< liftTCM (etaExpandCtor t)
49+
50+
compileTerm ms t
5151

5252

5353
-- | Whether to compile a function definition to λ□.

‎test/EtaCon.agda‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
module EtaCon where
2+
3+
open import Agda.Builtin.Nat
4+
open import Agda.Builtin.List
5+
6+
addone : Nat → Nat
7+
addone = suc
8+
9+
cons : {A : Set} → A → List A → List A
10+
cons = _∷_

0 commit comments

Comments
 (0)