Skip to content

Tactic.Derive: avoid pair-level decidable equality in genMutualHelpers (fixes deriving OOM) #42

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
williamdemeo wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Tactic.Derive: avoid pair-level decidable equality in genMutualHelpers (fixes deriving OOM) #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions Tactic/Derive.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ instance
_ = ContextMonad-MonadTC
_ = Functor-M {M = TC}
_ = Show-List
_ = DecEq-×

open ClauseExprM

Expand Down Expand Up @@ -159,11 +158,24 @@ open AllChainsTo using (allChainsTo)
-- Collect all non-empty wrapper chains (tagged with their terminating
-- seed) discovered in the constructors arguments of the constructors
-- of any seed.
-- Boolean equality on chain entries. Deliberately NOT the decidable
-- `_≟_` on pairs: `≡-dec` on Σ-types matches on the equality proof of
-- the first component, and normalising equality proofs between
-- reflection `Name`s goes through `Word64`/`ℕ` proofs whose normal
-- forms are astronomically large, blowing up the type checker.
eqChainEntry : WrapperChain × Name → WrapperChain × Name → Bool
eqChainEntry (c , t) (c' , t') = eqChain c c' ∧ (t ≡ᵇ t')
where
eqChain : WrapperChain → WrapperChain → Bool
eqChain [] [] = true
eqChain (n ∷ ns) (n' ∷ ns') = (n ≡ᵇ n') ∧ eqChain ns ns'
eqChain _ _ = false

genMutualHelpers : List Name → TC (List (WrapperChain × Name))
genMutualHelpers ns = do
tysPerSeed ← traverse
(λ n → L.map (unArg ∘ unAbs) <$> (L.concatMap (proj₁ ∘ viewTy ∘ proj₂) <$> getConstrs n)) ns
return $ deduplicate _≟_ $ L.concatMap (allChainsTo ns) $ concat tysPerSeed
return $ L.deduplicateᵇ eqChainEntry $ L.concatMap (allChainsTo ns) $ concat tysPerSeed

module _ (arity : ℕ) (genCe : (Term → Maybe Name) → List SinglePattern → List (NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term))) where
-- Generate the declaration & definition of a particular derivation.
Expand Down
2 changes: 2 additions & 0 deletions Tactic/Derive/DecEq.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,4 +153,6 @@ private

unquoteDecl DecEq-N₁ DecEq-N₂ = derive-DecEq $ (quote N₁ , DecEq-N₁) ∷ (quote N₂ , DecEq-N₂) ∷ []

unquoteDecl DecEq-N₃ = derive-DecEq [ (quote N₃ , DecEq-N₃) ]

-- Expected: DecEq-Term DecEq-Product
8 changes: 8 additions & 0 deletions Tactic/Derive/TestTypes.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,14 @@ data N₂ where
n₂ : N₂
n₁→₂ : N₁ → N₂

-- Two constructors with the same wrapper chain (`List N₃`).
-- Deduplicating the discovered chains must not evaluate a pair-level
-- decidable equality: its proof normalisation explodes on reflection
-- names. Guards the Boolean dedup in `genMutualHelpers`.
data N₃ : Set where
n₃ˡ : List N₃ → N₃
n₃ʳ : List N₃ → N₃

AllTestTypes : List Name
AllTestTypes = quote E0 ∷ quote E1 ∷ quote E2 ∷ quote E3 ∷ quote R1 ∷ quote R2 ∷ quote M₁ ∷ quote M₂ ∷ quote E5 ∷ []

Expand Down
Loading