Module Counter

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.

Open Scope nat_scope.

Definition counter := PMap.t nat.

Definition init_counter : counter := PMap.init 0.

Definition reset_counters (filter:list node) (cs : counter) : counter :=
    List.fold_right (fun n cs0 => cs0 # n <- 0) cs filter.

Definition inc_counter (n : node) (cs : counter) : counter :=
  cs # n <- (cs !! n + 1).

Lemma init_counters_zero:
  forall n,
    init_counter # n = 0.