From 8113c6d6536277a08abe6a5917bee4fbaaef939f Mon Sep 17 00:00:00 2001 From: whatisRT Date: Thu, 23 Apr 2026 17:31:18 +0200 Subject: [PATCH 1/2] Improve deriving support for nested types This _does_ support the builtin `Term` datatype, but both generating the instance and evaluating it are incredibly slow, so there is some future work. However, there are some test cases for data types that are supported now that haven't been previously. --- Tactic/Derive.agda | 191 ++++++++++++++++++++++++++--------- Tactic/Derive/DecEq.agda | 8 +- Tactic/Derive/Show.agda | 8 +- Tactic/Derive/TestTypes.agda | 19 +++- 4 files changed, 174 insertions(+), 52 deletions(-) diff --git a/Tactic/Derive.agda b/Tactic/Derive.agda index 1eaad749..c73617d8 100644 --- a/Tactic/Derive.agda +++ b/Tactic/Derive.agda @@ -3,9 +3,9 @@ -- checker. Writing an actual derivation strategy then does not -- require dealing with any mutual recursion, it is all handled here. -- --- TODO: This breaks with: --- - mutual recursion that nests too deep (i.e. deeper than 1, e.g. Term) --- - indexed datatypes that require absurd clauses (e.g. Vec) +-- TODO: This breaks with indexed datatypes that require absurd clauses (e.g. Vec) +-- +-- TODO: This is very slow for mutual recursion that nests too deep (e.g. Term) -- -- TODO: support type classes with more than one field -- @@ -27,7 +27,6 @@ import Data.Bool.ListAction as L import Data.List as L hiding (any) import Data.List.NonEmpty as NE import Data.String as S -open import Data.Maybe using (fromMaybe) open import Reflection.Tactic open import Reflection.Utils open import Reflection.Utils.TCI @@ -44,13 +43,32 @@ open import Class.Traversable instance _ = ContextMonad-MonadTC - _ = Functor-M + _ = Functor-M {M = TC} _ = Show-List + _ = DecEq-× open ClauseExprM +-- A wrapper chain `[n₁ , n₂ , … , nₖ]` represents the applied type +-- `n₁ (n₂ (… (nₖ dName)))`. +WrapperChain : Set +WrapperChain = List Name + +applyChain : WrapperChain → Term → Term +applyChain [] t = t +applyChain (n ∷ ns) t = n ∙⟦ applyChain ns t ⟧ + +-- Does the a path of the syntax tree of the term match the given +-- wrapper chain applied to `dName`? +matchesChain : WrapperChain → Name → Term → Bool +matchesChain [] dName (def n _) = ⌊ dName ≟ n ⌋ +matchesChain [] _ _ = false +matchesChain (n ∷ ns) dName (def n' args) = + ⌊ n ≟ n' ⌋ ∧ L.any (λ where (arg _ t) → matchesChain ns dName t) args +matchesChain _ _ _ = false + -- generate the type of the `className dName` instance -genClassType : ℕ → Name → Maybe Name → TC Type +genClassType : ℕ → Name → Maybe WrapperChain → TC Type genClassType arity dName wName = do params ← getParamsAndIndices dName let params' = L.map (λ where (abs x y) → abs x (hide y)) $ take (length params ∸ arity) params @@ -86,54 +104,133 @@ genClassType arity dName wName = do x' ← (abs "_" ∘ iArg) <$> (genSortInstance k k i) (x' ∷_) <$> (extendContext ("", hArg unknown) $ genSortInstanceWithCtx xs) - modifyClassType : Maybe Name → TypeView → Type - modifyClassType nothing (tel , ty) = tyView (tel , className ∙⟦ ty ⟧) - modifyClassType (just n) (tel , ty) = tyView (tel , className ∙⟦ n ∙⟦ ty ⟧ ⟧) - -lookupName : List (Name × Name) → Name → Maybe Name -lookupName = lookupᵇ (λ n n' → ⌊ n ≟ n' ⌋) - --- Look at the constructors of the argument and return all types that --- recursively contain it. This isn't very clever right now. -genMutualHelpers : Name → TC (List Name) -genMutualHelpers n = do - tys ← L.map (unArg ∘ unAbs) <$> (L.concatMap (proj₁ ∘ viewTy ∘ proj₂) <$> getConstrs n) - return $ deduplicate _≟_ $ L.mapMaybe helper tys - where - helper : Type → Maybe Name - helper (def n' args) = - if L.any (λ where (arg _ (def n'' _)) → ⌊ n ≟ n'' ⌋ ; _ → false) args - then just n' else nothing - helper _ = nothing - -module _ (arity : ℕ) (genCe : (Name → Maybe Name) → List SinglePattern → List (NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term))) where + modifyClassType : Maybe WrapperChain → TypeView → Type + modifyClassType nothing (tel , ty) = tyView (tel , className ∙⟦ ty ⟧) + modifyClassType (just ns) (tel , ty) = tyView (tel , className ∙⟦ applyChain ns ty ⟧) + +-- Entry in the translation table: ((chain , target data name) , instance name). +-- The chain applied to the target datatype gives the concrete type whose +-- instance we resolved to `instance name`. An empty chain represents a +-- user-declared base instance for the target itself. +TransEntry : Set +TransEntry = (WrapperChain × Name) × Name + +lookupByTerm : List TransEntry → Term → Maybe Name +lookupByTerm l ty = proj₂ <$> L.findᵇ (λ where ((c , t) , _) → matchesChain c t ty) l + +-- allChainsTo: +-- Look at the constructors of the argument and return all non-empty +-- wrapper chains `[n₁ , … , nₖ]` together with the mutual-peer name `t` +-- they terminate at, such that some constructor field has a subterm +-- of the form `n₁ (n₂ (… (nₖ t)))`. +private module AllChainsTo (ns : List Name) where + nameInSeeds : Name → Bool + nameInSeeds n' = L.any (_≡ᵇ n') ns + + -- All chains from the head of `t` down to some position equal to + -- some seed in `ns`. + mutual + chainsTo : Term → List (WrapperChain × Name) + chainsTo (def n' args) with nameInSeeds n' + ... | true = [ ([] , n') ] + ... | false = L.map (λ where (c , t) → (n' ∷ c , t)) (chainsToArgs args) + chainsTo _ = [] + + chainsToArgs : List (Arg Term) → List (WrapperChain × Name) + chainsToArgs [] = [] + chainsToArgs (arg _ t ∷ rest) = chainsTo t ++ chainsToArgs rest + + -- `chainsTo` applied to the term and, recursively, to every + -- argument position, so nested sub-chains are also collected. + -- Bare references to seeds themselves are skipped (no helper needed). + mutual + allChainsTo : Term → List (WrapperChain × Name) + allChainsTo t@(def n' args) with nameInSeeds n' + ... | true = [] + ... | false = chainsTo t ++ allChainsToArgs args + allChainsTo _ = [] + + allChainsToArgs : List (Arg Term) → List (WrapperChain × Name) + allChainsToArgs [] = [] + allChainsToArgs (arg _ t ∷ rest) = allChainsTo t ++ allChainsToArgs rest + +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. +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 + +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. - -- - -- Takes a dictionary (for mutual recursion), a wrapper (also for - -- mutual recursion), the name of the original type we want to derive - -- Show for and the name we want to define Show originally at. - deriveSingle : List (Name × Name) → Name → Name → Maybe Name → TC (Arg Name × Type × List Clause) - deriveSingle transName dName iName wName = inDebugPath "DeriveSingle" do - debugLog ("For: " ∷ᵈ dName ∷ᵈ []) - goalTy ← genClassType arity dName wName - ps ← constructorPatterns' (fromMaybe dName wName ∙) + -- `tgtData` is the target datatype and `wName` is an optional wrapper + -- chain; the resulting instance has type + -- `className (applyChain wName tgtData)` and is declared at `iName`. + -- Base instances (wName ≡ nothing) are declared with `iArg` so they + -- participate in instance search; helpers (wName ≡ just _) are + -- declared with `vArg` and referenced explicitly via `transName`. + + deriveSingle : List TransEntry → Name → Name → Maybe WrapperChain → TC (Arg Name × Type × List Clause) + deriveSingle transName tgtData iName wChain = inDebugPath "DeriveSingle" do + debugLog ("For: " ∷ᵈ tgtData ∷ᵈ []) + -- e.g. `⦃ DecEq A ⦄ → DecEq (List (Arg A))` for chain [List,Arg] + goalTy ← genClassType arity tgtData wChain + -- we only ever have to pattern-match on the outermost patterns + -- since we call other instances directly (i.e. we wouldn't match + -- on `Arg` in the above example, but rather call another helper + -- `⦃ DecEq A ⦄ → DecEq (Arg A)`) + let outerName = maybe (λ where [] → tgtData ; (x ∷ _) → x) tgtData wChain + ps ← constructorPatterns' (outerName ∙) -- TODO: find a good way of printing this --debugLogᵐ ("Constrs: " ∷ᵈᵐ ps ᵛⁿ ∷ᵈᵐ []ᵐ) cs ← local (λ c → record c { goal = inj₂ goalTy }) $ singleMatchExpr ([] , iArg (Pattern.proj projName)) $ contMatch $ multiMatchExprM $ - genCe (lookupName transName) ps - let defName = maybe (maybe vArg (iArg iName) ∘ lookupName transName) (iArg iName) wName + genCe (lookupByTerm transName) ps + -- only names declared by the user should participate in instance search + let defName = maybe (λ _ → vArg iName) (iArg iName) wChain return (defName , goalTy , clauseExprToClauses cs) - deriveMulti : Name × Name × List Name → TC (List (Arg Name × Type × List Clause)) - deriveMulti (dName , iName , hClasses) = do - hClassNames ← traverse ⦃ Functor-List ⦄ - (λ cn → freshName (showName className S.++ "-" S.++ showName cn S.++ showName dName)) hClasses - traverse ⦃ Functor-List ⦄ (deriveSingle (L.zip hClasses hClassNames) dName iName) (nothing ∷ L.map just hClasses) + -- Derive all instances for a group of mutually-defined seeds at once, + -- sharing a single translation table that covers both the user-named + -- base instances and the fresh wrapper-chain helpers. + deriveGroup : List (Name × Name) → TC (List (Arg Name × Type × List Clause)) + deriveGroup seeds = do + -- discover all wrapper-chain helpers needed by any seed's constructors, + -- e.g. ([List,Arg],Term) when Term has a `List (Arg Term)` field + helpers ← genMutualHelpers $ L.map proj₁ seeds + -- generate fresh, human-readable names for the helpers + helperNames ← traverse ⦃ Functor-List ⦄ mkHelperName helpers + let helperTable : List TransEntry + helperTable = L.zip helpers helperNames + + -- seeds get empty-chain entries so cross-seed references are + -- resolved explicitly rather than relying on instance search + seedTable : List TransEntry + seedTable = L.map (λ (s , i) → (([] , s) , i)) seeds + + -- all derivations share a single table so every mutual peer and helper is in scope + open D (seedTable ++ helperTable) + baseResults ← traverse deriveBase seeds + helperResults ← traverse deriveHelper helperTable + return (baseResults ++ helperResults) + where + mkHelperName : WrapperChain × Name → TC Name + mkHelperName (chain , tgt) = freshName + (showName className + S.++ L.foldr (λ n s → "-" S.++ showName n S.++ s) "" chain + S.++ "-" S.++ showName tgt) + + module D (transName : List (TransEntry)) where + deriveBase : Name × Name → TC (Arg Name × Type × List Clause) + deriveBase (s , i) = deriveSingle transName s i nothing + + deriveHelper : TransEntry → TC (Arg Name × Type × List Clause) + deriveHelper ((chain , tgt) , n) = deriveSingle transName tgt n (just chain) derive-Class : ⦃ TCOptions ⦄ → List (Name × Name) → UnquoteDecl derive-Class l = initUnquoteWithGoal (className ∙) $ - declareAndDefineFuns =<< runAndReset (concat <$> traverse ⦃ Functor-List ⦄ helper l) - where - helper : Name × Name → TC (List (Arg Name × Type × List Clause)) - helper (a , b) = do hs ← genMutualHelpers a ; deriveMulti (a , b , hs) + declareAndDefineFuns =<< runAndReset (deriveGroup l) diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda index 28c4ffe7..cbed810d 100644 --- a/Tactic/Derive/DecEq.agda +++ b/Tactic/Derive/DecEq.agda @@ -58,10 +58,10 @@ private pattern ``yes' x = quote _because_ ◇⟦ quote true ◇ ∣ x ⟧ pattern ``no' x = quote _because_ ◇⟦ quote false ◇ ∣ x ⟧ - module _ (transName : Name → Maybe Name) where + module _ (transName : Term → Maybe Name) where eqFromTerm : Term → Term → Term → Term - eqFromTerm (def n _) t t' with transName n + eqFromTerm ty@(def _ _) t t' with transName ty ... | just n' = def (quote _≟_) (iArg (n' ∙) ∷ vArg t ∷ vArg t' ∷ []) ... | nothing = quote _≟_ ∙⟦ t ∣ t' ⟧ eqFromTerm _ t t' = quote _≟_ ∙⟦ t ∣ t' ⟧ @@ -149,4 +149,8 @@ private unquoteDecl DecEq-M₁ DecEq-M₂ = derive-DecEq $ (quote M₁ , DecEq-M₁) ∷ (quote M₂ , DecEq-M₂) ∷ [] + unquoteDecl DecEq-E5 = derive-DecEq [ (quote E5 , DecEq-E5) ] + + unquoteDecl DecEq-N₁ DecEq-N₂ = derive-DecEq $ (quote N₁ , DecEq-N₁) ∷ (quote N₂ , DecEq-N₂) ∷ [] + -- Expected: DecEq-Term DecEq-Product diff --git a/Tactic/Derive/Show.agda b/Tactic/Derive/Show.agda index fe2b64a8..5233a6f9 100644 --- a/Tactic/Derive/Show.agda +++ b/Tactic/Derive/Show.agda @@ -45,9 +45,9 @@ wrapWithPars s = "(" ++S s ++S ")" genPars : Term → Term genPars t = quote wrapWithPars ∙⟦ t ⟧ -module _ (transName : Name → Maybe Name) where +module _ (transName : Term → Maybe Name) where showFromTerm : Term → Term → Term - showFromTerm (def n _) t with transName n + showFromTerm ty@(def _ _) t with transName ty ... | just n' = def (quote show) (iArg (n' ∙) ∷ vArg t ∷ []) ... | nothing = quote show ∙⟦ t ⟧ showFromTerm _ t = quote show ∙⟦ t ⟧ @@ -92,4 +92,8 @@ private unquoteDecl Show-M₁ Show-M₂ = derive-Show $ (quote M₁ , Show-M₁) ∷ (quote M₂ , Show-M₂) ∷ [] + unquoteDecl Show-E5 = derive-Show [ (quote E5 , Show-E5) ] + + unquoteDecl Show-N₁ Show-N₂ = derive-Show $ (quote N₁ , Show-N₁) ∷ (quote N₂ , Show-N₂) ∷ [] + -- Expected: Show-Product Show-Term diff --git a/Tactic/Derive/TestTypes.agda b/Tactic/Derive/TestTypes.agda index 254eda7c..8bc8a737 100644 --- a/Tactic/Derive/TestTypes.agda +++ b/Tactic/Derive/TestTypes.agda @@ -30,6 +30,10 @@ data E4 : {n : ℕ} → Fin n → Set where c1E4 : ∀ {k} → E4 {suc k} zero c2E4 : ∀ {k} {l} → E4 {suc k} (suc l) +data E5 : Set where + c1E5 : List (Maybe E5) → E5 + c2E5 : E5 + record R1 : Set where field f1R1 : E1 f2R1 : E2 ℕ @@ -54,8 +58,21 @@ data M₂ where m₂ : M₂ m₁→₂ : M₁ → M₂ +-- Like M₁/M₂ but N₁ wraps N₂ in a List. +-- This exercises cross-seed wrapper chains: when deriving for both seeds +-- together the helper `DecEq-List-N₂` (or `Show-List-N₂`) lands in the +-- same mutual group, making termination visible to Agda. +data N₁ : Set +data N₂ : Set +data N₁ where + n₁ : N₁ + n₂→₁ : List N₂ → N₁ +data N₂ where + n₂ : N₂ + n₁→₂ : N₁ → N₂ + AllTestTypes : List Name -AllTestTypes = quote E0 ∷ quote E1 ∷ quote E2 ∷ quote E3 ∷ quote R1 ∷ quote R2 ∷ quote M₁ ∷ quote M₂ ∷ [] +AllTestTypes = quote E0 ∷ quote E1 ∷ quote E2 ∷ quote E3 ∷ quote R1 ∷ quote R2 ∷ quote M₁ ∷ quote M₂ ∷ quote E5 ∷ [] open import Data.Bool using (Bool) public open import Data.Char using (Char) public From 3dcbca1cad1e46873d942c16d1d6100337b4cea8 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Wed, 6 May 2026 12:22:43 +0100 Subject: [PATCH 2/2] CI: fix Agda installation --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dbd56f5a..97479bc6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,7 +13,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 - - uses: omelkonian/setup-agda@v2.3 + - uses: omelkonian/setup-agda@main with: agda-version: 2.8.0 stdlib-version: 2.3