[Parameterised the compiler correctness statement on the source semantics.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081103094831
 + Placed the current (partial) compiler correctness proof, which uses
   the big-step semantics, under Semantics.BigStep.
] adddir ./Semantics/BigStep
move ./CompilerCorrectness ./Semantics/BigStep/CompilerCorrectness
hunk ./CompilerCorrectness.agda 5
-module CompilerCorrectness where
+-- The compiler correctness statement is parameterised on a source
+-- language semantics.
hunk ./CompilerCorrectness.agda 8
+open import Semantics
+
+module CompilerCorrectness (S : Sem) where
+
+open Sem S
hunk ./CompilerCorrectness.agda 14
-open import Semantics.BigStep
hunk ./CompilerCorrectness.agda 15
-import Bar; open Bar _⟶_
-open import Infinite
hunk ./CompilerCorrectness.agda 16
-open import Data.Star
hunk ./CompilerCorrectness.agda 17
-open import Data.Colist
hunk ./CompilerCorrectness.agda 18
-open import Data.Unit
hunk ./CompilerCorrectness.agda 20
-infix 4 _⟶⋆_
-
--- Reflexive transitive closure.
-
-_⟶⋆_ : State -> State -> Set
-_⟶⋆_ = Star _⟶_
-
--- "Infinite closure".
-
-_⟶∞ : State -> Set
-_⟶∞ = Infinite _⟶_
-
hunk ./CompilerCorrectness.agda 25
-  throws  : e ↯[ i ]       -> Matches e i ⟪ i , [] ⟫
+  throws  : e ⇓[ i ] throw -> Matches e i ⟪ i , [] ⟫
hunk ./CompilerCorrectness.agda 28
--- starting one (according to _⇓[_]_). Furthermore, if no final state
--- is reached, then the original expression can loop.
+-- starting one. Furthermore, if no final state is reached, then the
+-- original expression can loop.
hunk ./Everything.agda 12
+-- An abstract specification of a semantics.
+
+import Semantics
+
hunk ./Everything.agda 60
--- Statement of compiler correctness. Uses the big-step semantics.
+-- Statement of compiler correctness.
hunk ./Everything.agda 64
--- Proof of compiler correctness.
+-- Proof of compiler correctness (uses the big-step semantics).
hunk ./Everything.agda 66
-import CompilerCorrectness.Completeness
-import CompilerCorrectness.BarTheorem
-import CompilerCorrectness.Soundness  -- Currently contains postulate.
-import CompilerCorrectness.Proof
+import Semantics.BigStep.CompilerCorrectness.Completeness
+import Semantics.BigStep.CompilerCorrectness.BarTheorem
+import Semantics.BigStep.CompilerCorrectness.Soundness  -- Currently contains postulate.
+import Semantics.BigStep.CompilerCorrectness.Proof
addfile ./Semantics.agda
hunk ./Semantics.agda 1
+------------------------------------------------------------------------
+-- An abstract specification of a semantics
+------------------------------------------------------------------------
+
+module Semantics where
+
+open import Syntax
+
+-- I don't assume any properties of the semantics.
+
+record Sem : Set1 where
+  field
+    -- x ⇓[ i ] v means that x _can_ terminate with the value (or
+    -- exception) v.
+    _⇓[_]_ : forall {t} -> Expr t -> Status -> Value -> Set
+
+    -- x ⇑[ i ] means that x _can_ fail to terminate.
+    _⇑[_] : forall {t} -> Expr t -> Status -> Set
hunk ./Semantics/BigStep.agda 8
+open import Semantics
hunk ./Semantics/BigStep.agda 67
+
+-- The semantics.
+
+BigStep : Sem
+BigStep = record
+  { _⇓[_]_ = _⇓[_]_
+  ; _⇑[_]  = _⇑[_]
+  }
hunk ./Semantics/BigStep/CompilerCorrectness/BarTheorem.agda 5
-module CompilerCorrectness.BarTheorem where
+module Semantics.BigStep.CompilerCorrectness.BarTheorem where
hunk ./Semantics/BigStep/CompilerCorrectness/BarTheorem.agda 10
-open import CompilerCorrectness
+import CompilerCorrectness as CC; open CC BigStep
hunk ./Semantics/BigStep/CompilerCorrectness/Completeness.agda 5
-module CompilerCorrectness.Completeness where
+module Semantics.BigStep.CompilerCorrectness.Completeness where
hunk ./Semantics/BigStep/CompilerCorrectness/Completeness.agda 10
-open import CompilerCorrectness
+import CompilerCorrectness as CC; open CC BigStep
hunk ./Semantics/BigStep/CompilerCorrectness/Proof.agda 5
-module CompilerCorrectness.Proof where
+module Semantics.BigStep.CompilerCorrectness.Proof where
hunk ./Semantics/BigStep/CompilerCorrectness/Proof.agda 8
-open import CompilerCorrectness
-open import CompilerCorrectness.Completeness
-open import CompilerCorrectness.Soundness
+open import Semantics.BigStep
+import CompilerCorrectness as CC; open CC BigStep
+open import Semantics.BigStep.CompilerCorrectness.Completeness
+open import Semantics.BigStep.CompilerCorrectness.Soundness
hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 6
-module CompilerCorrectness.Soundness where
+module Semantics.BigStep.CompilerCorrectness.Soundness where
hunk ./Semantics/BigStep/CompilerCorrectness/Soundness.agda 13
-open import CompilerCorrectness
-open import CompilerCorrectness.BarTheorem
+import CompilerCorrectness as CC; open CC BigStep
+open import Semantics.BigStep.CompilerCorrectness.BarTheorem
hunk ./Semantics/SmallStep.agda 8
+open import Semantics
hunk ./Semantics/SmallStep.agda 176
+-- The semantics.
+
+SmallStep : Sem
+SmallStep = record
+  { _⇓[_]_ = \x i v -> x ˢ ⟶⋆[ i ] done v
+  ; _⇑[_]  = \x i   -> x ˢ ⟶∞[ i ]
+  }
+
hunk ./VirtualMachine.agda 15
+open import Infinite
hunk ./VirtualMachine.agda 92
+infix 4 _⟶⋆_
+
+-- Reflexive transitive closure.
+
+_⟶⋆_ : State -> State -> Set
+_⟶⋆_ = Star _⟶_
+
+-- "Infinite closure".
+
+_⟶∞ : State -> Set
+_⟶∞ = Infinite _⟶_
+