% Analyser support code %

%AM: internal variables ...%
let AnalTopEnv = ref (inl ()) : (void + TopAllEnv') ref;

let AnalFudgeType = ref (inl ()): (void +
       (| Star: TypTerm' -> TypTerm'; Bool: TypTerm';
          Int: TypTerm'; Real: TypTerm'; String: TypTerm';
          Dynamic: TypTerm'; Xn: TypTerm'
       |) ) ref;
let SysTypes() = outr(!AnalFudgeType);
let AnalFudgeFns = ref ([]: (
  (object#(object->void)list -> void) # (SMCode' list list -> SMCode' list)
                            ) list);
let AnalysisLevel = ref 0;

%%
% These unsophisticated environments are used by InstOf and NewType.
  Eventually, a general abstract type of environments is needed, and all
  local environments maintained by the analyser should be made instances
  of that type. %

let type ('a,'b) Env = (| Var: 'a; Binding: 'b |) list;

let EmptyEnv: ('a,'b) Env = nil;

let rec Bound( Eq:'a#'b->bool )( x:'a, Env:('b,'c) Env ): bool =
    if null( Env ) then false
    else if Eq( x, hd( Env ).Var ) then true
    else Bound( Eq )( x, tl( Env ) );

let rec Binding( Eq:'a#'a->bool )( x:'a, Env:('a,'b) Env ): 'b =
    if null( Env ) then failwith `Binding`
    else if Eq( x, hd( Env ).Var ) then hd( Env ). Binding
    else Binding( Eq )( x, tl( Env ) );

let rec Bind'( x:'a, v:'b, Env:('a,'b) Env ref ): unit =
    Env := (| Var=x; Binding=v |) :: !Env;

let rec New( Eq:'a#'a->bool, NewCopy:'a->'a )( x:'a, Env:('a,'a) Env ref ): 'a =
    if Bound( Eq )( x, !Env ) then
       Binding( Eq )( x, !Env )
    else
       let x' = NewCopy( x )
       in  ( Bind'( x, x', Env ); x' );
%%
% Timestamps %
let time = ref 0
ins { NewInt(): int = (time := !time + 1; !time) }

enc {

    GenFixedStamp(): TimeStamp' = absTimeStamp'([| Fixed=NewInt() |])

and GenStampVar(): TimeStamp' =
    absTimeStamp'[| Var=(| Stamp=NewInt(); Instance=ref[|absent|] |) |] }

enc { rec PruneStamp( stamp: TimeStamp' ): TimeStamp' =
    varcase repTimeStamp' stamp of
    [| Fixed. stamp;
       Var=(| Stamp; Instance |).
	 if (!Instance) is present then
	    let x = PruneStamp( (!Instance) as present )
	    in  ( Instance := [| present=x |]; x )
	  else stamp
    |] }

enc PrintTimeStamp( stamp: TimeStamp' ): unit =
    ( outtok(`<`);
      varcase repTimeStamp'(PruneStamp(stamp)) of
      [| Fixed=t. printint(t);
	 Var=v. ( outtok(`*`); printint(v.Stamp) )
      |];
      outtok(`>`) )

enc EqTimeStamps( stamp:TimeStamp', stamp':TimeStamp' ): bool =
    let st = PruneStamp( stamp ) and st' = PruneStamp( stamp' )
    in  varcase repTimeStamp'(st) of
	[| Fixed=t. varcase repTimeStamp'(st') of
		    [| Fixed=t'. t=t'; Var. false |];
	   Var=v. varcase repTimeStamp'(st') of
		  [| Fixed. false;
		     Var=v'. (v.Stamp)=(v'.Stamp) |] |]

enc TimeStampToInt( stamp: TimeStamp' ): int =
    varcase repTimeStamp'(PruneStamp(stamp)) of
    [| Fixed=t. t;
       Var=v. v.Stamp
    |]

enc NewStamp( stamp: TimeStamp' ): TimeStamp' =
    let RS = repTimeStamp'(PruneStamp(stamp))
    in  varcase RS of
	[| Fixed=i. stamp;
	   Var=v. GenStampVar()
	|]

%
enc rec IdentifyStamps( s1: TimeStamp', s2: TimeStamp', err ): unit =
    let s1' = PruneStamp(s1)
    and s2' = PruneStamp(s2)
    in	varcase repTimeStamp' s1' of
	[| Fixed=t1. varcase repTimeStamp' s2' of
		     [| Fixed=t2. if t1=t2 then () else err();
			Var=v2. v2.Instance := [| present=s1' |] |];
	   Var=v1.   varcase repTimeStamp' s2' of
		     [| Fixed=t2. v1.Instance := [| present=s2' |];
			Var=v2. if (v1.Stamp)<>(v2.Stamp) then
				   v1.Instance := [| present=s2' |]
				else ()
		     |]
	|]
%
enc rec IdentifyStamps( s1: TimeStamp', s2: TimeStamp', err ): unit =
    let s1' = PruneStamp(s1)
    and s2' = PruneStamp(s2)
    in	if EQPTR(s1',s2') then ()
        else varcase repTimeStamp' s1' of
	[| Fixed=t1. err();
	   Var=v1.   v1.Instance := [| present=s2' |]
	|]

enc TopLevelTimeStamp = absTimeStamp'[| Fixed = ~1 |] ;

%%
% Handles %
let EqHandle( H1: Handle', H2: Handle' ): bool =
    EqTimeStamps( (repHandle' H1).Stamp, (repHandle' H2).Stamp )

and IdentifyHandles( H1: Handle', H2: Handle', err ): unit =
    IdentifyStamps( repHandle'(H1).Stamp, repHandle'(H2).Stamp, err )

and HandleToInt( H: Handle' ): int = TimeStampToInt(repHandle'(H).Stamp)

and NameOfHandle( H: Handle' ): Atom' = !(repHandle'(H).AtomicName)

and StampOfHandle( H: Handle' ): TimeStamp' =  PruneStamp( repHandle'(H).Stamp )

and SetAtomicName( H: Handle', A: Atom' ): unit =
    repHandle'(H).AtomicName := A

and PrintAtomicName( H: Handle' ): unit =
    ( PrintAtom( !(repHandle'(H).AtomicName) );
      if !Debug.TimeStamps then PrintTimeStamp( repHandle'(H).Stamp ) else () )

and AllocHandle( Ide: Atom', Stamp: TimeStamp' ): Handle' =
    absHandle'(| Stamp=Stamp; AtomicName=ref(Ide) |);

%%
let rec EqList(eq: ('a # 'a) -> bool, l: 'a list, m: 'a list): bool =
  if null(l) then null(m)
  else if null(m) then false
  else if eq(hd l,hd m) then EqList(eq,tl l,tl m) else false;

% Treat the pair of lists l and r as determining a list of pairs, and
  apply f to successive pairs %
let rec pairapp(f:'a#'b->unit,err,l:'a list,r:'b list):unit =
    if null(l) And null(r) then ()
    else if null(l) Or null(r) then err()
    else ( f(hd(l),hd(r)); pairapp(f,err,tl(l),tl(r)) );

let type QQQTagList' = [|Flexi: TypTagDList'; Solid: TypTagList';
                         TagInstance: TypTerm'|];

%%
%{  -----  TYPE ALLOCATOR  -----  }%
let BuildTypConVar( Handle: Handle', Args: TypArgs', Instance: TypTerm' opt ref ): TypTerm' =
    absTypTerm'[| TypConVar=
	(| ConVarHandle=Handle; ConVarArgs=Args; Instance=Instance |) |];

let AllocTypConVarByHandle( Handle: Handle', Args: TypArgs' ): TypTerm' =
    BuildTypConVar( Handle, Args, ref[|absent|] );

let GenTypConVar( Ide: Atom', Args: TypArgs' ): TypTerm' =
    AllocTypConVarByHandle( AllocHandle( Ide, GenStampVar() ), Args );

let AllocTypDefOperByHandle( Handle: Handle', Guarded: LoopCheck' ref,
                             Args: TypArgs', Body: TypTerm' ): TypTerm' =
    absTypTerm'[| TypDefOper = (| Guarded = Guarded; DefHandle=Handle; 
                                  DefArgs=Args; DefBody=Body |) |];

let AllocTypDefOper(Stamp: TimeStamp', Ide: Atom',
		    Args: TypArgs', Body: TypTerm'): TypTerm' =
    AllocTypDefOperByHandle( AllocHandle( Ide, Stamp ), 
                             ref [|Unknown|], Args, Body );

let GenFixedTypDefOper( Ide: Atom', Args: TypArgs', Body: TypTerm' ): TypTerm' =
    AllocTypDefOper( GenFixedStamp(), Ide, Args, Body );

let GenFlexTypDefOper( Ide: Atom', Args: TypArgs', Body: TypTerm' ): TypTerm' =
    AllocTypDefOper( GenStampVar(), Ide, Args, Body );

let AllocTypAbsInfo( Handle: Handle', Cons, AbsEqFn, AbsPrintFn ): AbsInfo' =
    (| AbsHandle=Handle; AbsCons=ref(Cons); AbsEqFn=ref(AbsEqFn);
       AbsPrintFn=ref(AbsPrintFn); EqDefined = ref [|Unknown|]; Extensible = ref 0 |);

let BuildTypAbsOper( AbsInfo: AbsInfo', AbsArgs: TypArgs' ): TypTerm' =
    absTypTerm'[| TypAbsOper= (| AbsArgs=AbsArgs; AbsInfo=AbsInfo |) |];

let AllocTypAbsOperByHandle( Handle: Handle', Args: TypArgs', EqFn, PrintFn ): TypTerm' =
    BuildTypAbsOper( AllocTypAbsInfo( Handle, [], EqFn, PrintFn ), Args );

let AllocTypAbsOper(Stamp: TimeStamp', AbsIde: Atom',
		    AbsArgs: TypArgs', AbsEqFn, AbsPrintFn): TypTerm' =
    AllocTypAbsOperByHandle( AllocHandle( AbsIde, Stamp ),
			   AbsArgs, AbsEqFn, AbsPrintFn );

let ReAllocTypAbsOper((|AbsArgs=_;AbsInfo|), NewArgs): TypTerm' =
    BuildTypAbsOper( AbsInfo, NewArgs );

let EqualADT(x: SMCode' list list): SMCode' list = failwith `CompEqualADT`;

let SetupEqFn t f = (repTypTerm' t as TypAbsOper.AbsInfo.AbsEqFn) := f;

let GenFixedTypAbsOper(AbsIde: Atom', AbsArgs: TypArgs'): TypTerm' =
  let (AbsPrintFn,AbsEqFn) =
    (let x = hd(!AnalFudgeFns) in (
     AnalFudgeFns := tl(!AnalFudgeFns);
     x)) ?? [`Hd`] (InitPrintFns.ADT,EqualADT) in
  AllocTypAbsOper(GenFixedStamp(),AbsIde,AbsArgs,AbsEqFn,AbsPrintFn);

let GenFlexTypAbsOper(AbsIde: Atom', AbsArgs: TypArgs' ): TypTerm' =
  AllocTypAbsOper(GenStampVar(),AbsIde,AbsArgs,EqualADT,InitPrintFns.ADT);

let AllocTypTagOper(TagSort: [|Record; Variant|], TagList: QQQTagList')
                   : TypTerm' =
  absTypTerm'[| TypTagOper= (| TagSort; TagList=ref TagList |) |];

let AllocTypTagList(Tag: Atom', Typ: TypTerm', Ttl: TypTagList'): TypTagList'
= (| Tag; Typ |) :: Ttl;

let AllocTypTagDList(Tag: Atom', Typ: TypTerm', Ttl: TypTagDList'): TypTagDList'
= dcons( (| Tag; Typ |), Ttl);

let AllocTypRecord(TagList: QQQTagList'): TypTerm'
=   AllocTypTagOper([|Record|],TagList);

let AllocTypVariant(TagList: QQQTagList'): TypTerm'
=   AllocTypTagOper([|Variant|],TagList);

let dummyTypTerm =
    AllocTypAbsOper(GenFixedStamp(),dummyAtom,[],EqualADT,InitPrintFns.ADT);

%%
% type variables %

let AllocTypVar(VarStamp: int, Generic: bool, Weak: bool, EtyVar: bool,
                OccurLevel: int, Instantiable: bool, Toplevel: bool): TypTerm'=
  let OL = if Generic then MaxInt else OccurLevel
  and I = if Generic then true else Instantiable
  in
    absTypTerm'[| TypVar=
       (| VarStamp=VarStamp; Instance= ref [|None|]; Toplevel=Toplevel;
          Generic= ref Generic; Weak=ref Weak; OccurLevel=ref OL;
	  Instantiable = ref I; Ety = ref EtyVar;
          TypVarCopy = ref dummyTypTerm;    %AM: random init value: never used%
	  CopyCounter = ref 0
       |)
    |];

let GenTypVar(Generic: bool, Weak: bool, Ety: bool, OccurLevel: int, 
              Instantiable: bool): TypTerm'
=   AllocTypVar(NewInt(),Generic,Weak,Ety,OccurLevel,Instantiable,false);

let GenTopTypVar(Weak: bool,Ety: bool): TypTerm'
=   AllocTypVar(NewInt(),true,Weak,Ety,MaxInt,true,true);

let EqTypVar(x,y) =
( let x,y = repTypTerm'(x),repTypTerm'(y) in
  if x is TypVar And y is TypVar then
     (x as TypVar).VarStamp = (y as TypVar).VarStamp
  else false );

% This is a hack: ConVarInstance uses code that uses Prune. %
let ConVarInstance = ref(\x.failwith `ConVarInstance`): (TypTerm'->TypTerm') ref;

let rec Prune(Typ: TypTerm'): TypTerm' =
  varcase repTypTerm' Typ of
  [| TypVar=x.
      varcase !(x.Instance) of
      [| None. Typ;
         Yes=i.
           ( let y = Prune(i) in
              (x.Instance := [| Yes=y |]; y))
      |];
    TypConVar=x.
	varcase !(x.Instance) of
	[| absent. Typ;
	   present=i. Prune((!ConVarInstance)(Typ))
	|];
    TypDefOper. Typ;
    TypAbsOper. Typ;
    TypTagOper=x.
      varcase !(x.TagList) of
      [| TagInstance=i.
           ( let y = Prune(i) in
              (x.TagList := [| TagInstance=y |]; y));
         Flexi. Typ;
         Solid. Typ
      |]
  |];

% FullPrune is prune, but also replaces uses of TypDefOper's by their
  definitions. %
let rec FullPrune(Typ: TypTerm'): TypTerm' =
  let x = Prune(Typ) in
    if repTypTerm'(x) is TypDefOper
      then FullPrune((repTypTerm'(x) as TypDefOper).DefBody)
      else x;

let PruneEqType(Typ: TypTerm'): TypTerm' = FullPrune(Typ);

let appTypTermVars(f: TypTerm' -> void, Typ: TypTerm'): void =
( let rec app1(Typ) =
    varcase repTypTerm' Typ of
    [| TypVar=x.
        varcase !(x.Instance) of
        [| None. f(Typ);
           Yes=i. app1(i)
        |];
      TypConVar=x.
	aplist( app1, x.ConVarArgs );
      TypDefOper=x.
          aplist(app1, x.DefArgs);
      TypAbsOper=x.
          aplist(app1, x.AbsArgs);
      TypTagOper=x.
        varcase !(x.TagList) of
        [| TagInstance=i. app1(i);
           Flexi=y. daplist(app2,y);
           Solid=y. aplist(app2,y)
        |]
    |]
  and app2(x: TagTypTerm') = app1(x.Typ)
  in app1(Typ));


let appEqTypTermVars(f: bool -> (TypTerm' -> void), eqerr: TypTerm' -> void,
                     Typ: TypTerm'): void =
( let f' = f true
  enc rec app1(Typ) = let Typ' = FullPrune(Typ) in
    varcase repTypTerm' Typ' of
    [| TypVar=x.
        varcase !(x.Instance) of
        [| None. f'(Typ);
           Yes=i. app1(i)
        |];
      TypConVar=x.
	aplist( app1, x.ConVarArgs );
      TypDefOper=x. % Should never happen %
          aplist(app1, x.DefArgs);
      TypAbsOper=x.
          % Should really use time stamps eventually %
          if (!x.AbsInfo.EqDefined) is No then eqerr(Typ)
          else let name = NameOfHandle(x.AbsInfo.AbsHandle) in 
          if EqAtom(name, AtomInt) Or EqAtom(name, AtomFloat)
             Or EqAtom(name, AtomString) then ()
          else if EqAtom(name, AtomCross)
               then aplist(app1, x.AbsArgs)
          else if EqAtom(name, AtomRef) Or EqAtom(name, AtomArray)
               then appTypTermVars((f false), Typ)
          else if EqAtom(name, AtomArrow)
               Or null(!(x.AbsInfo.AbsCons)) then eqerr(Typ) 
          else (
            if (!x.AbsInfo.EqDefined) is Yes then ()
            else
              (x.AbsInfo.EqDefined := [|Yes|];
               aplist((\y:(|VarName:SynBindIde'; VarType: TypTerm'|).
                       if (repTypTerm'(y.VarType)) is TypAbsOper
                       then let t = (repTypTerm'(y.VarType)) as TypAbsOper in
                         if EqAtom(NameOfHandle(t.AbsInfo.AbsHandle),AtomArrow)
                         then app1(hd(t.AbsArgs))
                         else ()
                       else app1(y.VarType)),
                   !(x.AbsInfo.AbsCons)))
              ?? [`Reenter`] (x.AbsInfo.EqDefined := [|No|]; ReEnter());
               
            aplist((\t.appTypTermVars((f false),t)), x.AbsArgs));
           
      TypTagOper=x.
        varcase !(x.TagList) of
        [| TagInstance=i. app1(i);
           Flexi=y. daplist(app2,y);
           Solid=y. aplist(app2,y)
        |]
    |]
  and app2(x: TagTypTerm') = app1(x.Typ)
  in app1(Typ));

%%
% built-in types %

let TypTupleTimeStamp=GenFixedStamp()
ins {

    TypTupleHandle = AllocHandle( AtomCross, TypTupleTimeStamp )

and TypUnitHandle = AllocHandle( AtomUnit, TypTupleTimeStamp )

enc IsTupleType(Typ) =
	let y = repTypTerm'(FullPrune Typ)
	in  if y is TypAbsOper
	    then EqHandle((y as TypAbsOper).AbsInfo.AbsHandle, TypTupleHandle )
	    else false

and { y = AllocTypAbsInfo( TypTupleHandle, [], EqualADT, InitPrintFns.Tuple )
      ins AllocTypTuple(x:TypTerm' list): TypTerm' =
	     BuildTypAbsOper(y,x) }

enc AllocTypUnit = AllocTypTuple[]

and IsTrivType(Typ) =
    if IsTupleType(Typ) then
	let y = repTypTerm'(FullPrune Typ)
	in  null( (y as TypAbsOper).AbsArgs )
    else false;

};

let TypFunTimeStamp=GenFixedStamp()
ins {

    TypFunHandle = AllocHandle( AtomArrow, TypFunTimeStamp )

enc IsFunType(Typ) =
	let y = repTypTerm'(FullPrune Typ)
	in  if (y is TypAbsOper)
	    then EqHandle( (y as TypAbsOper).AbsInfo.AbsHandle, TypFunHandle )
	    else false

and { y = AllocTypAbsInfo( TypFunHandle, [], EqualADT, InitPrintFns.Fun )
      ins AllocTypFun(NewDom,NewCod) =
	     BuildTypAbsOper(y,[NewDom;NewCod]) }
};

% This is a KLUDGE.  List must be made primitive, like tuples and functions. %
% NO - a way of allowing the user to extend the function used to print 
  objects should be provided, and then IsListType would not be required. %

let IsListType( Handle ): bool = EqAtom( NameOfHandle( Handle ), AtomList );

%%
let type NewTypVarEnv' = (TypTerm',TypTerm') Env
and      NewHandleEnv' = (Handle',Handle') Env
and      NewAbsTypEnv' = (AbsInfo',AbsInfo') Env
and      ConVarInfo' = (| Handle: Handle'; Instance: TypTerm' opt ref |)
enc type NewConVarEnv' = (ConVarInfo',ConVarInfo') Env;

% Invariant: ParentOfHandle(H) is in NHE %
let rec NewHandle( H: Handle', NHE: NewHandleEnv' ref ): Handle' =
    let FreshHandle( H: Handle' ): Handle' =
        AllocHandle( NameOfHandle(H), NewStamp( StampOfHandle(H) ))
    in  New( EqHandle, FreshHandle )( H, NHE );

let rec NewType( Typ: TypTerm', NHE, NTVE, NATE, NCVE ): TypTerm' =

    let LocalNewType( Typ: TypTerm' ): TypTerm' =
        NewType( Typ, NHE, NTVE, NATE, NCVE )

    enc rec NewTypVar( T: TypTerm' ): TypTerm' =
	let FreshTypVar( T: TypTerm' ): TypTerm' =
	    let RT = repTypTerm'(T) as TypVar
	    in  GenTypVar( true, !RT.Weak, !RT.Ety, MaxInt, true )
        in  New( EqTypVar, FreshTypVar )( T, NTVE )

    and NewTypDefOper( Typ: TypTerm', NewArgs: TypArgs', NewBody: TypTerm' ): TypTerm' =
        let RT = (repTypTerm' Typ) as TypDefOper
        in  AllocTypDefOperByHandle( NewHandle( RT.DefHandle, NHE ), 
                                     RT.Guarded, NewArgs, NewBody )

   and NewTypAbsOper( Typ: TypTerm', NewArgs: TypArgs' ): TypTerm' =
       let EqAbsInfo( I1: AbsInfo', I2: AbsInfo' ): bool =
	      EqHandle( I1.AbsHandle, I2.AbsHandle )
       and FreshAbsInfo( I: AbsInfo' ): AbsInfo' =
	      AllocTypAbsInfo( NewHandle( I.AbsHandle, NHE ), !I.AbsCons, !I.AbsEqFn, !I.AbsPrintFn )
       in  let RT = (repTypTerm' Typ) as TypAbsOper
	   enc NewInfo = New( EqAbsInfo, FreshAbsInfo )( RT.AbsInfo, NATE )
	   in  BuildTypAbsOper( NewInfo, NewArgs )

    and NewTypConVar( Typ: TypTerm', NewArgs: TypArgs' ): TypTerm' =
        let EqConVarInfo( I1: ConVarInfo', I2: ConVarInfo' ): bool =
            EqHandle( I1.Handle, I2.Handle )
        and FreshConVarInfo( I: ConVarInfo' ): ConVarInfo' =
	    let NewInstance: TypTerm' opt =
	        if (!I.Instance) is present then
	  	   [| present= LocalNewType((!I.Instance) as present) |]
	        else
		   [| absent |]
	    in  (| Handle= NewHandle( I.Handle, NHE ); Instance= ref( NewInstance ) |)
        in  let RT = (repTypTerm' Typ) as TypConVar
	    enc NewInfo = New( EqConVarInfo, FreshConVarInfo )
			     ( (| Handle=RT.ConVarHandle;Instance=RT.Instance |), NCVE )
	    in  BuildTypConVar( NewInfo.Handle, NewArgs, NewInfo.Instance )

    and NewArgs( ArgList: TypArgs' ): TypArgs' =
	map( LocalNewType )( ArgList )

    and rec NewTagDList( TagList: TagTypTerm' dlist ): TagTypTerm' dlist =
	if dnull( TagList ) then dnil
	else AllocTypTagDList( dhd(TagList).Tag,
		LocalNewType(dhd(TagList).Typ),
    		NewTagDList(dtl(TagList)) )

    and rec NewTagList( TagList: TagTypTerm' list ): TagTypTerm' list =
	if null( TagList ) then nil
	else AllocTypTagList( hd(TagList).Tag,
		LocalNewType(hd(TagList).Typ),
		NewTagList(tl(TagList)) )
    in

    varcase repTypTerm' Typ of
    [| TypVar=x.
	varcase !(x.Instance) of
	[| Yes=i. LocalNewType(i);
	   None.  if !(x.Generic) then NewTypVar( Typ ) else Typ
	|];
       TypConVar=x.
	NewTypConVar( Typ, NewArgs( x.ConVarArgs ) );
       TypDefOper=x.
	NewTypDefOper( Typ, NewArgs( x.DefArgs ), LocalNewType( x.DefBody ) );
       TypAbsOper=x.
	NewTypAbsOper( Typ, NewArgs( x.AbsArgs ) );
       TypTagOper=x.
        varcase !x.TagList of
	[| TagInstance=i. LocalNewType( i );
	   Flexi=y. AllocTypTagOper( x.TagSort, [| Flexi=NewTagDList(y) |] );
	   Solid=y. AllocTypTagOper( x.TagSort, [| Solid=NewTagList(y) |] )
	|]
    |];
%%
%{  -----  Hash-CONSing type copier  -----  }%

%AM: FreshType copies a type and substitutes new variables for generic ones.
     It marks them as non-generic which can be undone by FlagGenericVars.
     TidyType copies a type for top level use, sharing as much structure
     as possible %

let TypeCopyCounter = ref 0
and GenericInstance = ref true;

%AM: routines to enable freshtype to share more type structure... %
let rec { 

QCONS(x, h, t) =
  if EQPTR(hd(x),h) And EQPTR(tl(x),t) then x else h::t

and QAllocTypTagList(Old: TypTagList',
                     Typ: TypTerm', Ttl: TypTagList'): TypTagList' =
  if EQPTR(Typ, hd(Old).Typ) And EQPTR(Ttl, tl(Old)) then Old
  else AllocTypTagList(hd(Old).Tag, Typ, Ttl)

and QAllocTypConVar( Typ: TypTerm', ConVarArgs: TypArgs' ): TypTerm' =
    let x = repTypTerm' Typ as TypConVar
    in  if EQPTR( ConVarArgs, x.ConVarArgs ) then Typ
	else BuildTypConVar( x.ConVarHandle, ConVarArgs, x.Instance )

and QAllocTypAbsOper(Typ: TypTerm', AbsArgs: TypArgs'): TypTerm' =
    let x = repTypTerm' Typ as TypAbsOper
    in  if EQPTR( AbsArgs, x.AbsArgs ) then Typ
	else ReAllocTypAbsOper( x, AbsArgs )

and QAllocTypDefOper(Typ: TypTerm', DefArgs: TypArgs', DefBody: TypTerm'): TypTerm' =
    let x = repTypTerm' Typ as TypDefOper
    in  if EQPTR( DefArgs, x.DefArgs ) And EQPTR( DefBody, x.DefBody ) then Typ
	else AllocTypDefOperByHandle( x.DefHandle, x.Guarded, DefArgs, DefBody )

and QAllocTypSolidTagOper(Typ: TypTerm', TagList: TypTagList'): TypTerm' =
  let x = repTypTerm' Typ as TypTagOper in
  if EQPTR(TagList, (!x.TagList) as Solid) then Typ
  else AllocTypTagOper(x.TagSort, [|Solid=TagList|])

and CopyType (Typ: TypTerm'): TypTerm' =
    varcase repTypTerm' Typ of
    [| TypVar=x.
        varcase !(x.Instance) of
        [| Yes=i. CopyType(i);
	   None. if !(x.Generic) then
	   	    if !GenericInstance then
		       if !x.CopyCounter = !TypeCopyCounter then !x.TypVarCopy
		       else ( x.CopyCounter := !TypeCopyCounter;
			      x.TypVarCopy := GenTypVar(false,!x.Weak,!x.Ety,
                                                        !x.OccurLevel,true);
			      !x.TypVarCopy )
		    else Typ
		 else Typ
	|];
      TypConVar=x.
        QAllocTypConVar( Typ, CopyArgs( x.ConVarArgs ) );
      TypDefOper=x.
        QAllocTypDefOper(Typ,CopyArgs(x.DefArgs),CopyType(x.DefBody));
      TypAbsOper=x.
        QAllocTypAbsOper(Typ,CopyArgs(x.AbsArgs));
      TypTagOper=x.
        varcase !(x.TagList) of
        [| TagInstance=i. CopyType(i);
           Flexi=y. AllocTypTagOper(x.TagSort, [|Flexi=CopyTagDList(y)|]);
           Solid=y. QAllocTypSolidTagOper(Typ, CopyTagList(y))
        |]
    |]

  and CopyArgs(Args: TypArgs'): TypArgs' =
    if null(Args) then []
    else QCONS(Args, CopyType(hd(Args)), CopyArgs(tl(Args)))

  and CopyTagList(TagList: TagTypTerm' list): TagTypTerm' list =
    if null(TagList) then []
    else QAllocTypTagList(TagList, CopyType(hd(TagList).Typ),
                                   CopyTagList(tl TagList))

  and CopyTagDList(TagList: TagTypTerm' dlist): TagTypTerm' dlist =
    if dnull(TagList) then dnil
    else AllocTypTagDList(dhd(TagList).Tag, CopyType(dhd(TagList).Typ),
                                            CopyTagDList(dtl TagList))
}

ins FreshType(Typ: TypTerm'): TypTerm' =
( TypeCopyCounter := NewInt();
  GenericInstance := true;
  CopyType(Typ) )

and ApproxTidyType(Typ: TypTerm', TypDefn: bool): TypTerm' =
( GenericInstance := false;
  CopyType(Typ) ) ;

%%
let type InstEnv' = (TypTerm', TypTerm') Env;

%RH: both EqType and InstOf assume that record types are Solid. Is there a
 need to compare Flexi records?  What would the definition be?%

let {

rec EqType(Typ1: TypTerm', Typ2: TypTerm'): bool =
  let { Typ1 = FullPrune(Typ1) enc RepTyp1 = repTypTerm' Typ1 }
  and { Typ2 = FullPrune(Typ2) enc RepTyp2 = repTypTerm' Typ2 } in
  if RepTyp1 is TypVar then EqTypVar(Typ1,Typ2)
  else if RepTyp1 is TypConVar And RepTyp2 is TypConVar then
          let x1 = RepTyp1 as TypConVar and x2 = RepTyp2 as TypConVar
	  in  if EqHandle(x1.ConVarHandle,x2.ConVarHandle) then
		 EqList( EqType, x1.ConVarArgs, x2.ConVarArgs )
	      else false
  else if RepTyp1 is TypAbsOper And RepTyp2 is TypAbsOper
  then let x1 = RepTyp1 as TypAbsOper
       and x2 = RepTyp2 as TypAbsOper in
       if EqHandle(x1.AbsInfo.AbsHandle,x2.AbsInfo.AbsHandle)
       then EqList(EqType, x1.AbsArgs, x2.AbsArgs)
       else false
  else if RepTyp1 is TypTagOper And RepTyp2 is TypTagOper
  then  let x1 = RepTyp1 as TypTagOper
	and x2 = RepTyp2 as TypTagOper
	in  if (!x1.TagList) is Solid And (!x2.TagList) is Solid then
		let f(tt:TagTypTerm'):TypTerm' = tt.Typ
		in  EqList(EqType, map(f)((!x1.TagList) as Solid),
				map(f)((!x2.TagList) as Solid))
	    else false
  else false

enc rec InstOf(Typ1: TypTerm', Typ2: TypTerm', Env: InstEnv' ref): bool =
    let Typ1=FullPrune(Typ1) and Typ2=FullPrune(Typ2) in
    varcase repTypTerm' Typ1 of
    [| TypVar=x.
        varcase !(x.Instance) of
        [| Yes=i. failwith `InstOf`;
           None. if !(x.Generic) then
		    if Bound( EqTypVar )( Typ1, !Env ) then
		       EqType( Binding( EqTypVar )( Typ1, !Env ), Typ2 )
		    else
		       ( Bind'( Typ1, Typ2, Env ); true )
                 else if (repTypTerm' Typ1) is TypVar then
		    EqTypVar( Typ1, Typ2 )
		 else
		    false
        |];
      TypConVar=x1.
        let Typ2 = repTypTerm' Typ2
	in  if Typ2 is TypConVar then
	       let x2 = Typ2 as TypConVar
	       in  if EqHandle(x1.ConVarHandle,x2.ConVarHandle) then
		      EqList((\ (t1,t2).InstOf(t1,t2,Env)),
		             x1.ConVarArgs, x2.ConVarArgs)
		   else false
	    else false;
      TypDefOper. failwith `InstOf`;
      TypAbsOper=x1.
        let Typ2 = repTypTerm' Typ2 in
        if Typ2 is TypAbsOper
        then let x2 = Typ2 as TypAbsOper in
             if EqHandle(x1.AbsInfo.AbsHandle,x2.AbsInfo.AbsHandle)
             then EqList((\ (t1,t2).InstOf(t1,t2,Env)), x1.AbsArgs, x2.AbsArgs)
             else false
        else false;
      TypTagOper=x1.
	let Typ2 = repTypTerm' Typ2
	in  if Typ2 is TypTagOper then
		if ((!(Typ2 as TypTagOper).TagList) is Solid) And ((!x1.TagList) is Solid) then
		   let f(tt:TagTypTerm'):TypTerm' = tt.Typ
		   in EqList( (\ (t1,t2).InstOf(t1,t2,Env)),
		             map(f)((!x1.TagList) as Solid),
			     map(f)((!(Typ2 as TypTagOper).TagList) as Solid) )
		else false
	    else false
    |]

    }

ins {

%AM: InstanceOf tests whether Typ2 is an instance of Typ1%
InstanceOf(Typ1: TypTerm', Typ2: TypTerm'): bool =
    InstOf( Typ1, Typ2, ref [] )

and EqualType( Typ1, Typ2 ): bool =
    EqType( Typ1, Typ2 )

    };

% Hack for mlenv %
InstOf := InstanceOf;

%%
% 'Hashing' functions, using rather primitive lists of previous conses...%
let memohashsize = 1007;
let AddToMemo(memo: 'a list ref, elt: 'a) =
  (memo := append(!memo,[elt]);
   elt)
and Memo_CONS = ArrayOfFn(memohashsize, \n.ref ([]: TypArgs' list))
and Memo_TypTagList = ArrayOfFn(memohashsize, \n.ref ([]: TypTagList' list))
and Memo_TypVar = ref ([]: TypTerm' list)
and Memo_TypConVar = ref ([]: TypTerm' list)
and Memo_TypAbsOper = ArrayOfFn(memohashsize, \n.ref ([]: TypTerm' list))
and Memo_TypDefOper = ref ([]: TypTerm' list)
and Memo_TypTagOperRec = ref ([]: TypTerm' list)
and Memo_TypTagOperVar = ref ([]: TypTerm' list);

let HCONS((a:TypTerm', ah:int),
          (b:TypTerm' list, bh:int)): TypTerm' list # int =
  if ah<0 Or bh<0 then (a::b,~1) else
  let pos = (ah+2*bh) mod memohashsize
  enc memo = Memo_CONS sub (pos+1) in
  let rec find(l) = 
      if null(l) then AddToMemo(memo, a::b)
      else let x::m=l in
         if EQPTR(a, hd x) And EQPTR(b, tl x) then x
         else find(m)
  in (find(!memo), pos)

and HAllocTypTagList(Tag: Atom', (Typ: TypTerm', TypHash: int),
                     (Ttl: TypTagList', TlHash: int)): TypTagList' # int =
  if TypHash<0 Or TlHash<0 then (AllocTypTagList(Tag,Typ,Ttl), ~1) else
  let pos = (TypHash+2*TlHash) mod memohashsize
  enc memo = Memo_TypTagList sub (pos+1) in
  let rec find(l:TypTagList' list) = 
      if null(l) then AddToMemo(memo, AllocTypTagList(Tag, Typ, Ttl))
      else let x::m=l in
         if EqAtom(Tag, (hd x).Tag) And
            EQPTR(Typ, (hd x).Typ) And EQPTR(Ttl, tl x) then x
         else find(m)
  in (find(!memo), pos)

and HAllocTypConVar( ConVarHandle: Handle', (ConVarArgs: TypArgs', ArgHash: int) ): TypTerm' # int =
    if ArgHash<0 then
	( AllocTypConVarByHandle( ConVarHandle, ConVarArgs ), ~1 )
    else
	let pos = (17*HandleToInt(ConVarHandle)+ArgHash) mod memohashsize
	enc rec find(l) =
		if null(l) then
		   AddToMemo( Memo_TypConVar,
			      AllocTypConVarByHandle( ConVarHandle, ConVarArgs ) )
		else let t::m = l enc x = repTypTerm' t as TypConVar
		     in  if EQPTR( ConVarArgs, x.ConVarArgs ) And
		            EqHandle( ConVarHandle, x.ConVarHandle ) then t
			 else find(m)
	in  ( find(!Memo_TypConVar), pos )

and HAllocTypAbsOper(Typ: TypTerm', (AbsArgs: TypArgs', ArgHash: int))
                    :TypTerm' # int =
  let y = repTypTerm' Typ as TypAbsOper in
  if ArgHash<0 then (ReAllocTypAbsOper(y,AbsArgs),~1) else
  let pos = (17*HandleToInt(y.AbsInfo.AbsHandle)+ArgHash) mod memohashsize
  enc memo = Memo_TypAbsOper sub (pos+1) in
  let rec find(l) =
    if null(l) then AddToMemo(memo,
                        ReAllocTypAbsOper(y,AbsArgs))
    else let t::m=l enc x = repTypTerm' t as TypAbsOper in
    if EQPTR(AbsArgs, x.AbsArgs) And
       EqHandle(y.AbsInfo.AbsHandle,x.AbsInfo.AbsHandle)
    then t
    else find(m)
  in (find(!memo),pos)

and HAllocTypDefOper(DefHandle: Handle', Guarded: LoopCheck' ref,
                     (DefArgs: TypArgs', ArgHash: int),
                     (DefBody: TypTerm', BodyHash: int)): TypTerm' # int =
  if ArgHash<0 Or BodyHash<0
  then (AllocTypDefOperByHandle(DefHandle,Guarded,DefArgs,DefBody),~1) else
  let pos = (17*HandleToInt(DefHandle)+BodyHash+ArgHash) mod memohashsize in
  let rec find(l) =
    if null(l) then AddToMemo(Memo_TypDefOper,
                      AllocTypDefOperByHandle(DefHandle,Guarded,DefArgs,DefBody))
    else let t::m=l enc x = repTypTerm' t as TypDefOper in
       if EQPTR(DefArgs, x.DefArgs) And EQPTR(DefBody, x.DefBody) And
	  EqHandle(DefHandle,x.DefHandle)
       then t
       else find(m)
  in (find(!Memo_TypDefOper),pos)

and HAllocTypSolidTagOper(TagSort, (TagList: TypTagList', ArgHash: int))
                         : TypTerm' # int =
  if ArgHash<0 then (AllocTypTagOper(TagSort,[|Solid=TagList|]), ~1) else
  let memo = varcase TagSort of
  [|Record. Memo_TypTagOperRec; Variant. Memo_TypTagOperVar |] in
  let rec find(l) =
    if null(l) then AddToMemo(memo,
                              AllocTypTagOper(TagSort, [|Solid=TagList|]))
    else let t::m=l enc x = repTypTerm' t as TypTagOper in
       if EQPTR(TagList, (!x.TagList) as Solid) then t
       else find(m)
  in (find(!memo), ArgHash);

let DontUseTidy = ref false;

let unusedtoptypes = ref ([] : TypTerm' list)
enc NextTopTypVar(weak,ety) =
 ( let rec find(l: TypTerm' list) = if null(l)
      then let TVar = GenTopTypVar(weak,ety) in (
           Memo_TypVar := append(!Memo_TypVar,[TVar]);
           (TVar, []))
      else let x = repTypTerm'(hd l) as TypVar in
           if !x.Weak=weak And !x.Ety=ety then (hd l, tl l)
      else let (TVar, unused) = find(tl l) in
           (TVar, (hd l)::unused)
   enc (TVar, newunused) = find(!unusedtoptypes) in (
   unusedtoptypes := newunused;
   TVar))

ins rec { CopyType (Typ: TypTerm'): (TypTerm' # int) =
  varcase repTypTerm' Typ of
  [| TypVar=x.
       varcase !(x.Instance) of
       [| Yes=i. CopyType(i);
          None. if Not !(x.Generic) then (Typ,~1)
                else if x.Toplevel then (Typ,x.VarStamp)
                else let NewTyp = NextTopTypVar(!x.Weak,!x.Ety)
                     in (x.Instance := [|Yes=NewTyp|];
                         CopyType(NewTyp))
       |];
     TypConVar=x.
       varcase !(x.Instance) of
       [| present=i. CopyType((!ConVarInstance)(Typ));
          absent. HAllocTypConVar(x.ConVarHandle,CopyArgs(x.ConVarArgs))
       |];
     TypDefOper=x.
       HAllocTypDefOper(x.DefHandle,x.Guarded,CopyArgs(x.DefArgs),(x.DefBody,~1));
     TypAbsOper=x.
       HAllocTypAbsOper(Typ,CopyArgs(x.AbsArgs));
     TypTagOper=x.
       varcase !(x.TagList) of
       [| TagInstance=i. CopyType(i);
          Flexi=y. (AllocTypTagOper(x.TagSort,[|Flexi=CopyTagDList(y)|]), ~1);
          Solid=y. HAllocTypSolidTagOper(x.TagSort, CopyTagList(y))
       |]
  |]

  and CopyArgs(Args: TypArgs'): (TypArgs' # int) =
    if null(Args) then ([],0)
    else HCONS(CopyType(hd(Args)), CopyArgs(tl(Args)))

  and CopyTagList(TagList: TypTagList'): (TypTagList' # int) =
    if null(TagList) then ([],0)
    else HAllocTypTagList(hd(TagList).Tag, CopyType(hd(TagList).Typ),
                                           CopyTagList(tl TagList))

  and CopyTagDList(TagList: TypTagDList'): TypTagDList' =
    if dnull(TagList) then dnil
    else AllocTypTagDList(dhd(TagList).Tag, fst(CopyType(dhd(TagList).Typ)),
                                            CopyTagDList(dtl TagList))
  }

ins TidyType(Typ: TypTerm', TypDefn: bool): TypTerm' =
 if !DontUseTidy then Typ else
 ( unusedtoptypes := !Memo_TypVar;
   if TypDefn And (repTypTerm'(Typ) is TypDefOper)
   then let x = repTypTerm'(Typ) as TypDefOper in
     fst(HAllocTypDefOper(x.DefHandle,x.Guarded,CopyArgs(x.DefArgs),CopyType(x.DefBody)))
   else fst(CopyType(Typ)));

%AM: hack value and type environments to share as many types as possible%

let rec {TidyValEnv(Val:LocValEnv'): unit =
      aplist((\(q:LocEnvCell'). 
               (q.VarType := TidyType(!q.VarType,false);
                let refs = q.VarName.References in
                if !q.Hidden then () else refs := 100) ), 
             Val)

  and TidyTypEnv(Typ:LocTypEnv'): unit =
      aplist((\(q:LocTypEnvCell'). q.TypIde := TidyType(!q.TypIde,false)), 
             Typ)

};

% If DontUseTidy is now switched to false when processing structures etc,
  strange things happen !  - This needs to be looked at.... %

let TidyLocEnv(e: LocAllEnv'): LocAllEnv' =
  let (|Val; Typ; LastUse|) = e
   in (TidyTypEnv(Typ); TidyValEnv(Val); 
       DontUseTidy := true;
       DontUseTidy := false;
       e);

let rec ClearTypeVars(l) =
   if null l then () 
   else let x = repTypTerm'(hd l) as TypVar in
      (if !(x.Generic) then x.TypVarCopy := dummyTypTerm else ();
       ClearTypeVars(tl l));

let CopyFromTopEnv( topenv,
                    ValIdes, TypIdes ) =
   let newenv = CopyFromTopEnv( topenv,
                    ValIdes, TypIdes ) 
   enc _ = IterArray(Memo_CONS, \x.ref ([]: TypArgs' list))
   enc _ = IterArray(Memo_TypTagList, \x.ref ([]: TypTagList' list))
   enc _ = IterArray(Memo_TypAbsOper, \x.ref ([]: TypTerm' list))
   enc _ = ClearTypeVars(!Memo_TypVar)
   enc _ = Memo_TypVar := []
   enc _ = Memo_TypConVar := []
   enc _ = Memo_TypDefOper := []
   enc _ = Memo_TypTagOperRec := []
   enc _ = Memo_TypTagOperVar := []
   enc (| Val;Typ |) = newenv in
     (IterTopValEnv(Val: TopValEnv', (\(s,t,ob). Do(TidyType(t,false))));
      IterTopTypEnv(Typ: TopTypEnv', (\(a,t,b). Do(TidyType(t,false))));
%RJGDEL       IterTopExcEnv(Exc: TopExcEnv', (\(b,t). Do(TidyType(t,false))));%
      newenv  ) ;


%%
% Error handling %

let type Phrase' = [|
  Term:SynTerm'; CaseClause: SynTermCase';
  HandRule: SynHandRule';  Rule:SynRule';
  Decl:SynDecl'; Bind:SynBind';
  TypTerm:SynTypTerm' |];

let CurrentPhrase = ref( []: Phrase' list )
ins { {
    PushPhrase( phrase: Phrase' ): unit =
	CurrentPhrase := (phrase :: !CurrentPhrase)

and PopPhrase(): unit =
	CurrentPhrase := tl(!CurrentPhrase)

and ClearPhrase(): unit =
	CurrentPhrase := nil

and ShowErrorPhrase(phrase: Phrase'): void =
( varcase phrase of
  [| Term=x. SynTermPrint(x,5);
     CaseClause=x. SynTermCasePrint(x,5);
     HandRule=x. failwith `ShowErrorPhrase: handrule`;
     Rule=x. SynRulePrint(x,5);
     Decl=x. SynDeclPrint(x,5);
     Bind=x. SynBindPrint(x,5);
     TypTerm=x. SynTypTermPrint(x,5)
  |];
  PrintLn()
) }

enc ShowErrorContext() =
    if null(!CurrentPhrase) then
	outtok(`(syntactic context unknown)`)
    else
	ShowErrorPhrase(hd(!CurrentPhrase))

enc AnnounceError() =
    (outtok(`Type checking error in: `);
     ShowErrorContext(); PrintLn() )
};
%%
% Certain ``syntax'' errors can only be caught by the analyser. %
let SyntaxError(Msg: int) = 
  (outtok(`Syntax error in: `); ShowErrorContext(); PrintLn();
   if Msg=18 then outtok(`'ins' or an 'own' within a 'rec'`)
   else if Msg=19 then outtok(`non-function definition within a 'rec'`)
%  else if Msg=20
 then outtok(`'=' (not '<=>') within a 'rec' 'type'`) %
   else if Msg=22 then outtok(`There is a 'with' within a 'rec'`)
   else if Msg=23 then outtok(`'exception' is illegal within a 'rec'`)
   else if Msg=24 then outtok(`Non-atomic variable in pattern.`)
   else (outtok `unknown error `; printint(Msg));
   PrintLn(); ReEnter());

let UnboundVar(Ide: Atom') =
( AnnounceError();
  outtok(`Unbound value identifier: `);
  PrintAtom(Ide); PrintLn();
  ReEnter())

%RJGDEL and UnboundExcIde(Ide: Atom') =%
%RJGDEL ( AnnounceError();%
%RJGDEL   outtok(`Unbound exception identifier: `);%
%RJGDEL   PrintAtom(Ide); PrintLn();%
%RJGDEL   ReEnter())%

and UnboundConstructor(Ide: Atom') =
( AnnounceError();
  outtok(`Undefined value constructor: `);
  PrintAtom(Ide); PrintLn();
  ReEnter())

and DuplicatedVar(Ide: Atom') =
( AnnounceError();
  outtok(`Duplicated variable in pattern:  `);
  PrintAtom(Ide); PrintLn();
  ReEnter())

and UnboundTypIde (TypIde: Atom') =
( AnnounceError();
  outtok(`Unbound type identifier: `); PrintAtom(TypIde);
  PrintLn();  ReEnter())

and UnboundTypVar(TypVar: Atom') =
( AnnounceError();
  outtok(`Unbound type variable:   `);
  PrintAtom(TypVar); PrintLn();
  ReEnter())

and DuplicatedTypVar(TypVar: Atom') =
( AnnounceError();
  outtok(`Duplicated type variable:  `);
  PrintAtom(TypVar); PrintLn();
  ReEnter());

let UnguardedRec( t: Atom') = 
  ( AnnounceError(); 
    outtok(`Unguarded recursion in definition of type: `); 
    PrintAtom( t ); PrintLn(); 
    ReEnter() );

%%
%AM: Type environment handling stuff ... %

let IsHiddenType(x: LocTypEnvCell') = !x.Hidden;

let AllocTypEnv(TypNam: Atom', TypIde: TypTerm', Multiadic: bool,
                   Rest: LocTypEnv'): LocTypEnv'
= (| TypIde=ref TypIde; TypNam; Multiadic; Hidden=ref false |) :: Rest;

let rec RetrieveAtomicTypIde(Ide: Atom', Env: LocTypEnv'): TypTerm' # bool =
  if null(Env)
  then failwith `retrieve`
  else if EqAtom((hd Env).TypNam, Ide) And Not IsHiddenType((hd Env))
       then (!(hd Env).TypIde, (hd Env).Multiadic)
  else RetrieveAtomicTypIde(Ide,tl Env);

let RetrieveTypIde( ide: Atom', typenv: LocTypEnv'): TypTerm' # bool =

           RetrieveAtomicTypIde( ide, typenv ) ?? [`retrieve`]
	   RetrieveTypFromTop( ide, outr(!AnalTopEnv).Typ,UnboundTypIde);

%RJG 03-Mar-89 keep a hold on exn TypTerm' in case of later redeclarations%
%XnTypTerm is declared global in mlglob.ml%
%This will only be secure if at least one refenece has been made to an exn type val%
%this should be the case for SML saved state%
% 7-aug this is all rubbish %
%let RetrieveXnTypTerm () : TypTerm' =
    let _ = if (!XnTypTerm) is absent then
	let (t,_) = RetrieveTypIde(AtomXn,NilEnv)
	            ?? "retrieve" failwith `RetrieveXnTypTerm: no exn type!!`
	in  XnTypTerm := [| present = t |]
	    else ()
    in
	(!XnTypTerm) as present;
%	 


let rec HideOwnTypEnv(TopOwnEnv: LocTypEnv', BotOwnEnv: LocTypEnv')
			 : void =
  if length(TopOwnEnv) = length(BotOwnEnv) then () else
  ( (hd TopOwnEnv).Hidden:=true;
    HideOwnTypEnv(tl TopOwnEnv,BotOwnEnv));

let rec HideOwnConsInfo(TopOwnEnv: LocTypEnv', BotOwnEnv: LocTypEnv')
			 : void =
  if length(TopOwnEnv) = length(BotOwnEnv) then () else
  ( let t = !(hd TopOwnEnv).TypIde in 
    if repTypTerm'(t) is TypAbsOper
    then (repTypTerm'(t) as TypAbsOper).AbsInfo.AbsCons := []
    else ();
    HideOwnConsInfo(tl TopOwnEnv,BotOwnEnv));

%%
%Value environment%
%RJG 02-Mar-89:moved to after typenv%
let AllocAndCheckEnv(VarName: SynBindIde', VarType: TypTerm', Rest: LocEnv',
                     OldEnv: LocEnv', BoundByLambda: bool): LocEnv' =
( let rec checkdistinct(Env: LocEnv', n) =
        if n=0 then ()
        else if EqAtom(VarName.Ide, hd(Env).VarName.Ide)
             then DuplicatedVar(VarName.Ide)
        else checkdistinct(tl Env, n-1)
  in (checkdistinct(Rest, length(Rest)-length(OldEnv));
      (| VarName; Hidden = ref false; LambdaBound= ref BoundByLambda;
         VarType=ref VarType |) :: Rest));

%RJG 02-Mar-89 to allow constructorr construction for builtin excs %
let TempBindoccConstr( ide: Atom' ): SynBindIde' =  
(|  Ide = ide;
    References = ref 0;
    Constructor = [|yes = ref ([| zero |], %will be changed to xcon%
			       0,0,true) |];
    Inline = ref [|absent|];
    StkPosn = ref [| Local = ~1 |];
    MinFunArity = ref MaxInt;
    NativeCoded = ref false;
    SMorUser = [|NonPrimitive|];
    UserArity = ref ~1 |);  

let IsHiddenVar(x: LocEnvCell') = !x.Hidden;

let rec RetrieveAtomicVal(Ide: Atom', Env: LocEnv')
                :TypTerm' # SynBindIde' # bool # OverLoad' =
  if null(Env) then failwith `retrieve`
  else let x = hd Env in
       if EqAtom(Ide, x.VarName.Ide) And Not IsHiddenVar( x )
       then (!x.VarType, x.VarName, !x.LambdaBound, [|None|])
       else RetrieveAtomicVal(Ide,tl Env);


let CheckForBuiltInExc (topenvval,err) (ide)
                      :(TypTerm' # SynBindIde' # bool # OverLoad')= 
%RJG 02-Mar-89%
%based on old version in RetrieveExcIde%
let rec check(i,l,xa) =
    if (i>l) then err(ide)
    else if !(xa sub i) = repAtom'(ide)
	     then let bindexc = TempBindoccConstr(ide)
		  enc xntyp = SysTypes().Xn %RetrieveXnTypTerm() %
		  enc ext = (repTypTerm'(xntyp) as TypAbsOper).AbsInfo.Extensible
		  enc c = (bindexc.Constructor) as yes
		  enc _= c := ( [| xcon = ext |], !ext, MaxInt, true )
		  in
		      (UpdateTopValEnv(topenvval,
				      bindexc,
				      xntyp,
				       mkobj(xa sub i));
		       (xntyp,bindexc,false,[|None|]:OverLoad'))
	       ? failwith `CheckForBuiltinexc:check couldn't update environment` 

	 else
	     check(i+1,l,xa)
in
     check(1,LengthArray(CurrentState().BuiltInExceptions),
           CurrentState().BuiltInExceptions);

let RetrieveVal( ide: Atom', valenv: LocValEnv', 
                 err )
                :TypTerm' # SynBindIde' # bool # OverLoad' =
          RetrieveAtomicVal( ide, valenv ) 
          ?? [`retrieve`]
             let topenvval = outr(!AnalTopEnv).Val in
	     RetrieveValFromTop( ide, topenvval, CheckForBuiltInExc (topenvval,err));

let rec HideOwnValEnv(TopOwnEnv: LocEnv', BotOwnEnv: LocEnv'): void =
  if length(TopOwnEnv) = length(BotOwnEnv) then () else
  ( (hd TopOwnEnv).Hidden:=true; HideOwnValEnv(tl TopOwnEnv,BotOwnEnv));

%%
%AM: Exception environment stuff...%
%RJGDEL let IsHiddenExc(x: LocExcEnvCell') = !x.Hidden;%

%RJGDEL let AllocExcEnv(ExcIde: SynBindIde', ExcTyp: TypTerm',%
%RJGDEL                 Rest: LocExcEnv'): LocExcEnv' =%
%RJGDEL   (| ExcIde; ExcTyp; Hidden=ref false |) :: Rest;%

% This is an expanded version of MLBindoccExc in mlabscon, but must be repeated
  here until the order of loading the code is changed !!! %

%RJGDEL let TempBindoccExc( ide: Atom' ): SynBindIde' =  %
%RJGDEL (|  Ide = ide;%
%RJGDEL     References = ref 0;%
%RJGDEL     Constructor = [|no|];%
%RJGDEL     Inline = ref [|absent|];%
%RJGDEL     StkPosn = ref [| Local = ~1 |];%
%RJGDEL     MinFunArity = ref MaxInt;%
%RJGDEL     NativeCoded = ref false;%
%RJGDEL     SMorUser = [|NonPrimitive|];%
%RJGDEL     UserArity = ref ~1 |);  %

%RJGDEL let rec RetrieveAtomicExcIde(Ide: Atom', Env: LocExcEnv'): TypTerm' # SynBindIde' =%
%RJGDEL   if null(Env)%
%RJGDEL   then %
%RJGDEL     failwith `retrieve`%
%RJGDEL   else if EqAtom((hd Env).ExcIde.Ide, Ide) And Not !(hd Env).Hidden%
%RJGDEL        then ((hd Env).ExcTyp, (hd Env).ExcIde)%
%RJGDEL   else RetrieveAtomicExcIde(Ide,tl Env);%

%RJGDEL let RetrieveExcIde( ide: Atom',  excenv: LocExcEnv'%
%RJGDEL                     ) : TypTerm' # SynBindIde' =%
%RJGDEL     let CheckForBuiltInExc(x) = %
%RJGDEL         let rec check(i,l,xa) = %
%RJGDEL             if (i > l) then UnboundExcIde(x) %
%RJGDEL             else if !(xa sub i) = repAtom'(ide)%
%RJGDEL             then let bindexc = TempBindoccExc(ide) in%
%RJGDEL                  (UpdateTopExcEnv(outr(!AnalTopEnv).Exc, bindexc,AllocTypUnit,%
%RJGDEL                                   mkobj(xa sub i)); %
%RJGDEL                  (AllocTypUnit,bindexc))%
%RJGDEL             else check(i+1,l,xa) in%
%RJGDEL                  check(1,LengthArray(CurrentState().BuiltInExceptions),%
%RJGDEL                        CurrentState().BuiltInExceptions) in%
%RJGDEL              RetrieveAtomicExcIde( ide, excenv ) ?? [`retrieve`]%
%RJGDEL              RetrieveExcFromTop(ide,outr(!AnalTopEnv).Exc, CheckForBuiltInExc);%

%RJGDEL let rec HideOwnExcEnv(TopOwnEnv: LocExcEnv', BotOwnEnv: LocExcEnv'): void =();%
%RJGDEL   if length(TopOwnEnv) = length(BotOwnEnv) then () else%
%RJGDEL   ( (hd TopOwnEnv).Hidden:=true; HideOwnExcEnv(tl TopOwnEnv,BotOwnEnv));%




let HideOwnAllEnv(TopOwnEnv: LocAllEnv', BotOwnEnv: LocAllEnv'): void =
( 
  HideOwnValEnv(TopOwnEnv.Val, BotOwnEnv.Val);
  HideOwnTypEnv(TopOwnEnv.Typ, BotOwnEnv.Typ));
%RJGDEL   HideOwnExcEnv(TopOwnEnv.Exc, BotOwnEnv.Exc));%

%%
% Type variable environment stuff %

let AllocTypVarEnv (VarIde: Atom', TypVar: TypTerm',
                         Rest: TypVarEnv'): TypVarEnv'
= (| VarIde=VarIde; TypVar=TypVar |) :: Rest;

% set to false to make explicit type variables non--instantiable in scope %
let ETVInstantiable = ref(true);

%AM: find where a TypVar occurs in TopEnv, if it doesn't, add it and re-find%
let RetrieveSynTypVar(SynTypVar: Atom',
                      TopEnv: TypVarEnv' ref): TypTerm' # bool =
( let rec f(Env:TypVarEnv') =
    if null(Env) then
    ( TopEnv:=AllocTypVarEnv(SynTypVar,
                             GenTypVar(false,WeakAtom(SynTypVar),false,
                                       MaxInt,!ETVInstantiable),
                             !TopEnv);
      (hd(!TopEnv).TypVar,false))
    else if EqAtom(SynTypVar, (hd Env).VarIde) then (hd(Env).TypVar,true)
    else f(tl Env)
  in f(!TopEnv));

let RetrieveTypVar(TypVar: TypTerm',
                   TopEnv: TypVarEnv' ref): TypVarEnv' =
( let rec f(Env:TypVarEnv') =
    if null(Env) then
    ( TopEnv:=AllocTypVarEnv(dummyAtom,TypVar,!TopEnv);
      (!TopEnv,false))
    else if EqTypVar(TypVar,(hd Env).TypVar) then (Env,true)
    else f(tl Env)
  in fst(f(!TopEnv)));

let rec DeleteTypVar( TypVar: TypTerm', Env: TypVarEnv' ): TypVarEnv' =
    if null Env then Env
    else if EqTypVar( TypVar, (hd Env).TypVar ) then (tl Env)
    else hd( Env ) :: DeleteTypVar( TypVar, tl( Env ) );

%%
%{  -----   TYPE PRINTING  -----  }%

let type TypRole' = [| AtomIde;
                       AtomInfix: (| LeftArity: int; RightArity: int |);
                       %pre/postfix are special cases of this%
                       AtomMultifix
                    |];

% A kludge based on printnames rather than true type identity %
let {TypRole(Atom: Atom'): TypRole' =         %AM: temporary hack%
     if EqAtom(Atom,AtomCross) Or EqAtom(Atom,AtomPlus)
       then [|AtomMultifix|]
     else if EqAtom(Atom,AtomArrow)
       then [|AtomInfix=(|LeftArity=1; RightArity=1|) |]
     else [|AtomIde|]
and [asciia] = explodeascii(`a`)

}

ins TypePrint(Typ: TypTerm', TypVarEnv: TypVarEnv' ref, TypEnv: LocTypEnv',
	      TopEnv: TopAllEnv',
	      FlagHidden: bool, ExpandConVars: bool ): void =
( let VarPrint(TypVar: TypTerm', TypVarEnv: TypVarEnv' ref): void =
  ( let Letter = length(RetrieveTypVar(TypVar,%{VAR}%TypVarEnv))-1 in
    let TypVar = repTypTerm'(TypVar) as TypVar in
    let Letter,Primes = Letter mod 26, Letter/26 in (
    if !Debug.TypeVariables And (Not !TypVar.Generic) then
	(outtok(`!`); if !TypVar.Instantiable then () else outtok(`@`))
    else ();
    outtok(`'`);
    if !TypVar.Ety then outtok(`'`) else ();   
    if !TypVar.Weak then outtok(`_`) else ();
    outtok(implodeascii [asciia + Letter]);
    repeattok(Primes, `'`);
    if !Debug.TypeVariables then (
      outtok(`[`);
      if !TypVar.OccurLevel=MaxInt then
	outtok(`I`)
      else
	printint(!TypVar.OccurLevel);
      outtok(`]`)
    ) else ();
    if !Debug.TimeStamps then
       ( outtok(`<`); printint(TypVar.VarStamp); outtok(`>`) )
    else ()
  ))

  enc GetTypHandle( Handle: Handle' ): Handle' list # bool =
      let IsAvailableTyp( H: Handle' ): bool =
	  ( let (t,_) =
	      RetrieveAtomicTypIde( NameOfHandle( H ), TypEnv ) ?? [`retrieve`]
	      RetrieveTypFromTop( NameOfHandle( H ), TopEnv.Typ, 
                                  (\x.failwith `retrieve`) )
	    enc SelHandle( t: TypTerm' ): Handle' =
		varcase repTypTerm'(t) of
		[| TypAbsOper=x. x.AbsInfo.AbsHandle;
		   TypDefOper=x. x.DefHandle;
		   TypConVar=x. x.ConVarHandle;
		   TypVar. failwith `SelHandle`;
		   TypTagOper. failwith `SelHandle`
		|]
	    in  if EqHandle( H, SelHandle( t ) ) then true
		else let t = FullPrune(t)
		     in  EqHandle( H, SelHandle( t ) )
	  ) ?? [`retrieve`] false
      in  if IsAvailableTyp( Handle ) then ([Handle], false)
          else ([Handle], true)
  enc PrintTypHandle( path: Handle' list, hidden: bool ): unit =
         (listprint(path,PrintAtomicName,`.`);
          if hidden And FlagHidden then outtok(`[hidden]`) else () )

  enc rec Print(Typ: TypTerm', TypVarEnv: TypVarEnv' ref, TopLevel: bool): void =
  ( let PrintParamType(Handle: Handle', hpath, ArgList: TypArgs') =
      % AM: the next line is a bit of a hack... %
      let (Handle, hpath) = 
                 if EqHandle( Handle, TypTupleHandle ) And null( ArgList )
		 then (TypUnitHandle,([TypUnitHandle],false))
                 else (Handle, hpath)
      in varcase TypRole(NameOfHandle(Handle)) of
      [| AtomIde.
            if null(ArgList) then PrintTypHandle( hpath )
            else 
              (if TopLevel then () else outtok(`(`);
               if null(tl ArgList) then
                 (Print(hd(ArgList),%{VAR}%TypVarEnv,false);
	          outtok(` `))
               else
                 (outtok(`(`);
                  listprint(ArgList,
	          (\q. Print(q,%{VAR}%TypVarEnv,false)), `,`);
                  outtok(`) `));
	       PrintTypHandle( hpath );
               if TopLevel then () else outtok(`)`));

        AtomInfix=(|LeftArity; RightArity|).
          ( let (LeftArgs,RightArgs) = split(ArgList,LeftArity,RightArity) in (
            if TopLevel then () else outtok(`(`);
            if LeftArity=0 then ()
            else if LeftArity=1 then
              (Print(hd LeftArgs,%{VAR}%TypVarEnv,false); outtok(` `))
            else
            ( outtok(`(`); 
              listprint(LeftArgs,
	          (\q. Print(q,%{VAR}%TypVarEnv,false)), `,`);
              outtok(`) `));
	    PrintTypHandle( hpath );
            if RightArity=0 then ()
            else if RightArity=1 then
              (outtok(` `); Print(hd RightArgs,%{VAR}%TypVarEnv,false))
            else
            ( outtok(` (`);
              listprint(RightArgs,
	          (\q. Print(q,%{VAR}%TypVarEnv,false)), `,`);
              outtok(`)`));
            if TopLevel then () else outtok(`)`)));

        AtomMultifix.
	  ( if TopLevel then () else outtok(`(`);
            Print(hd ArgList,%{VAR}%TypVarEnv,false);
            let rec f(Args) =
	    ( outtok(` `); PrintTypHandle( hpath );
	      outtok(` `);
	      ( if null(tl Args) then
	          Print(hd Args,%{VAR}%TypVarEnv,false)
	        else
		( Print(hd Args,%{VAR}%TypVarEnv,false);
		  f(tl Args))))
	    in (f(tl ArgList); if TopLevel then () else outtok(`)`) ))
      |]
    in varcase repTypTerm' Typ of
    [| TypVar=x.
         varcase !(x.Instance) of
         [| None.  VarPrint(Typ,%{VAR}%TypVarEnv);
            Yes=i. Print(i,  %{VAR}%TypVarEnv,TopLevel)
         |];
       TypConVar=x.
	 varcase !(x.Instance) of
	 [| absent.PrintParamType(x.ConVarHandle, GetTypHandle(x.ConVarHandle),
                                  x.ConVarArgs);
	    present. if ExpandConVars then
	                Print( (!ConVarInstance)(Typ), TypVarEnv, TopLevel )
		     else
		        PrintParamType(x.ConVarHandle,
                                       GetTypHandle(x.ConVarHandle),
                                       x.ConVarArgs)
	 |];
       TypDefOper=x.
         let (path,hidden) = GetTypHandle(x.DefHandle)
          in if hidden % Should possibly just keep unwinding until a 
                         definition is encountered that is not hidden,
                         rather than unwinding fully in this case %
             then Print(FullPrune(Typ), TypVarEnv, TopLevel)
             else
               PrintParamType(x.DefHandle, (path, hidden), x.DefArgs);
       TypAbsOper=x.
         PrintParamType(x.AbsInfo.AbsHandle,GetTypHandle(x.AbsInfo.AbsHandle),
                        x.AbsArgs);
       TypTagOper=x.
         let rec TypeTagListPrint(Typ: TypTerm', TypVarEnv: TypVarEnv' ref) =
           let y = (repTypTerm' Typ) as TypTagOper in
           let TagTypPrint(q: TagTypTerm') =
            ( PrintAtom(q.Tag);
              if (x.TagSort is Variant) And IsTrivType(q.Typ) then ()
              else (outtok(`:`); Print(q.Typ,%{VAR}%TypVarEnv,true))) in
           varcase !y.TagList of
           [| TagInstance=t.  TypeTagListPrint(t, TypVarEnv);
              Flexi=l. if dnull(l) then outtok(` ... `)
                       else (dlistprint(l,TagTypPrint,`, `);outtok(`, ... `));
              Solid=l. if null(l) then outtok(` `)
                       else listprint(l,TagTypPrint,`, `) |]
         in
            ( PrintBra(x.TagSort);
              TypeTagListPrint(Typ,%{VAR}%TypVarEnv);
              PrintKet(x.TagSort))
    |])

in %{TypePrint}%
  Print(Typ,%{VAR}%TypVarEnv,true));

TypPrintFn := \t. TypePrint(t,(ref NilEnv):TypVarEnv' ref,
                            NilEnv,outr(!AnalTopEnv),true,true);

%%
% Error handling (continued). %
let ErrorTypePrint( Typ, TypVarEnv, FlagHidden ): unit =
    if isr(!AnalTopEnv) then
       TypePrint( Typ, TypVarEnv, NilEnv, outr(!AnalTopEnv), FlagHidden, true )
    else
       outtok(`** ErrorTypePrint: No top--level environment! **`);

let TypeError(Typ1: TypTerm', Typ2: TypTerm') =
( outtok(`Type clash  in:  `);  ShowErrorContext(); PrintLn();
  let TypVarEnv = ref (NilEnv: TypVarEnv') in
  let ShowDefOper(Typ: TypTerm') =
    if repTypTerm'(Prune Typ) is TypDefOper then
      (outtok(`(defined as)     `);
       ErrorTypePrint(FullPrune Typ,%{VAR}%TypVarEnv,false);
       PrintLn())
    else () in (
  outtok(`Looking  for a:  `); ErrorTypePrint(Typ1,%{VAR}%TypVarEnv,true);PrintLn();
  ShowDefOper(Typ1);
  outtok(`I have found a:  `); ErrorTypePrint(Typ2,%{VAR}%TypVarEnv,true);PrintLn();
  ShowDefOper(Typ2);
  ReEnter()) );

let EqTypeError(Typ: TypTerm') =
( outtok(`Type clash  in:  `);  ShowErrorContext(); PrintLn();
  let TypVarEnv = ref (NilEnv: TypVarEnv') in
  let ShowDefOper(Typ: TypTerm') =
    if repTypTerm'(Prune Typ) is TypDefOper then
      (outtok(`(defined as)     `);
       ErrorTypePrint(FullPrune Typ,%{VAR}%TypVarEnv,false);
       PrintLn())
    else () in (
  outtok(`There is no equality defined on type `); 
  ErrorTypePrint(Typ,%{VAR}%TypVarEnv,true);PrintLn();
  ShowDefOper(Typ);
  ReEnter()) );


let NonInstantiableError(Typ1: TypTerm', Typ2:TypTerm') =
( AnnounceError();
  let TypVarEnv = ref( NilEnv: TypVarEnv') in (
    outtok(`The type variable `); ErrorTypePrint( Typ1, TypVarEnv, false );
    outtok(` may not be instantiated to `); ErrorTypePrint( Typ2, TypVarEnv, false );
    outtok(` within its scope.`); PrintLn();
    ReEnter()) )

and AmbiguousOverload(Ide: Atom', Typ: TypTerm') =
( AnnounceError();
  outtok(`Unresolvable overloaded identifier:  `);
  PrintAtom(Ide); PrintLn();
  outtok(`Definition cannot be found for the type:  `);
  ErrorTypePrint(Typ, ref NilEnv, false); PrintLn();
  ReEnter() )

and VariantError(VariantType: TypTerm', Phrase: Phrase') =
( outtok(`Type checking error in: `); ShowErrorPhrase( Phrase ); PrintLn();
  outtok(`Unresolvable Variant or Record type:    `);
  ErrorTypePrint(VariantType, ref NilEnv, false); PrintLn();
  ReEnter() )

and ImportError( FileName: string ): unit =
    ( AnnounceError();
      outtok `Import error using file `; outtok FileName;
      PrintLn(); ReEnter() );

%%
let TagPosition(VarType: TypTerm', Phrase:Phrase')
               (VarTag: Atom'): int#int =
  let VarTagOper = repTypTerm'(Prune(VarType)) as TypTagOper in
  varcase !VarTagOper.TagList of
  [| TagInstance. failwith `TagPosition`;
     Flexi. VariantError(VarType,Phrase);
     Solid=TagList.
       let rec f(n:int, l:TypTagList') =
         if null(l) then failwith `TagPosition`
         else if EqAtom(hd(l).Tag, VarTag) then n
         else f(n+1, tl l) in
       (f(0,TagList), length(TagList))
  |];


let SolidTagList(RecTagList: SynBindRecord' list,
                 VarType: TypTerm', Phrase:Phrase') () :SynBindRecord' list =
%RJG: changed to allow numeric labelled records to unify with tuples
      this means that the pruned type is no longer necessarily a tagtypterm%

  let {rec ExtendTagList(rectaglist: SynBindRecord' list,
                         taglist: TypTagList') =
     if null(taglist) then [] 
     else if null(rectaglist)
     then (|RecKey=(hd taglist).Tag; RecField=absSynBind'[|SynBindAny|]|)
          ::ExtendTagList(rectaglist,tl taglist)
     else if EqAtom(hd(rectaglist).RecKey,hd(taglist).Tag)
     then hd(rectaglist)::ExtendTagList(tl rectaglist,tl taglist)
     else (|RecKey=(hd taglist).Tag; RecField=absSynBind'[|SynBindAny|]|)
          ::ExtendTagList(rectaglist,tl taglist)}

  and f () = failwith `SolidTagList`
  and {rec ExtTagsFromTuple(n:int, rectaglist: SynBindRecord' list,
                         typlist: TypArgs') =
     if null(typlist) then [] %maybe should check to see that rectaglist
                               isn't null here%
     else if null(rectaglist) 
     then (|RecKey=intToAtom'(n,f); RecField=absSynBind'[|SynBindAny|]|)
          ::ExtTagsFromTuple(n+1,rectaglist,tl typlist)
     else let hkey = hd(rectaglist).RecKey
          in 
           if isNumLabel (hkey) 
           then if Atom'toInt (hkey) = n 
                then hd(rectaglist)
                     ::ExtTagsFromTuple(n+1,tl rectaglist,tl typlist)
                else (|RecKey=intToAtom'(n,f); 
                       RecField=absSynBind'[|SynBindAny|]|)
                     ::ExtTagsFromTuple(n+1,rectaglist,tl typlist)
           else f ()}

  and prVarType = repTypTerm'(Prune(VarType)) in
  if prVarType is TypTagOper 
  then
     varcase !(prVarType as TypTagOper).TagList of
     [| TagInstance. f ();
        Flexi. VariantError(VarType,Phrase);
        Solid=TagList. ExtendTagList(RecTagList,TagList)
     |]
  else
     if prVarType is TypAbsOper %RJG: has to be a tuple type%
     then ExtTagsFromTuple(1,RecTagList,(prVarType as TypAbsOper).AbsArgs)
     else f ();


%%
%{  -----   TYPE UNIFICATION  -----  }%

%AM: subsidiary routines for FlagGenericVars%
let OccursVarInType(TypeVar: TypTerm', Typ: TypTerm'): bool =
( let rec Occ(Typ) =
  varcase repTypTerm' Typ of
  [| TypVar=x.
      varcase !(x.Instance) of
      [| None. EqTypVar(TypeVar,Typ);
         Yes=i. Occ(i)
      |];
    TypConVar=x.
	exists(Occ, x.ConVarArgs);
    TypDefOper=x.
        exists(Occ, x.DefArgs);
    TypAbsOper=x.
        exists(Occ, x.AbsArgs);
    TypTagOper=x.
      varcase !(x.TagList) of
      [| TagInstance=i. Occ(i);
         Flexi=y. dexists((\q. Occ(q.Typ)),y);
         Solid=y. exists((\q. Occ(q.Typ)),y)
      |]
  |]
  in Occ(Typ))

%AM: note that we needn't search TopEnv in the following due to the fact %
%    that no member of it can be lambda bound                            %
ins rec OccursLambdaBound(Typ: TypTerm', Env: LocEnv'): bool =
  if null(Env) then false
  else if !(hd Env).LambdaBound
       then if OccursVarInType(Typ,!(hd Env).VarType)
            then true
            else OccursLambdaBound(Typ,tl Env)
       else OccursLambdaBound(Typ,tl Env)

ins FlagGenericVars(Typ: TypTerm', Env: LocEnv', TypVarEnv : TypVarEnv' ref): void =
  let FlagGenericVar(TypeVar: TypTerm'): void =
  ( let x = repTypTerm'(TypeVar) as TypVar in
     (if !(x.Generic) then ()
      else if OccursLambdaBound(TypeVar,Env) then x.Generic:=false
      else if !(x.Weak) then x.Generic :=  !(x.OccurLevel) > !AnalysisLevel
      else if Not !(x.Instantiable) then
            ( if !(x.OccurLevel) >= !AnalysisLevel then
		( x.Generic := true;
		  TypVarEnv := DeleteTypVar( TypeVar, !TypVarEnv ) )
	      else ()
	    )
      else x.Generic := true ;
      if !(x.Generic) then (x.Instantiable := true; x.OccurLevel := MaxInt)
      else ()
     )
  )
  in appTypTermVars(FlagGenericVar, Typ)

enc FlagGenericVarsInNilEnv(Typ: TypTerm'): void =
  FlagGenericVars(Typ,NilEnv,(ref NilEnv):TypVarEnv' ref);

%AM: the routine FlagGenericRecDeclVars is used for the FIX(lambda) -> LET
     change in Milner's type checking of recursive definitions (q.v.).
     The top n variables of Env (defined by a single REC) are made
     generic and let-bound. %
let rec FlagGenericRecDeclVars(Env: LocEnv', n: int, OldEnv: LocEnv',TypVarEnv:TypVarEnv' ref): void =
  if n=0 then () else
  ( FlagGenericVars(!(hd Env).VarType, OldEnv,TypVarEnv);
    (hd Env).LambdaBound := false;
    FlagGenericRecDeclVars(tl Env, n-1, OldEnv,TypVarEnv));

%%
%AM: the next routine and its call comes from Dave MacQueen%
let PropagateOccurrenceLevel(Typ: TypTerm', Level: int): void =
  let f(t:TypTerm') = let x = repTypTerm'(t) as TypVar in
                          x.OccurLevel:=min(Level, !x.OccurLevel)
  in appTypTermVars(f, Typ);

%AM: propagate is a glorified occur-check, which knows about weak variables%
let Propagate(TypeVar: TypTerm', Typ: TypTerm', WeakVar: bool, EtyVar: bool,
              VarOccurLevel: int): void =
  let f(etyvar:bool)(t:TypTerm') = let x = repTypTerm'(t) as TypVar in
            ( if EqTypVar(TypeVar,t) then TypeError(TypeVar,Typ) else ();
              if WeakVar then x.Weak:=true else ();
              if etyvar then x.Ety:=true else ();
              x.OccurLevel:=min(VarOccurLevel, !x.OccurLevel))
  in if EtyVar 
     then appEqTypTermVars(f, EqTypeError, Typ)
     else appTypTermVars((f false), Typ);


let UnifyInternalError() = failwith `Unify internal error`

ins rec {
% RH: caller must prune both Typ1 and Typ2; Typ1' and Typ2' are
  the original terms, used to preserve DefOper's for printing. %
UnifyType( Typ1: TypTerm', Typ2: TypTerm', Typ1', Typ2' ): void =
  varcase repTypTerm' Typ1 of
  [|TypVar=x.
      varcase !(x.Instance) of
      [| None.  if EqTypVar(Typ1,Typ2) then ()
		else if Not !(x.Instantiable) then
		  if (repTypTerm' Typ2) is TypVar then
		    let y = (repTypTerm' Typ2) as TypVar in
			if !(y.Instantiable) then
			   ( Propagate( Typ2, Typ1', !y.Weak, !y.Ety, !y.OccurLevel);
			     y.Instance := [| Yes = Typ1' |]
			   )
			else
			   NonInstantiableError(Typ2',Typ1')
		  else
		    NonInstantiableError(Typ1',Typ2')
	        else ( Propagate(Typ1,Typ2',!x.Weak,!x.Ety,!x.OccurLevel);
                       x.Instance := [|Yes=Typ2'|] );
         Yes=i. UnifyInternalError()
      |];

    TypConVar=x.
	varcase !(x.Instance) of
	[| present. UnifyInternalError();
	   absent.  varcase repTypTerm' Typ2 of
		    [| TypVar=y.
			varcase !(y.Instance) of
			[| Yes. UnifyInternalError();
			   None. if Not !(y.Instantiable) then
			    	   NonInstantiableError(Typ2',Typ1')
				else ( Propagate(Typ2,Typ1',!y.Weak,!y.Ety,!y.OccurLevel);
				       y.Instance := [|Yes=Typ1'|] )
			|];
		       TypConVar=y.
		        varcase !(y.Instance) of
			[| absent.
			      (	IdentifyHandles( x.ConVarHandle, y.ConVarHandle,
					   \ ().TypeError(Typ1',Typ2') );
				if length(x.ConVarArgs) <> length(y.ConVarArgs) then
				   TypeError(Typ1',Typ2')
				else
				   UnifyArgs(x.ConVarArgs,y.ConVarArgs) );
			   present. UnifyInternalError()
			|];
		       TypDefOper=y.
			UnifyType( Typ1, FullPrune( Typ2 ), Typ1', Typ2' );
		       TypAbsOper. TypeError( Typ1', Typ2' );
		       TypTagOper. TypeError( Typ1', Typ2' )
		    |]
	|];

    TypDefOper=x. 
      varcase repTypTerm' Typ2 of
      [| TypVar=y.
          varcase !(y.Instance) of
          [| None. if Not !(y.Instantiable) then NonInstantiableError(Typ2',Typ1')
		   else ( Propagate(Typ2,Typ1',!y.Weak,!y.Ety,!y.OccurLevel);
			  y.Instance := [|Yes=Typ1'|] );
             Yes=i. UnifyInternalError()
          |];
	 TypConVar=y. UnifyType( FullPrune(Typ1), Typ2, Typ1', Typ2' );
         TypAbsOper. UnifyType( FullPrune(Typ1), Typ2, Typ1', Typ2' );
         TypTagOper. UnifyType( FullPrune(Typ1), Typ2, Typ1', Typ2' );
         TypDefOper=y.
	  ( %IdentifyHandles(x.DefHandle,y.DefHandle,\().failwith `UDN`);%
	    if Not( EqHandle(x.DefHandle, y.DefHandle) ) then failwith `UDN`
	    else if length(x.DefArgs)<>length(y.DefArgs) then
		TypeError(Typ1',Typ2')
	    else
		UnifyArgs(x.DefArgs, y.DefArgs) )
	  ?? [`UDN`] UnifyType( FullPrune(Typ1), FullPrune(Typ2), Typ1', Typ2' )
      |];
            
    TypAbsOper=x.
      varcase repTypTerm' Typ2 of
      [| TypVar=y.
          varcase !(y.Instance) of
          [| None. if Not !(y.Instantiable) then NonInstantiableError(Typ2',Typ1')
                   else ( Propagate(Typ2,Typ1',!y.Weak,!y.Ety,!y.OccurLevel);
                          y.Instance := [|Yes=Typ1'|] );
             Yes=i. UnifyInternalError()
          |];
	TypConVar=y. TypeError( Typ1', Typ2' );
        TypDefOper=y.
	  UnifyType( Typ1, FullPrune(Typ2), Typ1', Typ2' );
        TypAbsOper=y.
	  (%IdentifyHandles(x.AbsInfo.AbsHandle,y.AbsInfo.AbsHandle,\().TypeError(Typ1',Typ2'));%
	    if Not( EqHandle( x.AbsInfo.AbsHandle, y.AbsInfo.AbsHandle ) ) Or
	       ( length(x.AbsArgs) <> length(y.AbsArgs) ) then
		TypeError(Typ1',Typ2')
	    else
		UnifyArgs(x.AbsArgs,y.AbsArgs) );

%RJG tuple unifies record type if 
  (a) record is numlabbed and "flexi" (solid records converted at parsetime)
  (b) max(numlab) of record <= length tuple
  (c) "in order" types unify%

        TypTagOper=y.
          if y.TagSort is Record andalso IsTupleType(Typ1) then 
             case !(y.TagList) of [|
              TagInstance. TypeError(Typ1',Typ2');
              Solid. TypeError(Typ1',Typ2');
              Flexi=dl. 
                let rec f (a:TypArgs',b:TagTypTerm' dlist,n:int) =
                    if dnull(b) then () else
                    if null(a) then TypeError(Typ1',Typ2') else
                    let tag = (dhd b).Tag in
                      if isNumLabel(tag) then 
                           if Atom'toInt(tag) = n then
                              (PruneAndUnify(hd a,(dhd b).Typ); 
                               f (tl a, dtl b,n+1))
                           else f(tl a, b,n+1)
                      else TypeError(Typ1',Typ2')
                in
                  (f(x.AbsArgs,dl,1); y.TagList := [|TagInstance=Typ1|])
              |]
          else TypeError(Typ1',Typ2')
      |];

    TypTagOper=x.
      varcase repTypTerm' Typ2 of
         [| TypVar=y.
             varcase !(y.Instance) of
             [| None. if Not !(y.Instantiable) then NonInstantiableError(Typ2',Typ1')
                      else (Propagate(Typ2,Typ1',!y.Weak,!y.Ety,!y.OccurLevel);
                           y.Instance := [|Yes=Typ1'|] );
                Yes=i. UnifyInternalError()
             |];
	   TypConVar=y. TypeError( Typ1', Typ2' );
           TypDefOper=y. UnifyType( Typ1, FullPrune(Typ2), Typ1', Typ2' );
           TypAbsOper=y. 
             if x.TagSort is Record andalso IsTupleType(Typ2) then
               case !(x.TagList) of [|
                 TagInstance. TypeError(Typ1',Typ2');
                 Solid. TypeError(Typ1',Typ2');
                 Flexi=dl.
                   let rec f (a:TypArgs',b:TagTypTerm' dlist,n:int) =
                    if dnull(b) then () else
                    if null(a) then TypeError(Typ1',Typ2') else
                    let tag = (dhd b).Tag in
                      if isNumLabel(tag) then 
                           if Atom'toInt(tag) = n then
                              (PruneAndUnify(hd a,(dhd b).Typ); 
                               f (tl a, dtl b,n+1))
                           else f(tl a, b,n+1)
                      else TypeError(Typ1',Typ2')
                   in
                     (f(y.AbsArgs,dl,1); x.TagList := [|TagInstance=Typ2|])
                 |] 
             else TypeError(Typ1',Typ2') ;
          
           TypTagOper=y.
             if x.TagSort<>y.TagSort then TypeError(Typ1',Typ2')
             else if share(x.TagList,y.TagList) then ()
             % the last line fixes (hacks) a bug creating loops %
             else UnifyTagList(Typ1, Typ2, \().TypeError(Typ1',Typ2'))
          |]
  |]

and UnifyTagList(Typ1: TypTerm', Typ2: TypTerm', ErrorFn: void->void): void =
  let x = repTypTerm' Typ1 as TypTagOper
  and y = repTypTerm' Typ2 as TypTagOper in
  varcase !x.TagList of
  [| TagInstance=i. UnifyInternalError();
     Solid=l1.
       varcase !y.TagList of
       [| TagInstance=i. UnifyInternalError();
          Solid=l2.
            let rec f(a:TypTagList',b:TypTagList') =
              if null(a) then if null(b) then () else ErrorFn()
              else if null(b) then ErrorFn() else
              if EqAtom((hd a).Tag, (hd b).Tag)
              then (PruneAndUnify((hd a).Typ, (hd b).Typ); f(tl a,tl b))
              else ErrorFn()
            in f(l1,l2);
          Flexi=l2.
            let rec f(a:TypTagList',b:TypTagDList') =
              if dnull(b) then () else
              if null(a) then ErrorFn() else
              if EqAtom((hd a).Tag, (dhd b).Tag)
              then (PruneAndUnify((hd a).Typ, (dhd b).Typ); f(tl a,dtl b))
              else f(tl a, b)
            in (f(l1,l2); y.TagList:=[|TagInstance=Typ1|])
       |];
     Flexi=l1.
       varcase !y.TagList of
       [| TagInstance=i. UnifyInternalError();
          Solid=l2.
            let rec f(a:TypTagDList',b:TypTagList') =
              if dnull(a) then () else
              if null(b) then ErrorFn() else
              if EqAtom((dhd a).Tag, (hd b).Tag)
              then (PruneAndUnify((dhd a).Typ, (hd b).Typ); f(dtl a,tl b))
              else f(a, tl b)
            in (f(l1,l2); x.TagList:=[|TagInstance=Typ2|]);
          Flexi=l2.
            let rec f(a:TypTagDList',b:TypTagDList'): TypTagDList' =
              if dnull(b) then a else
              if dnull(a) then b else
              if EqAtom((dhd a).Tag, (dhd b).Tag) then
              ( PruneAndUnify((dhd a).Typ, (dhd b).Typ);
                let x = f(dtl a,dtl b) in (
                dtlset(a,x);
                dtlset(b,x);		%AM: useless?%
                a))
              else if LtAtom((dhd a).Tag, (dhd b).Tag) then
              ( dtlset(a, f(dtl(a), b)); a)
              else
              ( dtlset(b, f(a, dtl(b))); b)
            in (y.TagList:=[|Flexi=f(l1,l2)|];
                x.TagList:=[|TagInstance=Typ2|])
       |]
  |]

%AM: UnifyArgs unifies a pair of lists of TypTerm'. PRECONDITION: same length%
and UnifyArgs(Args1: TypArgs', Args2: TypArgs'): void =
  if null(Args1)
  then if null(Args2) then () else failwith `UnifyArgs: precondition`
  else if null(Args2) then failwith `UnifyArgs: precondition`
  else
  ( PruneAndUnify(hd Args1, hd Args2);
    UnifyArgs(tl Args1, tl Args2))

and PruneAndUnify( S: TypTerm', T: TypTerm' ): unit =
    let S' = Prune( S ) and T' = Prune( T )
    in  UnifyType( S', T', S', T' )
}

enc Unify(Typ1: TypTerm', Typ2: TypTerm'): TypTerm' =
( PruneAndUnify(Typ1,Typ2);
  Typ1
 %{Typ1 is often a forced defined type; returning Typ1 improves type prints}%
 %AM: we should build a better term during unification%
);

%%
% return the instance corresponding to an occurrence of an instantiated
  type constructor variable. %
let ConVarInstance'( Typ: TypTerm' ): TypTerm' =
    let RT = (repTypTerm' Typ) as TypConVar
    enc I = (!(RT.Instance)) as present
    enc I' = FreshType(I)
    enc RI' = repTypTerm'(I')
    enc Args =  varcase RI' of
		[| TypDefOper=x. x.DefArgs;
		   TypAbsOper=x. x.AbsArgs;
		   TypConVar=x. x.ConVarArgs;
		   TypVar. failwith `ConVarInstance`;
		   TypTagOper. failwith `ConVarInstance`
		|]
    in  ( 
%          outtok( `[ Taking instance of `); PrintAtomicName( RT.ConVarHandle ); PrintLn();
	  outtok( `Instance field is `); ErrorTypePrint( I,  ref[], false );
	  outtok( ` = `); ErrorTypePrint( FullPrune(I), ref[], false); PrintLn();
	  outtok( `Fresh instance is `); ErrorTypePrint( I', ref[], false);
	  outtok( ` = `); ErrorTypePrint( FullPrune(I'), ref[], false ); PrintLn(); %
	  UnifyArgs( Args, RT.ConVarArgs );
%	  outtok( `Result is `); ErrorTypePrint( I', ref[], false );
	  outtok( ` = `); ErrorTypePrint( FullPrune(I'), ref[], false );
	  outtok( ` ]`); %
          I' );

% set up linkage %
ConVarInstance := ConVarInstance';

% overloading %

let rec FindOverType(Ide: Atom', Typ: TypTerm',
                     l: (TypTerm' # SynBindIde') list): SynBindIde' =
  if null(l) then AmbiguousOverload(Ide,Typ)
  else let (t,b)::m = l in
       if InstanceOf(t,Typ) then b
       else FindOverType(Ide, Typ, m);

% datatype constructor maintenance %

let type ValueSet' = (| Zero: bool; Pointer: bool|);

let UnionSet(a:ValueSet',b:ValueSet'):ValueSet' =
  (| Zero = a.Zero Or b.Zero; Pointer = a.Pointer Or b.Pointer |)
and DisjointSet(a:ValueSet',b:ValueSet'):bool =
  (Not (a.Zero And b.Zero)) And (Not (a.Pointer And b.Pointer))
and EmptySet = (|Zero=false; Pointer=false|): ValueSet';

let ValueSet(Typ:TypTerm'): ValueSet' =
  varcase repTypTerm'(FullPrune Typ) of
  [| TypVar.     (|Zero=true; Pointer=true|);
     TypConVar.  (|Zero=true; Pointer=true|);	%cannot happen (??) %
     TypDefOper. (|Zero=true; Pointer=true|);	%cannot happen, FullPrune%
     TypAbsOper=x.
	let Handle = x.AbsInfo.AbsHandle in
        if EqHandle(Handle,TypTupleHandle)
        then if null(x.AbsArgs) then (|Zero=true; Pointer=false|)
                                else (|Zero=false; Pointer=true|)
%
        else if EqHandle(Handle,TypStringHandle)
	        Or EqHandle(Handle,TypRefHandle)
             then (|Zero=false; Pointer=true|)
%
        else (|Zero=true; Pointer=true|);
     TypTagOper=x.
       varcase x.TagSort of
       [| Variant. (|Zero=false; Pointer=true|);
          Record.
            varcase !x.TagList of
            [| Solid=x. if null(x) then (|Zero=false; Pointer=true|)
                               else (|Zero=false; Pointer=true|);
               Flexi. (|Zero=true; Pointer=true|);
               TagInstance. (|Zero=true; Pointer=true|)
            |]
       |]
  |];

let rec DisjointValues(l: SynDataDef' list, sofar: ValueSet'): bool =
  if null(l) then true
  else let h::t = l
       enc v = ValueSet(!h.ConstrArgType) in
       if DisjointSet(v, sofar) then DisjointValues(t, UnionSet(v,sofar))
                                else false;

let FlagConstructors(l: SynDataDef' list): void =
%RJG this is not used in the maintenance of extensible constructors -
 see mlanal.ml%
  let size = length(l) in
  if (if size=1 then EqAtom((hd l).AbsBinder.Ide,AtomRef) else false)
  then  %AM: ***HACK***%
    let p = (hd l).AbsBinder.Constructor as yes
    enc (_,_,_,impappl) = !p
    in p := ([|ref|],0,1,impappl)
  else
  if (if size=2 then DisjointValues(l,EmptySet) else false)
  then
  Do (revitlist (\(q,rep). \n. (let p = (q.AbsBinder.Constructor as yes)
                          enc (_,_,_,impappl) = !p
                          in p := (rep,n,size,impappl);
                          n+1))
                (map (\q. (q, if ValueSet(!q.ConstrArgType).Pointer
                              then [|pointer|] else [|zero|])) l)
                0)
  else
  Do (revitlist (\q. \n. (let p = (q.AbsBinder.Constructor as yes)
                          enc (_,_,_,impappl) = !p
                          in p := ([|variant|],n,size,impappl);
                          n+1))
                l 0);

%%
% maintainenance of last--use information for compiler %

let UpdateLastUse(Binder: SynBindIde', Ide: SynTerm', LastUse) =
   let rec checklist(binder, ide, lastuse, lu) =
      if null(lu) then lastuse := (binder,ref [ide]) :: !lastuse
      else if EQPTR(fst(hd(lu)),Binder)
         then snd(hd(lu)) := [ide]
      else checklist(binder, ide, lastuse, tl(lu))
    in checklist(Binder, Ide, LastUse, !LastUse);

let rec SetLastUseFlag(usagelist,OldEnv:LocAllEnv',lambterm) = 
   if null usagelist then ()
   else 
       (let rec freevar(valenv:LocEnv',binder) = 
             if null valenv then false
             else if EQPTR(hd(valenv).VarName, binder) then true
             else freevar(tl(valenv),binder) in
        if freevar(OldEnv.Val, fst(hd(usagelist)))
        then UpdateLastUse(fst(hd(usagelist)), lambterm, OldEnv.LastUse)
        else
          aplist((\x.let syn = repSynTerm' x in
                      if syn is SynIde
                      then (syn as SynIde).LastUse := true
                      else (syn as SynLamb).LastUseFreeVar :=
                        fst(hd(usagelist)):: !(syn as SynLamb).LastUseFreeVar),
                  !(snd(hd(usagelist))));
        SetLastUseFlag(tl(usagelist),OldEnv,lambterm));

%%

let NewSynBindIde( sbi: SynBindIde' ): SynBindIde' =
    (|  Ide=sbi.Ide; References=ref(!sbi.References); 
        % ********** The treatment of the Inline field requires more  ****
          ********** thought.  Here is a temporary fix !              **** %
        Inline = 
	  if (sbi.Constructor) is yes then sbi.Inline else ref(!sbi.Inline);
	Constructor=
	  if (sbi.Constructor) is yes then
	     [| yes=ref(!((sbi.Constructor) as yes)) |]
	  else [|no|];
	NativeCoded=ref(!sbi.NativeCoded);
        MinFunArity=ref(!sbi.MinFunArity);
	UserArity=ref(!sbi.UserArity); SMorUser=sbi.SMorUser;
	StkPosn=ref(!sbi.StkPosn) |);

%%
% CorrPairApp is used to march through a pair of environments, applying a
  binary function to corresponding pairs of entries.  Both environments are
  assumed to be sorted.  All entries in the second must appear in the first,
  but there can be more entries in the first. %
let rec CorrPairApp(f:'a#'a->'b,eq:'a#'a->bool,err,l:'a list,r:'a list): unit =
    let rec scan(cell:'a,list:'a list):'a#('a list)=
	if null(list) then err(cell)
	else if eq(cell,hd(list)) then (hd(list),tl(list))
	else scan(cell,tl(list))
    in  if null(r) then ()
 	else let cr = hd(r)
	     enc (cl,rl) = scan(cr,l)
	     in  ( f(cl,cr); CorrPairApp(f,eq,err,rl,tl(r)) );

let CopySynBindIde( SgSBI: SynBindIde', StSBI: SynBindIde' ): unit =
    ( % Set References field to a big number to prevent inline expansion %
      SgSBI.References := 100; StSBI.References := 100; 

      if (SgSBI.Constructor) is yes And (StSBI.Constructor) is yes then
         ((SgSBI.Constructor) as yes) := !((StSBI.Constructor) as yes)
      else ();
      SgSBI.Inline := !StSBI.Inline;
      SgSBI.StkPosn := [| Local= ~1 |];
      SgSBI.MinFunArity := !StSBI.MinFunArity;
      SgSBI.NativeCoded := !StSBI.NativeCoded;
      SgSBI.UserArity := !StSBI.UserArity
      %* SMorUser field not copied; change when overloading introduced? *% );
%%

let rec AndList(f,l) =
  if null l then true
  else if f(hd l) then AndList(f, tl l) else false;

let rec AndDList(f,l) =
  if dnull l then true
  else if f(dhd l) then AndDList(f, dtl l) else false;

let rec Guarded(typ: TypTerm'): bool =
  varcase repTypTerm' typ of
  [| TypVar=x.
       if (!(x.Instance)) is None then true else Guarded(Prune(typ));
     TypConVar=x. false;
     TypDefOper=x.
       varcase !(x.Guarded) of
       [| Unknown.
            (x.Guarded := [|No|]; 
             if Guarded(x.DefBody)
             then if AndList(Guarded,x.DefArgs) 
                  then (x.Guarded := [|Yes|]; true)
                  else false
             else false);
          Yes. true;
          No. false
       |];
     TypAbsOper=x. AndList(Guarded,x.AbsArgs);
     TypTagOper=x. 
       varcase !(x.TagList) of
       [| TagInstance=t. Guarded(t);
          Solid=tli. AndList((\x:TagTypTerm'. Guarded(x.Typ)), tli);
          Flexi=dtli.AndDList((\x:TagTypTerm'. Guarded(x.Typ)), dtli)
       |]
  |];
