A few more ring solver improvements

.github/workflows/ci.yml

@@ -5,6 +5,7 @@ on:
   push:
     paths:
       - '**.agda'
+      - '**.lagda.md'
       - '*.agda-lib'
       - '.github/workflows/**.yml'
     branches: [master]

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).

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

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₁

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

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

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 _          = []

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