equation1.spad

)abbrev category IEVALAB InnerEvalable
-- FOR THE BENEFIT OF LIBAX0 GENERATION
++ Author:
++ Basic Operations:
++ Related Domains:
++ Also See: Evalable
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   This category provides \spadfun{eval} operations.
++   A domain may belong to this category if it is possible to make
++   ``evaluation'' substitutions.  The difference between this
++   and \spadtype{Evalable} is that the operations in this category
++   specify the substitution as a pair of arguments rather than as
++   an equation.
InnerEvalable(A : SetCategory, B : Type) : Category == with
    eval : (%, A, B) -> %
       ++ eval(f, x, v) replaces x by v in f.
    eval : (%, List A, List B) -> %
       ++ eval(f, [x1, ..., xn], [v1, ..., vn]) replaces xi by vi in f.
 add
    eval(f : %, x : A, v : B) == eval(f, [x], [v])

)abbrev category EVALAB Evalable
++ Author:
++ Basic Operations:
++ Related Domains:
++ Also See: FullyEvalable
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   This category provides \spadfun{eval} operations.
++   A domain may belong to this category if it is possible to make
++   ``evaluation'' substitutions.
Evalable(R : SetCategory) : Category == InnerEvalable(R, R) with
    eval : (%, Equation R) -> %
       ++ eval(f, x = v) replaces x by v in f.
    eval : (%, List Equation R) -> %
       ++ eval(f, [x1 = v1, ..., xn = vn]) replaces xi by vi in f.
 add
    eval(f : %, eq : Equation R) == eval(f, [eq])
    eval(f : %, xs : List R, vs : List R) == eval(f, [x = v for x in xs for v in vs])

)abbrev domain EQ Equation
--FOR THE BENEFIT  OF LIBAX0 GENERATION
++ Author: Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: April 1985
++ Basic Operations: =
++ Related Domains:
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   Equations as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "=" to "equation".  Otherwise, it will
--   find a modemap for "=" in the domain of the arguments.

