Library AllStructures

Require Import List.
Require Import Common.
Require Import Program.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import Heap.
Require Import ValuesNTypes.
Require Import ArithOps.
Require Import Arithmetic.

It is a technical module that groups together all modules which provide basic definitions required for semantics formalisation. All modules with semantics definition should depend on the same instance of this module.

@author Patryk Czarnik

Module Type ALL_STRUCTURES.
  Declare Module M_RuntimeStructures : RUNTIME_STRUCTURES.
  Declare Module M_Program : PROGRAM_W_CONSTRUCTORS
    with Module M_ProgramStructures := M_RuntimeStructures.M_Heap.M_ProgramStructures.
  Declare Module M_Arithmetics: ARITHMETICS M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Module M_ProgramStructuresFacts := ProgramStructuresFacts M_Program.M_ProgramStructures.
  Module M_RuntimeStructuresFacts := RuntimeStructuresFacts M_RuntimeStructures.
  Module M_HeapFacts := HeapFacts M_RuntimeStructures.M_Heap.
End ALL_STRUCTURES.