#include "tpl_os_kernel.h"          /* tpl_schedule */
#include "tpl_os_timeobj_kernel.h"  /* tpl_counter_tick */
#include "tpl_machine_interface.h"  /* tpl_switch_context_from_it */

#define OS_START_SEC_CODE
#include "tpl_memmap.h"
%

foreach interrupt in INTERRUPT do
  let counterFct := @( )
  foreach counter in HARDWARECOUNTERS do
    if counter::SOURCE == interrupt::NAME then
      let counterFct += counter::NAME
    end if
  end foreach
  foreach counter in counterFct
    before
%
FUNC(void, OS_CODE) Ack% ! interrupt::NAME %(void){}

FUNC(void, OS_CODE) tpl_tick_% ! interrupt::NAME %()
{
%
    do
      %  tpl_counter_tick(&% !counter::VALUE %_counter_desc);
%
    after %
  Ack% ! interrupt::NAME %();
  if (tpl_kern.need_schedule)
  {
    tpl_schedule_from_running();
  }
}
%
  end foreach
end foreach
%
#define OS_STOP_SEC_CODE
#include "tpl_memmap.h"