------------------------------------------------------------------------
-- The Agda standard library
--
-- "Evaluating" a polynomial, using Horner's method.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.Polynomial.Parameters
module Tactic.RingSolver.Core.Polynomial.Semantics
{r₁ r₂ r₃ r₄}
(homo : Homomorphism r₁ r₂ r₃ r₄)
where
open import Data.Nat.Base using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
open import Data.Vec.Base using (Vec; []; _∷_; uncons)
open import Data.List.Base using ([]; _∷_)
open import Data.Product.Base using (_,_; _×_)
open import Data.List.Kleene using (_+; _*; ∹_; _&_; [])
open Homomorphism homo hiding (_^_)
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring
drop : ∀ {i n} → i ≤′ n → Vec Carrier n → Vec Carrier i
drop ≤′-refl xs = xs
drop (≤′-step i+1≤n) (_ ∷ xs) = drop i+1≤n xs
drop-1 : ∀ {i n} → suc i ≤′ n → Vec Carrier n → Carrier × Vec Carrier i
drop-1 si≤n xs = uncons (drop si≤n xs)
{-# INLINE drop-1 #-}
_*⟨_⟩^_ : Carrier → Carrier → ℕ → Carrier
x *⟨ ρ ⟩^ zero = x
x *⟨ ρ ⟩^ suc i = ρ ^ (suc i) * x
{-# INLINE _*⟨_⟩^_ #-}
------------------------------------------------------------------------
-- Evaluation
------------------------------------------------------------------------
-- Why do we have three functions here? Why are they so weird looking?
--
-- These three functions are the main bottleneck for all of the proofs:
-- as such, slight changes can dramatically affect the length of proof
-- code.
mutual
_⟦∷⟧_ : ∀ {n} → Poly n × Coeff n * → Carrier × Vec Carrier n → Carrier
(x , []) ⟦∷⟧ (ρ , ρs) = ⟦ x ⟧ ρs
(x , (∹ xs)) ⟦∷⟧ (ρ , ρs) = ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
⅀⟦_⟧ : ∀ {n} → Coeff n + → (Carrier × Vec Carrier n) → Carrier
⅀⟦ x ≠0 Δ i & xs ⟧ (ρ , ρs) = ((x , xs) ⟦∷⟧ (ρ , ρs)) *⟨ ρ ⟩^ i
{-# INLINE ⅀⟦_⟧ #-}
⟦_⟧ : ∀ {n} → Poly n → Vec Carrier n → Carrier
⟦ Κ x ⊐ i≤n ⟧ _ = ⟦ x ⟧ᵣ
⟦ ⅀ xs ⊐ i≤n ⟧ Ρ = ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
{-# INLINE ⟦_⟧ #-}
------------------------------------------------------------------------
-- Performance
------------------------------------------------------------------------
-- As you might imagine, the implementation of the functions above
-- seriously affect performance. What you might not realise, though,
-- is that the most important component is the *order of the arguments*.
-- For instance, if we change:
--
-- (x , xs) ⟦∷⟧ (ρ , ρs) = ρ * ⅀⟦ xs ⟧ (ρ , ρs) + ⟦ x ⟧ ρs
--
-- To:
--
-- (x , xs) ⟦∷⟧ (ρ , ρs) = ⟦ x ⟧ ρs + ⅀⟦ xs ⟧ (ρ , ρs) * ρ
--
-- We get a function that's several orders of magnitude slower!
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4