//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at Sun 20-Jul-2003 by the VDM-SL to C++ Code Generator
// (v3.7.7 - Thu 02-Jan-2003)
//
// Supported compilers:
// 	gcc version 2.95.2 on Sun Solaris 2.6, Linux, HP-UX10
// 	VC++ version 6.0 on Windows98, Windows NT
//



#include "mixed_ustack.h"



TYPE_mixed_ustack_IntStackNode &TYPE_mixed_ustack_IntStackNode::Init (Int p1, TYPE_mixed_ustack_IntStack p2) {  SetField(1, p1);
  SetField(2, p2);
  return * this;

}


Int TYPE_mixed_ustack_IntStackNode::get_Content () const {
  return (Int) GetField(1);
}


void TYPE_mixed_ustack_IntStackNode::set_Content (const Int &p) {  SetField(1, p);
}


TYPE_mixed_ustack_IntStack TYPE_mixed_ustack_IntStackNode::get_Next () const {
  return (TYPE_mixed_ustack_IntStack) GetField(2);
}


void TYPE_mixed_ustack_IntStackNode::set_Next (const TYPE_mixed_ustack_IntStack &p) {  SetField(2, p);
}


void init_mixed_ustack_VDMLib () {  VDMGetDefaultRecInfoMap().NewTag(TAG_TYPE_mixed_ustack_IntStackNode, 2);
  VDMGetDefaultRecInfoMap().SetSymTag(TAG_TYPE_mixed_ustack_IntStackNode, L"mixed_ustack`IntStackNode");
  AddRecordTag(L"mixed_ustack`IntStackNode", TAG_TYPE_mixed_ustack_IntStackNode);
  VDMGetDefaultRecInfoMap().NewTag(TOKEN, 1);
  VDMGetDefaultRecInfoMap().SetSymTag(TOKEN, L"token");

}

#ifdef DEF_mixed_ustack_USERIMPL

#include "mixed_ustack_userimpl.cc"


#endif


void init_mixed_ustack () {  init_mixed_ustack_VDMLib();
}

#ifndef DEF_mixed_ustack_Pop

TYPE_mixed_ustack_IntStack vdm_mixed_ustack_Pop (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S) {  Generic varRes_2;

  if (vdm_mixed_ustack_S.IsRecord()) 

    if (((Record) vdm_mixed_ustack_S).Is(vdm_mixed_ustack_IntStackNode)) 
      varRes_2 = ((Record) vdm_mixed_ustack_S).GetField(pos_mixed_ustack_IntStackNode_Next);
    else 
      RunTime(L"Run-Time Error:Unknown record field selector");
  else 
    RunTime(L"Run-Time Error:A record was expected");
  return (Generic) varRes_2;

}

#endif

#ifndef DEF_mixed_ustack_pre_Pop

Bool vdm_mixed_ustack_pre_Pop (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S) {
  return (Generic) (Bool) !(vdm_mixed_ustack_S == Nil());
}

#endif

#ifndef DEF_mixed_ustack_post_Pop

Bool vdm_mixed_ustack_post_Pop (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S, const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_RESULT) {  Bool varRes_3;
  bool tmpQuant_4 = false;
  NotSupported(L"The construct is not supported: type bind");
  varRes_3 = (Bool) tmpQuant_4;
  return (Generic) varRes_3;

}

#endif

#ifndef DEF_mixed_ustack_Top

Int vdm_mixed_ustack_Top (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S) {  Int varRes_2;

  if (vdm_mixed_ustack_S.IsRecord()) 

    if (((Record) vdm_mixed_ustack_S).Is(vdm_mixed_ustack_IntStackNode)) 
      varRes_2 = ((Record) vdm_mixed_ustack_S).GetField(pos_mixed_ustack_IntStackNode_Content);
    else 
      RunTime(L"Run-Time Error:Unknown record field selector");
  else 
    RunTime(L"Run-Time Error:A record was expected");
  return (Generic) varRes_2;

}

#endif

#ifndef DEF_mixed_ustack_pre_Top

Bool vdm_mixed_ustack_pre_Top (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S) {
  return (Generic) (Bool) !(vdm_mixed_ustack_S == Nil());
}

#endif

#ifndef DEF_mixed_ustack_post_Top

Bool vdm_mixed_ustack_post_Top (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S, const Int &vdm_mixed_ustack_RESULT) {  Bool varRes_3;
  bool tmpQuant_4 = false;
  NotSupported(L"The construct is not supported: type bind");
  varRes_3 = (Bool) tmpQuant_4;
  return (Generic) varRes_3;

}

#endif

#ifndef DEF_mixed_ustack_Push

TYPE_mixed_ustack_IntStack vdm_mixed_ustack_Push (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S, const Int &vdm_mixed_ustack_E) {  Record varRes_3(vdm_mixed_ustack_IntStackNode, length_mixed_ustack_IntStackNode);
  varRes_3 = Record(vdm_mixed_ustack_IntStackNode, length_mixed_ustack_IntStackNode);
  varRes_3.SetField(1, vdm_mixed_ustack_E);
  varRes_3.SetField(2, vdm_mixed_ustack_S);
  return (Generic) varRes_3;

}

#endif

#ifndef DEF_mixed_ustack_pre_Push

Bool vdm_mixed_ustack_pre_Push (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S, const Int &vdm_mixed_ustack_E) {
  return (Generic) (Bool) true;
}

#endif

#ifndef DEF_mixed_ustack_post_Push

Bool vdm_mixed_ustack_post_Push (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_S, const Int &vdm_mixed_ustack_E, const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_RESULT) {  Bool varRes_4;
  Record var2_6(vdm_mixed_ustack_IntStackNode, length_mixed_ustack_IntStackNode);
  var2_6 = Record(vdm_mixed_ustack_IntStackNode, length_mixed_ustack_IntStackNode);
  var2_6.SetField(1, vdm_mixed_ustack_E);
  var2_6.SetField(2, vdm_mixed_ustack_S);
  varRes_4 = (Bool) (vdm_mixed_ustack_RESULT == var2_6);
  return (Generic) varRes_4;

}

#endif

#ifndef DEF_mixed_ustack_Empty

TYPE_mixed_ustack_IntStack vdm_mixed_ustack_Empty () {
  return (Generic) Nil();
}

#endif

#ifndef DEF_mixed_ustack_pre_Empty

Bool vdm_mixed_ustack_pre_Empty () {
  return (Generic) (Bool) true;
}

#endif

#ifndef DEF_mixed_ustack_post_Empty

Bool vdm_mixed_ustack_post_Empty (const TYPE_mixed_ustack_IntStack &vdm_mixed_ustack_RESULT) {
  return (Generic) (Bool) (vdm_mixed_ustack_RESULT == Nil());
}

#endif