Add ring solver

Class/MonadError.agda

@@ -16,6 +16,10 @@ record MonadError (E : Set e) (M : ∀ {f} → Set f → Set f) : Setω where
     error : E → M A
     catch : M A → (E → M A) → M A
 
+  instance
+    Alternative-M : Alternative M
+    Alternative-M = record { _<|>_ = λ x y → catch x (λ _ → y) }
+
 open MonadError
 
 MonadError-TC : MonadError (List ErrorPart) TC

Reflection/Utils/Args.agda

@@ -4,13 +4,21 @@ module Reflection.Utils.Args where
 open import Meta.Prelude
 open import Meta.Init
 
-open import Data.List using (map; zip)
+open import Data.List using (map; zip; reverse; length)
 open import Data.Fin using (toℕ)
+open import Data.Vec.Base using (Vec; []; _∷_)
+import Data.Vec.Base as Vec
+import Data.Maybe as Maybe
 open import Relation.Nullary using (Dec)
 
 open import Reflection.AST.Argument.Information
 import Reflection.AST.Argument.Visibility as Vis
 
+takeFirst : ∀ {ℓ} {A : Set ℓ} (n : ℕ) → List A → Maybe (Vec A n)
+takeFirst zero    _        = just []
+takeFirst (suc _) []       = nothing
+takeFirst (suc n) (x ∷ xs) = Maybe.map (x ∷_) (takeFirst n xs)
+
 getVisibility : Arg A → Visibility
 getVisibility (arg (arg-info v _) _) = v
 
@@ -33,6 +41,17 @@ vArgs = λ where
   (vArg x ∷ xs) → x ∷ vArgs xs
   (_      ∷ xs) → vArgs xs
 
+visibleCount : Args A → ℕ
+visibleCount = length ∘ vArgs
+
+-- Take the last `n` visible arguments of a `def`. Returns `nothing`
+-- if the term isn't a `def` or has fewer than `n` visible
+-- arguments. Hidden arguments and any leading visible arguments
+-- beyond the last `n` are skipped.
+getVisibleArgs : ∀ n → Term → Maybe (Vec Term n)
+getVisibleArgs n (def _ xs) = Maybe.map Vec.reverse (takeFirst n (reverse (vArgs xs)))
+getVisibleArgs _ _ = nothing
+
 argInfo : Arg A → ArgInfo
 argInfo (arg i _) = i
 

Reflection/Utils/Core.agda

@@ -5,7 +5,13 @@ open import Meta.Prelude
 open import Meta.Init
 
 open import Data.Product using (map₁)
-open import Data.List using (map)
+open import Data.List using (map; findIndexᵇ)
+import Data.List as List
+import Data.Maybe as Maybe
+import Data.Fin as Fin
+import Reflection.AST.Name as Name
+open import Reflection.AST.AlphaEquality using (_=α=_)
+open import Reflection.AST.Literal using (nat)
 
 import Reflection.AST.Abstraction as Abs
 import Reflection.AST.Argument as Arg
@@ -21,6 +27,34 @@ tyName = λ where
   (def n _) → just n
   _         → nothing
 
+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
+
+-- 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
+
+-- Extract a `ℕ` value from a term shaped as `lit (nat n)` or a chain
+-- of `suc`/`zero` constructors.
+extractNat : Term → Maybe ℕ
+extractNat (lit (nat n))        = just n
+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)
+
 -- ** 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/Metas.agda

@@ -4,7 +4,9 @@ module Reflection.Utils.Metas where
 open import Meta.Prelude
 open import Meta.Init
 
-open import Data.List using (_++_)
+import Data.Bool.ListAction as B
+open import Data.List
+import Reflection.AST.Meta as Meta
 
 isMeta : Term → Bool
 isMeta = λ where
@@ -35,3 +37,16 @@ mutual
     [] → []
     (clause _ _ t      ∷ c) → findMetas t ++ findMetasCl c
     (absurd-clause _ _ ∷ c) → findMetasCl c
+
+metaId : Term → Maybe Meta
+metaId (meta x _) = just x
+metaId _          = nothing
+
+findMetaIds : Term → List Meta
+findMetaIds = mapMaybe metaId ∘ findMetas
+
+firstMeta : Term → Maybe Meta
+firstMeta = head ∘ findMetaIds
+
+shareMeta : List Meta → List Meta → Bool
+shareMeta xs ys = B.any (λ x → B.any (Meta._≡ᵇ_ x) ys) xs

Reflection/Utils/TCM.agda

@@ -9,3 +9,65 @@ 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

Tactic.agda

@@ -22,3 +22,6 @@ open import Tactic.Derive.DecEqFast
 open import Tactic.Derive.Show public
 open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests
 open import Tactic.Derive.Convertible public
+
+open import Tactic.Solver.Ring
+open import Tactic.Solver.Ring.Tests