--* From C1GOMEZ%WATSON.vnet.ibm.com@yktvmv.watson.ibm.com Tue Sep 6 10:56:59 1994 --* Received: from yktvmv-ob.watson.ibm.com by asharp.watson.ibm.com (AIX 3.2/UCB 5.64/930311) --* id AA30414; Tue, 6 Sep 1994 10:56:59 -0400 --* Received: from watson.vnet.ibm.com by yktvmv.watson.ibm.com (IBM VM SMTP V2R3) --* with BSMTP id 6577; Tue, 06 Sep 94 10:57:03 EDT --* Received: from YKTVMV by watson.vnet.ibm.com with "VAGENT.V1.0" --* id --* for asbugs@watson; Tue, 06 Sep 94 10:57:02 -0400 --* Received: from YKTVMV by watson.vnet.ibm.com with "VAGENT.V1.0" --* id 4805; Tue, 6 Sep 1994 10:57:01 EDT --* Received: from spadserv.watson.ibm.com by yktvmv.watson.ibm.com --* (IBM VM SMTP V2R3) with TCP; Tue, 06 Sep 94 10:57:00 EDT --* Received: by spadserv.watson.ibm.com (AIX 3.2/UCB 5.64/900524) --* id AA31730; Tue, 6 Sep 1994 10:57:28 -0400 --* Date: Tue, 6 Sep 1994 10:57:28 -0400 --* From: teresa@spadserv.watson.ibm.com --* X-External-Networks: yes --* Message-Id: <9409061457.AA31730@spadserv.watson.ibm.com> --* To: asbugs@watson.ibm.com --* Subject: [1] Bug: 2 constraints not checked --@ Fixed by: SSD Mon Mar 20 08:26:34 EST 1995 --@ Tested by: none --@ Summary: Fixed type form creation for definitions with inferred types. -- Command line: asharp claw.as -- Version: 0.36.5 for AIX RS/6000 -- Original bug file name: claw.as -- THIS IS A HIGH PRIORITY BUG FOR ME, BECAUSE I CANNOT CONTINUE MY WORK. -- 0.65, just comments for transcendental and failed --- tlois.as -- Constructible laws +++ ConstructibleLawCategory(K: DFIELDC) +++ ConstructibleLaw(K: DFIELDC) #include "aslib" #pile #library dynlib "dyn.aso" #library dpolib "dpol.aso" #library dgpolib "dgpol.aso" import from dynlib import from dpolib import from dgpolib +++ Comments. ConstructibleLawCategory(K:DynamicFieldCategory): Category == with Poly ==> DynamicUnivariatePolynomial(K) Gpol ==> DynamicConstructibleGeneralizedPolynomial(K,Poly) LGpol ==> List Gpol S ==> String Kind ==> Enumeration(al,any,ex,fa,tr) Ugpf ==> Union(gpol:Gpol,failed:Enumeration(failed)) SplitGP ==> Record(ppP:Ugpf,gcd:Ugpf,ppQ:Ugpf) SplitSC ==> Record(ppP:Ugpf,gcd:Ugpf,fac:Ugpf,ppQ:Ugpf) Split ==> Record(notEq:%,Eq:%) -- operations <<: (TextWriter,%) -> TextWriter reduce: % -> % ++ reduce(la) -- no reduction, no splitting = : (%,%) -> Boolean build: (Kind,String,LGpol) -> % ++ build(st,sy,ligp) anyElement?: % -> Boolean ++ anyElement?(la) returns true if and only if there is not constraint algebraic?: % -> Boolean ++ algebraic?(la) returns true if and only if la is algebraic exception?: % -> Boolean ++ exception?(la) returns true if and only if la is exception --transcendent?: % -> Boolean ++ transcendent?(la) returns true if and only if la is transcendent failed?: % -> Boolean ++ failed?(la) returns true if and only if la is failed symbol: % -> String ++ symbol(la) returns the symbol of la listOfGPolynomials: % -> LGpol ++ listOfGPolynomials(la) returns the list of polynomials in la -- splitting refineLaw: (%, List Poly) -> % -- only used from equality (and similars) in closure -- to solve problem with denominators ++ characteristic must be 0 ++ refineLaw(la,lp) returns a law la1 similar to la ++ la1 has more polynomials of lower degree than la ++ * la must be an exception or algebraic law ++ * lp must be a list of squarefree polynomials ++ and not empty split: (%,Gpol) -> Split ++ split(la,gp) splitAny: (%,Gpol) -> Split ++ splitAny(la,gp) splitAlgebraic: (%,Gpol) -> Split ++ splitAlgebraic(la,gp) splitException: (%,Gpol) -> Split ++ splitException(ls,gp) --splitTranscendent: (%,Gpol) -> Split ++ splitTranscendent(la,gp) +++ For a description of dynamic constructible laws, +++ see comments for ConstructibleLawCategory ConstructibleLaw(K:DynamicFieldCategory): ConstructibleLawCategory(K) with == add Poly ==> DynamicUnivariatePolynomial(K) Gpol ==> DynamicConstructibleGeneralizedPolynomial(K,Poly) LGpol ==> List Gpol S ==> String SI ==> SingleInteger Kind ==> Enumeration(al,any,ex,fa,tr) Ugpf ==> Union(gpol:Gpol,failed:Enumeration(failed)) SplitGP ==> Record(ppP:Ugpf,gcd:Ugpf,ppQ:Ugpf) SplitSC ==> Record(ppP:Ugpf,gcd:Ugpf,fac:Ugpf,ppQ:Ugpf) Split ==> Record(notEq:%,Eq:%) -- representation Rep == Record(kin:Kind,sym:String,lgpol:LGpol) import from Rep import from SingleInteger import from Union(spg:SplitGP,spc:SplitSC) -- declarations default la,la1,la2: % default gp,gp1,gp2: Gpol default ligp,ligp1,ligp2: LGpol default p: Poly default lp: List Poly default sy: String default ki: Kind default fl: Flag default tt: SplitGP default tto: Record(lgp:LGpol,ugp:Ugpf) default uu: Union(spg:SplitGP,spc:SplitSC) default ugpf: Ugpf default pri: TextWriter -- internal functions equalAux: (%,%) -> Boolean splitAux: (LGpol,Gpol) -> LGpol splitExceptionAux: (LGpol,Gpol) -> Record(lgp:LGpol,ugp:Ugpf) -- define -- reduction reduce(la):% == ligp:= [reduce(gp) for gp in rep(la).lgpol] build(rep(la).kin,rep(la).sym,ligp) -- no reduction, no splitting equalAux(la1:%,la2:%):Boolean == ligp1:= listOfGPolynomials(la1) ligp2:= listOfGPolynomials(la2) (#ligp1 ~= #ligp2)$SI => false bb:Boolean:= true for gp1 in ligp1 for gp2 in ligp2 repeat bb:= roughEqual?(gp1,gp2)$Gpol not bb => break bb la1 = la2 :Boolean == anyElement?(la1) => anyElement?(la2) algebraic?(la1) => algebraic?(la2) => equalAux(la1,la2) false exception?(la1) => exception?(la2) => equalAux(la1,la2) false never build(ki,sy,ligp):% == per [ki,sy,ligp] anyElement?(la):Boolean == rep(la).kin = any algebraic?(la):Boolean == rep(la).kin = al exception?(la):Boolean == rep(la).kin = ex --transcendent?(la):Boolean == rep(la).kin = tr failed?(la):Boolean == rep(la).kin = fa symbol(la):String == rep(la).sym listOfGPolynomials(la):LGpol == rep(la).lgpol pri << la :TextWriter == sy:= rep(la).sym ligp:= rep(la).lgpol failed? la => pri << sy << " failed" anyElement? la => pri << "any " << sy -- transcendent? la => pri << sy << " transcendent" algebraic? la => linear? ligp.first => pri << sy << " = " <<$K constant(ligp.first) <<(pri,ligp.first,sy) pri << " = 0" exception? la => ligp1:= [gp for gp in ligp | info(gp)] gp1:= ligp1.first ligp1:= rest ligp1 if linear?(gp1) then pri << sy << " /= " <<$K constant(gp1) else <<(pri,gp1,sy) pri << " /= 0" for gp in ligp1 repeat pri << ", " if linear?(gp) then pri << sy << " /= " <<$K constant(gp) else <<(pri,gp,sy) pri << " /= 0" pri never -- splitting refineLaw(la,lp):% == ligp:= [gp for gp in rep(la).lgpol] if algebraic? la then gp1:= first ligp ligp:= rest ligp for p in lp repeat lgpolaux:LGpol:= [] gpaux:Gpol:= build(p,squarefree(),false) while not(empty? ligp) repeat gp:= first ligp ligp:= rest ligp tt:= splitSquarefree(gp,gpaux) if tt.ppP case gpol then lgpolaux:= cons(tt.ppP.gpol,lgpolaux) if tt.gcd case gpol then lgpolaux:= cons(tt.gcd.gpol,lgpolaux) if tt.ppQ case failed then lgpolaux:= concat(reverse ligp,lgpolaux) break else gpaux:= tt.ppQ.gpol ligp:= reverse lgpolaux if algebraic? la then ligp:= cons(gp1,ligp) build(rep(la).kin,rep(la).sym,ligp) splitAux(ligp:LGpol,gp:Gpol):LGpol == empty? ligp => cons(gp,ligp) ligp1:= [] while not empty?(ligp) repeat gp1:= ligp.first ligp:= rest ligp uu:= flag(gp1) = noFlag() => [splitSpecialCase(gp1,gp)] [split(gp1,gp)] if uu case spg then if uu.spg.ppP case gpol then ligp1:= cons(uu.spg.ppP.gpol,ligp1) if uu.spg.gcd case gpol then ligp1:= cons(uu.spg.gcd.gpol,ligp1) if uu.spg.ppQ case gpol then if empty? ligp then ligp1:= cons(uu.spg.ppQ.gpol,ligp1) else gp:= uu.spg.ppQ.gpol else ligp1:= concat(reverse(ligp),ligp1) break else -- uu case spc if uu.spc.ppP case gpol then ligp1:= cons(uu.spc.ppP.gpol,ligp1) if uu.spc.gcd case gpol then ligp1:= cons(uu.spc.gcd.gpol,ligp1) if uu.spc.fac case gpol then ligp1:= cons(uu.spc.fac.gpol,ligp1) if uu.spc.ppQ case gpol then if empty? ligp then ligp1:= cons(uu.spc.ppQ.gpol,ligp1) else gp:= uu.spc.ppQ.gpol else ligp1:= concat(reverse(ligp),ligp1) break reverse ligp1 splitExceptionAux(ligp,gp):Record(lgpol:LGpol,ugp:Ugpf) == ligp1:= [] ugpf:= [gp] while not empty? ligp repeat gp1:= ligp.first ligp:= rest ligp uu:= flag(gp1) = noFlag() => [splitSpecialCase(gp1,gp)] [split(gp1,gp)] if uu case spg then if uu.spg.ppP case gpol then ligp1:= cons(uu.spg.ppP.gpol,ligp1) if uu.spg.gcd case gpol then ligp1:= cons(uu.spg.gcd.gpol,ligp1) if uu.spg.ppQ case gpol then if empty? ligp then ugpf:= [gp] else gp:= uu.spg.ppQ.gpol else -- uu.spg.ppQ case failed ligp1:= concat(reverse(ligp),ligp1) ugpf:= [failed] break else -- uu case spc if uu.spc.ppP case gpol then ligp1:= cons(uu.spc.ppP.gpol,ligp1) if uu.spc.gcd case gpol then ligp1:= cons(uu.spc.gcd.gpol,ligp1) if uu.spc.fac case gpol then ligp1:= cons(uu.spc.fac.gpol,ligp1) if uu.spc.ppQ case gpol then if empty? ligp then ugpf:= [gp] else gp:= uu.spc.ppQ.gpol else -- uu.spc.ppQ case failed ligp1:= concat(reverse(ligp),ligp1) ugpf:= [failed] break [reverse ligp1,ugpf] split(la,gp):Split == -- failed? la => error "LAW MUST BE NOT FAILED IN split$CLAW" anyElement? la => splitAny(la,gp) algebraic? la => splitAlgebraic(la,gp) exception? la => splitException(la,gp) --transcendent? la => splitTranscendent(la,gp) never splitAny(la,gp):Split == sy:= rep(la).sym ligp:= [gp] [build(ex,sy,ligp),build(al,sy,ligp)] splitAlgebraic(la,gp):Split == sy:= rep(la).sym ligp:= [gp1 for gp1 in rep(la).lgpol] gp1:= ligp.first ligp:= rest ligp tt:= split(gp1,gp) tt.gcd case failed => ligp:= splitAux(ligp,refineInfo(gp)) ligp:= cons(gp1,ligp) [build(al,sy,ligp),build(fa,sy,[])] tt.ppP case failed => if tt.ppQ case gpol then ligp:= splitAux(ligp,refineInfo(tt.ppQ.gpol)) ligp:= cons(gp1,ligp) [build(fa,sy,[]),build(al,sy,ligp)] if tt.ppQ case gpol then ligp:= splitAux(ligp,refineInfo(tt.ppQ.gpol)) ligp1:= concat(ligp,[refineInfo(tt.gcd.gpol)]) ligp1:= cons(tt.ppP.gpol,ligp1) ligp2:= concat(ligp,[refineInfo(tt.ppP.gpol)]) ligp2:= cons(tt.gcd.gpol,ligp2) [build(al,sy,ligp1),build(al,sy,ligp2)] splitException(la,gp):Split == sy:= rep(la).sym ligp:= [gp1 for gp1 in rep(la).lgpol] tto:= splitExceptionAux(ligp,gp) tto.ugp case failed => [build(ex,sy,tto.lgp),build(fa,sy,[])] ligp1:= concat(tto.lgp,[tto.ugp.gpol]) ligp2:= [refineInfo(gp1) for gp1 in tto.lgp] ligp2:= cons(tto.ugp.gpol,ligp2) [build(ex,sy,ligp1),build(al,sy,ligp2)] -- splitTranscendent(la,gp):Split == -- sy:= rep(la).sym -- ligp:= [gp1 for gp1 in rep(la).lgpol] -- ligp:= splitAux(ligp,refineInfo(gp)) -- [build(tr,sy,ligp),build(fa,sy,[])]