-- 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.


import '"i-object"
)package "BOOT"

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 getDualSignatureFromDB first t ]

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 := getConstructorCategoryFromDB t
  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 (getConstructorKindFromDB catName = "category") =>
    cat in CDR seen => conditions
    RPLACD(seen,[cat,:CDR seen])
    subCat := getConstructorCategoryFromDB catName
    -- 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 (op := first t) and IDENTP op and constructor? op =>
    dt := destructT op
    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
  getDualSignatureFromDB opOf functor

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)