From 20f643b8d37999e9da8c4e011c68830d91073279 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Fri, 12 Jun 2026 22:33:43 +0200 Subject: [PATCH 1/2] Tactic.Solver: Improve the split between `Ring` and `Algebra` solver Also fix a few more performance issues & parsing bugs --- Reflection/Utils.agda | 3 + Reflection/Utils/AtomStore.agda | 52 ++ Reflection/Utils/Core.agda | 45 +- Reflection/Utils/Goal.agda | 75 +++ Reflection/Utils/Records.agda | 31 + Reflection/Utils/Reduction.agda | 107 +++ Reflection/Utils/TCM.agda | 62 -- Tactic/Solver/Algebra.agda | 654 +++++++++++-------- Tactic/Solver/Ring.agda | 416 +++++------- Tactic/Solver/Ring/IntegerCoefficients.agda | 13 +- Tactic/Solver/Ring/Tests.agda | 2 + Tactic/Solver/Ring/Tests/BundleVariants.agda | 9 + Tactic/Solver/Ring/Tests/EdgeCases.agda | 349 ++++++++++ Tactic/Solver/Ring/Tests/Equations.agda | 83 ++- Tactic/Solver/Ring/Tests/HasAddOp.agda | 79 +++ 15 files changed, 1344 insertions(+), 636 deletions(-) create mode 100644 Reflection/Utils/AtomStore.agda create mode 100644 Reflection/Utils/Goal.agda create mode 100644 Reflection/Utils/Reduction.agda create mode 100644 Tactic/Solver/Ring/Tests/EdgeCases.agda create mode 100644 Tactic/Solver/Ring/Tests/HasAddOp.agda diff --git a/Reflection/Utils.agda b/Reflection/Utils.agda index 1fa9cf26..19860ed4 100644 --- a/Reflection/Utils.agda +++ b/Reflection/Utils.agda @@ -6,3 +6,6 @@ open import Reflection.Utils.Records public open import Reflection.Utils.Args public open import Reflection.Utils.Metas public open import Reflection.Utils.Substitute public +open import Reflection.Utils.Reduction public +open import Reflection.Utils.AtomStore public +open import Reflection.Utils.Goal public diff --git a/Reflection/Utils/AtomStore.agda b/Reflection/Utils/AtomStore.agda new file mode 100644 index 00000000..243c31d2 --- /dev/null +++ b/Reflection/Utils/AtomStore.agda @@ -0,0 +1,52 @@ +------------------------------------------------------------------------ +-- A store mapping "atoms" — subterms a macro abstracts over — to +-- variable indices. +-- +-- An atom is stored as a pair of its *original spelling* — what the +-- macro should splice into emitted terms, so nothing the user wrote +-- ever appears unfolded — and its weak-head normal form, which acts +-- as a second identity key: two spellings of the same value (two +-- definitions unfolding to the same constructor form) count as one +-- atom. Whnf-equality implies definitional equality, so emitting the +-- first-seen spelling for both stays type-correct. +-- +-- PERFORMANCE WARNING: keep the store operations as separate, +-- first-order list traversals whose results the caller forces +-- promptly (e.g. a `just i ← pure (atomStoreIndex …)` pattern). A +-- fused insert-and-index traversal returning a pair looks equivalent +-- but builds thunk chains that Agda's reflection evaluator +-- re-evaluates without sharing — on an 8-atom goal this blew up from +-- milliseconds to an out-of-memory kill +-- (see `Tactic.Solver.Ring.Tests.EdgeCases` / big8). + +{-# OPTIONS --safe --without-K #-} +module Reflection.Utils.AtomStore where + +open import Meta.Prelude + +import Data.Maybe as Maybe +open import Data.List using (map) +open import Reflection +open import Reflection.AST.AlphaEquality using (_=α=_) + +Atom : Set +Atom = Term × Term -- (original spelling , whnf key) + +AtomStore : Set +AtomStore = List Atom + +atomMatches : Atom → Atom → Bool +atomMatches (orig , whnf) (o , w) = (orig =α= o) ∨ (whnf =α= w) + +insertAtomStore : Atom → AtomStore → AtomStore +insertAtomStore a [] = a ∷ [] +insertAtomStore a (b ∷ rest) = + if atomMatches a b then b ∷ rest else b ∷ insertAtomStore a rest + +atomStoreIndex : Atom → AtomStore → Maybe ℕ +atomStoreIndex a [] = nothing +atomStoreIndex a (b ∷ rest) = + if atomMatches a b then just 0 else Maybe.map suc (atomStoreIndex a rest) + +atomSpellings : AtomStore → List Term +atomSpellings = map proj₁ diff --git a/Reflection/Utils/Core.agda b/Reflection/Utils/Core.agda index f82b278f..4fdebbee 100644 --- a/Reflection/Utils/Core.agda +++ b/Reflection/Utils/Core.agda @@ -15,6 +15,7 @@ open import Reflection.AST.Literal using (nat) import Reflection.AST.Abstraction as Abs import Reflection.AST.Argument as Arg +open import Reflection.Utils.Args using (vArgs) -- ** basics @@ -31,11 +32,23 @@ insertName : Name → List Name → List Name insertName n [] = n ∷ [] insertName n (m ∷ ms) = if n Name.≡ᵇ m then m ∷ ms else m ∷ insertName n ms +-- Boolean equality on optional names. Deliberately *not* +-- `Class.DecEq`'s `_==_`: this sits on solver hot paths +-- and measured ~15% slower per macro call. +_≡ᵐ_ : Maybe Name → Maybe Name → Bool +just n ≡ᵐ just m = n Name.≡ᵇ m +nothing ≡ᵐ nothing = true +_ ≡ᵐ _ = false + +-- Peels leading λ-binders before reading the head Name. +headName : Term → Maybe Name +headName (def nm _) = just nm +headName (lam _ (abs _ body)) = headName body +headName _ = nothing + -- Insert the def-name of `t` to `xs`, η-contract if required pickDefName : Term → List Name → List Name -pickDefName (def n _) xs = insertName n xs -pickDefName (lam _ (abs _ body)) xs = pickDefName body xs -pickDefName _ xs = xs +pickDefName t xs = Maybe.maybe′ (λ n → insertName n xs) xs (headName t) -- Extract a `ℕ` value from a term shaped as `lit (nat n)` or a chain -- of `suc`/`zero` constructors. @@ -45,15 +58,23 @@ extractNat (quote ℕ.zero ◆) = just 0 extractNat (quote ℕ.suc ◆⟦ x ⟧) = Maybe.map ℕ.suc (extractNat x) extractNat _ = nothing --- ** atom-table helpers (α-equality based) - -insertAtom : Term → List Term → List Term -insertAtom t [] = t ∷ [] -insertAtom t (a ∷ as) = if t =α= a then a ∷ as else a ∷ insertAtom t as - --- Look up `t`'s index in `xs` up to α-equality -findAtomIndex : Term → List Term → Maybe ℕ -findAtomIndex t xs = Maybe.map Fin.toℕ (findIndexᵇ (t =α=_) xs) +-- For wrapped numeric carriers like ℤ's `+_`: peel one +-- `con C (n ∷ [])` layer. +peelLitCon : Name → Term → Maybe ℕ +peelLitCon C (con nm xs) = case nm Name.≡ᵇ C of λ where + false → nothing + true → case vArgs xs of λ where + (a ∷ []) → extractNat a + _ → nothing +peelLitCon _ _ = nothing + +-- `extractNat`, also accepting numerals under the given wrapper. +extractCarrierNat : Maybe Name → Term → Maybe ℕ +extractCarrierNat mC t = case extractNat t of λ where + (just n) → just n + nothing → case mC of λ where + (just C) → peelLitCon C t + nothing → nothing -- ** alternative view of function types as a pair of a list of arguments and a return type TypeView = List (Abs (Arg Type)) × Type diff --git a/Reflection/Utils/Goal.agda b/Reflection/Utils/Goal.agda new file mode 100644 index 00000000..ab18402c --- /dev/null +++ b/Reflection/Utils/Goal.agda @@ -0,0 +1,75 @@ +------------------------------------------------------------------------ +-- Helpers for macros that inspect the hole's type and build a term +-- for it. + +{-# OPTIONS --safe --without-K #-} +module Reflection.Utils.Goal where + +open import Meta.Prelude + +open import Reflection +open import Reflection.AST.Argument +open import Reflection.Utils.Args using (getVisibleArgs) +open import Reflection.Utils.Metas using (isMeta; findMetaIds; firstMeta; shareMeta) +import Data.Vec as Vec +open import Data.List using (null) + +-- Run a continuation under the goal type's pi-prefix (weak-head +-- reducing each layer, never normalising). The continuation gets the +-- number of binders entered and the type beneath them; its result is +-- wrapped in lambdas of matching visibility. The ℕ is fuel. +underPis : ℕ → Type → (ℕ → Type → TC Term) → TC Term +underPis = go 0 + where + go : ℕ → ℕ → Type → (ℕ → Type → TC Term) → TC Term + go n 0 ty k = k n ty + go n (suc fuel) ty k = do + ty' ← reduce ty + case ty' of λ where + (pi a@(arg (arg-info av _) dom) (abs s b)) → do + case firstMeta dom of λ where + (just m) → blockOnMeta m + nothing → pure tt + body ← extendContext s a (go (suc n) fuel b k) + pure (lam av (abs s body)) + t → k n t + +-- The last two visible arguments of a relation application. +equationSides : Term → Maybe (Term × Term) +equationSides t = case getVisibleArgs 2 t of λ where + (just (lhs Vec.∷ rhs Vec.∷ Vec.[])) → just (lhs , rhs) + _ → nothing + +-- `equationSides`, with a friendly error for non-equation goals. +requireEquationSides : Term → TC (Term × Term) +requireEquationSides t = case equationSides t of λ where + (just p) → pure p + nothing → typeError + ( strErr "Malformed call to algebraic solver. " + ∷ strErr "Expected target type to be of shape LHS ≈ RHS. " + ∷ strErr "Instead: " + ∷ termErr t + ∷ []) + +-- Metavariable policy for solver-style macros: if one side has metas +-- not shared with the other, only this macro could solve them, so +-- blocking would retry forever — error instead. Otherwise block on +-- the first meta and retry once elaboration has resolved it. +blockOnEquationMetas : String → (equation lhs rhs : Term) → TC ⊤ +blockOnEquationMetas macroName equation lhs rhs = do + let bothStructured = not (isMeta lhs) ∧ not (isMeta rhs) + let metasL = findMetaIds lhs + let metasR = findMetaIds rhs + let anyMetas = not (null metasL ∧ null metasR) + let sharedMeta = shareMeta metasL metasR + if bothStructured ∧ anyMetas ∧ not sharedMeta + then typeError + ( strErr macroName + ∷ strErr ": the goal `LHS ≈ RHS` has at least one side " + ∷ strErr "containing a metavariable that could not be resolved. To run this " + ∷ strErr "solver you must add type annotations to resolve these variables." + ∷ []) + else pure tt + case firstMeta equation of λ where + (just m) → blockOnMeta m + nothing → pure tt diff --git a/Reflection/Utils/Records.agda b/Reflection/Utils/Records.agda index a10324c0..6e7c23cf 100644 --- a/Reflection/Utils/Records.agda +++ b/Reflection/Utils/Records.agda @@ -7,6 +7,11 @@ open import Meta.Init open import Data.List using (map) open import Class.DecEq using (_==_) +open import Reflection.AST.Term using (_⋯⟅∷⟆_) +open import Reflection.TCM.Syntax using (_>>=_) +open import Reflection.Utils.Reduction using (headReduce; resolveToName) +import Agda.Builtin.Reflection as B using (TC) + mkRecord : List (Name × Term) → Term mkRecord fs = pat-lam (map (λ (fn , e) → clause [] [ vArg (proj fn) ] e) fs) [] @@ -15,3 +20,29 @@ updateField fs rexp fn fexp = flip pat-lam [] $ flip map fs $ λ f → clause [] [ vArg (proj f) ] $ if f == fn then fexp else (f ∙⟦ rexp ⟧) + +------------------------------------------------------------------------ +-- Projecting reasonable terms of fields out of record value +-- +-- Getting a field from a record value in such a way that we don't +-- reduce too little or to much is quite delicate. For example, from the +-- semiring ℚ, the `1#` field should give us `1ℚ`, never its `mkℚ ...` +-- unfolding. `projectField` handles this appropriately. + +private + fieldFuel : ℕ + fieldFuel = 16 + +module _ (k : ℕ) (r : Term) (f : Name) where + + fieldProjection : Term + fieldProjection = def f (k ⋯⟅∷⟆ r ⟨∷⟩ []) + + projectField : B.TC Term + projectField = do + r' ← headReduce fieldFuel r + resolveToName (stuckOn r') fieldFuel fieldProjection + where + stuckOn : Term → List Name + stuckOn (def nm _) = nm ∷ [] + stuckOn _ = [] diff --git a/Reflection/Utils/Reduction.agda b/Reflection/Utils/Reduction.agda new file mode 100644 index 00000000..331f2a1b --- /dev/null +++ b/Reflection/Utils/Reduction.agda @@ -0,0 +1,107 @@ +------------------------------------------------------------------------ +-- Controlled reduction for syntactic inspection of Terms. +-- +-- Agda's two reflection primitives sit at the wrong extremes for a +-- macro that wants to *look at* a term rather than compute with it: +-- +-- * `reduce` (whnf) unfolds until the head is canonical. That loses +-- names: the whnf of `1ℚ` is `mkℚ (+ 1) 0 ⟨proof⟩`, useless if the +-- macro needs to recognise or block the *name* `1ℚ`. +-- * `normalise` does that everywhere at once, and on proof-carrying +-- carriers (ℚ, …) routinely produces enormous terms. +-- +-- The remedy is `withReduceDefs`, which restricts which definitions +-- may unfold — but it needs to be told names *in advance*, and when +-- chasing a definition chain you only learn the next name by taking a +-- step. The functions here package the resulting step-by-step +-- patterns: +-- +-- * `whnfBlocking ns t` — plain whnf with the names `ns` left +-- opaque. Use when you know exactly which boundary to stop at +-- (e.g. reducing a goal while keeping its operators intact). +-- +-- * `headReduce n t` — unfold the head definition one name at a +-- time (re-targeting the allow-list at each step), until the term +-- is structural (constructor, lambda, …) or stuck. Use when you +-- want a term's *shape* and the names along the way are noise: +-- e.g. pushing a record value through alias layers to find the +-- record constructor — or the stuck application obstructing it. +-- +-- * `resolveToName extra n t` — like `headReduce`, but stops at the +-- last *name* of the chain: a nullary definition is only entered +-- if its body is again a bare name (an alias). Use when the name +-- is the answer: resolving `CommutativeSemiring.1# R` should +-- yield `1ℚ`, not its unfolding. The `extra` names are +-- additionally allowed to unfold at every step; see +-- `Reflection.Utils.Records` for why that matters when +-- projecting out of record values. +-- +-- All three are depth-limited (`n` is fuel) and total. + +{-# OPTIONS --safe --without-K #-} +module Reflection.Utils.Reduction where + +open import Meta.Prelude + +open import Reflection +open import Reflection.AST.Term using (clause) +open import Reflection.AST.Definition using (function) +open import Reflection.AST.AlphaEquality using (_=α=_) +import Agda.Builtin.Reflection as B using (withReduceDefs) + +-- Weak-head normalisation with white/blacklisted names +whnfBlocking : List Name → Term → TC Term +whnfBlocking ns t = B.withReduceDefs (false , ns) (reduce t) + +whnfOnlyUnfolding : List Name → Term → TC Term +whnfOnlyUnfolding ns t = B.withReduceDefs (true , ns) (reduce t) + +private + mutual + -- The shared worker. `peel` selects the policy for a nullary + -- `def`: entered unconditionally (structure mode, `false`), or + -- only while its body is again a bare name (name mode, `true`). + -- + -- For an applied `def`, one step unfolds *only* the current head + -- (plus `extra`): reduction can't skip past an intermediate name, + -- because that name was not in this step's allow-list. The loop + -- then re-targets the new head and continues while progress is + -- made. + -- + -- Arguments are reduced in structure mode first: when the head is + -- a projection, this lets `reduce` compute it by projecting from + -- the (now exposed) record value, rather than falling back to + -- inlining the projection's clauses. + go : (peel : Bool) (extra : List Name) → ℕ → Term → TC Term + go peel extra 0 t = pure t + go peel extra (suc k) t@(def nm []) = do + d ← getDefinition nm + case (peel , d) of λ where + (false , function (clause [] [] body ∷ _)) → go peel extra k body + (true , function (clause [] [] body@(def _ []) ∷ _)) → go peel extra k body + _ → pure t + go peel extra (suc k) (def nm args) = do + args' ← goArgs k args + t' ← whnfOnlyUnfolding (nm ∷ extra) (def nm args') + if t' =α= def nm args' + then pure t' -- no progress + else go peel extra k t' + go peel extra (suc _) t = pure t + + -- Recursing with `go` here (rather than plain `reduce`) is + -- required: whnf treats a nullary definition whose body is a + -- record expression as a value and will not unfold it. + goArgs : ℕ → Args Term → TC (Args Term) + goArgs _ [] = pure [] + goArgs k (arg i t ∷ as) = do + t' ← go false [] k t + as' ← goArgs k as + pure (arg i t' ∷ as') + +-- Structure mode +headReduce : ℕ → Term → TC Term +headReduce = go false [] + +-- Name mode +resolveToName : List Name → ℕ → Term → TC Term +resolveToName = go true diff --git a/Reflection/Utils/TCM.agda b/Reflection/Utils/TCM.agda index b50162e9..6f872ef9 100644 --- a/Reflection/Utils/TCM.agda +++ b/Reflection/Utils/TCM.agda @@ -9,65 +9,3 @@ import Class.MonadReader as C import Class.MonadTC as C open import Reflection.Utils.TCI {TC} ⦃ C.Monad-TC ⦄ ⦃ C.MonadError-TC ⦄ ⦃ record { ask = C.initTCEnv ; local = λ _ x → x } ⦄ ⦃ C.MonadTC-TC ⦄ public - -open import Meta.Prelude -open import Reflection.AST.Term using (clause) -open import Reflection.AST.Definition using (function) -open import Reflection.AST.AlphaEquality using (_=α=_) -import Agda.Builtin.Reflection as B using (withReduceDefs) - --- Depth-limited weak-head reduction that unfolds one `def` at a time. --- --- Each step head-reduces every argument first, then asks Agda's --- `reduce` to unfold *only* the outer `def`. Stops at a fixed point --- or when fuel runs out. More aggressive than `reduce` (which won't --- chase a chain of `def x = def y = …`) but more controlled than --- `normalise`. --- --- The argument pass is required to reduce record projections, so that --- when the outer def is a projection, `reduce` can compute it cleanly --- instead of falling back to inlining the projection's whole body. --- --- It's a bit awkward that we only reduce the `nm` in the case with no --- arguments, but this is the only configuration I've found that makes --- the ring solver work. - -mutual - headReduce : ℕ → Term → TC Term - headReduce 0 t = pure t - headReduce (suc k) (def nm []) = do - d ← getDefinition nm - case d of λ where - (function (clause [] [] body ∷ _)) → headReduce k body - _ → pure (def nm []) - headReduce (suc k) (def nm args) = do - args' ← reduceArgs k args - t' ← B.withReduceDefs (true , nm ∷ []) (reduce (def nm args')) - if t' =α= def nm args' - then pure t' -- no progress - else headReduce k t' - headReduce (suc _) t = pure t - - reduceArgs : ℕ → Args Term → TC (Args Term) - reduceArgs _ [] = pure [] - reduceArgs k (arg i t ∷ as) = do - t' ← headReduce k t - as' ← reduceArgs k as - pure (arg i t' ∷ as') - --- Like `headReduce`, but stops at a nullary `def` whose body is not --- itself a nullary `def`. -headReducePeel : ℕ → Term → TC Term -headReducePeel 0 t = pure t -headReducePeel (suc k) t@(def nm []) = do - d ← getDefinition nm - case d of λ where - (function (clause [] [] body@(def _ []) ∷ _)) → headReducePeel k body - _ → pure t -headReducePeel (suc k) (def nm args) = do - args' ← reduceArgs k args - t' ← B.withReduceDefs (true , nm ∷ []) (reduce (def nm args')) - if t' =α= def nm args' - then pure t' - else headReducePeel k t' -headReducePeel (suc _) t = pure t diff --git a/Tactic/Solver/Algebra.agda b/Tactic/Solver/Algebra.agda index afeccd4e..f061c525 100644 --- a/Tactic/Solver/Algebra.agda +++ b/Tactic/Solver/Algebra.agda @@ -1,11 +1,40 @@ ------------------------------------------------------------------------ --- Generic core for reflection-based algebraic-structure solvers. +-- Generic core for reflection-based algebraic-structure solver +-- frontends: turns a description of a structure (a `Theory`) into a +-- working solver macro. `Tactic.Solver.Ring` is the model instance. -- --- A `Theory` describes a particular algebraic structure by giving: --- * the bundle type `R` is expected to inhabit; --- * its operators (arities + Term patterns to detect them); --- * an optional `LiteralMatch` for theories with literals; --- * how to encode them into a backend polynomial AST. +-- To add a solver for a new structure (monoid, lattice, …), write: +-- +-- * a `Theory`, whose main content is `detect`: given the user's +-- bundle Term, produce a `DetectedTheory` — +-- · `operators`: one entry per piece of syntax, pairing a Term +-- whose head identifies goal occurrences (usually +-- `projectField` of the bundle, see +-- `Reflection.Utils.Records`) with its arity and its encoder +-- into the backend solver's expression AST; +-- · `literalSpec`: how numerals look on the carrier, if the +-- backend supports literal coefficients; +-- · `blockedNames`: the operator/constant heads, to be kept +-- opaque while the goal is analysed; +-- · `encodeEq`/`finishSolve`: the equation node and the final +-- solver call; +-- +-- * a macro that type-checks its bundle argument against the +-- structure's bundle type and calls `solveByTheory`. +-- +-- `solveByTheory` takes care of everything else: +-- +-- * the goal type: walking under its pi-prefix (type aliases, +-- binder visibility), splitting the equation, and the +-- metavariable retry/error policy; +-- * inspecting the goal without ever normalising it: each step is +-- a weak-head reduction with `blockedNames` opaque, so reduction +-- stops exactly when recognised syntax surfaces; +-- * atoms: unrecognised subterms become solver variables, kept +-- exactly as the user wrote them (a literal like `1ℚ` is never +-- unfolded into the emitted call) and deduplicated up to whnf; +-- * encoding both sides and unifying the hole with the assembled +-- solver call. {-# OPTIONS --without-K --safe #-} @@ -14,322 +43,383 @@ module Tactic.Solver.Algebra where open import Agda.Builtin.Reflection using (withReduceDefs) open import Data.Bool -open import Data.List as List using (List; _∷_; []; _++_; replicate; null) -open import Data.Maybe as Maybe using (Maybe; just; nothing) +open import Data.List as List using (List; _∷_; []; replicate; filterᵇ) +open import Data.Maybe as Maybe using (Maybe; just; nothing; _<∣>_) open import Data.Nat -open import Data.Nat.Reflection open import Data.Product +open import Data.String using (String) open import Data.Unit -open import Data.Vec using (_∷_; []) +open import Data.Vec as Vec using (Vec) open import Function +open import Class.Functor +open import Class.Monad.Instances +open import Class.Traversable + open import Reflection +open import Reflection.AST.AlphaEquality using (_=α=_) open import Reflection.AST.Argument open import Reflection.AST.DeBruijn import Reflection.AST.Name as Name open import Reflection.AST.Term -open import Reflection.TCM.Syntax +open import Reflection.TCM.Syntax hiding (_<$>_) open import Reflection.Utils.Args open import Reflection.Utils.Core -open import Reflection.Utils.Metas -open import Reflection.Utils.TCM +open import Reflection.Utils.Records using (fieldProjection; projectField) +open import Reflection.Utils.AtomStore using (Atom; AtomStore; insertAtomStore; atomStoreIndex; atomSpellings) +open import Reflection.Utils.Goal using (underPis; requireEquationSides; blockOnEquationMetas) ------------------------------------------------------------------------ --- I. Reflection helpers - --- Peels leading λ-binders before reading the head Name. -headName : Term → Maybe Name -headName (def nm _) = just nm -headName (lam _ (abs _ body)) = headName body -headName _ = nothing - -_≡ᵐ_ : Maybe Name → Maybe Name → Bool -just n ≡ᵐ just m = n Name.≡ᵇ m -nothing ≡ᵐ nothing = true -_ ≡ᵐ _ = false - --- For wrapped numeric carriers like ℤ's `+_`: peel one `con C (n ∷ [])` layer. -peelLitCon : Name → Term → Maybe ℕ -peelLitCon C (con nm xs) = case nm Name.≡ᵇ C of λ where - false → nothing - true → case vArgs xs of λ where - (a ∷ []) → extractNat a - _ → nothing -peelLitCon _ _ = nothing - -extractCarrierNat : Maybe Name → Term → Maybe ℕ -extractCarrierNat mC t = case extractNat t of λ where - (just n) → just n - nothing → case mC of λ where - (just C) → peelLitCon C t - nothing → nothing +-- I. Classification helpers. + +-- A projected operator like `def CSR._+_ (R ⟨∷⟩ a ⟨∷⟩ b ⟨∷⟩ [])` +-- carries the bundle as a leading visible arg; this returns how many +-- such prefix args to skip before reaching the operator's last +-- `arity` visibles. +-- +-- This assumes any extra visibles beyond `arity` are a *prefix* +-- (bundle arguments). That holds for the operators of a bundle over +-- a `Set` carrier. It fails for a *function* carrier (`A → B`, with +-- pointwise `_≈_`): there `_+_ f g x` over-applies the operator with +-- the point `x` as a trailing arg, which `opDrop` would mistake for +-- a bundle prefix and so misread the operands. Function-typed +-- carriers are therefore unsupported (they fail loudly, not +-- unsoundly: the operands come out wrong and the backend `refl` +-- won't typecheck). +opDrop : ℕ → Args Term → ℕ +opDrop arity xs = visibleCount xs ∸ arity ------------------------------------------------------------------------ -- II. Theory specification. -- --- `detect` and `encode` are separated so the macro can collect atoms --- (which needs operator detection only) before the atom count is --- known (which `encode` needs). +-- The proof term the driver emits has the shape +-- +-- λ p₁ … pₖ → solve R n (λ x₁ … xₙ → lhs′ := rhs′) refl a₁ … aₙ +-- +-- with k binders for the goal's pi-prefix, n the number of atoms, +-- the aᵢ the atoms themselves, and lhs′/rhs′ the goal's two sides +-- re-encoded as backend expressions over the variables xᵢ, joined by +-- the backend's equation former (`_:=_` for the ring backends). +-- Atom i appears in the body as a reference to binder xᵢ₊₁ (the +-- backend's `solve` applies this n-ary function to the variable +-- expressions `var 0F … var (n−1)F`, in atom-store order — matching +-- the trailing aᵢ). The +-- encoders below build the pieces of this term, and `EncodeEnv` +-- carries the two things they +-- need but that are only known once both sides of the goal have been +-- parsed: the atom count n, and the bundle Term at the right de +-- Bruijn depth for the splice position. (Encoders take the env as an +-- argument — rather than being constructed after parsing — so that +-- `detect` can return each operator's detection pattern and encoder +-- as one value, with no ordering invariant between separate lists.) +-- +-- The explicit `R`/`n` splices possible via passing `EncodeEnv` into +-- the `encode` functions earn their keep: inferring them is +-- semantically fine but measured ~11× slower on the test suite. -record OperatorMatch : Set where - constructor opMatch +record EncodeEnv : Set where field - opTerm : Term - arity : ℕ + -- The bundle, weakened past the k pi-binders, for splicing at the + -- solver call. + R↓ : Term + numAtoms : ℕ -- n --- For theories with literal coefficients (the ring solvers). Other --- theories supply `nothing`. -record LiteralMatch : Set where - constructor litMatch - field - -- ℤ-style wrapper (e.g. ℤ's `+_`); `nothing` for unwrapped ℕ-style. - litCon : Maybe Name - peelSuc : Bool + -- The bundle for splicing inside the `λ x₁ … xₙ → …` body. + R↓↓ : Term + R↓↓ = weaken numAtoms R↓ -record TheoryDetect : Set where +record Operator : Set where field - -- The order chosen here is the source of truth: `opEncoders` in - -- `TheoryEncode` must use the same order. - operatorMatches : List OperatorMatch - -- Names to feed `withReduceDefs` so the operator boundary stays - -- opaque while the macro inspects the user's term. - blockedNames : List Name - literalMatch : Maybe LiteralMatch - -record TheoryEncode : Set where + -- Pattern: goal subterms whose head Name matches `opTerm`'s + -- (lambda-peeled) head are occurrences of this operator. + opTerm : Term + arity : ℕ + -- Builds the backend expression for an occurrence of this + -- operator: given Terms of the backend's expression type for the + -- operands, produce one for the operator applied to them — e.g. + -- the ring `_+_` maps operand encodings x, y to the Term `x :+ y`. + encode : EncodeEnv → Vec Term arity → Term + +-- The first operator whose `opTerm` has head `nm`. +findOperator : List Operator → Name → Maybe Operator +findOperator [] _ = nothing +findOperator (o ∷ os) nm = + if just nm ≡ᵐ headName (Operator.opTerm o) + then just o + else findOperator os nm + +-- A slot declares one piece of the structure's syntax: the bundle +-- field it is detected from, paired with its `Operator` content. +-- `derived` marks syntax that is not a field (e.g. a ring's `_-_`): +-- it is resolved by *normalising* its projection, so occurrences +-- match via their unfolding. +data SlotKind : Set where + op derived : SlotKind + +record Slot : Set where field - -- Parallel to `TheoryDetect.operatorMatches`. - opEncoders : List (List Term → Term) - encodeNat : ℕ → Term - -- Maps `suc t` to the polynomial Term for `1 + t`. - sucPeel : Term → Term - encodeVar : ℕ → Term - encodeEq : Term → Term → Term - -- Body has `numAtoms` polynomial-var binders introduced. - finishSolve : (lambdaBody : Term) (atoms : List Term) → Term - --- Operator match paired with its encoder. -record OperatorEntry : Set where + fieldName : Name + arity : ℕ + kind : SlotKind + encode : EncodeEnv → Vec Term arity → Term + +mkSlot : (nm : Name) (a : ℕ) → SlotKind → (EncodeEnv → Vec Term a → Term) → Slot +mkSlot nm a k e = record { fieldName = nm ; arity = a ; kind = k ; encode = e } + +slotIsConcrete : Slot → Bool +slotIsConcrete s = case Slot.kind s of λ where + derived → false + op → true + +-- Resolve each slot against the bundle (`k` = the bundle type's +-- parameter count): concrete fields by name-preserving projection, +-- derived syntax by normalisation. +resolveSlots : ℕ → List Slot → Term → TC (List (Slot × Term)) +resolveSlots k slots R = traverse (λ s → (s ,_) <$> slotTerm s) slots + where + slotTerm : Slot → TC Term + slotTerm s = case Slot.kind s of λ where + derived → normalise (fieldProjection k R (Slot.fieldName s)) + op → projectField k R (Slot.fieldName s) + +operatorsOf : List (Slot × Term) → List Operator +operatorsOf = List.map λ (s , t) → + record { opTerm = t ; arity = Slot.arity s ; encode = Slot.encode s } + +-- The concrete slots' head names: see `DetectedTheory.blockedNames`. +blockedOf : List (Slot × Term) → List Name +blockedOf = List.foldr pickDefName [] + ∘ List.map proj₂ + ∘ filterᵇ (slotIsConcrete ∘ proj₁) + +-- The resolved Term of the slot declared from the given field. +lookupSlot : Name → List (Slot × Term) → Maybe Term +lookupSlot nm [] = nothing +lookupSlot nm ((s , t) ∷ rest) = + if nm Name.≡ᵇ Slot.fieldName s then just t else lookupSlot nm rest + +-- For theories with literal coefficients (the ring solvers). +record LiteralSpec : Set where field - opTerm : Term - arity : ℕ - encode : List Term → Term - -mkOperatorEntry : OperatorMatch → (List Term → Term) → OperatorEntry -mkOperatorEntry (opMatch t a) enc = record { opTerm = t ; arity = a ; encode = enc } - -record Theory : Set₁ where + -- Wrapper constructor for numerals (ℤ's `+_`); `nothing` for + -- carriers whose numerals are bare ℕ literals. + litCon : Maybe Name + -- Constructor for negative numerals (ℤ's `-[1+_]`), for theories + -- whose coefficients support negation; its payload `n` denotes + -- the value `-(1+n)`. + negLitCon : Maybe Name + -- Peel bare `suc`s (ℕ-style carriers): `suc t ≈ 1# + t`. + peelSuc : Bool + -- Peel `suc`s under the wrapper: sound iff the wrapper is an + -- additive homomorphism, `C (suc n) ≈ 1# + C n` (true for `+_`). + peelWrappedSuc : Bool + -- Encoders for the above. `encodeSucPeel` maps an encoded `t` to + -- the encoding of `1# + t`. + encodeNat : EncodeEnv → ℕ → Term + encodeNegSuc : EncodeEnv → ℕ → Term + encodeSucPeel : EncodeEnv → Term → Term + +-- Everything `detect` learned about the user's bundle. +record DetectedTheory : Set where field - bundleType : Term - State : Set - detect : Term → TC (TheoryDetect × State) - -- R↓↓ = R weakened past `numPiVars + numAtoms` lambdas (used - -- inside the polynomial-λ body). - -- R↓ = R weakened past `numPiVars` (used outside, by `finishSolve`). - encode : (R↓↓ R↓ : Term) (numAtoms : ℕ) (state : State) → TheoryEncode + operators : List Operator + literalSpec : Maybe LiteralSpec + -- Names that must stay opaque while the goal is inspected, fed + -- to `withReduceDefs`. Must contain every operator's + -- (lambda-peeled) head name. + blockedNames : List Name + encodeEq : EncodeEnv → Term → Term → Term + finishSolve : EncodeEnv → (lambdaBody : Term) (atoms : List Term) → Term + +record Theory : Set where + field + -- Used in error messages. + macroName : String + detect : Term → TC DetectedTheory ------------------------------------------------------------------------ --- III. Operator classification and conversion. - --- Generic classifier: pick the first entry whose `opTerm` has `nm` --- as its (lambda-peeled) head `def`. -classifyOp : ∀ {A : Set} → (A → Term) → List A → Name → Maybe A -classifyOp _ [] _ = nothing -classifyOp getTerm (a ∷ as) nm = - if just nm ≡ᵐ headName (getTerm a) - then just a - else classifyOp getTerm as nm - --- A projected operator like `def CSR._+_ (R ⟨∷⟩ a ⟨∷⟩ b ⟨∷⟩ [])` --- carries the bundle as a leading visible arg; this returns how many --- such prefix args to skip before reaching the operator's last --- `arity` visibles. -opDrop : ℕ → Args Term → ℕ -opDrop arity xs = visibleCount xs ∸ arity - -convertTerm : TheoryDetect → TheoryEncode → (Term → TC Term) → Term → TC Term -convertTerm det enc fallback = convert +-- III. Numeral recognition. + +-- How a (weak-head-reduced) goal subterm looks through the theory's +-- literal description. +data NumeralView : Set where + natLit : ℕ → NumeralView -- the numeral `n` + negsucLit : ℕ → NumeralView -- the numeral `-(1+n)` + sucOf : Term → NumeralView -- `1# + ⟦payload⟧` (bare or wrapped suc) + wrappedOpaque : Term → NumeralView -- wrapper around a non-numeral; + -- payload = whnf key for atomising + notNumeral : NumeralView + +-- First match wins: numeral, negative numeral, bare `suc`, and — +-- the only TC case, since it must reduce under the wrapper — a +-- wrapper application. +numeralView : Maybe LiteralSpec → Term → TC NumeralView +numeralView nothing _ = pure notNumeral +numeralView (just ls) t = + case (natural <∣> negative <∣> bareSuc) of λ where + (just v) → pure v + nothing → wrapper where - open TheoryDetect det - open TheoryEncode enc + open LiteralSpec ls + + natural : Maybe NumeralView + natural = Maybe.map natLit (extractCarrierNat litCon t) + + negative : Maybe NumeralView + negative = Maybe.map negsucLit (Maybe.maybe′ (λ C → peelLitCon C t) nothing negLitCon) + + bareSuc : Maybe NumeralView + bareSuc = case (peelSuc , t) of λ where + (true , con (quote suc) (arg (arg-info visible _) x ∷ [])) → just (sucOf x) + _ → nothing + + -- `C (suc n)` peels to `1# + C n`; anything else under the wrapper + -- is an atom, with the wrapper-of-reduced-tail as its whnf key. + peelUnderWrapper : Name → Term → TC NumeralView + peelUnderWrapper C inner = do + inner' ← reduce inner + pure (case inner' of λ where + (con (quote suc) (arg (arg-info visible _) x ∷ [])) → sucOf (con C (vArg x ∷ [])) + _ → wrappedOpaque (con C (vArg inner' ∷ []))) + + wrapper : TC NumeralView + wrapper = case t of λ where + (con C (arg (arg-info visible _) inner ∷ [])) → + if peelWrappedSuc ∧ (just C ≡ᵐ litCon) + then peelUnderWrapper C inner + else pure notNumeral + _ → pure notNumeral - ops : List OperatorEntry - ops = List.zipWith mkOperatorEntry operatorMatches opEncoders - - litCon : Maybe Name - litCon = Maybe.maybe LiteralMatch.litCon nothing literalMatch - - peelSuc-on : Bool - peelSuc-on = Maybe.maybe LiteralMatch.peelSuc false literalMatch - - mutual - convert : Term → TC Term - convert t = case (literalMatch , extractCarrierNat litCon t) of λ where - (just _ , just n) → pure (encodeNat n) - _ → convertHead t - - convertHead : Term → TC Term - convertHead t@(def nm xs) = case classifyOp OperatorEntry.opTerm ops nm of λ where - nothing → fallback t - (just e) → do - let open OperatorEntry e - args ← convertVisibleArgs (opDrop arity xs) xs - pure (encode args) - convertHead t@(con (quote suc) (arg (arg-info visible _) x ∷ [])) = - if peelSuc-on then sucPeel <$> convert x else fallback t - convertHead t = fallback t - - convertVisibleArgs : ℕ → Args Term → TC (List Term) - convertVisibleArgs _ [] = pure [] - convertVisibleArgs (suc d) (arg (arg-info visible _) _ ∷ xs) = convertVisibleArgs d xs - convertVisibleArgs 0 (arg (arg-info visible _) x ∷ xs) = do - x' ← convert x - xs' ← convertVisibleArgs 0 xs - pure (x' ∷ xs') - convertVisibleArgs d (_ ∷ xs) = convertVisibleArgs d xs - -collectAtoms : TheoryDetect → Term → List Term → TC (List Term) -collectAtoms det = collect - where - open TheoryDetect det +------------------------------------------------------------------------ +-- V. Parsing a goal side into its deferred backend encoding. - litCon : Maybe Name - litCon = Maybe.maybe LiteralMatch.litCon nothing literalMatch +private + fuel : ℕ + fuel = 1024 -- Should be sufficient for anything practicl - peelSuc-on : Bool - peelSuc-on = Maybe.maybe LiteralMatch.peelSuc false literalMatch +-- An `Encoding` is a backend expression awaiting the `EncodeEnv` +-- (only known once both sides are parsed). Parsing composes the +-- encodings directly — there is no intermediate syntax tree. +Encoding : Set +Encoding = EncodeEnv → Term - mutual - collect : Term → List Term → TC (List Term) - collect t acc = case (literalMatch , extractCarrierNat litCon t) of λ where - (just _ , just _) → pure acc - _ → collectHead t acc - - collectHead : Term → List Term → TC (List Term) - collectHead (def nm xs) acc = case classifyOp OperatorMatch.opTerm operatorMatches nm of λ where - nothing → pure (insertAtom (def nm xs) acc) - (just (opMatch _ arity)) → collectArgs (opDrop arity xs) xs acc - collectHead t@(con (quote suc) ((arg (arg-info visible _) x ∷ []))) acc = - if peelSuc-on then collect x acc else pure (insertAtom t acc) - collectHead t acc = pure (insertAtom t acc) - - collectArgs : ℕ → Args Term → List Term → TC (List Term) - collectArgs _ [] acc = pure acc - collectArgs (suc d) (arg (arg-info visible _) _ ∷ xs) acc = collectArgs d xs acc - collectArgs 0 (arg (arg-info visible _) x ∷ xs) acc = collect x acc >>= collectArgs 0 xs - collectArgs d (_ ∷ xs) acc = collectArgs d xs acc - --- Used to seed `withReduceDefs`'s block list with the operator --- names we'll encounter. -collectOpNames : TheoryDetect → Term → List Name → TC (List Name) -collectOpNames det = collect +-- Parse a goal side, threading the atom store through. +-- +-- Each node is brought to weak-head normal form first — the caller +-- wraps this in `withReduceDefs` blocking the theory's names, so whnf +-- stops exactly when an operator or numeral surfaces, while aliases, +-- β-redexes and other definitions unfold. A subterm that exposes +-- neither is atomised with its original spelling (section IV). +parseGoalTerm : DetectedTheory → Term → AtomStore → TC (Encoding × AtomStore) +parseGoalTerm det = parse fuel where - open TheoryDetect det - + open DetectedTheory det + + -- The numeral encodings are only formed when `numeralView` ran + -- under `just` a literal spec, so the `unknown` fallback is + -- unreachable. + litEnc : (LiteralSpec → EncodeEnv → Term) → Encoding + litEnc f = Maybe.maybe′ f (λ _ → unknown) literalSpec + + -- The bottom of the recogniser cascade: every subterm in which + -- `parse` finds no theory syntax ends up here. `orig` is the + -- subterm exactly as the user wrote it — the only form that may + -- appear in the emitted call; `whnf` is whatever reduced form the + -- caller already has, used only as the store's second identity key + -- (never emitted). Returns the encoding referencing the atom's + -- solver binder. + atomise : (orig whnf : Term) → AtomStore → TC (Encoding × AtomStore) + atomise orig whnf acc = do + let acc' = insertAtomStore (orig , whnf) acc + -- see `Reflection.Utils.AtomStore` for why we do this + just i ← pure (atomStoreIndex (orig , whnf) acc') + where nothing → typeError + ( strErr "Internal error in Tactic.Solver.Algebra: atom " + ∷ termErr orig + ∷ strErr " not found after insertion." + ∷ []) + -- Atom i refers to the i-th of the n binders wrapped around the + -- body by the driver; the outermost binder is atom 0. + pure ((λ env → var (EncodeEnv.numAtoms env ∸ suc i) []) , acc') + + -- The ℕ argument is recursion-depth fuel (the per-node `reduce` + -- makes the recursion non-structural); it bounds the *depth* of the + -- recognised expression structure, so running out — at which point + -- the subterm is atomised whole — is purely theoretical. mutual - collect : Term → List Name → TC (List Name) - collect (def nm xs) acc = case classifyOp OperatorMatch.opTerm operatorMatches nm of λ where - nothing → pure acc - (just (opMatch _ arity)) → collectArgs (opDrop arity xs) xs (insertName nm acc) - collect _ acc = pure acc - - collectArgs : ℕ → Args Term → List Name → TC (List Name) - collectArgs _ [] acc = pure acc - collectArgs (suc d) (arg (arg-info visible _) _ ∷ xs) acc = collectArgs d xs acc - collectArgs 0 (arg (arg-info visible _) x ∷ xs) acc = collect x acc >>= collectArgs 0 xs - collectArgs d (_ ∷ xs) acc = collectArgs d xs acc + parse : ℕ → Term → AtomStore → TC (Encoding × AtomStore) + parse zero t acc = atomise t t acc + parse (suc k) t acc = do + t' ← reduce t + nv ← numeralView literalSpec t' + case nv of λ where + (natLit n) → pure (litEnc (λ ls env → LiteralSpec.encodeNat ls env n) , acc) + (negsucLit n) → pure (litEnc (λ ls env → LiteralSpec.encodeNegSuc ls env n) , acc) + (sucOf tail) → + (λ (e , acc') → litEnc (λ ls env → LiteralSpec.encodeSucPeel ls env (e env)) , acc') + <$> parse k tail acc + (wrappedOpaque w) → atomise t w acc + notNumeral → parseHead k t t' acc + + parseHead : ℕ → (orig whnf : Term) → AtomStore → TC (Encoding × AtomStore) + parseHead k orig t'@(def nm xs) acc = case findOperator operators nm of λ where + nothing → atomise orig t' acc + (just o) → let open Operator o in do + (just (es , acc')) ← parseVisibleArgs k arity (opDrop arity xs) xs acc + -- Fewer than `arity` operands in the spine (possible when + -- the carrier is a function type): atomise the whole term. + where nothing → atomise orig t' acc + pure ((λ env → encode env (Vec.map (λ e → e env) es)) , acc') + + parseHead k orig t' acc = atomise orig t' acc + + -- Skip `d` visible arguments, then parse exactly `n`. + parseVisibleArgs : ℕ → (n d : ℕ) → Args Term → AtomStore + → TC (Maybe (Vec Encoding n × AtomStore)) + parseVisibleArgs k zero _ _ acc = + pure (just (Vec.[] , acc)) + parseVisibleArgs k (suc n) (suc d) (arg (arg-info visible _) _ ∷ xs) acc = + parseVisibleArgs k (suc n) d xs acc + parseVisibleArgs k (suc n) 0 (arg (arg-info visible _) x ∷ xs) acc = do + e , acc' ← parse k x acc + m ← parseVisibleArgs k n 0 xs acc' + pure (Maybe.map (λ (es , acc'') → (e Vec.∷ es) , acc'') m) + parseVisibleArgs k (suc n) d (_ ∷ xs) acc = + parseVisibleArgs k (suc n) d xs acc + parseVisibleArgs k (suc n) _ [] acc = + pure nothing ------------------------------------------------------------------------ --- IV. The generic macro core. - -malformedClosedEqError : ∀ {a} {A : Set a} → Term → TC A -malformedClosedEqError found = typeError - ( strErr "Malformed call to algebraic solver." - ∷ strErr "Expected target type to be of shape LHS ≈ RHS." - ∷ strErr "Instead: " - ∷ termErr found - ∷ []) - --- The `nothing` branch is unreachable on well-formed input — --- `collectAtoms` already inserted every term `convertTerm` will --- look up — but we error loudly rather than silently emit a default. -private - atomFB : TheoryEncode → List Term → Term → TC Term - atomFB enc atoms t = do - just i ← pure (findAtomIndex t atoms) - where nothing → typeError - ( strErr "Internal error in solve-≈: atom " - ∷ termErr t - ∷ strErr " was not found in the atom list." - ∷ []) - pure (TheoryEncode.encodeVar enc i) +-- VI. The generic macro core. --- Precondition: `R` has been type-checked against `Theory.bundleType` --- by the caller (e.g. via `Tactic.Solver.Ring.detectSide`). -solveByTheory : (thy : Theory) → Term → Term → TC ⊤ -solveByTheory thy `R hole = do - det , state ← Theory.detect thy `R - let bundleNs = TheoryDetect.blockedNames det - - `hole₀ ← inferType hole - let _ , equation₀ = stripPis `hole₀ - opNames ← case getVisibleArgs 2 equation₀ of λ where - (just (lhs₀ ∷ rhs₀ ∷ [])) → collectOpNames det lhs₀ bundleNs >>= collectOpNames det rhs₀ - _ → pure bundleNs - - withReduceDefs (false , opNames) $ do - -- `normalise`, not `reduce`: Agda's elaborator can leave the - -- goal type wrapped in lambdas that need β-reducing first. - `hole ← normalise `hole₀ - let variablesAndTypes , equation = stripPis `hole - let sides = getVisibleArgs 2 equation - - -- Deadlock detection: if some side has a meta not shared with - -- the other side, `blockOnMeta` would retry forever (only this - -- macro could resolve it). Shared metas are fine — Agda - -- propagates constraints across `≈`. - case sides of λ where - (just (lhs ∷ rhs ∷ [])) → do - let bothStructured = not (isMeta lhs) ∧ not (isMeta rhs) - let metasL = findMetaIds lhs - let metasR = findMetaIds rhs - let anyMetas = not (null metasL ∧ null metasR) - let sharedMeta = shareMeta metasL metasR - if bothStructured ∧ anyMetas ∧ not sharedMeta - then typeError - ( strErr "solve-≈: the goal `LHS ≈ RHS` has at least one side " - ∷ strErr "containing a metavariable that could not be resolved. To run this " - ∷ strErr "solver you must add type annotations to resolve these variables." - ∷ []) - else pure tt - _ → pure tt - - case firstMeta `hole of λ where - (just m) → blockOnMeta m - nothing → pure tt - let variables = List.map proj₁ variablesAndTypes - let numPiVars = List.length variables - - just (lhs ∷ rhs ∷ []) ← pure sides - where nothing → malformedClosedEqError `hole - - atoms₀ ← collectAtoms det lhs [] - atoms ← collectAtoms det rhs atoms₀ +private + -- Build the solver call for the equation, `numPiVars` binders below + -- the hole's context. + solveEquation : String → DetectedTheory → Term → ℕ → Term → TC Term + solveEquation macroName det `R numPiVars equation = do + lhs , rhs ← requireEquationSides equation + blockOnEquationMetas macroName equation lhs rhs + + lhsEnc , store₀ ← parseGoalTerm det lhs [] + rhsEnc , store ← parseGoalTerm det rhs store₀ + let atoms = atomSpellings store let numAtoms = List.length atoms - let `R↓↓ = weaken (numPiVars + numAtoms) `R - let `R↓ = weaken numPiVars `R - let enc = Theory.encode thy `R↓↓ `R↓ numAtoms state - - `lhsExpr ← convertTerm det enc (atomFB enc atoms) lhs - `rhsExpr ← convertTerm det enc (atomFB enc atoms) rhs - - let open TheoryEncode enc - let lambdaBody = encodeEq `lhsExpr `rhsExpr + let env = record { R↓ = weaken numPiVars `R ; numAtoms = numAtoms } + let open DetectedTheory det + let lambdaBody = encodeEq env (lhsEnc env) (rhsEnc env) let f = prependVLams (replicate numAtoms "x") lambdaBody - let solverCall = finishSolve f atoms + pure (finishSolve env f atoms) - -- Re-introduce the pi-binders the user didn't pattern-bind. - let final = prependVLams variables solverCall - unify hole final +-- Precondition: `R` has been type-checked against the structure's +-- bundle type by the caller (e.g. via `Tactic.Solver.Ring.detectSide`). +solveByTheory : Theory → Term → Term → TC ⊤ +solveByTheory thy `R hole = do + let open Theory thy + det ← detect `R + holeTy ← inferType hole + -- Only the goal *analysis* runs with the theory's names blocked + final ← withReduceDefs (false , DetectedTheory.blockedNames det) + (underPis fuel holeTy (solveEquation macroName det `R)) + unify hole final diff --git a/Tactic/Solver/Ring.agda b/Tactic/Solver/Ring.agda index b4abe59d..94058f62 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring.agda @@ -8,8 +8,16 @@ -- * CR → `Tactic.Solver.Ring.IntegerCoefficients R` (ℤ -- coefficients, real negation; recognises `_-_` and `-_`). -- --- Built on `Tactic.Solver.Algebra`. For a new structure (monoid, --- lattice, …), write a fresh `Theory` and macro alongside this one. +-- Built on `Tactic.Solver.Algebra`, which owns the generic pipeline; +-- this module only says what a ring is: +-- +-- * the *slot table* (`csrSlots`/`crSlots`): one entry per piece of +-- ring syntax, pairing the bundle field it is detected from with +-- the encoder producing its polynomial-AST Term; +-- * how literals look on the carrier (`detectLitStyle`, +-- `mkLiteralSpec`); +-- * how to assemble the final `solve n (λ xs → lhs := rhs) refl` +-- call (`finishSolve`). {-# OPTIONS --without-K --safe #-} @@ -17,141 +25,123 @@ module Tactic.Solver.Ring where open import Algebra using (CommutativeSemiring; CommutativeRing) -open import Data.Bool using (Bool; true; false) -open import Data.Fin using (Fin) -open import Data.Integer using (ℤ; +_) -open import Data.List as List using (List; _∷_; []; map; foldr; length; drop; zip; filterᵇ; reverse) +open import Data.Bool using (Bool; true; false; if_then_else_) +open import Data.Integer using (ℤ; +_; -[1+_]) +open import Data.List as List using (List; _∷_; []) open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe) open import Data.Nat using (ℕ; suc; zero) -import Data.Vec as Vec -open import Data.Nat.Reflection -open import Data.Product using (_,_; _×_; proj₁; proj₂; uncurry) +open import Data.Nat.Reflection using (toTerm) +open import Data.Product using (_,_; _×_) open import Data.Unit +open import Data.Vec as Vec using (Vec) open import Function open import Class.Functor open import Class.Monad.Instances -open import Class.Traversable open import Reflection open import Reflection.AST.Argument import Reflection.AST.Name as Name open import Reflection.AST.Term open import Reflection.TCM.Syntax hiding (_<$>_) -open import Reflection.Utils.Args using (vArgs; takeFirst) -open import Reflection.Utils.Core using (extractNat; pickDefName) -open import Reflection.Utils.TCM using (headReduce; headReducePeel) +open import Reflection.Utils.Args using (vArgs) +open import Reflection.Utils.Core using (extractNat) +open import Reflection.Utils.Records + using (fieldProjection; projectField) open import Tactic.Solver.Algebra import Tactic.Solver.Ring.IntegerCoefficients as IntC ------------------------------------------------------------------------- --- `Algebra.Solver.Ring.Polynomial`'s `con`, `var`, and `:-_` are --- nested constructors inside a four-parameter module. Defining --- top-level aliases lets the macro reflect them by name (with just --- `R` as the visible argument) rather than reconstructing all four --- module parameters. - -module Solver {c ℓ} (R : CommutativeSemiring c ℓ) where +module NatC {c ℓ} (R : CommutativeSemiring c ℓ) where open import Algebra.Solver.Ring.NaturalCoefficients.Default R public conP : ∀ {n} → ℕ → Polynomial n conP = con - varP : ∀ {n} → Fin n → Polynomial n - varP = var - ------------------------------------------------------------------------ --- Backend reflection helpers (private). +-- The two ring flavours and their backend names. private data RingSide : Set where csr cr : RingSide - data LitStyle : Set where - natStyle : LitStyle -- bare ℕ literals; peel `suc`. - wrapped : Name → LitStyle -- `con C ⟨ n ⟩` (e.g. ℤ's `+_`). - - -- Threaded from `detect` to `encode`. - record RingState : Set where - field - litStyle : Maybe LitStyle - ------------------------------------------------------------------------- --- Operator-projection Terms from the user's bundle. - -private - projTerm : Name → Term → Term - projTerm nm R = def nm (2 ⋯⟅∷⟆ R ⟨∷⟩ []) - - csrAdd csrMul csrZero csrOne : Name - csrAdd = quote CommutativeSemiring._+_ - csrMul = quote CommutativeSemiring._*_ - csrZero = quote CommutativeSemiring.0# - csrOne = quote CommutativeSemiring.1# - - crAdd crMul crSub crNeg crZero crOne : Name - crAdd = quote CommutativeRing._+_ - crMul = quote CommutativeRing._*_ - crSub = quote CommutativeRing._-_ - crNeg = quote (CommutativeRing.-_) - crZero = quote CommutativeRing.0# - crOne = quote CommutativeRing.1# - bundleTypeOf : RingSide → Term bundleTypeOf csr = def (quote CommutativeSemiring) (2 ⋯⟨∷⟩ []) bundleTypeOf cr = def (quote CommutativeRing) (2 ⋯⟨∷⟩ []) + conName addName mulName eqName solveName reflName zeroName oneName : RingSide → Name + conName csr = quote NatC.conP ; conName cr = quote IntC.conP + addName csr = quote NatC._:+_ ; addName cr = quote IntC._:+_ + mulName csr = quote NatC._:*_ ; mulName cr = quote IntC._:*_ + eqName csr = quote NatC._:=_ ; eqName cr = quote IntC._:=_ + solveName csr = quote NatC.solve ; solveName cr = quote IntC.solve + zeroName csr = quote CommutativeSemiring.0# ; zeroName cr = quote CommutativeRing.0# + oneName csr = quote CommutativeSemiring.1# ; oneName cr = quote CommutativeRing.1# + reflName csr = quote CommutativeSemiring.refl ; reflName cr = quote CommutativeRing.refl + ------------------------------------------------------------------------ --- Polynomial-AST Term builders. Calling shape: --- `def NAME (2 hidden + R-bundle ⟨∷⟩ numVars ⟅∷⟆ ⟨args…⟩)`, --- pulling NAMEs from `Solver.*` for CSR and `IntC.*` for CR. +-- Polynomial-AST encoders. Every backend name re-exported by +-- `NatC`/`IntC` has telescope `{c ℓ} (R) {n} → … Polynomial n …`, +-- where the hidden `n` is the expression type's variable-count +-- index — equal to the atom count. Each emitted node instantiates +-- `R` and `n` explicitly: +-- `def NAME (2 hidden ∷ R ⟨∷⟩ numAtoms ⟅∷⟆ ⟨args…⟩)`. private - defP : (R `n : Term) → Name → List (Arg Term) → Term - defP R `n nm args = - def nm (2 ⋯⟅∷⟆ R ⟨∷⟩ `n ⟅∷⟆ args) - - conName varName addName mulName eqName solveName reflName - : RingSide → Name - conName csr = quote Solver.conP ; conName cr = quote IntC.conP - varName csr = quote Solver.varP ; varName cr = quote IntC.varP - addName csr = quote Solver._:+_ ; addName cr = quote IntC._:+_ - mulName csr = quote Solver._:*_ ; mulName cr = quote IntC._:*_ - eqName csr = quote Solver._:=_ ; eqName cr = quote IntC._:=_ - solveName csr = quote Solver.solve ; solveName cr = quote IntC.solve - reflName csr = quote CommutativeSemiring.refl - reflName cr = quote CommutativeRing.refl + defP : EncodeEnv → Name → List Term → Term + defP env nm args = + def nm (2 ⋯⟅∷⟆ EncodeEnv.R↓↓ env ⟨∷⟩ toTerm (EncodeEnv.numAtoms env) ⟅∷⟆ List.map vArg args) - `con : RingSide → (R `n : Term) → Term → Term - `con s R `n c = defP R `n (conName s) (c ⟨∷⟩ []) + -- A `def`-headed backend operator, applied to the encoded operands. + opEnc : ∀ {n} → Name → EncodeEnv → Vec Term n → Term + opEnc nm env args = defP env nm (Vec.toList args) - `var : RingSide → (R `n : Term) → Term → Term - `var s R `n i = defP R `n (varName s) (i ⟨∷⟩ []) - - `:+ : RingSide → (R `n : Term) → Term → Term → Term - `:+ s R `n x y = defP R `n (addName s) (x ⟨∷⟩ y ⟨∷⟩ []) + -- ℕ literal `n` rendered at the polynomial-coefficient type: + -- ℕ for CSR (`toTerm n`), ℤ for CR (wrapped with `+_`). + natLitTerm : RingSide → ℕ → Term + natLitTerm csr n = toTerm n + natLitTerm cr n = con (quote +_) (toTerm n ⟨∷⟩ []) - `:* : RingSide → (R `n : Term) → Term → Term → Term - `:* s R `n x y = defP R `n (mulName s) (x ⟨∷⟩ y ⟨∷⟩ []) + -- The polynomial constant `n`. + constEnc : RingSide → ℕ → EncodeEnv → Term + constEnc s n env = defP env (conName s) (natLitTerm s n ∷ []) - `:- : (R `n : Term) → Term → Term → Term - `:- R `n x y = defP R `n (quote IntC._:-_) (x ⟨∷⟩ y ⟨∷⟩ []) +------------------------------------------------------------------------ +-- The slot tables: all ring syntax, each piece pairing the bundle +-- field it is detected from with its encoder. - `:-‿ : (R `n : Term) → Term → Term - `:-‿ R `n x = defP R `n (quote IntC.negP) (x ⟨∷⟩ []) +private + csrSlots : List Slot + csrSlots = + mkSlot (quote CommutativeSemiring._+_) 2 op (opEnc (addName csr)) + ∷ mkSlot (quote CommutativeSemiring._*_) 2 op (opEnc (mulName csr)) + ∷ mkSlot (zeroName csr) 0 op (λ env _ → constEnc csr 0 env) + ∷ mkSlot (oneName csr) 0 op (λ env _ → constEnc csr 1 env) + ∷ [] - `:= : RingSide → (R `n : Term) → Term → Term → Term - `:= s R `n x y = defP R `n (eqName s) (x ⟨∷⟩ y ⟨∷⟩ []) + crSlots : List Slot + crSlots = + mkSlot (quote CommutativeRing._+_) 2 op (opEnc (addName cr)) + ∷ mkSlot (quote CommutativeRing._*_) 2 op (opEnc (mulName cr)) + ∷ mkSlot (quote CommutativeRing._-_) 2 derived (opEnc (quote IntC._:-_)) + ∷ mkSlot (quote (CommutativeRing.-_)) 1 op (opEnc (quote IntC.negP)) + ∷ mkSlot (zeroName cr) 0 op (λ env _ → constEnc cr 0 env) + ∷ mkSlot (oneName cr) 0 op (λ env _ → constEnc cr 1 env) + ∷ [] - `refl : RingSide → (R : Term) → Term - `refl s R = def (reflName s) (2 ⋯⟅∷⟆ R ⟨∷⟩ 1 ⋯⟅∷⟆ []) + slotsFor : RingSide → List Slot + slotsFor csr = csrSlots + slotsFor cr = crSlots ------------------------------------------------------------------------ -- Literal-style recognition from the bundle's `0#` and `1#` Terms. private + data LitStyle : Set where + natStyle : LitStyle -- bare ℕ literals; peel `suc`. + wrapped : Name → LitStyle -- `con C ⟨ n ⟩` (e.g. ℤ's `+_`). + detectLitStyle : Term → Term → Maybe LitStyle detectLitStyle (con cz argsZ) (con co argsO) = case (cz Name.≡ᵇ co) of λ where @@ -170,191 +160,79 @@ private (just 0 , just 1) → just natStyle _ → nothing ------------------------------------------------------------------------- --- Operator detection: concrete record peek + abstract-projection --- fallback. - -private - collectDefNames : List Term → List Name - collectDefNames = List.foldr pickDefName [] - - -- A slot's role. `op` is a generic concrete operator field; - -- `derived` is additional syntax that isn't a field; `zeroLit` and - -- `oneLit` mark literals. - data SlotKind : Set where - op zeroLit oneLit derived : SlotKind - - -- An operator slot: `(projection-name , arity , kind)`. The slot - -- order is the source of truth for `operatorMatches` (and so must - -- align with `opEncoders` in `mkEncode`). - Slot : Set - Slot = Name × ℕ × SlotKind - - slotProj : Slot → Name - slotProj s = proj₁ s - - slotArity : Slot → ℕ - slotArity s = proj₁ (proj₂ s) + -- ℤ's `+_` wrapper is special: it is an additive homomorphism, so + -- the parser may peel `suc`s under it, and (on the CR side, whose + -- coefficients are ℤ) `-[1+_]` is its negative counterpart. + mkLiteralSpec : RingSide → Maybe LitStyle → Maybe LiteralSpec + mkLiteralSpec _ nothing = nothing + mkLiteralSpec s (just style) = just (record + { litCon = litConOf style + ; negLitCon = negConOf s style + ; peelSuc = isNat style + ; peelWrappedSuc = isPos style + ; encodeNat = λ env n → constEnc s n env + ; encodeNegSuc = λ env n → defP env (conName s) (con (quote -[1+_]) (toTerm n ⟨∷⟩ []) ∷ []) + ; encodeSucPeel = λ env t → defP env (addName s) (constEnc s 1 env ∷ t ∷ []) + }) + where + litConOf : LitStyle → Maybe Name + litConOf natStyle = nothing + litConOf (wrapped C) = just C - slotKind : Slot → SlotKind - slotKind s = proj₂ (proj₂ s) + isNat : LitStyle → Bool + isNat natStyle = true + isNat _ = false - slotIsConcrete : Slot → Bool - slotIsConcrete s with slotKind s - ... | derived = false - ... | _ = true + isPos : LitStyle → Bool + isPos (wrapped C) = C Name.≡ᵇ quote +_ + isPos _ = false - csrSlots : List Slot - csrSlots = (csrAdd , 2 , op) - ∷ (csrMul , 2 , op) - ∷ (csrZero , 0 , zeroLit) - ∷ (csrOne , 0 , oneLit) - ∷ [] - - crSlots : List Slot - crSlots = (crAdd , 2 , op) - ∷ (crMul , 2 , op) - ∷ (crSub , 2 , derived) - ∷ (crNeg , 1 , op) - ∷ (crZero , 0 , zeroLit) - ∷ (crOne , 0 , oneLit) - ∷ [] - - slotsFor : RingSide → List Slot - slotsFor csr = csrSlots - slotsFor cr = crSlots - - mkLitMatch : Maybe LitStyle → Maybe LiteralMatch - mkLitMatch nothing = nothing - mkLitMatch (just natStyle) = just (litMatch nothing true) - mkLitMatch (just (wrapped C)) = just (litMatch (just C) false) - - -- Pull the `0` and `1` slot Terms by kind. Returns `nothing` if - -- either is missing from the slot list. - findZeroOne : List (Slot × Term) → Maybe (Term × Term) - findZeroOne = go nothing nothing - where - go : Maybe Term → Maybe Term → List (Slot × Term) → Maybe (Term × Term) - go (just z) (just o) _ = just (z , o) - go _ _ [] = nothing - go mz mo ((s , t) ∷ rest) with slotKind s - ... | zeroLit = go (just t) mo rest - ... | oneLit = go mz (just t) rest - ... | _ = go mz mo rest - - detectFor : RingSide → Term → TC (TheoryDetect × RingState) - detectFor side R = do - R' ← headReduce 16 R - let slots = slotsFor side - let concreteN = length (filterᵇ slotIsConcrete slots) - case R' of λ where - (con _ args) → case Maybe.map Vec.toList (takeFirst concreteN (drop 2 (vArgs args))) of λ where - (just rawOps) → do - concOps ← traverse ⦃ Functor-List ⦄ (headReducePeel 16) rawOps - slotted ← zipSlots slots concOps - slottedLit ← traverse ⦃ Functor-List ⦄ (λ (s , t) → (s ,_) <$> headReduce 16 t) slotted - let blockNs = collectDefNames concOps - let ls = maybe (uncurry detectLitStyle) nothing (findZeroOne slottedLit) - pure - ( record - { operatorMatches = List.map (λ (s , t) → opMatch t (slotArity s)) slotted - ; blockedNames = blockNs - ; literalMatch = mkLitMatch ls - } - , record { litStyle = ls } - ) - nothing → abstractPath slots - _ → abstractPath slots - where - zipSlots : List Slot → List Term → TC (List (Slot × Term)) - zipSlots [] _ = pure [] - zipSlots (s ∷ rest) ops = case slotKind s of λ where - derived → do - t ← normalise (projTerm (slotProj s) R) - rs ← zipSlots rest ops - pure ((s , t) ∷ rs) - _ → case ops of λ where - (t ∷ ops') → do - rs ← zipSlots rest ops' - pure ((s , t) ∷ rs) - [] → pure [] - - abstractPath : List Slot → TC (TheoryDetect × RingState) - abstractPath slots = do - ts ← traverse ⦃ Functor-List ⦄ normalise (List.map (λ s → projTerm (slotProj s) R) slots) - pure - ( record - { operatorMatches = List.map (λ (s , t) → opMatch t (slotArity s)) (zip slots ts) - ; blockedNames = [] - ; literalMatch = nothing - } - , record { litStyle = nothing } - ) + negConOf : RingSide → LitStyle → Maybe Name + negConOf cr (wrapped C) = if C Name.≡ᵇ quote +_ then just (quote -[1+_]) else nothing + negConOf _ _ = nothing ------------------------------------------------------------------------ --- Encoder construction. +-- Detection: resolve the slot table against the bundle +-- (`resolveSlots`/`projectField` handle the bundle's possible shapes +-- — constructor, copattern-compiled record expression, abstract +-- value — uniformly). private - -- ℕ literal `n` rendered at the polynomial-coefficient type: - -- ℕ for CSR (`toTerm n`), ℤ for CR (wrapped with `+_`). - natLitTerm : RingSide → ℕ → Term - natLitTerm csr n = toTerm n - natLitTerm cr n = con (quote +_) (toTerm n ⟨∷⟩ []) - - mkEncode : (s : RingSide) → (R↓↓ R↓ : Term) - → (numAtoms : ℕ) → Maybe LitStyle → TheoryEncode - mkEncode s R↓↓ R↓ numAtoms litStyle = record - { opEncoders = ops s - ; encodeNat = encNat - ; sucPeel = sucPeelFn - ; encodeVar = encVar - ; encodeEq = `:= s R↓↓ `n - ; finishSolve = finish - } + detectFor : RingSide → Term → TC DetectedTheory + detectFor side R = do + slotted ← resolveSlots numParams (slotsFor side) R + ls ← litStyleOf slotted + pure (record + { operators = operatorsOf slotted + ; literalSpec = mkLiteralSpec side ls + ; blockedNames = blockedOf slotted + ; encodeEq = λ env x y → defP env (eqName side) (x ∷ y ∷ []) + ; finishSolve = finish + }) where - `n = toTerm numAtoms - - opAdd : List Term → Term - opAdd (x ∷ y ∷ _) = `:+ s R↓↓ `n x y - opAdd _ = unknown - - opMul : List Term → Term - opMul (x ∷ y ∷ _) = `:* s R↓↓ `n x y - opMul _ = unknown - - opSub : List Term → Term - opSub (x ∷ y ∷ _) = `:- R↓↓ `n x y - opSub _ = unknown - - opNeg : List Term → Term - opNeg (x ∷ _) = `:-‿ R↓↓ `n x - opNeg _ = unknown - - opZero : List Term → Term - opZero _ = `con s R↓↓ `n (natLitTerm s 0) - - opOne : List Term → Term - opOne _ = `con s R↓↓ `n (natLitTerm s 1) - - -- The order here MUST match what `detectCSR`/`detectCR` emit - -- for `operatorMatches`. - ops : RingSide → List (List Term → Term) - ops csr = opAdd ∷ opMul ∷ opZero ∷ opOne ∷ [] - ops cr = opAdd ∷ opMul ∷ opSub ∷ opNeg ∷ opZero ∷ opOne ∷ [] - - encNat : ℕ → Term - encNat n = `con s R↓↓ `n (natLitTerm s n) - - sucPeelFn : Term → Term - sucPeelFn inner = - `:+ s R↓↓ `n (`con s R↓↓ `n (natLitTerm s 1)) inner - - encVar : ℕ → Term - encVar i = `var s R↓↓ `n (toFinTerm i) - - finish : Term → List Term → Term - finish lambdaBody atoms = - def (solveName s) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ `n ⟨∷⟩ lambdaBody ⟨∷⟩ `refl s R↓ ⟨∷⟩ List.map vArg atoms) + numParams : ℕ + numParams = 2 + + -- Plain whnf before `detectLitStyle`: it only needs the head + -- constructor, and a step-wise head reduction is pathologically + -- slow on carriers like ℚ whose literals unfold into + -- proof-carrying terms. + litStyleOf : List (Slot × Term) → TC (Maybe LitStyle) + litStyleOf slotted = + case (lookupSlot (zeroName side) slotted , lookupSlot (oneName side) slotted) of λ where + (just z , just o) → do + z' ← reduce z + o' ← reduce o + pure (detectLitStyle z' o') + _ → pure nothing + + finish : EncodeEnv → Term → List Term → Term + finish env body atoms = + def (solveName side) + (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ toTerm (EncodeEnv.numAtoms env) ⟨∷⟩ body ⟨∷⟩ `refl ⟨∷⟩ List.map vArg atoms) + where + R↓ = EncodeEnv.R↓ env + `refl = def (reflName side) (2 ⋯⟅∷⟆ R↓ ⟨∷⟩ 1 ⋯⟅∷⟆ []) ------------------------------------------------------------------------ -- The macro. @@ -362,10 +240,8 @@ private private ringTheory : RingSide → Theory ringTheory s = record - { bundleType = bundleTypeOf s - ; State = RingState - ; detect = detectFor s - ; encode = λ R↓↓ R↓ n st → mkEncode s R↓↓ R↓ n (RingState.litStyle st) + { macroName = "solve-≈" + ; detect = detectFor s } detectSide : Term → TC (RingSide × Term) diff --git a/Tactic/Solver/Ring/IntegerCoefficients.agda b/Tactic/Solver/Ring/IntegerCoefficients.agda index 56fd37ab..1700a1c9 100644 --- a/Tactic/Solver/Ring/IntegerCoefficients.agda +++ b/Tactic/Solver/Ring/IntegerCoefficients.agda @@ -15,7 +15,6 @@ module Tactic.Solver.Ring.IntegerCoefficients open import Algebra.Bundles using (RawRing) open import Algebra.Solver.Ring.AlmostCommutativeRing using (AlmostCommutativeRing; fromCommutativeRing ; _-Raw-AlmostCommutative⟶_) -open import Data.Fin.Base using (Fin) open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; _⊖_; _◃_) open import Data.Integer.Properties as ℤP using ([1+m]⊖[1+n]≡m⊖n; +◃n≡+n; _≟_) @@ -211,16 +210,14 @@ open import Algebra.Solver.Ring ℤ-rawRing R-acr morphism dec public hiding (⟦_⟧) ------------------------------------------------------------------------ --- Top-level aliases so the macro can reflect `con`, `var`, `:-_` by --- name (they're constructors nested inside `Algebra.Solver.Ring`'s --- four-parameter module otherwise). The `def`-shaped `_:+_`, `_:*_`, --- `_:-_`, `_:=_` don't need aliases. +-- Definition aliases for the *constructors* the macro emits: +-- constructor re-exports are not re-parameterised the way definition +-- re-exports are, so without these the macro could not supply `R` +-- explicitly (see the `NatC` module in `Tactic.Solver.Ring`). The +-- `def`-shaped `_:+_`, `_:*_`, `_:-_`, `_:=_` need no aliases. conP : ∀ {n} → ℤ → Polynomial n conP = con -varP : ∀ {n} → Fin n → Polynomial n -varP = var - negP : ∀ {n} → Polynomial n → Polynomial n negP = :-_ diff --git a/Tactic/Solver/Ring/Tests.agda b/Tactic/Solver/Ring/Tests.agda index 6cecdeff..5fbafb67 100644 --- a/Tactic/Solver/Ring/Tests.agda +++ b/Tactic/Solver/Ring/Tests.agda @@ -3,4 +3,6 @@ module Tactic.Solver.Ring.Tests where open import Tactic.Solver.Ring.Tests.BundleVariants open import Tactic.Solver.Ring.Tests.CommutativeRing open import Tactic.Solver.Ring.Tests.Comparison +open import Tactic.Solver.Ring.Tests.EdgeCases open import Tactic.Solver.Ring.Tests.Equations +open import Tactic.Solver.Ring.Tests.HasAddOp diff --git a/Tactic/Solver/Ring/Tests/BundleVariants.agda b/Tactic/Solver/Ring/Tests/BundleVariants.agda index 6903c561..ed13644b 100644 --- a/Tactic/Solver/Ring/Tests/BundleVariants.agda +++ b/Tactic/Solver/Ring/Tests/BundleVariants.agda @@ -54,6 +54,9 @@ module InlineRecordZ where comm+ : ∀ a b → (a + b) ≈ (b + a) comm+ = solve-≈ myZ'' + one-mul : ∀ a → (a * (ℤ.+ 1)) ≈ a + one-mul a = solve-≈ myZ'' + ------------------------------------------------------------------------ -- 3. η-expanded operators. @@ -163,6 +166,9 @@ module RecordUpdateOfAliasZ where comm+ : ∀ a b → (a + b) ≈ (b + a) comm+ = solve-≈ myZUpdated + zero-add : ∀ a → ((ℤ.+ 0) + a) ≈ a + zero-add a = solve-≈ myZUpdated + ------------------------------------------------------------------------ -- 8. Record update with η-expanded field values. @@ -181,6 +187,9 @@ module RecordUpdateηZ where comm+ : ∀ a b → (a + b) ≈ (b + a) comm+ = solve-≈ myZUpdatedη + one-mul : ∀ a → (a * (ℤ.+ 1)) ≈ a + one-mul a = solve-≈ myZUpdatedη + ------------------------------------------------------------------------ -- 9. Inlined operator body (KNOWN FAILURE). Instead of referring to -- `ℤ._*_`, write its definition `sign i Sign.* sign j ◃ ∣i∣ ℕ.* diff --git a/Tactic/Solver/Ring/Tests/EdgeCases.agda b/Tactic/Solver/Ring/Tests/EdgeCases.agda new file mode 100644 index 00000000..07b1e1e7 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/EdgeCases.agda @@ -0,0 +1,349 @@ +{-# OPTIONS --safe --without-K #-} + +------------------------------------------------------------------------ +-- Frontend edge cases: goal shapes and bundle shapes beyond the basic +-- Equations matrix. Each module probes one mechanism of the macro +-- frontend (goal whnf-stripping, atom identity, literal recognition, +-- binder handling, bundle resolution). +------------------------------------------------------------------------ + +module Tactic.Solver.Ring.Tests.EdgeCases where + + +open import Algebra using (CommutativeRing; CommutativeSemiring) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Tactic.Solver.Ring using (solve-≈) + +------------------------------------------------------------------------ +-- 1. Goal type behind a definition (whnf must unfold the alias). + +module GoalTypeAlias where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + Goal : ℕ → ℕ → Set + Goal a b = a + b ≡ b + a + + test : ∀ a b → Goal a b + test a b = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 2. Goal *side* behind a definition (whnf must unfold to expose ops). + +module GoalSideAlias where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + myExpr : ℕ → ℕ → ℕ + myExpr a b = a + b + + test : ∀ a b → myExpr a b ≡ b + a + test a b = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 3. Ops exposed only by computation (foldr over a concrete list). + +module FoldrExposed where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + open import Data.List using (foldr; _∷_; []) + + test : ∀ a b → foldr _+_ 0 (a ∷ b ∷ []) ≡ b + a + test a b = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 4. Hidden and mixed-visibility pi binders. + +module HiddenPis where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + hidden : ∀ {a b} → a + b ≡ b + a + hidden = solve-≈ +-*-commutativeSemiring + + mixed : ∀ {a} b → a + b ≡ b + a + mixed = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 5. `0#`/`1#` written as projections of a *concrete* bundle. + +module ProjectionLiterals where + open import Data.Nat using (ℕ) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + open CommutativeSemiring +-*-commutativeSemiring using (_≈_; _*_; _+_; 1#; 0#) + + one-mul : ∀ a → 1# * a ≈ a + one-mul a = solve-≈ +-*-commutativeSemiring + + zero-add : ∀ a → 0# + a ≈ a + zero-add a = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 6. Same, on ℚ (projection must stop at the blocked literal name). + +module ProjectionLiteralsℚ where + import Data.Rational.Properties as ℚP + open CommutativeRing ℚP.+-*-commutativeRing using (_≈_; _*_; 1#) + + one-mul : ∀ q → 1# * q ≈ q + one-mul q = solve-≈ ℚP.+-*-commutativeRing + +------------------------------------------------------------------------ +-- 7. Concrete ℚ subtraction and negation (CR side; `_-_` is a +-- derived slot and must be matched via unfolding). + +module ℚSubNeg where + open import Data.Rational using (ℚ; 0ℚ; _+_; _*_; _-_; -_) + import Data.Rational.Properties as ℚP + + sub-comm : ∀ p q → p - q ≡ - q + p + sub-comm p q = solve-≈ ℚP.+-*-commutativeRing + + neg-zero : - 0ℚ ≡ 0ℚ + neg-zero = solve-≈ ℚP.+-*-commutativeRing + + neg-distrib : ∀ p q → - (p + q) ≡ - p - q + neg-distrib p q = solve-≈ ℚP.+-*-commutativeRing + +------------------------------------------------------------------------ +-- 8. Negation applied to a literal (CR ℤ). + +module NegLiteral where + open import Data.Integer using (ℤ; +_; _+_; _*_; -_) + open import Data.Integer.Properties using (+-*-commutativeRing) + + neg-lit : ∀ a → - (+ 1) * a ≡ - a + neg-lit a = solve-≈ +-*-commutativeRing + +------------------------------------------------------------------------ +-- 9. ℤ literal *aliases* (`0ℤ`, `1ℤ` unfold to `+ 0`, `+[1+ 0 ]`). + +module ℤLiteralAliases where + open import Data.Integer using (ℤ; 0ℤ; 1ℤ; +_; _+_; _*_) + open import Data.Integer.Properties using (+-*-commutativeSemiring) + + one-mul : ∀ a → 1ℤ * a ≡ a + one-mul a = solve-≈ +-*-commutativeSemiring + + zero-add : ∀ a → 0ℤ + a ≡ a + zero-add a = solve-≈ +-*-commutativeSemiring + + two : 1ℤ + 1ℤ ≡ + 2 + two = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 10. ℕ: zero-annihilation with bare literals. + +module ℕZero where + open import Data.Nat using (ℕ; _+_; _*_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + zero-mul : ∀ a → a * 0 ≡ 0 + zero-mul a = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 11. Bundle written inline at the call site (accessor application, +-- no top-level alias). + +module InlineAccessor where + open import Data.Rational using (ℚ; 1ℚ; _+_; _*_) + import Data.Rational.Properties as ℚP + + one-mul : ∀ q → q * 1ℚ ≡ q + one-mul q = solve-≈ (CommutativeRing.commutativeSemiring ℚP.+-*-commutativeRing) + +------------------------------------------------------------------------ +-- 12. Bundle defined in a where-clause (lifted, applied to module +-- params; record expressions there are copattern definitions too). + +module WhereBundle where + open import Data.Integer as ℤ using (ℤ) + import Data.Integer.Properties as ℤP + + test : ∀ (a b : ℤ) → a ℤ.+ b ≡ b ℤ.+ a + test a b = solve-≈ myR + where + myR : CommutativeSemiring _ _ + myR = record + { Carrier = ℤ ; _≈_ = _≡_ + ; _+_ = ℤ._+_ ; _*_ = ℤ._*_ + ; 0# = ℤ.+ 0 ; 1# = ℤ.+ 1 + ; isCommutativeSemiring = ℤP.+-*-isCommutativeSemiring + } + +------------------------------------------------------------------------ +-- 13. Moderately large ℕ literal (encodeNat currently builds a +-- suc-chain Term of that depth). + +module BigLiteral where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + test : ∀ a → 100 + a ≡ a + 100 + test a = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 14. The equation stated via `Setoid._≈_` of the bundle's setoid. + +module ViaSetoid where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + open import Relation.Binary using (Setoid) + open CommutativeSemiring +-*-commutativeSemiring using (setoid) + + test : ∀ a b → Setoid._≈_ setoid (a + b) (b + a) + test a b = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 15. `solve-≈` under `trans` (one side of the hole's equation is a +-- meta that the other proof determines; must block + retry, not hang). + +module UnderTrans where + open import Data.Nat using (ℕ; _+_; _*_) + open import Data.Nat.Properties using (+-*-commutativeSemiring; *-comm) + open import Relation.Binary.PropositionalEquality using (trans; sym) + + test : ∀ a b → (a + b) * a ≡ a * a + b * a + test a b = trans (*-comm (a + b) a) (solve-≈ +-*-commutativeSemiring) + +------------------------------------------------------------------------ +-- 16. Negative ℤ literals (`-[1+_]`/`-1ℤ`), recognised on the CR side +-- and encoded as negative ℤ coefficients. + +module NegativeLiterals where + open import Data.Integer using (ℤ; -1ℤ; 1ℤ; -[1+_]; +_; _+_; _*_; -_) + open import Data.Integer.Properties using (+-*-commutativeRing) + + neg-one-mul : ∀ a → -1ℤ * a ≡ - a + neg-one-mul a = solve-≈ +-*-commutativeRing + + neg-lit-add : -[1+ 1 ] + (+ 2) ≡ + 0 + neg-lit-add = solve-≈ +-*-commutativeRing + + neg-times-neg : -1ℤ * -1ℤ ≡ 1ℤ + neg-times-neg = solve-≈ +-*-commutativeRing + +------------------------------------------------------------------------ +-- 17. Atom identity is up to whnf: two definitions of the same value +-- on opposite sides count as one atom (the first spelling is what +-- lands in the emitted call). + +module AtomSpelling where + open import Data.Rational using (ℚ; ½; _+_; _*_) + import Data.Rational.Properties as ℚP + + q₁ q₂ : ℚ + q₁ = ½ + q₂ = ½ + + spelled : ∀ q → q₁ + q ≡ q + q₂ + spelled q = solve-≈ ℚP.+-*-commutativeRing + +------------------------------------------------------------------------ +-- 18. `suc` under ℤ's `+_` wrapper peels to `1 + _` (sound because +-- `+_` is an additive homomorphism). + +module WrappedSuc where + open import Data.Nat using (suc) + open import Data.Integer using (ℤ; +_; _+_; _*_; -_) + open import Data.Integer.Properties using (+-*-commutativeSemiring; +-*-commutativeRing) + + wrapped-suc : ∀ n → + suc n ≡ + n + + 1 + wrapped-suc n = solve-≈ +-*-commutativeSemiring + + wrapped-suc-cr : ∀ n → + suc (suc n) ≡ + n + + 2 + wrapped-suc-cr n = solve-≈ +-*-commutativeRing + + mixed : ∀ n → (- (+ suc n)) * (+ 1) ≡ (- (+ 1)) + (- (+ n)) + mixed n = solve-≈ +-*-commutativeRing + +------------------------------------------------------------------------ +-- 19. Nested record updates: two copattern layers between the bundle +-- and its fields (`resolveToName`'s per-step head re-targeting must +-- chase through both). + +module NestedUpdates where + open import Data.Integer as ℤ using (ℤ) + import Data.Integer.Properties as ℤP + + twice : CommutativeSemiring _ _ + twice = record (record ℤP.+-*-commutativeSemiring { 0# = ℤ.+ 0 }) { 1# = ℤ.+ 1 } + + open CommutativeSemiring twice + + comm+ : ∀ a b → (a + b) ≈ (b + a) + comm+ a b = solve-≈ twice + + one-mul : ∀ a → (a * (ℤ.+ 1)) ≈ a + one-mul a = solve-≈ twice + +------------------------------------------------------------------------ +-- 20. Instance and level binders in the goal's pi-prefix +-- (`underPis` must re-introduce them with matching visibility). + +module ExoticBinders where + open import Data.Nat using (ℕ; _+_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + open import Level using (Level) + + record Tag : Set where + constructor mkTag + + inst : ⦃ _ : Tag ⦄ → ∀ a b → a + b ≡ b + a + inst = solve-≈ +-*-commutativeSemiring + + lvl : ∀ {ℓ} (A : Set ℓ) (a b : ℕ) → a + b ≡ b + a + lvl = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 21. Operator reached through a user alias: whnf unfolds the alias +-- to the blocked operator head. + +module AliasedOperator where + open import Data.Integer as ℤ using (ℤ) + open import Data.Integer.Properties using (+-*-commutativeSemiring) + + myPlus : ℤ → ℤ → ℤ + myPlus = ℤ._+_ + + test : ∀ a b → myPlus a b ≡ b ℤ.+ a + test a b = solve-≈ +-*-commutativeSemiring + +------------------------------------------------------------------------ +-- 22. `-[1+ x ]` with a variable payload is not a numeral: it must +-- atomise (whole), not crash the negative-literal recogniser. + +module NegsucVariable where + open import Data.Nat using (ℕ) + open import Data.Integer using (ℤ; -[1+_]; _+_) + open import Data.Integer.Properties using (+-*-commutativeRing) + + ok : ∀ n a → -[1+ n ] + a ≡ a + -[1+ n ] + ok n a = solve-≈ +-*-commutativeRing + +------------------------------------------------------------------------ +-- 23. Perf canaries (attributed costs, not frontend defects — the +-- macro itself measures ~80ms on the analogous abstract/ℤ goals): +-- a computed numeral pays the backend's `n × 1#` evaluation; concrete +-- ℚ atoms pay whnf of proof-carrying `_/_` normalisation. + +module PerfCanaries where + module ComputedLiteral where + open import Data.Nat using (ℕ; _+_; _^_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + big : ∀ a → a + 2 ^ 16 ≡ 2 ^ 16 + a + big a = solve-≈ +-*-commutativeSemiring + + module ConcreteℚAtoms where + open import Data.Rational using (ℚ; _+_; _/_) + open import Data.Integer using (+_) + import Data.Rational.Properties as ℚP + + q₁ q₂ q₃ q₄ q₅ q₆ q₇ q₈ : ℚ + q₁ = + 1 / 2 ; q₂ = + 2 / 3 ; q₃ = + 3 / 4 ; q₄ = + 4 / 5 + q₅ = + 5 / 6 ; q₆ = + 6 / 7 ; q₇ = + 7 / 8 ; q₈ = + 8 / 9 + + shuffle : (q₁ + (q₂ + (q₃ + (q₄ + (q₅ + (q₆ + (q₇ + q₈))))))) + ≡ (q₈ + (q₇ + (q₆ + (q₅ + (q₄ + (q₃ + (q₂ + q₁))))))) + shuffle = solve-≈ ℚP.+-*-commutativeRing diff --git a/Tactic/Solver/Ring/Tests/Equations.agda b/Tactic/Solver/Ring/Tests/Equations.agda index 2bb0a273..7f931ed3 100644 --- a/Tactic/Solver/Ring/Tests/Equations.agda +++ b/Tactic/Solver/Ring/Tests/Equations.agda @@ -2,10 +2,10 @@ module Tactic.Solver.Ring.Tests.Equations where -open import Algebra using (CommutativeSemiring) +open import Algebra using (CommutativeRing; CommutativeSemiring) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality using (_≡_) -open import Tactic.Solver.Ring using (solve-≈ ; module Solver) +open import Tactic.Solver.Ring using (solve-≈) ------------------------------------------------------------------------ -- Limitations @@ -598,3 +598,82 @@ module StressTest {c ℓ} (R : CommutativeSemiring c ℓ) where ((((c * e) + (c * f)) + ((c * g) + (c * h))) + (((d * e) + (d * f)) + ((d * g) + (d * h))))) expand8-≈ a b c d e f g h = solve-≈ R + +------------------------------------------------------------------------ +-- ℚ: the carrier whose literals (`0ℚ`, `1ℚ`, `½`, …) unfold into +-- proof-carrying `mkℚ` terms and must never be unfolded by the macro. + +module ℚDerived where + open import Data.Rational using (ℚ; 0ℚ; 1ℚ; ½; _+_; _*_) + import Data.Rational.Properties as ℚP + + ℚ-CSR : CommutativeSemiring _ _ + ℚ-CSR = CommutativeRing.commutativeSemiring ℚP.+-*-commutativeRing + + -- Bundle literals must be recognised as `1#`/`0#`. + one-mulʳ : ∀ q → q * 1ℚ ≡ q + one-mulʳ q = solve-≈ ℚ-CSR + + one-mulˡ : ∀ q → 1ℚ * q ≡ q + one-mulˡ q = solve-≈ ℚ-CSR + + zero-addˡ : ∀ q → 0ℚ + q ≡ q + zero-addˡ q = solve-≈ ℚ-CSR + + lit-only : 1ℚ * 1ℚ ≡ 1ℚ + lit-only = solve-≈ ℚ-CSR + + -- Non-bundle literals (`½`) are atoms; they must keep their + -- spelling (not be unfolded to `mkℚ …`) on both sides. + half-comm : ∀ q → q * ½ ≡ ½ * q + half-comm q = solve-≈ ℚ-CSR + + half-distrib : ∀ q r → ½ * (q + r) ≡ ½ * q + ½ * r + half-distrib q r = solve-≈ ℚ-CSR + + -- Bundle literal and non-bundle literal together. + half-one : ∀ q → (q * ½) * 1ℚ ≡ ½ * q + half-one q = solve-≈ ℚ-CSR + + -- Same goals through the directly-defined ring, as a control. + module DirectControl where + one-mulʳ′ : ∀ q → q * 1ℚ ≡ q + one-mulʳ′ q = solve-≈ ℚP.+-*-commutativeRing + + half-comm′ : ∀ q → q * ½ ≡ ½ * q + half-comm′ q = solve-≈ ℚP.+-*-commutativeRing + +------------------------------------------------------------------------ +-- ℤ: wrapped numeric literals (`+ n`) through a derived bundle. + +module ℤDerived where + open import Data.Integer using (ℤ; +_; _+_; _*_) + import Data.Integer.Properties as ℤP + + ℤ-CSR : CommutativeSemiring _ _ + ℤ-CSR = CommutativeRing.commutativeSemiring ℤP.+-*-commutativeRing + + lit-two : (+ 2) ≡ (+ 1) + (+ 1) + lit-two = solve-≈ ℤ-CSR + + one-mulʳ : ∀ a → a * (+ 1) ≡ a + one-mulʳ a = solve-≈ ℤ-CSR + + lit-coeff : ∀ a → (+ 2) * a ≡ a + a + lit-coeff a = solve-≈ ℤ-CSR + +------------------------------------------------------------------------ +-- A second def-layer on top of the accessor. + +module DoubleAlias where + open import Data.Rational using (ℚ; 1ℚ; _+_; _*_) + import Data.Rational.Properties as ℚP + + ℚ-CSR₁ : CommutativeSemiring _ _ + ℚ-CSR₁ = CommutativeRing.commutativeSemiring ℚP.+-*-commutativeRing + + ℚ-CSR₂ : CommutativeSemiring _ _ + ℚ-CSR₂ = ℚ-CSR₁ + + one-mulʳ : ∀ q → q * 1ℚ ≡ q + one-mulʳ q = solve-≈ ℚ-CSR₂ diff --git a/Tactic/Solver/Ring/Tests/HasAddOp.agda b/Tactic/Solver/Ring/Tests/HasAddOp.agda new file mode 100644 index 00000000..e6607c16 --- /dev/null +++ b/Tactic/Solver/Ring/Tests/HasAddOp.agda @@ -0,0 +1,79 @@ +{-# OPTIONS --without-K --safe #-} + +------------------------------------------------------------------------ +-- Goals whose `_+_` is `Class.HasAdd._+_` rather than the bundle's +-- own addition. +------------------------------------------------------------------------ + +module Tactic.Solver.Ring.Tests.HasAddOp where + +open import Algebra using (CommutativeSemiring; CommutativeRing) +open import Class.HasAdd +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Tactic.Solver.Ring using (solve-≈) + +------------------------------------------------------------------------ +-- Concrete carriers, via the stdlib `HasAdd` instances. + +module ℕ where + open import Data.Nat using (ℕ) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + comm : ∀ (a b : ℕ) → a + b ≡ b + a + comm a b = solve-≈ +-*-commutativeSemiring + + assoc : ∀ (a b c : ℕ) → (a + b) + c ≡ a + (b + c) + assoc a b c = solve-≈ +-*-commutativeSemiring + + rearrange : ∀ (a b c d : ℕ) → (a + b) + (c + d) ≡ (d + c) + (b + a) + rearrange a b c d = solve-≈ +-*-commutativeSemiring + +module ℤ where + open import Data.Integer using (ℤ) + open import Data.Integer.Properties using (+-*-commutativeRing) + + comm : ∀ (a b : ℤ) → a + b ≡ b + a + comm a b = solve-≈ +-*-commutativeRing + + rearrange : ∀ (a b c : ℤ) → a + (b + c) ≡ c + (a + b) + rearrange a b c = solve-≈ +-*-commutativeRing + +module ℚ where + open import Data.Rational using (ℚ) + import Data.Rational.Properties as ℚP + + comm : ∀ (a b : ℚ) → a + b ≡ b + a + comm a b = solve-≈ ℚP.+-*-commutativeRing + +------------------------------------------------------------------------ +-- Abstract bundles, via a `HasAdd Carrier` instance built from the +-- bundle's own addition. + +module AbstractCSR {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R using (Carrier; _≈_) renaming (_+_ to _+ᵇ_) + + instance + hasAdd : HasAdd Carrier + hasAdd ._+_ = _+ᵇ_ + + comm : ∀ a b → (a + b) ≈ (b + a) + comm a b = solve-≈ R + + assoc : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc a b c = solve-≈ R + + rearrange : ∀ a b c d → ((a + b) + (c + d)) ≈ ((d + c) + (b + a)) + rearrange a b c d = solve-≈ R + +module AbstractCR {c ℓ} (R : CommutativeRing c ℓ) where + open CommutativeRing R using (Carrier; _≈_) renaming (_+_ to _+ᵇ_) + + instance + hasAdd : HasAdd Carrier + hasAdd ._+_ = _+ᵇ_ + + comm : ∀ a b → (a + b) ≈ (b + a) + comm a b = solve-≈ R + + assoc : ∀ a b c → ((a + b) + c) ≈ (a + (b + c)) + assoc a b c = solve-≈ R From 8e38b55bff6f46b2d4cc2e171630c8c501a7ede8 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Mon, 15 Jun 2026 12:04:20 +0200 Subject: [PATCH 2/2] Add documentation --- .github/workflows/ci.yml | 1 + README.md | 6 ++ Tactic/Solver/Algebra.agda | 3 +- Tactic/Solver/Ring.lagda.md | 104 ++++++++++++++++++++ Tactic/Solver/{Ring.agda => Ring/Core.agda} | 9 +- Tactic/Solver/Ring/IntegerCoefficients.agda | 2 +- 6 files changed, 120 insertions(+), 5 deletions(-) create mode 100644 Tactic/Solver/Ring.lagda.md rename Tactic/Solver/{Ring.agda => Ring/Core.agda} (97%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 97479bc6..e61f6246 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,6 +5,7 @@ on: push: paths: - '**.agda' + - '**.lagda.md' - '*.agda-lib' - '.github/workflows/**.yml' branches: [master] diff --git a/README.md b/README.md index 39fa0c51..b7db35ad 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,12 @@ Browse the Agda code in HTML [here](https://agda.github.io/agda-stdlib-meta). +## Ring solver (`Tactic.Solver.Ring`) + +`solve-≈` is a reflection-based solver for commutative-(semi)ring +equalities. See the [ring solver +documentation](Tactic/Solver/Ring.lagda.md). + ## Version compatibility We mirror the version numbers of [agda-stdlib](https://github.com/agda/agda-stdlib). diff --git a/Tactic/Solver/Algebra.agda b/Tactic/Solver/Algebra.agda index f061c525..b1355dc8 100644 --- a/Tactic/Solver/Algebra.agda +++ b/Tactic/Solver/Algebra.agda @@ -413,7 +413,8 @@ private pure (finishSolve env f atoms) -- Precondition: `R` has been type-checked against the structure's --- bundle type by the caller (e.g. via `Tactic.Solver.Ring.detectSide`). +-- bundle type by the caller (e.g. via +-- `Tactic.Solver.Ring.Core.detectSide`). solveByTheory : Theory → Term → Term → TC ⊤ solveByTheory thy `R hole = do let open Theory thy diff --git a/Tactic/Solver/Ring.lagda.md b/Tactic/Solver/Ring.lagda.md new file mode 100644 index 00000000..973deeb2 --- /dev/null +++ b/Tactic/Solver/Ring.lagda.md @@ -0,0 +1,104 @@ +# Ring solver + +`solve-≈` proves equalities that hold in any commutative semiring or +commutative ring. It is a practical, reflection-based frontend to the +standard library's `Algebra.Solver.Ring`. + +This file is literate Agda. The implementation lives in +`Tactic.Solver.Ring.Core`; here we only define the macro, so that +jumping to its definition lands on this documentation. + +The solver handles both `CommutativeSemiring` and `CommutativeRing`, +see below. + +```agda +{-# OPTIONS --without-K --safe #-} +module Tactic.Solver.Ring where + +open import Algebra using (CommutativeSemiring; CommutativeRing) +open import Reflection using (Term; TC) +open import Data.Unit using (⊤) +open import Relation.Binary.PropositionalEquality using (_≡_) + +open import Tactic.Solver.Ring.Core using (solve-≈-macro) + +macro + solve-≈ : Term → Term → TC ⊤ + solve-≈ = solve-≈-macro +``` + +# Examples + +## A first example: ℕ + +Pass the bundle whose operations appear in the goal; `∀`-bound +variables are handled. + +```agda +module ℕ-example where + open import Data.Nat using (ℕ; _+_; _*_) + open import Data.Nat.Properties using (+-*-commutativeSemiring) + + distrib : ∀ a b c → (a + b) * c ≡ (c * a) + (c * b) + distrib a b = solve-≈ +-*-commutativeSemiring +``` + +## Rings: subtraction and negation + +A `CommutativeRing` bundle additionally lets the goal use `_-_` and +`-_`. + +```agda +module ℤ-example where + open import Data.Integer using (ℤ; _+_; _*_; _-_; -_) + open import Data.Integer.Properties using (+-*-commutativeRing) + + difference-of-squares : ∀ a b → (a - b) * (a + b) ≡ a * a - b * b + difference-of-squares a b = solve-≈ +-*-commutativeRing + + negation : ∀ a b → - (a + b) ≡ - a - b + negation a b = solve-≈ +-*-commutativeRing +``` + +## Literals + +Each carrier's numeric literals are recognised as ring constants — +`0`/`1` on ℕ, `+ n` on ℤ, `0ℚ`/`1ℚ` on ℚ. + +```agda +module ℚ-example where + open import Data.Rational using (ℚ; 0ℚ; 1ℚ; _+_; _*_) + import Data.Rational.Properties as ℚP + + unit : ∀ q → q * 1ℚ ≡ q + unit q = solve-≈ ℚP.+-*-commutativeRing + + zero : ∀ q → (q + 0ℚ) * 1ℚ ≡ q + zero q = solve-≈ ℚP.+-*-commutativeRing +``` + +## Abstract bundles + +The carrier need not be concrete; under an abstract bundle, state the +goal with its `_≈_`. + +```agda +module abstract-example {c ℓ} (R : CommutativeSemiring c ℓ) where + open CommutativeSemiring R + + rearrange : ∀ a b c d → ((a + b) + (c + d)) ≈ ((d + c) + (b + a)) + rearrange a b c d = solve-≈ R +``` + +## Scope and limitations + +- The goal's relation may be the bundle's `_≈_`, or propositional + `_≡_` when that is the bundle's equality (as for ℕ/ℤ/ℚ). +- Subterms the solver does not recognise as ring syntax become opaque + *atoms*: it proves the goal treating them as fresh variables, so an + identity that depends on their internal structure will not be found. +- Carriers that are themselves function types (with a pointwise + `_≈_`) are not supported. + +`Tactic.Solver.Ring.Tests.*` exercises many more goals and bundle +shapes. diff --git a/Tactic/Solver/Ring.agda b/Tactic/Solver/Ring/Core.agda similarity index 97% rename from Tactic/Solver/Ring.agda rename to Tactic/Solver/Ring/Core.agda index 94058f62..ee57d587 100644 --- a/Tactic/Solver/Ring.agda +++ b/Tactic/Solver/Ring/Core.agda @@ -1,7 +1,10 @@ ------------------------------------------------------------------------ --- A reflection-based ring solver. +-- Implementation of the reflective ring solver. See +-- `Tactic.Solver.Ring` for user-facing documentation. If you want to +-- use the ring solver, please import `Tactic.Solver.Ring` rather than +-- this module. -- --- `solve-≈` accepts either a `CommutativeSemiring` or a +-- `solve-≈-macro` accepts either a `CommutativeSemiring` or a -- `CommutativeRing` and dispatches to the appropriate backend: -- * CSR → `Algebra.Solver.Ring.NaturalCoefficients.Default R` -- (ℕ coefficients, no negation); @@ -21,7 +24,7 @@ {-# OPTIONS --without-K --safe #-} -module Tactic.Solver.Ring where +module Tactic.Solver.Ring.Core where open import Algebra using (CommutativeSemiring; CommutativeRing) diff --git a/Tactic/Solver/Ring/IntegerCoefficients.agda b/Tactic/Solver/Ring/IntegerCoefficients.agda index 1700a1c9..a1f5be4c 100644 --- a/Tactic/Solver/Ring/IntegerCoefficients.agda +++ b/Tactic/Solver/Ring/IntegerCoefficients.agda @@ -213,7 +213,7 @@ open import Algebra.Solver.Ring ℤ-rawRing R-acr morphism dec public -- Definition aliases for the *constructors* the macro emits: -- constructor re-exports are not re-parameterised the way definition -- re-exports are, so without these the macro could not supply `R` --- explicitly (see the `NatC` module in `Tactic.Solver.Ring`). The +-- explicitly (see the `NatC` module in `Tactic.Solver.Ring.Core`). The -- `def`-shaped `_:+_`, `_:*_`, `_:-_`, `_:=_` need no aliases. conP : ∀ {n} → ℤ → Polynomial n