%{  -----  ANALYSER  -----  }%

%{ * TypeChecking
      (checking type consistency of expressions);
  * Primitives
      (mark the variables corresponding to primitive operations (e.g. hd))
  * Reference Numbers
      (number of times a variable is referred inside its scope);
  * Function Arity
      (min arity of usage of a (curried-) function identifier);
  * Useless Code
      (a function which is never referenced will not be compiled);
  * Useless Closures
      (a function with min arity > 0 does not need a closure);
}%

%---------------------------------------- TypTerm %
let rec AnalyseTypTerm(SynTyp: SynTypTerm', Env: LocTypEnv', 
        TypVarEnv: TypVarEnv' ref, InTypDecl: bool, IgnoreImp:bool):TypTerm' =

  let {rec AnalyseTypArgs(Args: SynTypTerm' list): TypArgs' =
  if null(Args) then [] else
    AnalyseTypTerm(hd(Args),Env,%{VAR}%TypVarEnv,InTypDecl, IgnoreImp) ::
      AnalyseTypArgs(tl(Args))}

  and {rec AnalyseTypTagList(Args: (|Tag:Atom';Arg:SynTypTerm'|) list): TypTagList' =
  if null(Args) then [] else
    let x = hd(Args) in
    AllocTypTagList(x.Tag,
                    AnalyseTypTerm(x.Arg,Env,%{VAR}%TypVarEnv,InTypDecl,IgnoreImp),
                    AnalyseTypTagList(tl(Args)))}

enc _ = PushPhrase[|TypTerm=SynTyp|]
enc Result =
  varcase repSynTypTerm' SynTyp of
  [| SynTypVar=x.
      ( let (TypVar: TypTerm', Found: bool) =
	    RetrieveSynTypVar(x.VarIde,%{VAR}%TypVarEnv) in (
        if InTypDecl And Not Found then
%RJG 27-apr-89 if an imperative tyvar is found, ignore if flag set%
%              ( for exception declarations of the form exception Foo of '_a%
%14-july-89 Need to make the type variable non-generic if found here%
	   if IgnoreImp And (WeakAtom (x.VarIde)) then
            (let tv = (repTypTerm'(TypVar) as TypVar) in
               (tv.OccurLevel := !AnalysisLevel - 1; tv.Generic := false))
	   else UnboundTypVar(x.VarIde)
	else ();
        TypVar));
    SynTypAppl=x.
      ( let OperIde = if repAtom'(x.OperIde)=`.` then
                      (outtok(`***Warning '.' used as type:`);
		       ShowErrorContext(); PrintLn(); AtomUnit)
                      else if repAtom'(x.OperIde)=`tok` then
                      (outtok(`***Warning 'tok' used as type:`);
		       ShowErrorContext(); PrintLn(); AtomString)
                      else x.OperIde in
        let (TypOper: TypTerm', Multi: bool) =
            RetrieveTypIde(OperIde,Env) in
        let ArgList = AnalyseTypArgs(x.Args) in
        varcase repTypTerm' TypOper of
        [| TypVar. Crash();
	  TypConVar=y.
	     if length(y.ConVarArgs) = length(ArgList) then
	        let Result = FreshType(TypOper)
		in  ( UnifyArgs(((repTypTerm' Result) as TypConVar).ConVarArgs,
		                ArgList); Result )
	     else TypeError( TypOper, GenFixedTypAbsOper( NameOfHandle(y.ConVarHandle), ArgList ) );
	  TypDefOper=y.
           ( if length(y.DefArgs)=length(ArgList)
	     then ( let Result = FreshType(TypOper) in (
		    UnifyArgs((repTypTerm'(Result) as TypDefOper).DefArgs,
			      ArgList);
		    Result))
	     else TypeError(TypOper,   %AM: A hack for TypeError is next%
			    GenFixedTypAbsOper( NameOfHandle(y.DefHandle), ArgList ) ) );
          TypAbsOper=y.
             if Multi Or length(y.AbsArgs)=length(ArgList)
	     then if length(ArgList)=0 then TypOper
		  else ReAllocTypAbsOper(y, ArgList)
	     else TypeError(TypOper, ReAllocTypAbsOper(y, ArgList));
          TypTagOper=y. Crash()
        |]);
    SynTypTagAppl=x.
        AllocTypTagOper(x.TagSort,
          [|Solid=AnalyseTypTagList(x.Args)|])
  |]
  enc _ = PopPhrase()
  in Result;

%%
%---------------------------------------- TypDecl %
let rec AnalyseTypParams (Params: SynTypParams',
                      ParamsEnv: TypVarEnv' ref): TypArgs' =
  if null(Params) then []
  else
  ( let (x, Found:bool) = RetrieveSynTypVar(hd(Params),%{VAR}%ParamsEnv) in (
    if Found
      then DuplicatedTypVar(hd(Params))
      else ();    % if Not found then ParamsEnv has been updated %
    x :: AnalyseTypParams(tl(Params),ParamsEnv)));


let AnalyseDataDefs(l: SynDataDef' list, f: SynTypTerm' -> TypTerm',
                    IsoOp: TypTerm', OldEnv: LocValEnv',
                    CheckEnv: LocValEnv'): LocValEnv' =
  let NewEnv = ref OldEnv in
  let rec g(l: SynDataDef' list) =
    if null(l) then !NewEnv
    else let hddef::rest = l in (
         hddef.ConstrArgType := f(hddef.Term);
         let p = hddef.AbsBinder.Constructor as yes
         enc (_,_,_,impappl) = !p
         enc ConstrType = if impappl then IsoOp
                          else AllocTypFun(!hddef.ConstrArgType,IsoOp)
         enc c = (repTypTerm'(IsoOp) as TypAbsOper).AbsInfo.AbsCons 
         in (NewEnv := AllocAndCheckEnv(hddef.AbsBinder, ConstrType,
                                       !NewEnv, CheckEnv, false);
             c := (|VarName=hddef.AbsBinder; 
                    VarType= ConstrType|):: !c);
         g(rest))
  in g(l);


let AnalyseConst(c: SynConst'): TypTerm' =
  case c of
  [| int. SysTypes().Int;
     real. SysTypes().Real;
     string. SysTypes().String |];


%---------------------------------------- Term %

let rec {AnalyseTerm(Term: SynTerm',
                AllEnv: LocAllEnv',
                TypVarEnv: TypVarEnv' ref,
                FunctionPosition: int): TypTerm' =
let _ = PushPhrase[|Term=Term|]
enc Result =
varcase repSynTerm' Term of
[| SynIde=x.
  ( let (Typ: TypTerm', Binder, LambdaBound, overloadings) =
           RetrieveVal(x.Ide, AllEnv.Val, UnboundVar)
    enc (| Ide; References; MinFunArity; SMorUser; NativeCoded; 
           Constructor; Inline; UserArity; StkPosn |) = Binder in
    let IdeType = if LambdaBound then Typ else FreshType(Typ) in (
    References := !References+1;
    MinFunArity := min(FunctionPosition,!MinFunArity);
    x.Binder := varcase overloadings of
                [| None. \().Binder;
                   Some=l. \().FindOverType(Ide,IdeType,l) |];
    UpdateLastUse(Binder, Term, AllEnv.LastUse);
    varcase SMorUser of
    [| NonPrimitive. ();
       OverLoaded. ();
       PseudoOp=OpCode.
         let f(Typ) = hd(((repTypTerm' Typ) as TypAbsOper).AbsArgs) in
         varcase OpCode of
         [| OpEqual. x.MonoType := f(f(IdeType));
            OpNotEq. x.MonoType := f(f(IdeType));
            OpWrite. x.MonoType := f(IdeType)
         |]
    |];
    IdeType));

  SynConst=x.    AnalyseConst(x);

  SynTuple=x.
    AllocTypTuple(map (\q.AnalyseTerm(q,AllEnv,%{VAR}%TypVarEnv,0)) x);

  SynList=x.
    if null(x) then (SysTypes().Star)(GenTypVar(false,false,false,MaxInt,true))
    else
    ( let rec AnalyseListTail(Tail,BaseType) = if null(Tail) then BaseType else
	AnalyseListTail(
	  tl(Tail),
	  Unify(BaseType, AnalyseTerm(hd(Tail),AllEnv,%{VAR}%TypVarEnv,0)) )
      in
      (SysTypes().Star)(AnalyseListTail(
	tl(x),
	AnalyseTerm(hd(x),AllEnv,%{VAR}%TypVarEnv,0))));

  SynRecord=x.
  ( let rec AnalyseRecFields(RecFields: SynTermRecord' list): TypTagList' =
      if null(RecFields) then []
      else let (| RecKey; RecField |) = hd(RecFields) in
             AllocTypTagList(RecKey,
               AnalyseTerm(RecField,AllEnv,%{VAR}%TypVarEnv,0),
               AnalyseRecFields(tl RecFields))
    in AllocTypRecord[|Solid=AnalyseRecFields(x)|]);

  SynVariant=x.
  ( let Typ =
      AllocTypVariant[|Flexi=
        AllocTypTagDList(x.VarKey,
          AnalyseTerm(x.VarField,AllEnv,%{VAR}%TypVarEnv,0),
          dnil)|] in
    (x.VarPos:=TagPosition(Typ,[|Term=Term|]); Typ));

  SynCond=x.
  ( Do(Unify(SysTypes().Bool,AnalyseTerm(x.CondIf,AllEnv,%{VAR}%TypVarEnv,0)));
    Unify(AnalyseTerm(x.CondThen,AllEnv,%{VAR}%TypVarEnv,0),
          AnalyseTerm(x.CondElse,AllEnv,%{VAR}%TypVarEnv,0)) );

  SynWhile=x.
  ( Do(Unify(SysTypes().Bool,AnalyseTerm(x.WhileCond,AllEnv,TypVarEnv,0)));
    Do (Unify(GenTypVar(true,false,false,MaxInt,true),
              AnalyseTerm(x.WhileBody,AllEnv,%{VAR}%TypVarEnv,0)));
    AllocTypUnit );

  SynLamb=x.
  ( AnalysisLevel := !AnalysisLevel+1;
    let (NewEnv: LocAllEnv') =
       (|
	 Val= AllEnv.Val; Typ= AllEnv.Typ; LastUse= ref [] |)
    enc (LftTyp,RhtTyp) = AnalyseMatch(x.Match,NewEnv,%{VAR}%TypVarEnv) in (
    AnalysisLevel := !AnalysisLevel-1;
    SetLastUseFlag(!NewEnv.LastUse,AllEnv,Term);
    AllocTypFun(LftTyp,RhtTyp)));

  SynNewCase=x.
    let SelTyp = AnalyseTerm(x.Select, AllEnv,%{VAR}%TypVarEnv,0) in
    let (LftTyp,RhtTyp) = AnalyseMatch(x.Match,AllEnv,%{VAR}%TypVarEnv) in (
    Do (Unify(LftTyp, SelTyp));
    RhtTyp);

  SynAppl=x.
  ( let FunType=
      AnalyseTerm(x.Fun,AllEnv,%{VAR}%TypVarEnv,FunctionPosition+1) in
    let _ = PropagateOccurrenceLevel(FunType,!AnalysisLevel) in
    let ArgType=AnalyseTerm(x.Arg,AllEnv,%{VAR}%TypVarEnv,0) in
    let ResType=GenTypVar(false,false,false,MaxInt,true) in (
    %{Optimized Version: produces less garbage...
        if IsFunTyp(FunType) then
        ( let AbsArgs = GetAbsTypArgs(FunType) in (
	  Do (Unify(hd(AbsArgs), ArgType));
	  Do (Unify(hd(tl(AbsArgs)), ResType))))
        else    }%
    Do (Unify(FunType, AllocTypFun(ArgType,ResType)));
    ResType));

%AM: isn't the next varcase like that for lists?%
  SynCase=x.
  ( let rec AnalyseCases(Cases: SynTermCase' list, ResType: TypTerm')
                        : TypTagList' # TypTerm' =
      if null(Cases) then ([],ResType) else
        let x = hd(Cases)
	enc _ = PushPhrase[|CaseClause=x|] in
        let (BindType: TypTerm', NewEnv) =
          %AM: changed BoundByLambda (last) arg to false 3/10/84 %
          %AM: but caused problems with variant resolution, so restored%
          AnalyseBind2(x.Bind,AllEnv,%{VAR}%TypVarEnv,true) in
        let BodyType =
          AnalyseTerm(x.Body,NewEnv,%{VAR}%TypVarEnv,0) in
        let _ = PopPhrase()
	enc (TTL,ResType2) = AnalyseCases(tl(Cases),
                                          Unify(ResType,BodyType)) in
	 (AllocTypTagList(x.Tag,BindType,TTL), ResType2)
    in
    let SelectType = AnalyseTerm(x.Select,AllEnv,%{VAR}%TypVarEnv,0) in
    let (TTL,ResType) = AnalyseCases(x.Cases,GenTypVar(false,false,false,MaxInt,true)) in
    let CasesType = AllocTypVariant[|Solid=TTL|] in (
    Do (Unify(SelectType,CasesType));
    ResType));

  SynJumpcase=x. 
  let SelTyp = AnalyseTerm(x.Select, AllEnv,%{VAR}%TypVarEnv,0) in
    let (LftTyp,RhtTyp) = AnalyseJumpcases(x.Cases,AllEnv,%{VAR}%TypVarEnv) in (
    Do (Unify(LftTyp, SelTyp));
    RhtTyp);

  SynLet=x.
    let NewEnv = AnalyseDecl2(x.Decl,AllEnv,%VAR%TypVarEnv)
     in AnalyseTerm(x.Scope,NewEnv,%{VAR}%TypVarEnv,0);

  SynQuaOp=x.
  ( let (LftTyp: TypTerm') =
        AnalyseTerm(x.QuaArg,AllEnv,%{VAR}%TypVarEnv,0) in
%AM:    let (FieldTyp: TypTerm') = GenTypVar(false,false,false,!AnalysisLevel,true) in %
    let (FieldTyp: TypTerm') = GenTypVar(false,false,false,MaxInt,true) in
    let (TagList: TypTagDList') = AllocTypTagDList(x.QuaIde,FieldTyp,dnil) in
    let (Typ: TypTerm', Result: TypTerm') = varcase x.QuaOp of
      [| SynQuaDot. (AllocTypRecord[|Flexi=TagList|], FieldTyp);
         SynQuaIs.  (AllocTypVariant[|Flexi=TagList|], SysTypes().Bool);
         SynQuaAs.  (AllocTypVariant[|Flexi=TagList|], FieldTyp) |] in (
    Do (Unify(Typ,LftTyp));	%AM: 12/10/83 swapped 1st 2 args%
    x.QuaPos := TagPosition(Typ,[|Term=Term|]);
    Result));

  SynForce=x.
    Unify(AnalyseTypTerm(x.ForceType,AllEnv.Typ,%{VAR}%TypVarEnv,false,false),
          AnalyseTerm(x.ForceTerm,AllEnv,%{VAR}%TypVarEnv,FunctionPosition));

  SynTagType=x.
    let ArgTyp = AnalyseTerm(x.Arg,AllEnv,%{VAR}%TypVarEnv,FunctionPosition)
     in ( x.Type := ArgTyp; 
          case x.Purpose of
          [|Print. ArgTyp; 
            Dynamic. SysTypes().Dynamic; 
            Cast. let ResType=GenTypVar(false,false,false,MaxInt,true) in ( 
                    Do(Unify(SysTypes().Dynamic, ArgTyp));
                    x.Type := ResType; ResType)
          |] );
  SynTrap=x.
    let LftTyp = AnalyseTerm(x.TrapLft,AllEnv,%{VAR}%TypVarEnv,0) in
    let RhtTyp = varcase x.TrapClass of
    [| SynTrapAll. AnalyseTerm(x.TrapRht,AllEnv,%{VAR}%TypVarEnv,0);
      SynTrapList=(| TrapList |).
        ( Do (Unify((SysTypes().Star)(SysTypes().String),
                     AnalyseTerm(TrapList,AllEnv,%{VAR}%TypVarEnv,0)));
          AnalyseTerm(x.TrapRht,AllEnv,%{VAR}%TypVarEnv,0));
      SynTrapLamb=(| TrapBind |).
          let (Typ,NewEnv) =
            AnalyseBind2(TrapBind,AllEnv,%{VAR}%TypVarEnv,true) in (
          Do (Unify(SysTypes().Xn,Typ));
          AnalyseTerm(x.TrapRht,NewEnv,%{VAR}%TypVarEnv,0))
    |]
    in Unify(LftTyp,RhtTyp);

  SynHandle=x.
%RJG 07-Mar-89%
    let ExpTyp = AnalyseTerm(x.HandLft, AllEnv, %{VAR}% TypVarEnv, 0) in
     let (LftTyp, RhtTyp) = AnalyseMatch(x.Match, AllEnv, %{VAR}% TypVarEnv) in
      ( Do (Unify(SysTypes().Xn, LftTyp); Unify(ExpTyp,RhtTyp)); ExpTyp);

  SynRaise=x.
%RJG 09-Mar-89%
  let ArgTyp = if EqAtom(x.ExcIde,AtomOldFail) then SysTypes().String
                                               else SysTypes().Xn
  in (
      Do (Unify(ArgTyp, AnalyseTerm(x.ExcArg,AllEnv,%{VAR}%TypVarEnv,0)));
      GenTypVar(false,false,false,MaxInt,true));
      

  SynSequence=x.
  ( Do (Unify(GenTypVar(true,false,false,MaxInt,true),
              AnalyseTerm(x.SeqLft,AllEnv,%{VAR}%TypVarEnv,0)));
    AnalyseTerm(x.SeqRht,AllEnv,%{VAR}%TypVarEnv,0))
|]
enc _ = PopPhrase() in Result
%%

%---------------------------------------- Match %

and AnalyseMatch(Match': SynRule' list,
                 AllEnv: LocAllEnv',
                 TypVarEnv: TypVarEnv' ref): (TypTerm' # TypTerm') =
  if null(Match')
  then (GenTypVar(false,false,false,MaxInt,true), GenTypVar(false,false,false,MaxInt,true))
  else let AnalyseRule((Bind',Body)) =
          let (BindType: TypTerm', NewAllEnv) =
                      AnalyseBind2(Bind',AllEnv,%{VAR}%TypVarEnv,true)
          enc (BodyType: TypTerm') =
                      AnalyseTerm(Body,NewAllEnv,%{VAR}%TypVarEnv,0)
          in  (BindType,BodyType)
       enc rec AnalyseRules(l: SynRule' list, sofar: TypTerm' # TypTerm') =
          if null(l) then sofar
	  else  let _ = PushPhrase[|Rule=hd(l)|]
		enc (x1,x2) = sofar and (y1,y2)=AnalyseRule(hd l)
		enc z = ( Unify(x1,y1), Unify(x2,y2) )
		in  ( PopPhrase(); AnalyseRules( tl l, z ) )
       in AnalyseRules(tl Match', AnalyseRule(hd Match'))


%RJG - this is analogous to AnalyseMatch and AnalyseCase in SynCase above
 not count of clauses check%


and AnalyseJumpcases(Cases: SynTermCase' list,
                 AllEnv: LocAllEnv',
                 TypVarEnv: TypVarEnv' ref): (TypTerm' # TypTerm') =

  if null(Cases)
  then (GenTypVar(false,false,false,MaxInt,true),  %never happens%
        GenTypVar(false,false,false,MaxInt,true))
  else let AnalyseRule(x:SynTermCase') =
       % AnalyseRule returns ((t1,t2),(v,n,e)) where
         t1,t2 : pattern, body  type of rule
         v     : kind of constructor (for code gen)
         n     : number of constructors in datatype%
          let (|Tag=tag;Bind=bind;Body=body|) = x
          %now treat tag/bind as a Bind Appl%
          enc (Typ,Binder,nullary,kind_noConstrs) =
	      let (t,b,_,_) = RetrieveVal(tag,AllEnv.Val,UnboundVar)
	      in case b.Constructor of
                 [| yes=p. let (kind,_,max,nullary) = !p
                           in (FreshType(t),b,nullary,(kind,max));
                    no. UnboundConstructor(tag) |]

          enc (BindType: TypTerm', NewAllEnv) =
              if nullary then (Typ,AllEnv)
	      else 
                let (ArgTyp,NewAllEnv) =
		            AnalyseBind2(bind,AllEnv,%VAR%TypVarEnv,true)
                enc ResTyp = GenTypVar(false,false,false,MaxInt,true) 
                in
		   (Do (Unify(Typ,AllocTypFun(ArgTyp,ResTyp)));
		    (ResTyp,NewAllEnv))

          enc (BodyType: TypTerm') =
                      AnalyseTerm(body,NewAllEnv,%{VAR}%TypVarEnv,0)
          in  ((BindType,BodyType),kind_noConstrs)
        %end of AnalyseRule%

       enc rec AnalyseRules(l: SynTermCase' list, sofar) =
       % AnalyseRules accumulates the unifed types of patterns and bodies,
         and the exhaustion of the patterns.  It also returns the kind
         constructor (only can be of "variant" kind) and the number of
         constructors (and hence the number of rules required) for an
         exhaustive match %
          if null(l) then sofar
	  else  let _ = PushPhrase[|CaseClause=hd(l)|]
		enc ((x1,x2),_) = sofar
		enc ((y1,y2),nn)=AnalyseRule(hd l)
		enc z = ( Unify(x1,y1), Unify(x2,y2) )
		in  ( PopPhrase(); AnalyseRules( tl l, (z,nn) ) )
          enc rec Exhaustive (pat:SynBind') (sofar:bool) : bool =
	      sofar andalso
	      varcase repSynBind'(pat) of
	      [| SynBindIde. true;
                 SynBindAny. true;
		 SynBindBoth=(p1,p2). Exhaustive p1 (Exhaustive p2 true);
		 SynBindTuple=l.  %ANdy, replace revitlist with fold in SML%
		    revitlist (\p.\b. Exhaustive p b) l true;
	         SynBindRecord=(l,_).
		    revitlist (\(|RecField=p; RecKey=_|).\b.
		                 Exhaustive p b) l true;
	         SynBindForce=(|ForceBind=p; ForceType=_|). Exhaustive p true;
		 SynBindVariant. false;
		 SynBindConst. false;
		 SynBindAppl=(|Ide=_;Binder=b:SynBindIde' ref;Arg=p;HowRead=_|).
		   let constr = (!b).Constructor
		   in if constr is yes 
                      then let (_,_,max,_) = !(constr as yes)
		           in Exhaustive p (max=1)
                      else false
              |]
       enc (result,(kind,noConstrs)) = 
            AnalyseRules(tl Cases, AnalyseRule(hd Cases))
       enc err x = ( AnnounceError(); outtok(x); PrintLn();  ReEnter())
       in  if Not (kind is variant) then 
              err (`Cannot compile this type for jumps`)
           else if (length(Cases) <> noConstrs) 
                then err (`All and only all constructors must be specified`)
                else (if (revitlist (\(|Bind=pat;Tag=_;Body=_|).
                                      Exhaustive pat) Cases true)
                      %double traversal of cases required as Unification
		       must be done before Exhaustive called to set up
		       SynBindIdes%
                      then () %exhaustive%
                      else (outtok(`***Warning: jump rules inexhaustive in:`);
			    PrintLn();
		            ShowErrorContext();
		            PrintLn());
		     result)
%%
%---------------------------------------- Decl %

and CheckDistinct( NewEnv: LocEnv', OldEnv: LocEnv'): unit =
        let rec checkdistinct(VarName: SynBindIde', Env: LocEnv', n) =
           if n=0 then ()
           else if EqAtom(VarName.Ide, hd(Env).VarName.Ide)
                then hd(Env).Hidden := true
           else checkdistinct(VarName, tl Env, n-1)
        enc rec checkdistinctenv(Env: LocEnv', n) =
           if n=0 then ()
           else if !(hd(Env).Hidden) then checkdistinctenv(tl Env, n-1)
           else (checkdistinct(hd(Env).VarName, tl Env, n-1);
                 checkdistinctenv(tl Env, n-1))
         in checkdistinctenv(NewEnv, length(NewEnv)-length(OldEnv))

and AnalyseDecl2(Decl: SynDecl', OldEnv: LocAllEnv',TypVarEnv:TypVarEnv' ref): LocAllEnv' =
  let NewValEnv = ref( OldEnv.Val )
  and NewTypEnv = ref( OldEnv.Typ )

  enc rec AnalyseDecl(Decl: SynDecl', OldEnv: LocAllEnv'): void =
  ( PushPhrase[|Decl=Decl|];
  varcase repSynDecl' Decl of
  [| SynDeclDefVal=x.
       let (Typ: TypTerm')
          = AnalyseBind(x.Bind,%{VAR}%NewValEnv,   %*** IMPROVE ***%!NewValEnv,
                        OldEnv.Typ, %{VAR}%TypVarEnv,false,OldEnv.LastUse)
        enc (DefTyp: TypTerm')
          = AnalyseTerm(x.Term,OldEnv,%{VAR}%TypVarEnv,0)
        in FlagGenericVars(Unify(Typ,DefTyp), OldEnv.Val,TypVarEnv);
     SynDeclDefTyp=x.
	let TypVarEnv = ref NilEnv in
        let (ParamsList: TypArgs')
	  = AnalyseTypParams(x.Params,%{VAR}%TypVarEnv) in
        let (NewOp: TypTerm') = varcase x.DefSort of
        [| ShortHand=t.
             let (NewDef: TypTerm')
               = AnalyseTypTerm(t.SynBinding,OldEnv.Typ,%{VAR}%TypVarEnv,true,false) in
             GenFixedTypDefOper(x.Bind,ParamsList,NewDef);
           Isomorphism=(| Constrs=l; Extensible=exbl; Extending=exng |).
             let IsoOp = GenFixedTypAbsOper(x.Bind,ParamsList) in (
             let f(t:SynTypTerm') = AnalyseTypTerm(t, OldEnv.Typ, 
						   %{VAR}%TypVarEnv,true,false) in
             NewValEnv := AnalyseDataDefs(l,f,IsoOp,!NewValEnv,!NewValEnv);
             FlagConstructors(l);
             IsoOp) |]
        in ( %AM: we use NilEnv in the next line since local type decls
                  have no free type variables (even by unification)%
             aplist(FlagGenericVarsInNilEnv, ParamsList);
             NewTypEnv:=AllocTypEnv(x.Bind,NewOp,false,!NewTypEnv));
    SynDeclDefExcon=y.failwith (`AnalyseDecl:SynDefExcon`);
    SynDeclAnd=(|Lft;Rht|).
      ( AnalyseDecl(Lft,OldEnv);
        AnalyseDecl(Rht,OldEnv));
    SynDeclEnc=(|Ext;Int|).
      ( AnalyseDecl(Ext,OldEnv);
        let (EncEnvBeg: LocAllEnv') =
	 (| Val= !NewValEnv; Typ= !NewTypEnv; %RJGDEL Exc= !NewExcEnv; %
            LastUse= OldEnv.LastUse |) in (
        AnalyseDecl(Int,EncEnvBeg)));
    SynDeclIns=(|Outs;Ins|).
      ( let (OwnEnvEnd: LocAllEnv') =
	  (|Val= !NewValEnv; Typ= !NewTypEnv; 
            LastUse= OldEnv.LastUse |) in (
        AnalyseDecl(Outs,OldEnv);
        let (OwnEnvBeg: LocAllEnv') =
	  (|Val= !NewValEnv; Typ= !NewTypEnv; 
            LastUse= OldEnv.LastUse |) in (
        AnalyseDecl(Ins,OwnEnvBeg);
        HideOwnAllEnv(OwnEnvBeg,OwnEnvEnd))));
    SynDeclWith=(|WithExt;WithInt|).
      ( let (WithValEnvEnd: LocEnv') = !NewValEnv
        and (WithTypEnvEnd: LocTypEnv') = !NewTypEnv in (
        AnalyseDecl(WithExt,OldEnv);
        let (WithEnvBeg: LocAllEnv') =
	    (|Val= !NewValEnv; Typ= !NewTypEnv; 
            LastUse= OldEnv.LastUse |) in (
        AnalyseDecl(WithInt,WithEnvBeg);
        HideOwnConsInfo(WithEnvBeg.Typ,WithTypEnvEnd);
	%RJG this is to make sure that abstypes not extensible%
	let rec CheckabstypeNotExtensible(TopOwnEnv: LocTypEnv', BotOwnEnv: LocTypEnv')	 : void =
  if length(TopOwnEnv) = length(BotOwnEnv) then () else
  ( let t = !(hd TopOwnEnv).TypIde in 
    if repTypTerm'(t) is TypAbsOper
    then if !(repTypTerm'(t) as TypAbsOper).AbsInfo.Extensible > 0
	 then (outtok(`abstype cannot be declared extensible`);PrintLn();
	       ShowErrorContext(); PrintLn(); ReEnter())
	 else ()
    else ();
    CheckabstypeNotExtensible(tl TopOwnEnv,BotOwnEnv)) in
        CheckabstypeNotExtensible(WithEnvBeg.Typ,WithTypEnvEnd);
        HideOwnValEnv(WithEnvBeg.Val,WithValEnvEnd))));
    SynDeclRec=(|Rec|).
        %AM: the following code is like it is for the following reason:
            Under Milner's type checking scheme "let rec f=e1 and g=e2"
            is typechecked as if it were
            "let (f,g) = (FIX: 'a # 'a -> 'a)(\(f,g).(e1,e2))"
            Thus we first simulate code for "lambda", then for "let". %
        let n = length(!NewValEnv)
	and IsoEnv = ref(!NewTypEnv) in (
        AnalysisLevel := !AnalysisLevel+1;
        AnalyseRecDeclVars(Rec,%{VAR}%NewValEnv, !NewValEnv,
                               %{VAR}%NewTypEnv, 
                               %{VAR}%IsoEnv, %VAR%TypVarEnv);
        AnalyseRecDecl(Rec,
	    (|Val= !NewValEnv; Typ= !NewTypEnv; 
            LastUse = OldEnv.LastUse|),!IsoEnv,%VAR%TypVarEnv);
        CheckGuarded(Rec);
        AnalysisLevel := !AnalysisLevel-1;
        FlagGenericRecDeclVars(!NewValEnv,length(!NewValEnv)-n,OldEnv.Val,TypVarEnv))

  |]; PopPhrase() )
  in (AnalyseDecl(Decl, OldEnv);

         (|Val= !NewValEnv; Typ= !NewTypEnv; 
         LastUse = OldEnv.LastUse |))

%%
%------------------------------------ RecDeclVars %

and AnalyseRecDeclVars(RecDecl: SynDecl', Env: LocEnv' ref, CheckEnv: LocEnv',
                       TypEnv: LocTypEnv' ref, 
		       IsoEnv: LocTypEnv' ref,
                       TypVarEnv:TypVarEnv' ref): void =
  ( PushPhrase[|Decl=RecDecl|];
  varcase repSynDecl' RecDecl of
  [| SynDeclDefVal=x.
      ( if repSynBind'(x.Bind) is SynBindIde
	   then () else SyntaxError(19);
        x.BindType:= AnalyseBind(x.Bind,%{VAR}%Env,CheckEnv,
                          !TypEnv,%{VAR}%TypVarEnv,true,ref [] %LastUse%));
     SynDeclDefTyp=x.
      ( x.TypVarEnv := NilEnv;
	x.TypParams := AnalyseTypParams(x.Params,x.TypVarEnv);
	varcase x.DefSort of
        [| ShortHand=t.
	     let def = GenTypVar(false,false,false,MaxInt,true)
	     enc newop = GenFixedTypDefOper(x.Bind,!x.TypParams,def)
	     in  ( TypEnv := AllocTypEnv(x.Bind,newop,false,!TypEnv);
		   t.TypBinding := newop );
           Isomorphism=(| Constrs=l; Extending=extending; Extensible=extable |).

             let IsoOp = if extending then
	                    if null (l) then %constructor-less decl%
			      let iso = GenFixedTypAbsOper(x.Bind,!x.TypParams)
			      enc a = (repTypTerm' (iso)) as TypAbsOper
                              enc _ = a.AbsInfo.Extensible := StartExtensibleFrom
			      enc _ = a.AbsInfo.EqDefined := [| No |]
			      in iso
			    else
			      (let (old,m) =
				if EqAtom(x.Bind,AtomXn)
				then (SysTypes().Xn %RetrieveXnTypTerm()%, false)
				else  RetrieveTypIde(x.Bind,!TypEnv)
			      % should TypEnv be something else??? %
			      enc oldoper = repTypTerm'(old) as TypAbsOper
				   ?? [`As`] (outtok `can only extend datatypes`;
					 PrintLn(); ShowErrorContext();
					 PrintLn(); ReEnter())

			      enc n = !oldoper.AbsInfo.Extensible

			      % imported and modified from analsupp.ml %
			      enc AllocTypAbsOperByAbsInfo
			       ( Info: AbsInfo', Args: TypArgs' ): TypTerm' =
			       absTypTerm'[| TypAbsOper=
			        (| AbsArgs=Args;
				   AbsInfo=
				    (| AbsHandle=Info.AbsHandle;
				       AbsCons=ref [];
				       AbsEqFn=Info.AbsEqFn;
				       AbsPrintFn=Info.AbsPrintFn;
				       EqDefined = Info.EqDefined;
				       Extensible = Info.Extensible |) |) |]

			      in if n > 0 %valid extensible %
			         then let iso = AllocTypAbsOperByAbsInfo (
				      oldoper.AbsInfo,!x.TypParams)
				      enc a = (repTypTerm' (iso) as TypAbsOper)
				      enc _ = a.AbsInfo.Extensible := n 
				      enc _ = a.AbsInfo.EqDefined := [| No |]
				      in iso
				 else
				  (outtok `datatype not declared extensible`;
					 PrintLn(); ShowErrorContext();
					 PrintLn(); ReEnter()))
			 else GenFixedTypAbsOper(x.Bind,!x.TypParams)
              enc f(t:SynTypTerm') = GenTypVar(false,false,false,MaxInt,true)
	      in  ( Env := AnalyseDataDefs(l, f, IsoOp, !Env, CheckEnv);
		    TypEnv:=AllocTypEnv(x.Bind,IsoOp,false,!TypEnv);
		    IsoEnv := AllocTypEnv(x.Bind,IsoOp,false,!IsoEnv) )
        |] );
    SynDeclDefExcon=x.
      let (typ,sbi,_,_) = RetrieveVal(x.CopyIde, CheckEnv, UnboundConstructor)
      enc BadConstructor (i,j) = (AnnounceError(); 
                    outtok (`Must be a constructor of type `);
                    outtok (i); PrintLn();
                    outtok(j); outtok(` : `);
                    PrintAtom(x.CopyIde); PrintLn(); ReEnter())
      enc (typConstr,_,_,_) = !(sbi.Constructor as yes)
               ?? [`As`] BadConstructor(`exn`,`Not a constructor`)
      enc _ = if Not (typConstr is xcon)
              then BadConstructor(`exn`,`Wrong type of constructor`)
              else ()
      enc _ = x.ConstrArgType := typ
      enc _ = x.Binder := \().sbi
      in Env := AllocAndCheckEnv(x.AbsBinder,typ,!Env,CheckEnv,false);

    SynDeclAnd=(|Lft;Rht|).
      ( AnalyseRecDeclVars(Lft,%{VAR}%Env,CheckEnv,%{VAR}%TypEnv,IsoEnv,%VAR%TypVarEnv);
        AnalyseRecDeclVars(Rht,%{VAR}%Env,CheckEnv,%{VAR}%TypEnv,IsoEnv,%VAR%TypVarEnv));
    SynDeclEnc=(|Ext;Int|).
      ( AnalyseRecDeclVars(Ext,%{VAR}%Env,CheckEnv,%{VAR}%TypEnv,IsoEnv,%VAR%TypVarEnv);
        AnalyseRecDeclVars(Int,%{VAR}%Env,CheckEnv,%{VAR}%TypEnv,IsoEnv,%VAR%TypVarEnv));
    SynDeclIns. SyntaxError(18);
    SynDeclWith. SyntaxError(22);
    SynDeclRec=(|Rec|).
        AnalyseRecDeclVars(Rec,%{VAR}%Env,CheckEnv,%{VAR}%TypEnv,IsoEnv,%VAR%TypVarEnv)
  |];
  PopPhrase() )

and CheckGuarded(RecDecl: SynDecl'): void =
  ( PushPhrase[|Decl=RecDecl|];
  varcase repSynDecl' RecDecl of
  [| SynDeclDefVal=x. ();
     SynDeclDefTyp=x.
      ( varcase x.DefSort of
        [| ShortHand=t.
             if Guarded(!t.TypBinding) then ()
             else UnguardedRec(x.Bind);
           Isomorphism=l. ()
        |] );
    SynDeclDefExcon=x. ();
    SynDeclAnd=(|Lft;Rht|).
      ( CheckGuarded(Lft); CheckGuarded(Rht) );
    SynDeclEnc=(|Ext;Int|).
      ( CheckGuarded(Ext); CheckGuarded(Int) );
    SynDeclIns. SyntaxError(18);
    SynDeclWith. SyntaxError(22);
    SynDeclRec=(|Rec|).
        CheckGuarded(Rec)
  |];
  PopPhrase() )

%%
%-------------------------------- RecDecl %

and AnalyseRecDecl(RecDecl: SynDecl', Env: LocAllEnv', IsoEnv: LocTypEnv', TypVarEnv:TypVarEnv' ref): void =
  ( PushPhrase[|Decl=RecDecl|];
  varcase repSynDecl' RecDecl of
  [| SynDeclDefVal=x.
       let refs = (repSynBind'(x.Bind) as SynBindIde).Binder.References
       enc r = !refs in          %AM: ignore recursive references%
       ( if repSynTerm'(x.Term) is SynLamb 
         then (repSynBind'(x.Bind) as SynBindIde).Binder.NativeCoded :=
	      !Debug.NativeCodeFns
         else SyntaxError(19);
         Do (Unify(!x.BindType, AnalyseTerm(x.Term,Env,%{VAR}%TypVarEnv,0)));
         refs := r);
     SynDeclDefTyp=x.
       ( varcase x.DefSort of
	 [| ShortHand=t.
              let def = AnalyseTypTerm(t.SynBinding,Env.Typ,
                                            x.TypVarEnv,true,false)
               in  Do( Unify( def, !t.TypBinding ) );
	    Isomorphism=(| Constrs=l; Extensible=extable; Extending=extending |).

             let n=length l
	     % start is the first constructor number for flagging %
	     % now need to flag this type as extensible if necessary by %
	     % updating the int ref of constructors declared so far	%
             enc (start,max,Extensible:int ref opt) = if extending Or extable then
			      (let (old,m) = RetrieveTypIde(x.Bind,Env.Typ)
			      % should TypEnv be something else??? %
			      enc oldoper = repTypTerm'(old) as TypAbsOper
				   ?? [`As`] (outtok `can only extend datatypes`;
					 ShowErrorContext(); PrintLn();
					 ReEnter())
			      enc nc =  max(!oldoper.AbsInfo.Extensible,
					    StartExtensibleFrom)
			      enc _ =  oldoper.AbsInfo.Extensible := nc
			 in (nc,nc+n,[|present=oldoper.AbsInfo.Extensible|]) )
			 else (0,n,[|absent|])
	     % retrieval reqd, extable to tag %
	     % new flag constructors without optimisation labelling %
	     % contructors from last count			    %
	     enc FlagConstructors(l: SynDataDef' list): void =
	     %RJG 09-Feb-89 all extensible datatype constructors now%
	     %are labelled as xcon type constructors with xcon      %
	     %pointing to the Extensible flag in TypTerm' for use in%
	     %mlcomp.ml%
	       let size = if extending Or extable then MaxInt else 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,max,impappl);
                          n+1))
                    (map (\q. (q, if ValueSet(!q.ConstrArgType).Pointer
                              then [|pointer|] else [|zero|])) l)
                    0)
		   else %RJG 09-Feb-89%
		   if size<MaxInt then
		    Do (revitlist (\q. \n. (let p = (q.AbsBinder.Constructor as yes)
                          enc (_,_,_,impappl) = !p
                          in p := ([|variant|],n,size,impappl);
                          n+1))
		    l start)
		   else %extensible%
		    Do (revitlist (\q. \n. (let p = (q.AbsBinder.Constructor as yes)
                          enc (_,_,_,impappl) = !p
			  enc xc = Extensible as present
			           ?? [`As`] failwith `AnalyseRecDecl:FlagConstructors`
                          in p := ([|xcon=xc|],n,size,impappl);
                          n+1))
		    l start)

	     %debugging%
%RJGDEL	     enc ListConstrs (l:SynDataDef' list) : void =%
%RJGDEL	     itlist (\(x:SynDataDef'). \y.let s = x.AbsBinder%
%RJGDEL			 enc (_,n,m,_) = !(s.Constructor as yes)%
%RJGDEL			 in (outtok(`Constr:`);outtok(repAtom' (s.Ide));%
%RJGDEL			     print n;outtok (`,`);print m;%
%RJGDEL			     ())) l ()%
	     
	     % in AnalyseDecl... %
	     in
              ( aplist((\h. Do (Unify(
                          AnalyseTypTerm(h.Term,Env.Typ,%{VAR}%x.TypVarEnv,true,extending Or extable),
                          !h.ConstrArgType))),
                       l);
                FlagConstructors(l))      %AM: note AFTER the Unify%
	 |];
	 x.TypVarEnv := NilEnv;
         aplist(FlagGenericVarsInNilEnv, !x.TypParams);
	 x.TypParams := []);
    SynDeclDefExcon=x. ();
    SynDeclAnd=x.
      ( AnalyseRecDecl(x.Lft,Env,IsoEnv,%VAR%TypVarEnv);
        AnalyseRecDecl(x.Rht,Env,IsoEnv,%VAR%TypVarEnv));
    SynDeclEnc=x.
      ( AnalyseRecDecl(x.Ext,Env,IsoEnv,%VAR%TypVarEnv);
        AnalyseRecDecl(x.Int,Env,IsoEnv,%VAR%TypVarEnv));
    SynDeclIns. failwith `AnalyseRecDecl`;
    SynDeclWith. failwith `AnalyseRecDecl`;
    SynDeclRec=x. AnalyseRecDecl(x.Rec,Env,IsoEnv,%VAR%TypVarEnv)

  |];
  PopPhrase() )

%%
%---------------------------------------- Bind %

and AnalyseBind(Bind': SynBind', Env: LocEnv' ref, OldEnv: LocEnv',
                TypEnv: LocTypEnv', 
		TypVarEnv: TypVarEnv' ref,
                BoundByLambda: bool, LastUse): TypTerm' =
  let rec AnalyseBindPart(Bind': SynBind'): TypTerm' =
  let _ = PushPhrase[|Bind=Bind'|]
  enc Result =
  varcase (repSynBind' Bind') of
  [| SynBindIde=(|Ide; Binder; PreBinder|).
      let p: (TypTerm'#SynBindIde') opt =
          (let CheckAtomic(id) =
           failwith `SynBindConst` 
           enc (a,b,_,_)=
               RetrieveVal(Binder.Ide, OldEnv, CheckAtomic)
           in case b.Constructor of
              [| yes=p. let (_,_,_,impappl) = !p in
                        if impappl then [|present=(a,b)|]
                        else (
                          outstring(`***Warning: Constructor used as `);
                          outstring(`variable in pattern:  `);
                          PrintAtom Ide; PrintLn();
                          [|absent|]);
                 no. [|absent|]
	      |]
	  ) ?? [`SynBindConst`] [| absent |]
      in case p of
      [|absent. 
           let Typ = GenTypVar(false,false,false,MaxInt,true) in (
           Env:=AllocAndCheckEnv(Binder,Typ,!Env,OldEnv,BoundByLambda);
           LastUse := (Binder,ref []) :: !LastUse;
           Typ);
        present=(Typ,Binder).
          (PreBinder := [|present=Binder|];
           FreshType(Typ))
      |];
    SynBindAny.   GenTypVar(false,false,false,MaxInt,true);
    SynBindConst=c.   AnalyseConst(c);
    SynBindTuple=x.
        AllocTypTuple(map AnalyseBindPart x);
    SynBindBoth=(x,y).
        Unify(AnalyseBindPart x, AnalyseBindPart y);
    SynBindAppl=x.
      let (Typ, Binder, _, _) = RetrieveVal(x.Ide, OldEnv, 
                                            UnboundVar)
      enc IdeType = FreshType(Typ)
      enc Typ = case Binder.Constructor of
      [| no. UnboundConstructor(x.Ide);
         yes=p. IdeType |]
      enc ArgTyp = AnalyseBindPart(x.Arg)
      enc ResTyp = GenTypVar(false,false,false,MaxInt,true) in (
      Do (Unify(Typ, AllocTypFun(ArgTyp,ResTyp)));
      x.Binder := Binder;
      ResTyp);
    SynBindRecord=(x,y).
      if y is solid
      then
        let {rec AnalyseBindRecFields(Bind': SynBindRecord' list): TypTagList' =
        if null(Bind') then [] else
        ( let (| RecKey; RecField |) = hd(Bind') in
          let RecType = AnalyseBindPart(RecField) in
          AllocTypTagList(RecKey,RecType,AnalyseBindRecFields(tl(Bind'))))}
        in AllocTypRecord[|Solid=AnalyseBindRecFields(x)|]
      else 
        let {rec AnalyseBindRecFields(Bind': SynBindRecord' list):TypTagDList' =
        if null(Bind') then dnil else
        ( let (| RecKey; RecField |) = hd(Bind') in
          let RecType = AnalyseBindPart(RecField) in
          AllocTypTagDList(RecKey,RecType,AnalyseBindRecFields(tl(Bind'))))}
        enc rectyp = AllocTypRecord[|Flexi=AnalyseBindRecFields(x)|]
        in ((y as flexi) := (SolidTagList(x,rectyp,[|Bind=Bind'|])); rectyp);
    SynBindVariant=x.
      ( let Typ=
          AllocTypVariant[|Flexi=
            AllocTypTagDList(x.VarKey, AnalyseBindPart(x.VarField), dnil)|]
        in ( x.VarPos:=TagPosition(Typ,[|Bind=Bind'|]);
             Typ));
    SynBindForce=x.
        Unify(AnalyseTypTerm(x.ForceType,TypEnv,%{VAR}%TypVarEnv,false,false),
		AnalyseBindPart(x.ForceBind))
  |]
  enc _ = PopPhrase()
  in  Result

  in AnalyseBindPart(Bind')

and AnalyseBind2(Bind': SynBind', AllEnv: LocAllEnv',
                 TypVarEnv: TypVarEnv' ref,
                 BoundByLambda: bool): (TypTerm' # LocAllEnv') =
( let NewValEnv = ref (AllEnv.Val) in
  let y = AnalyseBind(Bind', NewValEnv, AllEnv.Val, AllEnv.Typ, 
                      TypVarEnv, BoundByLambda, AllEnv.LastUse) in
  (y, (|Val= !NewValEnv; Typ=AllEnv.Typ; 
        LastUse= AllEnv.LastUse |) ))

}

%%
%---------------------------------------- Analyse - main entry point %
ins Analyse(Decl: SynDecl'): LocAllEnv' =
( AnalysisLevel:=0;
  ClearPhrase();
  let OldEnv = (| Val=NilEnv; Typ=NilEnv; LastUse= ref [] |)
  and TypVarEnv = (ref NilEnv):TypVarEnv' ref in
  let NewEnv = AnalyseDecl2(Decl,OldEnv,TypVarEnv) in
    (ClearPhrase(); 
       TidyLocEnv(NewEnv) ) );


%---------------------------------------- Initial environment entry point %

let StkPos = ref 0                             %AM: this is a hacked fix!%
enc DefineIde(Bind': SynBindIde', Typ: TypTerm'): TypTerm' =
  ( let Typ2 = FreshType(Typ) in (
    Bind'.StkPosn := [|Local = !StkPos|];       %AM: hack%
    StkPos := !StkPos + 1;
    FlagGenericVarsInNilEnv(Typ2);
    Typ2))

ins SetupEnvironment(l: (SynBindIde' # TypTerm') list): LocEnv' =
( let Env = ref (NilEnv: LocEnv') in
  let SetupIde(Bind',Typ) =
     Env:=AllocAndCheckEnv(Bind', DefineIde(Bind',Typ), !Env, NilEnv, false)
  in (AppList SetupIde l;
      !Env))

and SetupTypEnvironment(): LocTypEnv' =
( let TypEnv = ref (NilEnv: LocTypEnv') in
  let DefineTyp(Nam: Atom', Typ: TypTerm', Multi: bool): void =
    TypEnv:=AllocTypEnv(Nam,Typ,Multi,!TypEnv)
  and NewVar() = GenTypVar(true,false,false,MaxInt,true) in (
  DefineTyp(AtomUnit,AllocTypUnit,false);
  DefineTyp(AtomCross,AllocTypUnit,true);
  DefineTyp(AtomArrow,AllocTypFun(NewVar(),NewVar()),false);
  !TypEnv
))

ins InitLocAllEnv1(v: (SynBindIde' # TypTerm') list
		      %RJGDEL e: (SynBindIde' # TypTerm') list% ): LocAllEnv' =
( StkPos := 0;
  let Val=SetupEnvironment(v)
  and Typ=SetupTypEnvironment()
  in  TidyLocEnv(|Val;Typ;LastUse= ref [] |))
and InitLocAllEnv2(v: (SynBindIde' # TypTerm') list
): LocAllEnv' =
( StkPos := 0;
  let Val=SetupEnvironment(v)
  and Typ=NilEnv
  in  TidyLocEnv(|Val;Typ;LastUse= ref [] |));

let InitTypConstructors =
  (| TypVar = \(). GenTypVar(true,false,false,MaxInt,true);
     EtyTypVar = \(). GenTypVar(true,false,true,MaxInt,true);
     Unit=AllocTypUnit;
     Cross = \(x,y). AllocTypTuple([x;y]);
     Arrow = AllocTypFun
 |);

