egison-5.1.0: lib/math/expression.egi
--
--
-- Mathematics Expressions
--
--
inductive pattern MathValue :=
| frac MathValue MathValue
| (/) MathValue MathValue
| plus [(Term MathValue [..])]
| poly [(Term MathValue [..])]
| term MathValue [(MathValue, Integer)]
| mult MathValue MathValue
| (+) (Term MathValue [..]) MathValue
| (*) MathValue MathValue
| (^) Factor Integer
| symbol String [IndexExpr]
| apply1 (MathValue -> MathValue) MathValue
| apply2 (MathValue -> MathValue -> MathValue) MathValue MathValue
| apply3 (MathValue -> MathValue -> MathValue -> MathValue) MathValue MathValue MathValue
| apply4 (MathValue -> MathValue -> MathValue -> MathValue -> MathValue) MathValue MathValue MathValue MathValue
| quote MathValue
| func MathValue [MathValue]
inductive pattern IndexExpr :=
| sub MathValue
| sup MathValue
| user MathValue
def indexExpr : Matcher IndexExpr :=
matcher
| sub $ as (mathValue) with
| Sub $e -> [e]
| _ -> []
| sup $ as (mathValue) with
| Sup $e -> [e]
| _ -> []
| user $ as (mathValue) with
| User $e -> [e]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
def mathValue : Matcher MathValue :=
matcher
| frac $ $ as (mathValue, mathValue) with
| Frac $p1 $p2 -> [(p1, p2)]
| _ -> []
| $ / $ as (mathValue, mathValue) with
| Frac $p1 $p2 -> [(p1, p2)]
| _ -> []
| poly $ as (multiset (term mathValue)) with
-- Each element is statically Term MathValue [..], so `partialDiff $t x`
-- in the body dispatches to the Term instance at compile time.
| Frac (Plus $ts) (Plus [Term 1 []]) -> [ts]
| _ -> []
| plus $ as (multiset (term mathValue)) with
| Frac (Plus $ts) (Plus [Term 1 []]) -> [ts]
| _ -> []
| $ + $ as (term mathValue, mathValue) with
-- LHS is a single Term (statically), RHS is the rest of the polynomial.
| Frac (Plus $ts) (Plus [Term 1 []]) ->
matchAll ts as multiset something with
| $t :: $tss -> (t, sum' tss)
| _ -> []
| term $ $ as (mathValue, assocMultiset mathValue) with
-- Coefficient is `mathValue` (not `integer`) so that level-4 forms
-- with Frac coefficients (`CASTerm (CASFrac _ _) _`) are typed
-- correctly. Runtime PDP `Term $n $xs` extracts whatever coefficient
-- the CASTerm holds (Integer or Frac).
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, xs)]
| _ -> []
| $ ^ $ as (factor, integer) with
-- Single-factor monomial decomposition `x ^ n`. Matches a single-term
-- polynomial with one factor `(x, n)`. The base `$x` is bound with the
-- `factor` matcher, so its static type is Factor — recursive calls
-- like `partialDiff $x` then dispatch statically to the Factor instance.
| $tgt ->
match tgt as mathValue with
| term _ (($x, $n) :: []) -> [(x, n)]
| _ -> []
| mult $ $ as (mathValue, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| $ * $ as (mathValue, multExpr) with
-- Leading coefficient widened from `integer` to `mathValue` to allow
-- Frac coefficients in level-4 polynomial decomposition.
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| symbol $ $ as (string, list indexExpr) with
| Frac (Plus [Term 1 [(Symbol $v $js, 1)]]) (Plus [Term 1 []]) ->
[(v, js)]
| _ -> []
| apply1 $ $ as (something, mathValue) with
| Frac (Plus [Term 1 [(Apply1 $v $a1, 1)]]) (Plus [Term 1 []]) ->
[(v, a1)]
| _ -> []
| apply2 $ $ $ as (something, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply2 $v $a1 $a2, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2)]
| _ -> []
| apply3 $ $ $ $ as (something, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply3 $v $a1 $a2 $a3, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3)]
| _ -> []
| apply4 $ $ $ $ $ as (something, mathValue, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply4 $v $a1 $a2 $a3 $a4, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3, a4)]
| _ -> []
| quote $ as (mathValue) with
| Frac (Plus [Term 1 [(Quote $mexpr, 1)]]) (Plus [Term 1 []]) ->
[mexpr]
| _ -> []
| func $ $ as (mathValue, list mathValue) with
| Frac
(Plus [Term 1 [(Function $name $args, 1)]])
(Plus [Term 1 []]) ->
[(name, args)]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
def multExpr : Matcher MathValue :=
matcher
| ($ ^ $) * $ as (factor, integer, multExpr) with
| $tgt ->
matchAll tgt as mathValue with
| term _ (($x, $n) :: $rs) -> (x, n, product' (map (\(x, n) -> x ^' n) rs))
| $ ^ $ as (factor, integer) with
| $tgt ->
match tgt as mathValue with
| term _ (($x, $n) :: []) -> [(x, n)]
| _ -> []
| $ * $ as (mathValue, multExpr) with
-- First slot is `x ^' n` — for n > 1 this is no longer a Factor, so keep mathValue.
| $tgt ->
matchAll tgt as mathValue with
| term _ (($x, $n) :: $rs) -> (x ^' n, product' (map (\(x, n) -> x ^' n) rs))
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
def termExpr : Matcher MathValue := mathValue
-- Phase 5 Step 5.0: basic matchers (atoms, factor, symbol).
-- These deliberately delegate to `mathValue` so that they can be used as
-- generic decomposition matchers under the `factor` / `symbol` names while
-- the full parametric matchers below provide coefficient-aware variants.
def symbol : Matcher MathValue := mathValue
-- factor: matcher for atomic CAS shapes (single symbol, apply1-4, quote, func).
-- Returns Matcher Factor so that pattern variables bound through this matcher
-- get the static type Factor — enabling compile-time dispatch to the
-- `Differentiable Factor` instance from inside Term/Poly instances when the
-- pattern signature is `as (factor, integer)` (e.g. `$fx ^ $n`).
def factor : Matcher Factor :=
matcher
| symbol $ $ as (string, list indexExpr) with
| Frac (Plus [Term 1 [(Symbol $v $js, 1)]]) (Plus [Term 1 []]) ->
[(v, js)]
| _ -> []
| apply1 $ $ as (something, mathValue) with
| Frac (Plus [Term 1 [(Apply1 $v $a1, 1)]]) (Plus [Term 1 []]) ->
[(v, a1)]
| _ -> []
| apply2 $ $ $ as (something, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply2 $v $a1 $a2, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2)]
| _ -> []
| apply3 $ $ $ $ as (something, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply3 $v $a1 $a2 $a3, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3)]
| _ -> []
| apply4 $ $ $ $ $ as (something, mathValue, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply4 $v $a1 $a2 $a3 $a4, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3, a4)]
| _ -> []
| quote $ as (mathValue) with
| Frac (Plus [Term 1 [(Quote $mexpr, 1)]]) (Plus [Term 1 []]) ->
[mexpr]
| _ -> []
| func $ $ as (mathValue, list mathValue) with
| Frac
(Plus [Term 1 [(Function $name $args, 1)]])
(Plus [Term 1 []]) ->
[(name, args)]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
-- Phase 5 Step 5.1-5.3: parametric matchers `term`, `poly`, `frac`.
-- They share the same runtime behavior as `mathValue` but the coefficient
-- matcher is parametric (`m` rather than the hard-coded `integer`). Pattern
-- variables bound by `term $`, `mult $`, `$ * $` therefore have type `a` (the
-- coefficient type the user picked), enabling typed decomposition such as
-- `match p as poly (frac integer) with | term $c _ -> ...` where `c : Frac Integer`.
--
-- All three matchers share the structural patterns to ease delegation:
-- a single term is also a polynomial, a polynomial is also a fraction (over 1).
-- This keeps `match (3 * x) as poly integer with | term $c _ -> c` working
-- without requiring callers to coerce manually.
def term {a} (m: MatcherSlot a a) : Matcher (Term a [..]) :=
matcher
| term $ $ as (m, assocMultiset mathValue) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) -> [(n, xs)]
| _ -> []
| mult $ $ as (m, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| $ * $ as (m, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| symbol $ $ as (string, list indexExpr) with
| Frac (Plus [Term 1 [(Symbol $v $js, 1)]]) (Plus [Term 1 []]) ->
[(v, js)]
| _ -> []
| apply1 $ $ as (something, mathValue) with
| Frac (Plus [Term 1 [(Apply1 $v $a1, 1)]]) (Plus [Term 1 []]) ->
[(v, a1)]
| _ -> []
| apply2 $ $ $ as (something, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply2 $v $a1 $a2, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2)]
| _ -> []
| apply3 $ $ $ $ as (something, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply3 $v $a1 $a2 $a3, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3)]
| _ -> []
| apply4 $ $ $ $ $ as (something, mathValue, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply4 $v $a1 $a2 $a3 $a4, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3, a4)]
| _ -> []
| quote $ as (mathValue) with
| Frac (Plus [Term 1 [(Quote $mexpr, 1)]]) (Plus [Term 1 []]) -> [mexpr]
| _ -> []
| func $ $ as (mathValue, list mathValue) with
| Frac
(Plus [Term 1 [(Function $name $args, 1)]])
(Plus [Term 1 []]) ->
[(name, args)]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
def poly {a} (m: MatcherSlot a a) : Matcher MathValue :=
matcher
| poly $ as (multiset (term m)) with
| Frac (Plus $ts) (Plus [Term 1 []]) -> [ts]
| _ -> []
| plus $ as (multiset (term m)) with
| Frac (Plus $ts) (Plus [Term 1 []]) -> [ts]
| _ -> []
| $ + $ as (term m, poly m) with
| Frac (Plus $ts) (Plus [Term 1 []]) ->
matchAll ts as multiset something with
| $t :: $tss -> (t, sum' tss)
| _ -> []
-- Delegation to term-level patterns: a single-term value is also a polynomial
| term $ $ as (m, assocMultiset mathValue) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) -> [(n, xs)]
| _ -> []
| mult $ $ as (m, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| $ * $ as (m, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| symbol $ $ as (string, list indexExpr) with
| Frac (Plus [Term 1 [(Symbol $v $js, 1)]]) (Plus [Term 1 []]) ->
[(v, js)]
| _ -> []
| apply1 $ $ as (something, mathValue) with
| Frac (Plus [Term 1 [(Apply1 $v $a1, 1)]]) (Plus [Term 1 []]) ->
[(v, a1)]
| _ -> []
| apply2 $ $ $ as (something, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply2 $v $a1 $a2, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2)]
| _ -> []
| apply3 $ $ $ $ as (something, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply3 $v $a1 $a2 $a3, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3)]
| _ -> []
| apply4 $ $ $ $ $ as (something, mathValue, mathValue, mathValue, mathValue) with
| Frac (Plus [Term 1 [(Apply4 $v $a1 $a2 $a3 $a4, 1)]]) (Plus [Term 1 []]) ->
[(v, a1, a2, a3, a4)]
| _ -> []
| quote $ as (mathValue) with
| Frac (Plus [Term 1 [(Quote $mexpr, 1)]]) (Plus [Term 1 []]) -> [mexpr]
| _ -> []
| func $ $ as (mathValue, list mathValue) with
| Frac
(Plus [Term 1 [(Function $name $args, 1)]])
(Plus [Term 1 []]) ->
[(name, args)]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
def frac {a} (m: MatcherSlot a a) : Matcher MathValue :=
matcher
| frac $ $ as (m, m) with
| Frac $p1 $p2 -> [(p1, p2)]
| _ -> []
| $ / $ as (m, m) with
| Frac $p1 $p2 -> [(p1, p2)]
| _ -> []
-- Delegation to poly-level patterns: a non-fraction value is also Frac _ 1
| $ + $ as (mathValue, mathValue) with
| Frac (Plus $ts) (Plus [Term 1 []]) ->
matchAll ts as multiset something with
| $t :: $tss -> (t, sum' tss)
| _ -> []
| poly $ as (multiset mathValue) with
| Frac (Plus $ts) (Plus [Term 1 []]) -> [ts]
| _ -> []
-- Delegation to term-level patterns
| term $ $ as (mathValue, assocMultiset mathValue) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) -> [(n, xs)]
| _ -> []
| mult $ $ as (mathValue, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| $ * $ as (mathValue, multExpr) with
| Frac (Plus [Term $n $xs]) (Plus [Term 1 []]) ->
[(n, product' (map (\(x, n) -> x ^' n) xs))]
| _ -> []
| symbol $ $ as (string, list indexExpr) with
| Frac (Plus [Term 1 [(Symbol $v $js, 1)]]) (Plus [Term 1 []]) ->
[(v, js)]
| _ -> []
| apply1 $ $ as (something, mathValue) with
| Frac (Plus [Term 1 [(Apply1 $v $a1, 1)]]) (Plus [Term 1 []]) ->
[(v, a1)]
| _ -> []
| quote $ as (mathValue) with
| Frac (Plus [Term 1 [(Quote $mexpr, 1)]]) (Plus [Term 1 []]) -> [mexpr]
| _ -> []
| #$val as () with
| $tgt -> if val = tgt then [()] else []
| $ as something with
| $tgt -> [tgt]
-- mathExpr: an alias for `mathValue` used by older code and the parametric
-- matcher tests. Kept for backward compatibility.
def mathExpr : Matcher MathValue := mathValue
def isSymbol (mexpr: MathValue) : Bool :=
match mexpr as mathValue with
| symbol _ _ -> True
| _ -> False
def isApply (mexpr: MathValue) : Bool :=
match mexpr as mathValue with
| apply1 _ _ -> True
| apply2 _ _ _ -> True
| apply3 _ _ _ _ -> True
| apply4 _ _ _ _ _ -> True
| _ -> False
def isSimpleTerm (mexpr: MathValue) : Bool := isSymbol mexpr || isApply mexpr
def isTerm (mexpr: MathValue) : Bool :=
match mexpr as mathValue with
| term _ _ -> True
| #0 -> True
| _ -> False
def isPolynomial (mexpr: MathValue) : Bool :=
match mexpr as mathValue with
| poly _ -> True
| #0 -> True
| _ -> False
def isMonomial (mexpr: MathValue) : Bool :=
match mexpr as mathValue with
| poly [term _ _] / poly [term _ _] -> True
| #0 -> True
| _ -> False
--
-- Accessor
--
def fromMonomial (mexpr: MathValue) : (MathValue, MathValue) :=
match mexpr as mathValue with
| term $a $xs / term $b $ys ->
(a / b, foldl (*') 1 (map (uncurry (^')) xs) / foldl (*') 1 (map (uncurry (^')) ys))
--
-- Map
--
def mapPolys (fn: MathValue -> MathValue) (mexpr: MathValue) : MathValue :=
match mexpr as mathValue with
| $p1 / $p2 -> fn p1 /' fn p2
def fromPoly (mexpr: MathValue) : [MathValue] :=
match mexpr as mathValue with
| poly $ts1 / $q -> map (\t1 -> t1 /' q) ts1
def mapPoly (fn: MathValue -> MathValue) (mexpr: MathValue) : MathValue :=
match mexpr as mathValue with
| poly $ts1 / $q -> foldl (+') 0 (map (\t1 -> fn (t1 /' q)) ts1)
def mapTerms (fn: MathValue -> MathValue) (mexpr: MathValue) : MathValue :=
match mexpr as mathValue with
| poly $ts1 / poly $ts2 ->
foldl (+') 0 (map fn ts1) /' foldl (+') 0 (map fn ts2)
def mapSymbols (fn: MathValue -> MathValue) (mexpr: MathValue) : MathValue :=
mapTerms
(\match as mathValue with
| term $a $xs ->
a *' foldl
(*')
1
(map
(\(x, n) -> match x as mathValue with
| symbol _ _ -> fn x ^' n
| quote $q ->
let q' := mapSymbols fn q
in if q = q'
then x ^' n
else quoteScalar q' ^' n
| apply1 $g $a1 ->
let a1' := mapSymbols fn a1
in if a1 = a1'
then x ^' n
else fn (g a1') ^' n
| apply2 $g $a1 $a2 ->
let a1' := mapSymbols fn a1
a2' := mapSymbols fn a2
in if a1 = a1' && a2 = a2'
then x ^' n
else fn (g a1' a2') ^' n
| apply3 $g $a1 $a2 $a3 ->
let a1' := mapSymbols fn a1
a2' := mapSymbols fn a2
a3' := mapSymbols fn a3
in if a1 = a1' && a2 = a2' && a3 = a3'
then x ^' n
else fn (g a1' a2' a3') ^' n
| apply4 $g $a1 $a2 $a3 $a4 ->
let a1' := mapSymbols fn a1
a2' := mapSymbols fn a2
a3' := mapSymbols fn a3
a4' := mapSymbols fn a4
in if a1 = a1' && a2 = a2' && a3 = a3' && a4 = a4'
then x ^' n
else fn (g a1' a2' a3' a4') ^' n
| func _ $args ->
let args' := map (mapSymbols fn) args
in if args = args'
then x ^' n
else fn (updateFunctionArgs x args') ^' n)
xs))
mexpr
def scanAllTerms (mexpr: MathValue) (f: MathValue -> Bool) : Bool :=
match mexpr as mathValue with
| poly $ts1 / poly $ts2 -> any f (ts1 ++ ts2)
| _ -> not ((debug2 "scanAllTerms" mexpr) = mexpr) -- TODO: if tensorMap is inserted correctly, we canremove this
def containSymbol (x: MathValue) (mexpr: MathValue) : Bool :=
scanAllTerms mexpr
(\t -> match t as mathValue with
| term _ $xs ->
any
(\(y, _) -> match y as mathValue with
| #x -> True
| apply1 _ $a1 -> containSymbol x a1
| apply2 _ $a1 $a2 -> containSymbol x a1 || containSymbol x a2
| apply3 _ $a1 $a2 $a3 -> containSymbol x a1 || containSymbol x a2 || containSymbol x a3
| apply4 _ $a1 $a2 $a3 $a4 -> containSymbol x a1 || containSymbol x a2 || containSymbol x a3 || containSymbol x a4
| _ -> False)
xs
| _ -> False)
--
-- Substitute
--
def substitute (ls: [(MathValue, MathValue)]) (mexpr: MathValue) : MathValue :=
match ls as list (mathValue, mathValue) with
| [] -> mathNormalize mexpr
| ($x, $a) :: $rs -> substitute rs (substitute' x a mexpr)
def substitute' (x: MathValue) (a: MathValue) (mexpr: MathValue) : MathValue :=
mapSymbols (rewriteSymbol x a) mexpr
def rewriteSymbol (x: MathValue) (a: MathValue) (sexpr: MathValue) : MathValue :=
match sexpr as mathValue with
| #x -> a
| _ -> sexpr
def V.substitute (xs: Vector MathValue) (ys: Vector MathValue) (mexpr: MathValue) : MathValue :=
substitute (zip (tensorToList xs) (tensorToList ys)) mexpr
def expandAll (mexpr: MathValue) : MathValue :=
match mexpr as mathValue with
| ?isInteger -> mexpr
| ?isSymbol -> mexpr
-- function application
| apply1 $g $a1 -> `(g (expandAll a1))
| apply2 $g $a1 $a2 -> `(g (expandAll a1) (expandAll a2))
| apply3 $g $a1 $a2 $a3 -> `(g (expandAll a1) (expandAll a2) (expandAll a3))
| apply4 $g $a1 $a2 $a3 $a4 -> `(g (expandAll a1) (expandAll a2) (expandAll a3) (expandAll a4))
-- quote
| quote $g -> g
-- term (multiplication)
| term $a $ps -> a * product (map (\(x, n) -> expandAll x ^ n) ps)
-- polynomial
| poly $ts -> sum (map expandAll ts)
-- quotient
| $p1 / $p2 -> expandAll p1 / expandAll p2
def expandAll' (mexpr: MathValue) : MathValue :=
match mexpr as mathValue with
| ?isInteger -> mexpr
| ?isSymbol -> mexpr
-- function application
| apply1 $g $a1 -> `(g (expandAll' a1))
| apply2 $g $a1 $a2 -> `(g (expandAll' a1) (expandAll' a2))
| apply3 $g $a1 $a2 $a3 -> `(g (expandAll' a1) (expandAll' a2) (expandAll' a3))
| apply4 $g $a1 $a2 $a3 $a4 -> `(g (expandAll' a1) (expandAll' a2) (expandAll' a3) (expandAll' a4))
-- quote
| quote $g -> g
-- term (multiplication)
| term $a $ps -> a *' product' (map (\(x, n) -> expandAll' x ^' n) ps)
-- polynomial
| poly $ts -> sum' (map expandAll' ts)
-- quotient
| $p1 / $p2 -> expandAll' p1 / expandAll' p2
--
-- Coefficient
--
def coefficients (f: MathValue) (x: MathValue) : [MathValue] :=
let m := maximum (0 :: (matchAll f as mathValue with
| poly (term $a ((#x, $k) :: $ts) :: _) / _ -> k))
in map (coefficient f x) (between 0 m)
-- Use the matcher's `_ / $d` extraction (PDFracPat) for the divisor so
-- it is consistent with the `poly (...) / _` arm above: PDFracPat returns
-- (self, 1) for non-CASFrac forms (level-4 polys with Frac coefficients),
-- so no spurious division happens. The user-facing `denominator` primitive
-- would return the LCM of Frac denoms here and double-count.
def fracDenom (f: MathValue) : MathValue :=
match f as mathValue with | _ / $d -> d
def coefficient (f: MathValue) (x: MathValue) (m: Integer) : MathValue :=
if m = 0
then sum (matchAll f as mathValue with
| poly (term $a (!((#x, _) :: _) & $ts) :: _) / _ ->
foldl (*') a (map (uncurry (^')) ts)) / fracDenom f
else coefficient' f x m
def coefficient' (f: MathValue) (x: MathValue) (m: Integer) : MathValue :=
sum
(matchAll f as mathValue with
| poly (term $a ((#x, #m) :: (!((#x, _) :: _) & $ts)) :: _) /_ ->
foldl (*') a (map (uncurry (^')) ts)) /' fracDenom f
def L./ (xs: [MathValue]) (ys: [MathValue]) : ([MathValue], [MathValue]) :=
if length xs < length ys
then ([], xs)
else match (ys, xs) as (list mathValue, list mathValue) with
| ($y :: $yrs, $x :: $xrs) ->
let (zs, rs) := L./ (map2 (-) (take (length yrs) xrs) (map (* (x / y)) yrs) ++ drop (length yrs) xrs) ys
in (x / y :: zs, rs)
-- Phase A.5 primitives `mapPolyAll`, `mapTermAll`, `mapFracAll` are
-- registered in `Type/Check.hs`, so they're known to the type system
-- without needing forwarder definitions here.