From ab8cc85adde879fb963c94d15675783f2cf4b183 Mon Sep 17 00:00:00 2001 From: dos-reis Date: Tue, 14 Aug 2007 05:14:52 +0000 Subject: Initial population. --- src/interp/i-resolv.boot.pamphlet | 860 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 860 insertions(+) create mode 100644 src/interp/i-resolv.boot.pamphlet (limited to 'src/interp/i-resolv.boot.pamphlet') diff --git a/src/interp/i-resolv.boot.pamphlet b/src/interp/i-resolv.boot.pamphlet new file mode 100644 index 00000000..fd46a0e6 --- /dev/null +++ b/src/interp/i-resolv.boot.pamphlet @@ -0,0 +1,860 @@ +\documentclass{article} +\usepackage{axiom} + +\title{\File{src/interp/i-resolv.boot} Pamphlet} +\author{The Axiom Team} + +\begin{document} +\maketitle +\begin{abstract} +\end{abstract} +\eject +\tableofcontents +\eject + +\begin{verbatim} +new resolution: types and modes + +a type is any term (structure) which can be regarded as a + functor call +a basic type is the call of a nullary functor (e.g. (Integer)), + otherwise it is a structured type (e.g. (Polynomial (Integer))) +a functor together with its non-type arguments is called a + type constructor + +a mode is a type which can be partially specified, i.e. a term + containing term variables +a term variable (denoted by control-L) stands for any nullary or unary function + which was build from type constructors +this means, a term variable can be: + a function LAMBDA ().T, where T is a type + a function LAMBDA (X).T(X), where X is a variable for a type and + T a type containing this variable + a function LAMBDA X.X ("control-L can be disregarded") +examples: + P(control-L) can stand for (Polynomial (RationalFunction (Integer))) + G(control-L(I)) can stand for (Gaussian (Polynomial (Integer))), but also + for (Gaussian (Integer)) + + +Resolution of Two Types + +this symmetric resolution is done the following way: +1. if the same type constructor occurs in both terms, then the + type tower is built around this constructor (resolveTTEq) +2. the next step is to look for two constructors which have an + "algebraic relationship", this means, a rewrite rule is + applicable (e.g. UP(x,I) and MP([x,y],I)) + this is done by resolveTTRed +3. if none of this is true, then a tower of types is built + e.g. resolve P I and G I to P G I + +\end{verbatim} +\section{License} +<>= +-- 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. + +@ +<<*>>= +<> + +resolveTypeList u == + u is [a,:tail] => + + -- if the list consists entirely of variables then keep it explicit + allVars := + a is ['Variable,v] => [v] + nil + while allVars for b in tail repeat + allVars := + b is ['Variable,v] => insert(v, allVars) + nil + allVars => + null rest allVars => ['Variable, first allVars] + ['OrderedVariableList,nreverse allVars] + + for md in tail repeat + a := resolveTT(md,a) + null a => return nil + a + throwKeyedMsg("S2IR0002",NIL) + +-- resolveTT is in CLAMMED BOOT + +resolveTypeListAny tl == + rt := resolveTypeList tl + null rt => $Any + rt + +resolveTTAny(t1,t2) == + (t3 := resolveTT(t1, t2)) => t3 + $Any + +resolveTT1(t1,t2) == + -- this is the main symmetric resolve + -- first it looks for equal constructors on both sides + -- then it tries to use a rewrite rule + -- and finally it builds up a tower + t1=t2 => t1 + (t1 = '$NoValueMode) or (t2 = '$NoValueMode) => NIL + (t1 = $Void) or (t2 = $Void) => $Void + (t1 = $Any) or (t2 = $Any) => $Any + t1 = '(Exit) => t2 + t2 = '(Exit) => t1 + t1 is ['Union,:.] => resolveTTUnion(t1,t2) + t2 is ['Union,:.] => resolveTTUnion(t2,t1) + STRINGP(t1) => + t2 = $String => t2 + NIL + STRINGP(t2) => + t1 = $String => t1 + NIL + null acceptableTypesToResolve(t1,t2) => NIL + if compareTT(t1,t2) then + t := t1 + t1 := t2 + t2 := t + (t := resolveTTSpecial(t1,t2)) and isValidType t => t + (t := resolveTTSpecial(t2,t1)) and isValidType t => t + isSubTowerOf(t1,t2) and canCoerceFrom(t1,t2) => t2 + isSubTowerOf(t2,t1) and canCoerceFrom(t2,t1) => t1 + t := resolveTTRed(t1,t2) => t + t := resolveTTCC(t1,t2) => t + (t := resolveTTEq(t1,t2)) and isValidType t => t + [c1,:arg1] := deconstructT t1 + arg1 and + [c2,:arg2] := deconstructT t2 + arg2 and + t := resolveTT1(last arg1,last arg2) + t and ( resolveTT2(c1,c2,arg1,arg2,t) or + resolveTT2(c2,c1,arg2,arg1,t) ) + +acceptableTypesToResolve(t1,t2) == + -- this is temporary. It ensures that two types that have coerces + -- that really should be converts don't automatically resolve. + -- when the coerces go away, so will this. + acceptableTypesToResolve1(t1,t2) and + acceptableTypesToResolve1(t2,t1) + +acceptableTypesToResolve1(t1,t2) == + t1 = $Integer => + t2 = $String => NIL + true + t1 = $DoubleFloat or t1 = $Float => + t2 = $String => NIL + t2 = '(RationalNumber) => NIL + t2 = [$QuotientField, $Integer] => NIL + true + true + +resolveTT2(c1,c2,arg1,arg2,t) == + -- builds a tower and tests for all the necessary coercions + t0 := constructM(c2,replaceLast(arg2,t)) + canCoerceFrom(t,t0) and + t1 := constructM(c1,replaceLast(arg1,t0)) + canCoerceFrom(t0,t1) and t1 + +resolveTTUnion(t1 is ['Union,:doms],t2) == + unionDoms1 := + doms and first doms is [":",:.] => + tagged := true + [t for [.,.,t] in doms] + tagged := false + doms + member(t2,unionDoms1) => t1 + tagged => NIL + t2 isnt ['Union,:doms2] => + ud := nil + bad := nil + for d in doms while ^bad repeat + d = '"failed" => ud := [d,:ud] + null (d' := resolveTT(d,t2)) => bad := true + ud := [d',:ud] + bad => NIL + ['Union,:REMDUP reverse ud] + ud := nil + bad := nil + for d in doms2 while ^bad repeat + d = '"failed" => ud := append(ud,[d]) + null (d' := resolveTTUnion(t1,d)) => bad := true + ud := append(ud,CDR d') + bad => NIL + ['Union,:REMDUP ud] + +resolveTTSpecial(t1,t2) == + -- tries to resolve things that would otherwise get mangled in the + -- rest of the resolve world. I'll leave it for Albi to fix those + -- things. (RSS 1/-86) + + -- following is just an efficiency hack + (t1 = '(Symbol) or t1 is ['OrderedVariableList,.]) and PAIRP(t2) and + CAR(t2) in '(Polynomial RationalFunction) => t2 + + (t1 = '(Symbol)) and ofCategory(t2, '(IntegerNumberSystem)) => + resolveTT1(['Polynomial, t2], t2) + + t1 = '(AlgebraicNumber) and (t2 = $Float or t2 = $DoubleFloat) => + ['Expression, t2] + t1 = '(AlgebraicNumber) and (t2 = ['Complex, $Float] or t2 = ['Complex, $DoubleFloat]) => + ['Expression, CADR t2] + + t1 = '(AlgebraicNumber) and t2 is ['Complex,.] => + resolveTT1('(Expression (Integer)), t2) + + t1 is ['SimpleAlgebraicExtension,F,Rep,poly] => + t2 = Rep => t1 + t2 is ['UnivariatePolynomial,x,R] and (t3 := resolveTT(t1, R)) => + ['UnivariatePolynomial,x,t3] + t2 is ['Variable,x] and (t3 := resolveTT(t1, F)) => + ['UnivariatePolynomial,x,t3] + t2 is ['Polynomial,R] and (R' := resolveTT(Rep, t2)) => + R' = Rep => t1 + ['Polynomial,t1] + canCoerceFrom(t2,F) => t1 + nil + t1 = $PositiveInteger and ofCategory(t2,'(Ring)) => + resolveTT1($Integer,t2) + t1 = $NonNegativeInteger and ofCategory(t2,'(Ring)) => + resolveTT1($Integer,t2) + t1 is ['OrderedVariableList,[x]] => resolveTTSpecial(['Variable, x], t2) + t1 is ['OrderedVariableList,vl] => + ofCategory(t2,'(Ring)) => resolveTT(['Polynomial,'(Integer)],t2) + resolveTT($Symbol,t2) + t1 is ['Variable,x] => + EQCAR(t2,'SimpleAlgebraicExtension) => resolveTTSpecial(t2,t1) + t2 is ['UnivariatePolynomial,y,S] => + x = y => t2 + resolveTT1(['UnivariatePolynomial,x,'(Integer)],t2) + t2 is ['Variable,y] => + x = y => t1 +-- ['OrderedVariableList, MSORT [x,y]] + $Symbol + t2 = '(Symbol) => t2 + t2 is ['Polynomial,.] => t2 + t2 is ['OrderedVariableList, vl] and member(x,vl) => t2 + isPolynomialMode t2 => nil + ofCategory(t2, '(IntegerNumberSystem)) => resolveTT(['Polynomial, t2], t2) + resolveTT(['Polynomial,'(Integer)],t2) + t1 is ['FunctionCalled,f] and t2 is ['FunctionCalled,g] => + null (mf := get(f,'mode,$e)) => NIL + null (mg := get(g,'mode,$e)) => NIL + mf ^= mg => NIL + mf + t1 is ['UnivariatePolynomial,x,S] => + EQCAR(t2,'Variable) => + resolveTTSpecial(t2,t1) + EQCAR(t2,'SimpleAlgebraicExtension) => + resolveTTSpecial(t2,t1) + t2 is ['UnivariatePolynomial,y,T] => + (x = y) and (U := resolveTT1(S,T)) and ['UnivariatePolynomial,x,U] + nil + t1 = '(Pi) => + t2 is ['Complex,d] => defaultTargetFE t2 + t2 is ['AlgebraicNumber] => defaultTargetFE t2 + EQCAR(t2, 'Variable) or t2 = $Symbol => + defaultTargetFE($Symbol) + t2 is ['Polynomial, .] or t2 is ['Fraction, ['Polynomial, .]] => + defaultTargetFE(t2) + nil + t1 is ['Polynomial,['Complex,u1]] and t2 is ['Complex,u2] => + resolveTT1(t1,u2) + t1 is ['Polynomial,R] and t2 is ['Complex,S] => + containsPolynomial(S) => resolveTT1(['Polynomial,['Complex,R]],t2) + ['Polynomial,['Complex,resolveTT1(R,S)]] + t1 is ['Expression, R] and t2 is ['Complex,S] => + dom' := resolveTT(R, t2) + null dom' => nil + ['Expression, dom'] + t1 is ['Segment, dom] and t2 isnt ['Segment,.] => + dom' := resolveTT(dom, t2) + null dom' => nil + ['Segment, dom'] + nil + +resolveTTCC(t1,t2) == + -- tries to use canCoerceFrom information to see if types can be + -- coerced to one another + gt21 := GGREATERP(t2,t1) + (c12 := canCoerceFrom(t1,t2)) and gt21 => t2 + c21 := canCoerceFrom(t2,t1) + null (c12 or c21) => NIL + c12 and not c21 => t2 + c21 and not c12 => t1 + -- both are coerceable to each other + if gt21 then t1 else t2 + +resolveTTEq(t1,t2) == + -- tries to find the constructor of t1 somewhere in t2 (or vice versa) + -- and move the other guy to the top + [c1,:arg1] := deconstructT t1 + [c2,:arg2] := deconstructT t2 + t := resolveTTEq1(c1,arg1,[c2,arg2]) => t + t := ( arg1 and resolveTTEq2(c2,arg2,[c1,arg1]) ) => t + arg2 and resolveTTEq2(c1,arg1,[c2,arg2]) + +resolveTTEq1(c1,arg1,TL is [c2,arg2,:.]) == + -- takes care of basic types and of types with the same constructor + -- calls resolveTT1 on the arguments in the second case + null arg1 and null arg2 => + canCoerceFrom(c1,c2) => constructTowerT(c2,CDDR TL) + canCoerceFrom(c2,c1) and constructTowerT(c1,CDDR TL) + c1=c2 and + [c2,arg2,:TL] := bubbleType TL + until null arg1 or null arg2 or not t repeat + t := resolveTT1(CAR arg1,CAR arg2) => + arg := CONS(t,arg) + arg1 := CDR arg1 + arg2 := CDR arg2 + t and null arg1 and null arg2 and + t0 := constructM(c1,nreverse arg) + constructTowerT(t0,TL) + +resolveTTEq2(c1,arg1,TL is [c,arg,:.]) == + -- tries to resolveTTEq the type [c1,arg1] with the last argument + -- of the type represented by TL + [c2,:arg2] := deconstructT last arg + TL := [c2,arg2,:TL] + t := resolveTTEq1(c1,arg1,TL) => t + arg2 and resolveTTEq2(c1,arg1,TL) + +resolveTTRed(t1,t2) == + -- the same function as resolveTTEq, but instead of testing for + -- constructor equality, it looks whether a rewrite rule can be applied + t := resolveTTRed1(t1,t2,NIL) => t + [c1,:arg1] := deconstructT t1 + t := arg1 and resolveTTRed2(t2,last arg1,[c1,arg1]) => t + [c2,:arg2] := deconstructT t2 + arg2 and resolveTTRed2(t1,last arg2,[c2,arg2]) + +resolveTTRed1(t1,t2,TL) == + -- tries to apply a reduction rule on (Resolve t1 t2) + -- then it creates a type using the result and TL + EQ(t,term1RW(t := ['Resolve,t1,t2],$Res)) and + EQ(t,term1RW(t := ['Resolve,t2,t1],$Res)) => NIL + [c2,:arg2] := deconstructT t2 + [c2,arg2,:TL] := bubbleType [c2,arg2,:TL] + t2 := constructM(c2,arg2) + l := term1RWall(['Resolve,t1,t2],$Res) + for t0 in l until t repeat t := resolveTTRed3 t0 + l and t => constructTowerT(t,TL) + l := term1RWall(['Resolve,t2,t1],$Res) + for t0 in l until t repeat t := resolveTTRed3 t0 + l and t and constructTowerT(t,TL) + +resolveTTRed2(t1,t2,TL) == + -- tries to resolveTTRed t1 and t2 and build a type using TL + t := resolveTTRed1(t1,t2,TL) => t + [c2,:arg2] := deconstructT t2 + arg2 and resolveTTRed2(t1,last arg2,[c2,arg2,:TL]) + +resolveTTRed3(t) == + -- recursive resolveTTRed which handles all subterms of the form + -- (Resolve t1 t2) or subterms which have to be interpreted + atom t => t + t is ['Resolve,a,b] => + ( t1 := resolveTTRed3 a ) and ( t2 := resolveTTRed3 b ) and + resolveTT1(t1,t2) + t is ['Incl,a,b] => member(a,b) and b + t is ['SetDiff,a,b] => intersection(a,b) and SETDIFFERENCE(a,b) + t is ['SetComp,a,b] => + and/[member(x,a) for x in b] and SETDIFFERENCE(a,b) + t is ['SetInter,a,b] => intersection(a,b) + t is ['SetUnion,a,b] => union(a,b) + t is ['VarEqual,a,b] => (a = b) and a + t is ['SetEqual,a,b] => + (and/[member(x,a) for x in b] and and/[member(x,b) for x in a]) and a + [( atom x and x ) or ((not cs and x and not interpOp? x and x) + or resolveTTRed3 x) or return NIL + for x in t for cs in GETDATABASE(CAR t, 'COSIG) ] + +interpOp?(op) == + PAIRP(op) and + CAR(op) in '(Incl SetDiff SetComp SetInter SetUnion VarEqual SetEqual) + +--% Resolve Type with Category + +resolveTCat(t,c) == + -- this function attempts to find a type tc of category c such that + -- t can be coerced to tc. NIL returned for failure. + -- Example: t = Integer, c = Field ==> tc = RationalNumber + + -- first check whether t already belongs to c + ofCategory(t,c) => t + + -- if t is built by a parametrized constructor and there is a + -- condition on the parameter that matches the category, try to + -- recurse. An example of this is (G I, Field) -> G RN + + rest(t) and (tc := resolveTCat1(t,c)) => tc + + -- now check some specific niladic categories + c in '((Field) (EuclideanDomain)) and ofCategory(t,'(IntegralDomain))=> + eqType [$QuotientField, t] + + c = '(Field) and t = $Symbol => ['RationalFunction,$Integer] + + c = '(Ring) and t is ['FactoredForm,t0] => ['FactoredRing,t0] + + (t is [t0]) and (sd := getImmediateSuperDomain(t0)) and sd ^= t0 => + resolveTCat(sd,c) + + SIZE(td := deconstructT t) ^= 2=> NIL + SIZE(tc := deconstructT c) ^= 2 => NIL + ut := underDomainOf t + null isValidType(uc := last tc) => NIL + null canCoerceFrom(ut,uc) => NIL + nt := constructT(first td,[uc]) + ofCategory(nt,c) => nt + NIL + +resolveTCat1(t,c) == + -- does the hard work of looking at conditions on under domains + -- if null (ut := getUnderModeOf(t)) then ut := last dt + null (conds := getConditionsForCategoryOnType(t,c)) => NIL +--rest(conds) => NIL -- will handle later + cond := first conds + cond isnt [.,['has, pat, c1],:.] => NIL + rest(c1) => NIL -- make it simple + + argN := 0 + t1 := nil + + for ut in rest t for i in 1.. while (argN = 0) repeat + sharp := INTERNL('"#",STRINGIMAGE i) + sharp = pat => + argN := i + t1 := ut + + null t1 => NIL + null (t1' := resolveTCat(t1,c1)) => NIL + t' := copy t + t'.argN := t1' + t' + +getConditionsForCategoryOnType(t,cat) == + getConditionalCategoryOfType(t,[NIL],['ATTRIBUTE,cat]) + +getConditionalCategoryOfType(t,conditions,match) == + if PAIRP t then t := first t + t in '(Union Mapping Record) => NIL + conCat := GETDATABASE(t,'CONSTRUCTORCATEGORY) + REMDUP CDR getConditionalCategoryOfType1(conCat,conditions,match,[NIL]) + +getConditionalCategoryOfType1(cat,conditions,match,seen) == + cat is ['Join,:cs] or cat is ['CATEGORY,:cs] => + null cs => conditions + getConditionalCategoryOfType1([first cat,:rest cs], + getConditionalCategoryOfType1(first cs,conditions,match,seen), + match,seen) + cat is ['IF,., cond,.] => + matchUpToPatternVars(cond,match,NIL) => + RPLACD(conditions,CONS(cat,CDR conditions)) + conditions + conditions + cat is [catName,:.] and (GETDATABASE(catName,'CONSTRUCTORKIND) = 'category) => + cat in CDR seen => conditions + RPLACD(seen,[cat,:CDR seen]) + subCat := GETDATABASE(catName,'CONSTRUCTORCATEGORY) + -- substitute vars of cat into category + for v in rest cat for vv in $TriangleVariableList repeat + subCat := SUBST(v,vv,subCat) + getConditionalCategoryOfType1(subCat,conditions,match,seen) + conditions + +matchUpToPatternVars(pat,form,patAlist) == + -- tries to match pattern variables (of the # form) in pat + -- against expressions in form. If one is found, it is checked + -- against the patAlist to make sure we are using the same expression + -- each time. + EQUAL(pat,form) => true + isSharpVarWithNum(pat) => + -- see is pattern variable is in alist + (p := ASSOC(pat,patAlist)) => EQUAL(form,CDR p) + patAlist := [[pat,:form],:patAlist] + true + PAIRP(pat) => + not (PAIRP form) => NIL + matchUpToPatternVars(CAR pat, CAR form,patAlist) and + matchUpToPatternVars(CDR pat, CDR form,patAlist) + NIL + +--% Resolve Type with Mode + +-- only implemented for nullary control-L's (which stand for types) + +resolveTMOrCroak(t,m) == + resolveTM(t,m) or throwKeyedMsg("S2IR0004",[t,m]) + +resolveTM(t,m) == + -- resolves a type with a mode which may be partially specified + startTimingProcess 'resolve + $Subst : local := NIL + $Coerce : local := 'T + t := eqType t + m := eqType SUBSTQ("**",$EmptyMode,m) + tt := resolveTM1(t,m) + result := tt and isValidType tt and eqType tt + stopTimingProcess 'resolve + result + +resolveTM1(t,m) == + -- general resolveTM, which looks for a term variable + -- otherwise it looks whether the type has the same top level + -- constructor as the mode, looks for a rewrite rule, or builds up + -- a tower + t=m => t + m is ['Union,:.] => resolveTMUnion(t,m) + m = '(Void) => m + m = '(Any) => m + m = '(Exit) => t + containsVars m => + isPatternVar m => + p := ASSQ(m,$Subst) => + $Coerce => + tt := resolveTT1(t,CDR p) => RPLACD(p,tt) and tt + NIL + t=CDR p and t + $Subst := CONS(CONS(m,t),$Subst) + t + atom(t) or atom(m) => NIL + (t is ['Record,:tr]) and (m is ['Record,:mr]) and + (tt := resolveTMRecord(tr,mr)) => tt + t is ['Record,:.] or m is ['Record,:.] => NIL + t is ['Variable, .] and m is ['Mapping, :.] => m + t is ['FunctionCalled, .] and m is ['Mapping, :.] => m + if isEqualOrSubDomain(t, $Integer) then + t := $Integer + tt := resolveTMEq(t,m) => tt + $Coerce and + tt := resolveTMRed(t,m) => tt + resolveTM2(t,m) + $Coerce and canCoerceFrom(t,m) and m + +resolveTMRecord(tr,mr) == + #tr ^= #mr => NIL + ok := true + tt := NIL + for ta in tr for ma in mr while ok repeat + -- element is [':,tag,mode] + CADR(ta) ^= CADR(ma) => ok := NIL -- match tags + ra := resolveTM1(CADDR ta, CADDR ma) -- resolve modes + null ra => ok := NIL + tt := CONS([CAR ta,CADR ta,ra],tt) + null ok => NIL + ['Record,nreverse tt] + +resolveTMUnion(t, m is ['Union,:ums]) == + isTaggedUnion m => resolveTMTaggedUnion(t,m) + -- resolves t with a Union type + t isnt ['Union,:uts] => + ums := REMDUP spliceTypeListForEmptyMode([t],ums) + ums' := nil + success := nil + for um in ums repeat + (um' := resolveTM1(t,um)) => + success := true + um' in '(T TRUE) => ums' := [um,:ums'] + ums' := [um',:ums'] + ums' := [um,:ums'] + -- remove any duplicate domains that might have been created + m' := ['Union,:REMDUP reverse ums'] + success => + null CONTAINED('_*_*,m') => m' + t = $Integer => NIL + resolveTM1($Integer,m') + NIL + -- t is actually a Union if we got here + ums := REMDUP spliceTypeListForEmptyMode(uts,ums) + bad := nil + doms := nil + for ut in uts while ^bad repeat + (m' := resolveTMUnion(ut,['Union,:ums])) => + doms := append(CDR m',doms) + bad := true + bad => NIL + ['Union,:REMDUP doms] + +resolveTMTaggedUnion(t, m is ['Union,:ums]) == + NIL + +spliceTypeListForEmptyMode(tl,ml) == + -- splice in tl for occurrence of ** in ml + null ml => nil + ml is [m,:ml'] => + m = "**" => append(tl,spliceTypeListForEmptyMode(tl,ml')) + [m,:spliceTypeListForEmptyMode(tl,ml')] + +resolveTM2(t,m) == + -- resolves t with the last argument of m and builds up a tower + [cm,:argm] := deconstructT m + argm and + tt := resolveTM1(t,last argm) + tt and + ttt := constructM(cm,replaceLast(argm,tt)) + ttt and canCoerceFrom(tt,ttt) and ttt + +resolveTMEq(t,m) == + -- tests whether t and m have the same top level constructor, which, + -- in the case of t, could be bubbled up + (res := resolveTMSpecial(t,m)) => res + [cm,:argm] := deconstructT m + c := containsVars cm + TL := NIL + until b or not t repeat + [ct,:argt] := deconstructT t + b := + c => + SL := resolveTMEq1(ct,cm) + not EQ(SL,'failed) + ct=cm + not b => + TL := [ct,argt,:TL] + t := argt and last argt + b and + t := resolveTMEq2(cm,argm,[ct,argt,:TL]) + if t then for p in SL repeat $Subst := augmentSub(CAR p,CDR p,$Subst) + t + +resolveTMSpecial(t,m) == + -- a few special cases + t = $AnonymousFunction and m is ['Mapping,:.] => m + t is ['Variable,x] and m is ['OrderedVariableList,le] => + isPatternVar le => ['OrderedVariableList,[x]] + PAIRP(le) and member(x,le) => le + NIL + t is ['Fraction, ['Complex, t1]] and m is ['Complex, m1] => + resolveTM1(['Complex, ['Fraction, t1]], m) + t is ['Fraction, ['Polynomial, ['Complex, t1]]] and m is ['Complex, m1] => + resolveTM1(['Complex, ['Fraction, ['Polynomial, t1]]], m) + t is ['Mapping,:lt] and m is ['Mapping,:lm] => + #lt ^= #lm => NIL + l := NIL + ok := true + for at in lt for am in lm while ok repeat + (ok := resolveTM1(at,am)) => l := [ok,:l] + ok and ['Mapping,:reverse l] + t is ['Segment,u] and m is ['UniversalSegment,.] => + resolveTM1(['UniversalSegment, u], m) + NIL + +resolveTMEq1(ct,cm) == + -- ct and cm are type constructors + -- tests for a match from cm to ct + -- the result is a substitution or 'failed + not (CAR ct=CAR cm) => 'failed + SL := NIL + ct := CDR ct + cm := CDR cm + b := 'T + while ct and cm and b repeat + xt := CAR ct + ct := CDR ct + xm := CAR cm + cm := CDR cm + if not (atom xm) and CAR xm = ":" -- i.e. Record + and CAR xt = ":" and CADR xm = CADR xt then + xm := CADDR xm + xt := CADDR xt + b := + xt=xm => 'T + isPatternVar(xm) and + p := ASSQ(xm,$Subst) => xt=CDR p + p := ASSQ(xm,SL) => xt=CDR p + SL := augmentSub(xm,xt,SL) + b => SL + 'failed + +resolveTMEq2(cm,argm,TL) == + -- [cm,argm] is a deconstructed mode, + -- TL is a deconstructed type t + [ct,argt,:TL] := + $Coerce => bubbleType TL + TL + null TL and + null argm => constructM(ct,argt) +-- null argm => NIL + arg := NIL + while argt and argm until not tt repeat + x1 := CAR argt + argt := CDR argt + x2 := CAR argm + argm := CDR argm + tt := resolveTM1(x1,x2) => + arg := CONS(tt,arg) + null argt and null argm and tt and constructM(ct,nreverse arg) + +resolveTMRed(t,m) == + -- looks for an applicable rewrite rule at any level of t and tries + -- to bubble this constructor up to the top to t + TL := NIL + until b or not t repeat + [ct,:argt] := deconstructT t + b := not EQ(t,term1RW(['Resolve,t,m],$ResMode)) and + [c0,arg0,:TL0] := bubbleType [ct,argt,:TL] + null TL0 and + l := term1RWall(['Resolve,constructM(c0,arg0),m],$ResMode) + for t0 in l until t repeat t := resolveTMRed1 t0 + l and t + b or + TL := [ct,argt,:TL] + t := argt and last argt + b and t + +resolveTMRed1(t) == + -- recursive resolveTMRed which handles all subterms of the form + -- (Resolve a b) + atom t => t + t is ['Resolve,a,b] => + ( a := resolveTMRed1 a ) and ( b := resolveTMRed1 b ) and + resolveTM1(a,b) + t is ['Incl,a,b] => PAIRP b and member(a,b) and b + t is ['Diff,a,b] => PAIRP a and member(b,a) and SETDIFFERENCE(a,[b]) + t is ['SetIncl,a,b] => PAIRP b and and/[member(x,b) for x in a] and b + t is ['SetDiff,a,b] => PAIRP b and PAIRP b and + intersection(a,b) and SETDIFFERENCE(a,b) + t is ['VarEqual,a,b] => (a = b) and b + t is ['SetComp,a,b] => PAIRP a and PAIRP b and + and/[member(x,a) for x in b] and SETDIFFERENCE(a,b) + t is ['SimpleAlgebraicExtension,a,b,p] => -- this is a hack. RSS + ['SimpleAlgebraicExtension, resolveTMRed1 a, resolveTMRed1 b,p] + [( atom x and x ) or resolveTMRed1 x or return NIL for x in t] + +--% Type and Mode Representation + +eqType(t) == + -- looks for an equivalent but more simple type + -- eg, eqType QF I = RN + -- the new algebra orginization no longer uses these sorts of types +-- termRW(t,$TypeEQ) + t + +equiType(t) == + -- looks for an equivalent but expanded type + -- eg, equiType RN == QF I + -- the new algebra orginization no longer uses these sorts of types +-- termRW(t,$TypeEqui) + t + +getUnderModeOf d == + not PAIRP d => NIL +-- n := LASSOC(first d,$underDomainAlist) => d.n ----> $underDomainAlist NOW always NIL + for a in rest d for m in rest destructT d repeat + if m then return a + +--deconstructM(t) == +-- -- M is a type, which may contain type variables +-- -- results in a pair (type constructor . mode arguments) +-- CDR t and constructor? CAR t => +-- dt := destructT CAR t +-- args := [ x for d in dt for y in t | ( x := d and y ) ] +-- c := [ x for d in dt for y in t | ( x := not d and y ) ] +-- CONS(c,args) +-- CONS(t,NIL) + +deconstructT(t) == + -- M is a type, which may contain type variables + -- results in a pair (type constructor . mode arguments) + KDR t and constructor? CAR t => + dt := destructT CAR t + args := [ x for d in dt for y in t | ( x := d and y ) ] + c := [ x for d in dt for y in t | ( x := not d and y ) ] + CONS(c,args) + CONS(t,NIL) + +constructT(c,A) == + -- c is a type constructor, A a list of argument types + A => [if d then POP A else POP c for d in destructT CAR c] + c + +constructM(c,A) == + -- replaces top level RE's or QF's by equivalent types, if possible + containsVars(c) or containsVars(A) => NIL + -- collapses illegal FE's + CAR(c) = $FunctionalExpression => eqType defaultTargetFE CAR A + eqType constructT(c,A) + +replaceLast(A,t) == + -- replaces the last element of the nonempty list A by t (constructively + nreverse RPLACA(reverse A,t) + +destructT(functor)== + -- provides a list of booleans, which indicate whether the arguments + -- to the functor are category forms or not + GETDATABASE(opOf functor,'COSIG) + +constructTowerT(t,TL) == + -- t is a type, TL a list of constructors and argument lists + -- t is embedded into TL + while TL and t repeat + [c,arg,:TL] := TL + t0 := constructM(c,replaceLast(arg,t)) + t := canCoerceFrom(t,t0) and t0 + t + +bubbleType(TL) == + -- tries to move the last constructor in TL upwards + -- uses canCoerceFrom to test whether two constructors can be bubbled + [c1,arg1,:T1] := TL + null T1 or null arg1 => TL + [c2,arg2,:T2] := T1 + t := last arg1 + t2 := constructM(c2,replaceLast(arg2,t)) + arg1 := replaceLast(arg1,t2) + newCanCoerceCommute(c2,c1) or canCoerceCommute(c2, c1) => + bubbleType [c1,arg1,:T2] + TL + +bubbleConstructor(TL) == + -- TL is a nonempty list of type constructors and nonempty argument + -- lists representing a deconstructed type + -- then the lowest constructor is bubbled to the top + [c,arg,:T1] := TL + t := last arg + until null T1 repeat + [c1,arg1,:T1] := T1 + arg1 := replaceLast(arg1,t) + t := constructT(c1,arg1) + constructT(c,replaceLast(arg,t)) + +compareTT(t1,t2) == + -- 'T if type t1 is more nested than t2 + -- otherwise 'T if t1 is lexicographically greater than t2 + EQCAR(t1,$QuotientField) or + MEMQ(opOf t2,[$QuotientField, 'SimpleAlgebraicExtension]) => NIL + CGREATERP(PRIN2CVEC opOf t1,PRIN2CVEC opOf t2) + +@ +\eject +\begin{thebibliography}{99} +\bibitem{1} nothing +\end{thebibliography} +\end{document} -- cgit v1.2.3