Equation(S : Type) : public == private where
  Ex ==> OutputForm
  public ==> Type with
    "=": (S, S) -> %
        ++ a=b creates an equation.
    equation : (S, S) -> %
        ++ equation(a, b) creates an equation.
    swap : % -> %
        ++ swap(eq) interchanges left and right hand side of equation eq.
    lhs : % -> S
        ++ lhs(eqn) returns the left hand side of equation eqn.
    rhs : % -> S
        ++ rhs(eqn) returns the right hand side of equation eqn.
    map : (S -> S, %) -> %
        ++ map(f, eqn) constructs a new equation by applying f to both
        ++ sides of eqn.
    if S has InnerEvalable(Symbol, S) then
             InnerEvalable(Symbol, S)
    if S has SetCategory then
        SetCategory
        CoercibleTo Boolean
        if S has Evalable(S) then
           eval : (%, %) -> %
               ++ eval(eqn, x=f) replaces x by f in equation eqn.
           eval : (%, List %) -> %
               ++ eval(eqn, [x1=v1, ... xn=vn]) replaces xi by vi in equation eqn.
    if S has AbelianSemiGroup then
        AbelianSemiGroup
        "+": (S, %) -> %
            ++ x+eqn produces a new equation by adding x to both sides of
            ++ equation eqn.
        "+": (%, S) -> %
            ++ eqn+x produces a new equation by adding x to  both sides of
            ++ equation eqn.
    if S has AbelianGroup then
        AbelianGroup
        leftZero : % -> %
          ++ leftZero(eq) subtracts the left hand side.
        rightZero : % -> %
          ++ rightZero(eq) subtracts the right hand side.
        "-": (S, %) -> %
            ++ x-eqn produces a new equation by subtracting both sides of
            ++ equation eqn from x.
        "-": (%, S) -> %
            ++ eqn-x produces a new equation by subtracting x from  both sides of
            ++ equation eqn.
    if S has SemiGroup then
        SemiGroup
        "*": (S, %) -> %
            ++ x*eqn produces a new equation by multiplying both sides of
            ++ equation eqn by x.
        "*": (%, S) -> %
            ++ eqn*x produces a new equation by multiplying both sides of
            ++ equation eqn by x.
    if S has Monoid then
        Monoid
        leftOne : % -> Union(%,"failed")
          ++ leftOne(eq) divides by the left hand side, if possible.
        rightOne : % -> Union(%,"failed")
          ++ rightOne(eq) divides by the right hand side, if possible.
    if S has Group then
        Group
        leftOne : % -> Union(%,"failed")
          ++ leftOne(eq) divides by the left hand side.
        rightOne : % -> Union(%,"failed")
          ++ rightOne(eq) divides by the right hand side.
    if S has Ring then
      Ring
      BiModule(S, S)
    if S has CommutativeRing then
      Module(S)
      --Algebra(S)
    if S has IntegralDomain then
      factorAndSplit : % -> List %
        ++ factorAndSplit(eq) make the right hand side 0 and
        ++ factors the new left hand side. Each factor is equated
        ++ to 0 and put into the resulting list without repetitions.
    if S has PartialDifferentialRing(Symbol) then
      PartialDifferentialRing(Symbol)
    if S has Field then
      "/": (%, %) -> %
          ++ e1/e2 produces a new equation by dividing the left and right
          ++ hand sides of equations e1 and e2.
      inv : % -> %
          ++ inv(x) returns the multiplicative inverse of x.
    if S has ExpressionSpace then
        subst : (%, %) -> %
             ++ subst(eq1, eq2) substitutes eq2 into both sides of eq1
             ++ the lhs of eq2 should be a kernel
    if S has ConvertibleTo(InputForm) then ConvertibleTo(InputForm)

  private ==> add
    Rep := Record(lhs : S, rhs : S)
    eq1, eq2 : %
    s : S
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [equation(rcf.factor, 0) for rcf in factorList factor lhs eq0]
          [eq]
    l : S = r : S      == [l, r]
    equation(l, r) == [l, r]    -- hack!  See comment above.
    lhs eqn        == eqn.lhs
    rhs eqn        == eqn.rhs
    swap eqn     == [rhs eqn, lhs eqn]
    map(fn, eqn)   == equation(fn(eqn.lhs), fn(eqn.rhs))

    if S has InnerEvalable(Symbol, S) then
        s : Symbol
        ls : List Symbol
        x : S
        lx : List S
        eval(eqn, s, x) == eval(eqn.lhs, s, x) = eval(eqn.rhs, s, x)
        eval(eqn, ls, lx) == eval(eqn.lhs, ls, lx) = eval(eqn.rhs, ls, lx)
    if S has Evalable(S) then
        eval(eqn1 : %, eqn2 : %) : % ==
           eval(eqn1.lhs, eqn2 pretend Equation S) =
               eval(eqn1.rhs, eqn2 pretend Equation S)
        eval(eqn1 : %, leqn2 : List %) : % ==
           eval(eqn1.lhs, leqn2 pretend List Equation S) =
               eval(eqn1.rhs, leqn2 pretend List Equation S)
    if S has SetCategory then
        eq1 = eq2 == (eq1.lhs = eq2.lhs)@Boolean and
                     (eq1.rhs = eq2.rhs)@Boolean
        coerce(eqn : %) : Ex == eqn.lhs::Ex = eqn.rhs::Ex
        coerce(eqn : %) : Boolean == eqn.lhs = eqn.rhs
    if S has AbelianSemiGroup then
        eq1 + eq2 == eq1.lhs + eq2.lhs = eq1.rhs + eq2.rhs
        s + eq2 == [s, s] + eq2
        eq1 + s == eq1 + [s, s]
    if S has AbelianGroup then
        - eq == (- lhs eq) = (-rhs eq)
        s - eq2 == [s, s] - eq2
        eq1 - s == eq1 - [s, s]
        leftZero eq == 0 = rhs eq - lhs eq
        rightZero eq == lhs eq - rhs eq = 0
        0 == equation(0$S, 0$S)
        eq1 - eq2 == eq1.lhs - eq2.lhs = eq1.rhs - eq2.rhs
    if S has SemiGroup then
        eq1 : % * eq2 : % == eq1.lhs * eq2.lhs = eq1.rhs * eq2.rhs
        l : S   * eqn : % == l       * eqn.lhs = l       * eqn.rhs
        l : S * eqn : %  ==  l * eqn.lhs    =    l * eqn.rhs
        eqn : % * l : S  ==  eqn.lhs * l    =    eqn.rhs * l
        -- We have to be a bit careful here: raising to a +ve integer is OK
        -- (since it's the equivalent of repeated multiplication)
        -- but other powers may cause contradictions
        -- Watch what else you add here! JHD 2/Aug 1990
    if S has Monoid then
        1 == equation(1$S, 1$S)
        recip eq ==
          (lh := recip lhs eq) case "failed" => "failed"
          (rh := recip rhs eq) case "failed" => "failed"
          [lh@S, rh@S]
        leftOne eq ==
          (re := recip lhs eq) case "failed" => "failed"
          1 = rhs eq * re
        rightOne eq ==
          (re := recip rhs eq) case "failed" => "failed"
          lhs eq * re = 1
    if S has Group then
        inv eq == [inv lhs eq, inv rhs eq]
        leftOne eq == 1 = rhs eq * inv rhs eq
        rightOne eq == lhs eq * inv rhs eq = 1
    if S has Ring then
        characteristic() == characteristic()$S
        i : Integer * eq : % == (i::S) * eq
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [equation(rcf.factor, 0) for rcf in factorList factor lhs eq0]
          (S has Polynomial Integer) =>
            eq0 := rightZero eq
            MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _
               Integer, Polynomial Integer)
            p : Polynomial Integer := (lhs eq0) pretend Polynomial Integer
            [equation((rcf.factor) pretend S, 0) for rcf in factorList factor(p)$MF]
          [eq]
    if S has PartialDifferentialRing(Symbol) then
        differentiate(eq : %, sym : Symbol) : % ==
           [differentiate(lhs eq, sym), differentiate(rhs eq, sym)]
    if S has Field then
        eq1 : % / eq2 : % == eq1.lhs / eq2.lhs = eq1.rhs / eq2.rhs
        inv eq == [inv lhs eq, inv rhs eq]
    if S has ExpressionSpace then
        subst(eq1, eq2) ==
            eq3 := eq2 pretend Equation S
            [subst(lhs eq1, eq3), subst(rhs eq1, eq3)]
    if S has ConvertibleTo(InputForm) then
        convert(eq : %) : InputForm ==
            lf := convert(lhs(eq))@InputForm
            rf := convert(rhs(eq))@InputForm
            l_form := [convert('equation)@InputForm, lf, rf]$List(InputForm)
            convert(l_form)@InputForm

)abbrev package EQ2 EquationFunctions2
++ Author:
++ Basic Operations:
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++   This package provides operations for mapping the sides of equations.
EquationFunctions2(S : Type, R : Type) : with
    map : (S ->R , Equation S) -> Equation R
        ++ map(f, eq) returns an equation where f is applied to the sides of eq
 == add
    map(fn, eqn) == equation(fn lhs eqn, fn rhs eqn)

)abbrev category FEVALAB FullyEvalableOver
++ Author:
++ Basic Operations:
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: equation
++ Examples:
++ References:
++ Description:
++    This category provides a selection of evaluation operations
++    depending on what the argument type R provides.
FullyEvalableOver(R : SetCategory) : Category == with
    map : (R -> R, %) -> %
        ++ map(f, ex) evaluates ex, applying f to values of type R in ex.
    if R has Eltable(R, R) then Eltable(R, %)
    if R has Evalable(R) then Evalable(R)
    if R has InnerEvalable(Symbol, R) then InnerEvalable(Symbol, R)
 add
    if R has Eltable(R, R) then
      elt(x : %, r : R) == map(y +-> y(r), x)

    if R has Evalable(R) then
      eval(x : %, l : List Equation R) == map(y +-> eval(y, l), x)

    if R has InnerEvalable(Symbol, R) then
      eval(x : %, ls : List Symbol, lv : List R) ==
          map(y +-> eval(y, ls, lv), x)

--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.