--* From BMT%WATSON.vnet.ibm.com@yktvmh.watson.ibm.com  Fri Aug 20 21:27:01 1993
--* Received: from yktvmh.watson.ibm.com by radical.watson.ibm.com (AIX 3.2/UCB 5.64/900524)
--*           id AA18994; Fri, 20 Aug 1993 21:27:01 -0400
--* Received: from watson.vnet.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3)
--*    with BSMTP id 7304; Fri, 20 Aug 93 21:28:19 EDT
--* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0"
--*           id <A.BMT.NOTE.VAGENT2.7130.Aug.20.21:28:18.-0400>
--*           for asbugs@watson; Fri, 20 Aug 93 21:28:19 -0400
--* Received: from YKTVMH by watson.vnet.ibm.com with "VAGENT.V1.0"
--*           id 7128; Fri, 20 Aug 1993 21:28:18 EDT
--* Received: from cyst.watson.ibm.com by yktvmh.watson.ibm.com (IBM VM SMTP V2R3)
--*    with TCP; Fri, 20 Aug 93 21:28:18 EDT
--* Received: from spadserv.watson.ibm.com by cyst.watson.ibm.com (AIX 3.2/UCB 5.64/900528)
--*   id AA45813; Fri, 20 Aug 1993 21:27:16 -0400
--* Received: by spadserv.watson.ibm.com (AIX 3.2/UCB 5.64/900524)
--*           id AA21397; Fri, 20 Aug 1993 21:32:53 -0400
--* Date: Fri, 20 Aug 1993 21:32:53 -0400
--* From: bmt@spadserv.watson.ibm.com
--* X-External-Networks: yes
--* Message-Id: <9308210132.AA21397@spadserv.watson.ibm.com>
--* To: asbugs@watson.ibm.com
--* Subject: declaration for R and Mod in where clause not recognized [modring.as][29.8 (current)]

--@ Fixed  by:  SSD   Thu Jun 2 09:46:14 EDT 1994 
--@ Tested by:  none 
--@ Summary:    Use 'default x: T' to provide default types for function parameters from where clauses. 


#include "aslib.as"
#library DemoLib "asdem"
import from DemoLib

Bit ==> Boolean
Outport ==> OutPort

CommutativeRing:Category == Ring with


(ModularRing(R:CommutativeRing,Mod:AbelianMonoid, _
        reduction:(R,Mod) -> R,merge:(Mod,Mod) -> Partial(Mod), _
             exactQuo : (R,R,Mod) -> Partial(R)) : C == T)  where
--  R    :  CommutativeRing
--  Mod  :  AbelianMonoid

  C ==> Ring with
                modulus :   %     -> Mod
                coerce  :   %     -> R
                reduce  : (R,Mod) -> %
                exQuo   :  (%,%)  -> Partial(%)
                recip   :    %    -> Partial(%)
                inv     :    %    -> %

  T ==> add
    --representation
      Rep ==> Record(val:R,modulo:Mod)
      import from R
      import from  Mod
      import from  Rep
      import from  Partial R
      import from Partial Mod
      import from Partial %
    --declarations
      default x :%
      default y: %

    --define
      modulus(x:%):Mod   == rep(x).modulo
      coerce(x:%) :R == rep(x).val
--      coerce(i:Integer):% == per [i::R,0]
--      (i:Integer) * (x:%) : % == (i::%)*x
--      coerce(x:%):OutputForm == (rep(x).val)::OutputForm
      reduce (a:R,m:Mod) : %  == per [reduction(a,m),m]

      0 == per [0$R,0$Mod]
      1 == per [1$R,0$Mod]
      zero?(x:%):Bit == zero? rep(x).val
--      one?(x:%):Bit == one? rep(x).val

      newmodulo(m1:Mod,m2:Mod) : Mod ==
        r:=merge(m1,m2)
        failed?(r) => error "incompatible moduli"
        r::Mod

      (x:%)=(y:%) : Bit ==
        rep(x).val = rep(y).val => true
        rep(x).modulo = rep(y).modulo => false
        rep(x-y).val = 0
      (x:%) ~= (y:%) : Bit == not (x=y)
      apply(p:Outport,x:%):Outport == p(rep(x).val)
      (x:%)+(y:%) : %  == reduce((rep(x).val + rep(y).val),
                          newmodulo(rep(x).modulo,rep(y).modulo))
      (x:%)-(y:%) : % == reduce((rep(x).val - rep(y).val),
                         newmodulo(rep(x).modulo,rep(y).modulo))
      -(x:%):%  == reduce ((- rep(x).val),rep(x).modulo)
      +(x:%):% == x
      (x:%)*(y:%):% == reduce((rep(x).val *$R rep(y).val),newmodulo(rep(x).modulo,rep(y).modulo))

      exQuo(x:%,y:%) : Partial %  ==
        xm:=rep(x).modulo
        if xm ~= rep(y).modulo then xm:=newmodulo(xm,rep(y).modulo)
        r:=exactQuo(rep(x).val,rep(y).val,xm)
        failed?(r) => failed
        (per [r::R,xm])::Partial %

      --if R has EuclideanDomain then
      recip (x:%) : Partial % ==
        r:=exactQuo(1$R,rep(x).val,rep(x).modulo)
        failed?(r) => failed
        (per [r::R,rep(x).modulo])::Partial %

      inv (x:%) : % ==
        failed?(u:=recip x)  => error("not invertible")
        u::%



(ModularField(R,Mod,reduction:(R,Mod) -> R,_
               merge:(Mod,Mod) -> Union(Mod,"failed"),_
                      exactQuo : (R,R,Mod) -> Union(R,"failed")) : C == T)
 where
  R    :  CommutativeRing
  Mod  :  AbelianMonoid

  C == Field with
                modulus :   %     -> Mod
                coerce  :   %     -> R
                reduce  : (R,Mod) -> %
                exQuo   :  (%,%)  -> Union(%,"failed")

  T == ModularRing(R,Mod,reduction,merge,exactQuo)