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)

Included definitions

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

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


  Definition TSignature: Set := TShortName × list TType.

  Definition TQualifiedMethodName: Set := TClassName × TSignature.


  Definition TVar := N.

  Definition PVar_eqDec: eqDecS TVar := N_eqDec.

  Definition varFromNat: natTVar := N.of_nat.

  Definition varToNat: TVarnat := N.to_nat.
  Definition PvarNat: var, varFromNat (varToNat var) = var :=
  Definition PnatVar: n, varToNat (varFromNat n) = n :=

  Definition nextVar: TVarTVar :=

  Lemma PnextVarSucc: var, varToNat (nextVar var) = S (varToNat var).
    apply N2Nat.inj_succ.


  Module M_Var_as_OT
    := N_as_OT.

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