------------------------------------------------------------------------
-- Imports all the other modules
------------------------------------------------------------------------

module Everything where

-- The syntax of a simple language with exceptions and interrupts
-- (asynchronous exceptions).

import Syntax

-- An abstract specification of a semantics.

import Semantics

-- Big-step semantics.

import Semantics.BigStep

-- Infinite transition sequences, used by the small-step semantics.

import Infinite

-- Small-step semantics.

import Semantics.SmallStep
import Semantics.SmallStep.EvalCtxt

-- The two semantics are equivalent.

import Semantics.Equivalence
import Semantics.Equivalence.Lemmas

-- Definition of equivalence between two expressions. Uses the
-- big-step semantics.

import Equivalence

-- Some properties related to totality.

import Totality

-- Lemmas about the interrupt-block status.

import StatusLemmas

--  Some simple algebraic properties.

import AlgebraicProperties

-- A virtual machine and a compiler.

import VirtualMachine

-- The bar relation, used to state compiler correctness.

import Bar

-- Statement of compiler correctness.

import CompilerCorrectness

-- Proof of compiler correctness for the big-step semantics. One part
-- of this proof makes use of the small-step semantics.

import Semantics.BigStep.CompilerCorrectness.Completeness
import Semantics.BigStep.CompilerCorrectness.BarTheorem
import Semantics.BigStep.CompilerCorrectness.Soundness
import Semantics.BigStep.CompilerCorrectness

-- Partial proof of compiler correctness for the small-step semantics.

import Semantics.SmallStep.CompilerCorrectness.Soundness