Library ProgramStructuresImpl

An implementation of PROGRAM_STRUCTURES based on natural numbers. @author Patryk Czarnik

Require Import NArith.
Require Import FSets.FMaps.
Require Import FSets.FMapAVL.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.

Implementation of PROGRAM_STRUCTURES

This functor provides an implementation of PROGRAM_STRUCTURES signature, where basic values, such as PCs, variable indices, or names are implemented as natural numbers.

See signature for documentation of module fields.

Module ProgramStructuresImpl
    (_ValuesAndTypes : VALUES_AND_TYPES)
    <: PROGRAM_STRUCTURES_WITH_MAP
    <: PROGRAM_STRUCTURES.

Included definitions

  Open Local Scope type_scope.
  Module M_ValuesAndTypes := _ValuesAndTypes.
  Import _ValuesAndTypes.

  Lemma N_eqDec: eqDecS N.
  Proof.
    unfold eqDecS.
    unfold propDecS.
    decide equality.
    decide equality.
  Qed.

Names

Definition TSignature: Set := TShortName × list TType.

Definition TQualifiedMethodName: Set := TClassName × TSignature.

Var

  Definition TVar := N.

  Definition PVar_eqDec: eqDecS TVar := N_eqDec.

  Definition varFromNat: nat → TVar := N.of_nat.

  Definition varToNat: TVar → nat := N.to_nat.
  Definition PvarNat: ∀ var, varFromNat (varToNat var) = var := N2Nat.id.
  Definition PnatVar: ∀ n, varToNat (varFromNat n) = n := Nat2N.id.

  Definition nextVar: TVar → TVar :=
    N.succ.

  Lemma PnextVarSucc: ∀ var, varToNat (nextVar var) = S (varToNat var).
  Proof.
    intros.
    apply N2Nat.inj_succ.
  Qed.

Maps

  Module M_Var_as_OT
    := N_as_OT.

  Module M_VarMap
    := Make(M_Var_as_OT).
End ProgramStructuresImpl.