[Tried to simplify the small-step semantics.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080612215911
 + This variant only allows interrupts at redex positions. Infinite
   sequences of interrupts are not possible, since interrupts are
   immediately taken care of by the innermost exception handler (if
   any).
 + However, the presence of such non-small steps has an unwanted
   effect: the lift⟶ lemma is not valid. I think that it can be awkward
   to work with a semantics without this lemma.
] hunk ./Infinite.agda 5
-open import Relation.Binary
-
-module Infinite {S : Set} (_⟶_ : Rel S) where
+module Infinite where
hunk ./Infinite.agda 7
+open import Relation.Binary
hunk ./Infinite.agda 9
-open import Data.Function
hunk ./Infinite.agda 12
-infix  4 _⟶∞
hunk ./Infinite.agda 13
--- x ⟶∞ means that there is an infinite transition sequence starting
--- at x.
+-- Infinite _⟶_ x means that there is an infinite transition sequence
+-- starting at x.
hunk ./Infinite.agda 16
-codata _⟶∞ (x : S) : Set where
-  _◅∞_ : forall {y} -> x ⟶ y -> y ⟶∞ -> x ⟶∞
+codata Infinite {S : Set} (_⟶_ : Rel S) (x : S) : Set where
+  _◅∞_ : forall {y} -> x ⟶ y -> Infinite _⟶_ y -> Infinite _⟶_ x
hunk ./Infinite.agda 21
-_loops : forall {x} -> x ⟶ x -> x ⟶∞
+_loops : forall {S _⟶_} {x : S} -> x ⟶ x -> Infinite _⟶_ x
hunk ./Infinite.agda 24
-_◅◅∞_ : forall {x y} -> x ⟨ Star _⟶_ ⟩₁ y -> y ⟶∞ -> x ⟶∞
+_◅◅∞_ : forall {S _⟶_} {x y : S} ->
+        Star _⟶_ x y -> Infinite _⟶_ y -> Infinite _⟶_ x
hunk ./Infinite.agda 29
-map∞ : (F : S -> S) -> (forall {x y} -> x ⟶ y -> F x ⟶ F y) ->
-       forall {x} -> x ⟶∞ -> F x ⟶∞
+map∞ : forall {S₁ S₂} {R₁ : Rel S₁} {R₂ : Rel S₂}
+       (F : S₁ -> S₂) -> R₁ =[ F ]⇒ R₂ ->
+       forall {x} -> Infinite R₁ x -> Infinite R₂ (F x)
hunk ./Semantics/SmallStep.agda 7
-open import Syntax hiding (⌜_⌝; _<_>_)
-import Infinite
+open import Syntax
+open import Infinite
hunk ./Semantics/SmallStep.agda 11
+open import Data.Product
hunk ./Semantics/SmallStep.agda 16
--- Expressions locally annotated with interrupt status
+-- Redexes
hunk ./Semantics/SmallStep.agda 18
-infixl 7 _⊕_
-infixr 5 _catch_
-infixl 4 _>>_
-infix  3 _^_
-
-mutual
-
-  data AnnExpr t : Set where
-    _^_ : (x : AnnExpr' t) (i : Status) -> AnnExpr t
-
-  data AnnExpr' : Totality -> Set where
-    val     : forall {t} (n : ℕ) -> AnnExpr' t
-    throw   : forall {t} -> AnnExpr' t
-    loop    : AnnExpr' partial
-    _⊕_     : forall {t} (x y : AnnExpr t) -> AnnExpr' t
-    _>>_    : forall {t} (x : AnnExpr t) (y : Expr t) -> AnnExpr' t
-    _catch_ : forall {t} (x : AnnExpr t) (y : Expr t) -> AnnExpr' t
-    block   : forall {t} (x : Expr t) -> AnnExpr' t
-    unblock : forall {t} (x : Expr t) -> AnnExpr' t
-
--- The outermost status.
-
-status : forall {t} -> AnnExpr t -> Status
-status (x ^ i) = i
-
--- The initial annotation of an expression.
-
-mutual
-
-  annotate : forall {t} -> Expr t -> Status -> AnnExpr t
-  annotate x i = annotate' x i ^ i
-
-  annotate' : forall {t} -> Expr t -> Status -> AnnExpr' t
-  annotate' (val n)     i = val n
-  annotate' throw       i = throw
-  annotate' loop        i = loop
-  annotate' (x ⊕ y)     i = annotate x i ⊕  annotate y i
-  annotate' (x >> y)    i = annotate x i >>    y
-  annotate' (x catch y) i = annotate x i catch y
-  annotate' (block x)   i = block   x
-  annotate' (unblock x) i = unblock x
-
--- Removes the annotations.
-
-mutual
-
-  unannotate : forall {t} -> AnnExpr t -> Status -> Expr t
-  unannotate (x ^ U) B = unblock (unannotate' x U)
-  unannotate (x ^ B) U = block   (unannotate' x B)
-  unannotate (x ^ U) U = unannotate' x U
-  unannotate (x ^ B) B = unannotate' x B
-
-  unannotate' : forall {t} -> AnnExpr' t -> Status -> Expr t
-  unannotate' (val n)     i = val n
-  unannotate' throw       i = throw
-  unannotate' loop        i = loop
-  unannotate' (x ⊕ y)     i = unannotate x i ⊕ unannotate y i
-  unannotate' (x >> y)    i = unannotate x i >>    y
-  unannotate' (x catch y) i = unannotate x i catch y
-  unannotate' (block x)   i = block   x
-  unannotate' (unblock x) i = unblock x
-
-⌜_⌝ : forall {t} -> Value -> AnnExpr' t
-⌜ val n ⌝ = val n
-⌜ throw ⌝ = throw
+data Redex : forall {t} -> Expr t -> Set where
+  Loop    :                   Redex     loop
+  Add₁    : forall {t} m v -> Redex {t} (val m ⊕ ⌜ v ⌝)
+  Add₂    : forall {t} y   -> Redex {t} (throw ⊕ y)
+  Seqn    : forall {t} v y -> Redex {t} (⌜ v ⌝ >> y)
+  Catch   : forall {t} v y -> Redex {t} (⌜ v ⌝ catch y)
+  Block   : forall {t} v   -> Redex {t} (block   ⌜ v ⌝)
+  Unblock : forall {t} v   -> Redex {t} (unblock ⌜ v ⌝)
hunk ./Semantics/SmallStep.agda 35
-    _∶_⟶ʳ_ : forall t -> AnnExpr t -> AnnExpr t -> Set
+    _∶_⟶ʳ_ : forall t {e : Expr t} -> Redex e -> Expr t -> Set
hunk ./Semantics/SmallStep.agda 38
-  data _⟶ʳ_ : forall {t} -> AnnExpr t -> AnnExpr t -> Set where
-    Loop    : forall {i}           ->     loop                      ^ i ⟶ʳ loop        ^ i
-    Add₁    : forall {t i j k m n} -> t ∶ (val m ^ j) ⊕ (val n ^ k) ^ i ⟶ʳ val (m + n) ^ i
-    Add₂    : forall {t i j y}     -> t ∶ (throw ^ j) ⊕ y           ^ i ⟶ʳ throw       ^ i
-    Add₃    : forall {t i j k m}   -> t ∶ (val m ^ j) ⊕ (throw ^ k) ^ i ⟶ʳ throw       ^ i
-    Seqn₁   : forall {t i j m y}   -> t ∶ (val m ^ j) >> y          ^ i ⟶ʳ annotate y i
-    Seqn₂   : forall {t i j y}     -> t ∶ (throw ^ j) >> y          ^ i ⟶ʳ throw       ^ i
-    Catch₁  : forall {t i j m y}   -> t ∶ (val m ^ j) catch y       ^ i ⟶ʳ val m       ^ i
-    Catch₂  : forall {t i j y}     -> t ∶ (throw ^ j) catch y       ^ i ⟶ʳ annotate y B
-    Int     : forall {t x}         -> t ∶ x                         ^ U ⟶ʳ throw       ^ B
-    Block   : forall {t i x}       -> t ∶ block   x                 ^ i ⟶ʳ annotate x B
-    Unblock : forall {t i x}       -> t ∶ unblock x                 ^ i ⟶ʳ annotate x U
+  data _⟶ʳ_ : forall {t} {e : Expr t} -> Redex e -> Expr t -> Set where
+    Loop    :                       Loop            ⟶ʳ loop
+    Add₁    : forall {t m n} -> t ∶ Add₁ m (val n)  ⟶ʳ val (m + n)
+    Add₂    : forall {t y}   -> t ∶ Add₂ y          ⟶ʳ throw
+    Add₃    : forall {t m}   -> t ∶ Add₁ m throw    ⟶ʳ throw
+    Seqn₁   : forall {t m y} -> t ∶ Seqn  (val m) y ⟶ʳ y
+    Seqn₂   : forall {t y}   -> t ∶ Seqn  throw   y ⟶ʳ throw
+    Catch₁  : forall {t m y} -> t ∶ Catch (val m) y ⟶ʳ val m
+    Catch₂  : forall {t y}   -> t ∶ Catch throw   y ⟶ʳ block y
+    Block   : forall {t v}   -> t ∶ Block   v       ⟶ʳ ⌜ v ⌝
+    Unblock : forall {t v}   -> t ∶ Unblock v       ⟶ʳ ⌜ v ⌝
hunk ./Semantics/SmallStep.agda 53
--- Evaluation contexts.
+-- Evaluation contexts. Indexed on the status at the hole and the
+-- outermost status.
hunk ./Semantics/SmallStep.agda 56
-data EvalCtxt t : Set where
-  •           : EvalCtxt t
-  _•⊕_^_      : (E : EvalCtxt t) (y : AnnExpr t) (i : Status) -> EvalCtxt t
-  _•>>_^_     : (E : EvalCtxt t) (y : Expr    t) (i : Status) -> EvalCtxt t
-  _•catch_^_  : (E : EvalCtxt t) (y : Expr    t) (i : Status) -> EvalCtxt t
-  val_^_⊕•_^_ : (n : ℕ) (j : Status) (E : EvalCtxt t) (i : Status) ->
-                EvalCtxt t
+data EvalCtxt t : Status -> Status -> Set where
+  •        : forall {i} -> EvalCtxt t i i
+  _•<_>_   : forall {i j} (E : EvalCtxt t i j) (op : Op) (y : Expr t) ->
+             EvalCtxt t i j
+  val_⊕•_  : forall {i j} (m : ℕ) (E : EvalCtxt t i j) -> EvalCtxt t i j
+  block•   : forall {i j} (E : EvalCtxt t i B) -> EvalCtxt t i j
+  unblock• : forall {i j} (E : EvalCtxt t i U) -> EvalCtxt t i j
hunk ./Semantics/SmallStep.agda 68
-_[_] : forall {t} -> EvalCtxt t -> AnnExpr t -> AnnExpr t
-•                    [ y ] = y
-(E •⊕     x ^ i)     [ y ] = E [ y ] ⊕     x ^ i
-(E •>>    x ^ i)     [ y ] = E [ y ] >>    x ^ i
-(E •catch x ^ i)     [ y ] = E [ y ] catch x ^ i
-(val n ^ j ⊕• E ^ i) [ y ] = (val n ^ j) ⊕ E [ y ] ^ i
+_[_] : forall {t i j} -> EvalCtxt t i j -> Expr t -> Expr t
+•             [ y ] = y
+(E •< op > x) [ y ] = E [ y ] < op > x
+(val n ⊕• E)  [ y ] = val n ⊕ E [ y ]
+(block•   E)  [ y ] = block   (E [ y ])
+(unblock• E)  [ y ] = unblock (E [ y ])
hunk ./Semantics/SmallStep.agda 75
-------------------------------------------------------------------------
--- The semantics
+-- Composition of evaluation contexts.
hunk ./Semantics/SmallStep.agda 77
--- Single-step evaluation.
+infixr 10 _∘_
hunk ./Semantics/SmallStep.agda 79
-infix 2 _⟶_
+_∘_ : forall {t i j k} ->
+      EvalCtxt t j k -> EvalCtxt t i j -> EvalCtxt t i k
+•              ∘ E₂ = E₂
+(E₁ •< op > y) ∘ E₂ = (E₁ ∘ E₂) •< op > y
+(val n ⊕• E₁)  ∘ E₂ = val n ⊕• (E₁ ∘ E₂)
+block•   E₁    ∘ E₂ = block•   (E₁ ∘ E₂)
+unblock• E₁    ∘ E₂ = unblock• (E₁ ∘ E₂)
hunk ./Semantics/SmallStep.agda 87
-data _⟶_ {t} : AnnExpr t -> AnnExpr t -> Set where
-  reduction : forall {x y} (E : EvalCtxt t) ->
-              x ⟶ʳ y -> E [ x ] ⟶ E [ y ]
+-- Inverting a context (turning it outside-in).
hunk ./Semantics/SmallStep.agda 89
--- Reflexive transitive closure.
+status : forall {t i j} -> EvalCtxt t i j -> Status
+status {j = j} •     = j
+status (E •< op > y) = status E
+status (val m ⊕• E)  = status E
+status (block• E)    = B
+status (unblock• E)  = U
hunk ./Semantics/SmallStep.agda 96
-infix 2 _⟶⋆_
+infix 11 _⁻¹
hunk ./Semantics/SmallStep.agda 98
-_⟶⋆_ : forall {t} -> AnnExpr t -> AnnExpr t -> Set
-_⟶⋆_ = Star _⟶_
+_⁻¹ : forall {t i j} (E : EvalCtxt t i j) -> EvalCtxt t (status E) i
+•             ⁻¹ = •
+(E •< op > y) ⁻¹ = E ⁻¹ ∘ (• •< op > y)
+(val m ⊕• E)  ⁻¹ = E ⁻¹ ∘ (val m ⊕• •)
+block•   E    ⁻¹ = E ⁻¹ ∘ block• •
+unblock• E    ⁻¹ = E ⁻¹ ∘ unblock• •
hunk ./Semantics/SmallStep.agda 105
-module ⟶-Reasoning {t} = StarReasoning (_⟶_ {t})
+------------------------------------------------------------------------
+-- The semantics
hunk ./Semantics/SmallStep.agda 108
--- Infinite reduction sequences.
+-- Finds the innermost exception-handler in the evaluation context
+-- (which is assumed to have been inverted). The handler is returned
+-- in the appropriate context.
hunk ./Semantics/SmallStep.agda 112
-open module ⟶-Infinite {t} = Infinite (_⟶_ {t})
+unwind : forall {t i j} -> EvalCtxt t i j -> Expr t
+unwind •                  = throw     -- No exception handler.
+unwind (E •< |⊕| >     y) = unwind E
+unwind (E •< |>>| >    y) = unwind E
+unwind (E •< |catch| > y) = E ⁻¹ [ block y ]
+                            -- Interrupts are blocked in the handler.
+unwind (val m ⊕• E)       = unwind E
+unwind (block•   E)       = unwind E
+unwind (unblock• E)       = unwind E
hunk ./Semantics/SmallStep.agda 122
-------------------------------------------------------------------------
--- Some utility functions/lemmas
+-- Single-step evaluation.
hunk ./Semantics/SmallStep.agda 124
--- If we remove the annotations we get back the original expression.
+infix 2 _⟶[_]_
hunk ./Semantics/SmallStep.agda 126
-mutual
+data _⟶[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set where
+  Red : forall {t i j x} {r : Redex x} {y} (E : EvalCtxt t i j) ->
+        r ⟶ʳ y -> E [ x ] ⟶[ j ] E [ y ]
+  Int : forall {t j x} (r : Redex x) (E : EvalCtxt t U j) ->
+        E [ x ] ⟶[ j ] unwind (E ⁻¹)
hunk ./Semantics/SmallStep.agda 132
-  left-inverse : forall {t} (e : Expr t) i ->
-                 unannotate (annotate e i) i ≡ e
-  left-inverse e U = left-inverse' e U
-  left-inverse e B = left-inverse' e B
+Step : forall {t} -> Status -> Expr t -> Expr t -> Set
+Step i x y = x ⟶[ i ] y
hunk ./Semantics/SmallStep.agda 135
-  left-inverse' : forall {t} (e : Expr t) i ->
-                  unannotate' (annotate' e i) i ≡ e
-  left-inverse' (val n)     i = ≡-refl
-  left-inverse' throw       i = ≡-refl
-  left-inverse' loop        i = ≡-refl
-  left-inverse' (x ⊕ y)     i = ≡-cong₂ _⊕_     (left-inverse x i) (left-inverse y i)
-  left-inverse' (x >> y)    i = ≡-cong₂ _>>_    (left-inverse x i) ≡-refl
-  left-inverse' (x catch y) i = ≡-cong₂ _catch_ (left-inverse x i) ≡-refl
-  left-inverse' (block x)   i = ≡-refl
-  left-inverse' (unblock x) i = ≡-refl
+-- Reflexive transitive closure.
hunk ./Semantics/SmallStep.agda 137
--- Composition of evaluation contexts.
+infix 2 _⟶⋆[_]_
+
+_⟶⋆[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set
+x ⟶⋆[ i ] y = Star (Step i) x y
+
+module ⟶-Reasoning {t i} = StarReasoning (Step {t} i)
+
+-- Infinite reduction sequences.
hunk ./Semantics/SmallStep.agda 146
-infix 10 _∘_
+infix 2 _⟶∞[_]
hunk ./Semantics/SmallStep.agda 148
-_∘_ : forall {t} -> EvalCtxt t -> EvalCtxt t -> EvalCtxt t
-•                     ∘ E₂ = E₂
-(E₁ •⊕     y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •⊕     y ^ i
-(E₁ •>>    y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •>>    y ^ i
-(E₁ •catch y ^ i)     ∘ E₂ = (E₁ ∘ E₂) •catch y ^ i
-(val n ^ j ⊕• E₁ ^ i) ∘ E₂ = val n ^ j ⊕• (E₁ ∘ E₂) ^ i
+_⟶∞[_] : forall {t} -> Expr t -> Status -> Set
+x ⟶∞[ i ] = Infinite (Step i) x
hunk ./Semantics/SmallStep.agda 151
-∘-lemma : forall {t} (E₁ E₂ : EvalCtxt t) {x} ->
+------------------------------------------------------------------------
+-- Some utility functions/lemmas
+
+∘-lemma : forall {t i j k}
+          (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} ->
hunk ./Semantics/SmallStep.agda 157
-∘-lemma •                     E₂ = ≡-refl
-∘-lemma (E₁ •⊕     y ^ i)     E₂ = ≡-cong (\x -> x ⊕     y ^ i)       (∘-lemma E₁ E₂)
-∘-lemma (E₁ •>>    y ^ i)     E₂ = ≡-cong (\x -> x >>    y ^ i)       (∘-lemma E₁ E₂)
-∘-lemma (E₁ •catch y ^ i)     E₂ = ≡-cong (\x -> x catch y ^ i)       (∘-lemma E₁ E₂)
-∘-lemma (val n ^ j ⊕• E₁ ^ i) E₂ = ≡-cong (\x -> (val n ^ j) ⊕ x ^ i) (∘-lemma E₁ E₂)
+∘-lemma •              E₂ = ≡-refl
+∘-lemma (E₁ •< op > y) E₂ = ≡-cong (\x -> x < op > y)  (∘-lemma E₁ E₂)
+∘-lemma (val n ⊕• E₁)  E₂ = ≡-cong (\x -> (val n) ⊕ x) (∘-lemma E₁ E₂)
+∘-lemma (block•   E₁)  E₂ = ≡-cong block   (∘-lemma E₁ E₂)
+∘-lemma (unblock• E₁)  E₂ = ≡-cong unblock (∘-lemma E₁ E₂)
hunk ./Semantics/SmallStep.agda 165
-lift⟶ : forall {t x y} (E : EvalCtxt t) ->
-        x ⟶ y -> E [ x ] ⟶ E [ y ]
-lift⟶ E₁ (reduction {x = x} {y = y} E₂ r) =
-  ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶ y') (∘-lemma E₁ E₂)
-    (≡-subst (\x' -> x' ⟶ E₁ ∘ E₂ [ y ]) (∘-lemma E₁ E₂)
-       (reduction (E₁ ∘ E₂) r))
+-- Note that the following lemma is not true.
+
+lift⟶ : forall {t i j x y} (E : EvalCtxt t i j) ->
+        x ⟶[ i ] y -> E [ x ] ⟶[ j ] E [ y ]
+lift⟶ {j = j} E₁ (Red {x = x} {y = y} E₂ red) =
+  ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶[ j ] y') (∘-lemma E₁ E₂)
+    (≡-subst (\x' -> x' ⟶[ j ] E₁ ∘ E₂ [ y ]) (∘-lemma E₁ E₂)
+       (Red (E₁ ∘ E₂) red))
+lift⟶ E₁ (Int {x = x} r E₂) = {! !}
hunk ./Semantics/SmallStep.agda 175
-lift⟶⋆ : forall {t x y} (E : EvalCtxt t) ->
-         x ⟶⋆ y -> E [ x ] ⟶⋆ E [ y ]
+lift⟶⋆ : forall {t i j x y} (E : EvalCtxt t i j) ->
+         x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ]
hunk ./Semantics/SmallStep.agda 179
-lift⟶∞ : forall {t x} (E : EvalCtxt t) ->
-         x ⟶∞ -> E [ x ] ⟶∞
+lift⟶∞ : forall {t i j x} (E : EvalCtxt t i j) ->
+         x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ]
hunk ./Syntax.agda 14
-infixl 5 _catch_
-infixr 5 _finally_
-infixl 4 _>>_
+infixl 6 _catch_
+infixr 6 _finally_
+infixl 5 _>>_