diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dbd56f5..97479bc 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 diff --git a/Tactic/Derive.agda b/Tactic/Derive.agda index 1eaad74..c73617d 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 28c4ffe..cbed810 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 fe2b64a..5233a6f 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 254eda7..8bc8a73 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