[Evaluation contexts are no longer used to define the small-step semantics. Nils Anders Danielsson **20080624185631 + They are still used by some of the proofs, though. ] hunk ./Everything.agda 23 +import Semantics.SmallStep.EvalCtxt hunk ./Semantics/Equivalence.agda 10 +open import Semantics.SmallStep.EvalCtxt hunk ./Semantics/Equivalence.agda 48 - run (val n) ⟶⟨ Red • Val ⟩ + run (val n) ⟶⟨ Red Val ⟩ hunk ./Semantics/Equivalence.agda 51 - run throw ⟶⟨ Red • Throw ⟩ + run throw ⟶⟨ Red Throw ⟩ hunk ./Semantics/Equivalence.agda 54 - run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩ hunk ./Semantics/Equivalence.agda 56 - run (done (val m) ⊕ done (val n)) ⟶⟨ Red • Add₁ ⟩ + run (done (val m) ⊕ done (val n)) ⟶⟨ Red Add₁ ⟩ hunk ./Semantics/Equivalence.agda 59 - run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x↯) ⟩ - run (done throw ⊕ y ˢ) ⟶⟨ Red • Add₂ ⟩ + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x↯) ⟩ + run (done throw ⊕ y ˢ) ⟶⟨ Red Add₂ ⟩ hunk ./Semantics/Equivalence.agda 63 - run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩ hunk ./Semantics/Equivalence.agda 65 - run (done (val m) ⊕ done throw) ⟶⟨ Red • Add₃ ⟩ + run (done (val m) ⊕ done throw) ⟶⟨ Red Add₃ ⟩ hunk ./Semantics/Equivalence.agda 68 - run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |>>| > y ˢ) (big⇒small⇓ x⇓) ⟩ - run (done (val m) >> y ˢ) ⟶⟨ Red • Seqn₁ ⟩ + run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) >> y ˢ) ⟶⟨ Red Seqn₁ ⟩ hunk ./Semantics/Equivalence.agda 73 - run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |>>| > y ˢ) (big⇒small⇓ x↯) ⟩ - run (done throw >> y ˢ) ⟶⟨ Red • Seqn₂ ⟩ + run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x↯) ⟩ + run (done throw >> y ˢ) ⟶⟨ Red Seqn₂ ⟩ hunk ./Semantics/Equivalence.agda 77 - run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |catch| > y ˢ) (big⇒small⇓ x⇓) ⟩ - run (done (val m) catch y ˢ) ⟶⟨ Red • Catch₁ ⟩ + run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) catch y ˢ) ⟶⟨ Red Catch₁ ⟩ hunk ./Semantics/Equivalence.agda 81 - run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |catch| > y ˢ) (big⇒small⇓ x↯) ⟩ + run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x↯) ⟩ hunk ./Semantics/Equivalence.agda 83 - run (done throw catch done v) ⟶⟨ Red • Catch₂ ⟩ + run (done throw catch done v) ⟶⟨ Red Catch₂ ⟩ hunk ./Semantics/Equivalence.agda 86 - x ˢ ⟶⟨ Red • (Int (x ˢ-interruptible)) ⟩ + x ˢ ⟶⟨ Red (Int (x ˢ-interruptible)) ⟩ hunk ./Semantics/Equivalence.agda 90 - run (block (done v)) ⟶⟨ Red • Block ⟩ + run (block (done v)) ⟶⟨ Red Block ⟩ hunk ./Semantics/Equivalence.agda 94 - run (unblock (done v)) ⟶⟨ Red • Unblock ⟩ + run (unblock (done v)) ⟶⟨ Red Unblock ⟩ hunk ./Semantics/Equivalence.agda 98 -big⇒small⇑ (Loop loop⇑) ~ Red • Loop ◅∞ big⇒small⇑ loop⇑ -big⇒small⇑ (Add₁ x⇑) ~ lift⟶∞ (• •< |⊕| > _) (big⇒small⇑ x⇑) -big⇒small⇑ (Add₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •< |⊕| > _) (big⇒small⇓ x⇓) +big⇒small⇑ (Loop loop⇑) ~ Red Loop ◅∞ big⇒small⇑ loop⇑ +big⇒small⇑ (Add₁ x⇑) ~ lift⟶∞ (• •⊕ _) (big⇒small⇑ x⇑) +big⇒small⇑ (Add₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •⊕ _) (big⇒small⇓ x⇓) hunk ./Semantics/Equivalence.agda 103 -big⇒small⇑ (Seqn₁ x⇑) ~ lift⟶∞ (• •< |>>| > _) (big⇒small⇑ x⇑) -big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •< |>>| > _) (big⇒small⇓ x⇓) +big⇒small⇑ (Seqn₁ x⇑) ~ lift⟶∞ (• •>> _) (big⇒small⇑ x⇑) +big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •>> _) (big⇒small⇓ x⇓) hunk ./Semantics/Equivalence.agda 106 - Red • Seqn₁ + Red Seqn₁ hunk ./Semantics/Equivalence.agda 109 -big⇒small⇑ (Catch₁ x⇑) ~ lift⟶∞ (• •< |catch| > _) (big⇒small⇑ x⇑) -big⇒small⇑ (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •< |catch| > _) (big⇒small⇓ x↯) +big⇒small⇑ (Catch₁ x⇑) ~ lift⟶∞ (• •catch _) (big⇒small⇑ x⇑) +big⇒small⇑ (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •catch _) (big⇒small⇓ x↯) hunk ./Semantics/Equivalence.agda 128 -map⇓ • f ⇓ = f ⇓ -map⇓ (E •< |⊕| > y) f (Add₁ x↡ y↡) = Add₁ (map⇓ E f x↡) y↡ -map⇓ (E •< |⊕| > y) f (Add₂ x↯) = Add₂ (map⇓ E f x↯) -map⇓ (E •< |⊕| > y) f (Add₃ x↡ y↯) = Add₃ (map⇓ E f x↡) y↯ -map⇓ (E •< |⊕| > y) f Int = Int -map⇓ (E •< |>>| > y) f (Seqn₁ x↡ y⇓) = Seqn₁ (map⇓ E f x↡) y⇓ -map⇓ (E •< |>>| > y) f (Seqn₂ x↯) = Seqn₂ (map⇓ E f x↯) -map⇓ (E •< |>>| > y) f Int = Int -map⇓ (E •< |catch| > y) f (Catch₁ x↡) = Catch₁ (map⇓ E f x↡) -map⇓ (E •< |catch| > y) f (Catch₂ x↯ y⇓) = Catch₂ (map⇓ E f x↯) y⇓ -map⇓ (E •< |catch| > y) f Int = Int -map⇓ (val m ⊕• E) f (Add₁ x↡ y↡) = Add₁ x↡ (map⇓ E f y↡) -map⇓ (val m ⊕• E) f (Add₂ x↯) = Add₂ x↯ -map⇓ (val m ⊕• E) f (Add₃ x↡ y↯) = Add₃ x↡ (map⇓ E f y↯) -map⇓ (val m ⊕• E) f Int = Int -map⇓ (handler• E) f (Catch₁ ()) -map⇓ (handler• E) f (Catch₂ x↯ y⇓) = Catch₂ x↯ (map⇓ E f y⇓) -map⇓ (handler• E) f Int = Int -map⇓ (block• E) f (Block x⇓) = Block (map⇓ E f x⇓) -map⇓ (block• E) f Int = Int -map⇓ (unblock• E) f (Unblock x⇓) = Unblock (map⇓ E f x⇓) -map⇓ (unblock• E) f Int = Int +map⇓ • f ⇓ = f ⇓ +map⇓ (E •⊕ y) f (Add₁ x↡ y↡) = Add₁ (map⇓ E f x↡) y↡ +map⇓ (E •⊕ y) f (Add₂ x↯) = Add₂ (map⇓ E f x↯) +map⇓ (E •⊕ y) f (Add₃ x↡ y↯) = Add₃ (map⇓ E f x↡) y↯ +map⇓ (E •⊕ y) f Int = Int +map⇓ (E •>> y) f (Seqn₁ x↡ y⇓) = Seqn₁ (map⇓ E f x↡) y⇓ +map⇓ (E •>> y) f (Seqn₂ x↯) = Seqn₂ (map⇓ E f x↯) +map⇓ (E •>> y) f Int = Int +map⇓ (E •catch y) f (Catch₁ x↡) = Catch₁ (map⇓ E f x↡) +map⇓ (E •catch y) f (Catch₂ x↯ y⇓) = Catch₂ (map⇓ E f x↯) y⇓ +map⇓ (E •catch y) f Int = Int +map⇓ (val m ⊕• E) f (Add₁ x↡ y↡) = Add₁ x↡ (map⇓ E f y↡) +map⇓ (val m ⊕• E) f (Add₂ x↯) = Add₂ x↯ +map⇓ (val m ⊕• E) f (Add₃ x↡ y↯) = Add₃ x↡ (map⇓ E f y↯) +map⇓ (val m ⊕• E) f Int = Int +map⇓ (handler• E) f (Catch₁ ()) +map⇓ (handler• E) f (Catch₂ x↯ y⇓) = Catch₂ x↯ (map⇓ E f y⇓) +map⇓ (handler• E) f Int = Int +map⇓ (block• E) f (Block x⇓) = Block (map⇓ E f x⇓) +map⇓ (block• E) f Int = Int +map⇓ (unblock• E) f (Unblock x⇓) = Unblock (map⇓ E f x⇓) +map⇓ (unblock• E) f Int = Int hunk ./Semantics/Equivalence.agda 155 -map⇑ • f g ⇑ = g ⇑ -map⇑ (E •< |⊕| > y) f g (Add₁ x⇑) = Add₁ (map⇑ E f g x⇑) -map⇑ (E •< |⊕| > y) f g (Add₂ (_ , x↡) y⇑) = Add₂ (_ , map⇓ E f x↡) y⇑ -map⇑ (E •< |>>| > y) f g (Seqn₁ x⇑) = Seqn₁ (map⇑ E f g x⇑) -map⇑ (E •< |>>| > y) f g (Seqn₂ (_ , x↡) y⇑) = Seqn₂ (_ , map⇓ E f x↡) y⇑ -map⇑ (E •< |catch| > y) f g (Catch₁ x⇑) = Catch₁ (map⇑ E f g x⇑) -map⇑ (E •< |catch| > y) f g (Catch₂ x↯ y⇑) = Catch₂ (map⇓ E f x↯) y⇑ -map⇑ (val m ⊕• E) f g (Add₁ ()) -map⇑ (val m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) -map⇑ (handler• E) f g (Catch₁ ()) -map⇑ (handler• E) f g (Catch₂ x↯ y⇑) = Catch₂ x↯ (map⇑ E f g y⇑) -map⇑ (block• E) f g (Block x⇑) = Block (map⇑ E f g x⇑) -map⇑ (unblock• E) f g (Unblock x⇑) = Unblock (map⇑ E f g x⇑) +map⇑ • f g ⇑ = g ⇑ +map⇑ (E •⊕ y) f g (Add₁ x⇑) = Add₁ (map⇑ E f g x⇑) +map⇑ (E •⊕ y) f g (Add₂ (_ , x↡) y⇑) = Add₂ (_ , map⇓ E f x↡) y⇑ +map⇑ (E •>> y) f g (Seqn₁ x⇑) = Seqn₁ (map⇑ E f g x⇑) +map⇑ (E •>> y) f g (Seqn₂ (_ , x↡) y⇑) = Seqn₂ (_ , map⇓ E f x↡) y⇑ +map⇑ (E •catch y) f g (Catch₁ x⇑) = Catch₁ (map⇑ E f g x⇑) +map⇑ (E •catch y) f g (Catch₂ x↯ y⇑) = Catch₂ (map⇓ E f x↯) y⇑ +map⇑ (val m ⊕• E) f g (Add₁ ()) +map⇑ (val m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) +map⇑ (handler• E) f g (Catch₁ ()) +map⇑ (handler• E) f g (Catch₂ x↯ y⇑) = Catch₂ x↯ (map⇑ E f g y⇑) +map⇑ (block• E) f g (Block x⇑) = Block (map⇑ E f g x⇑) +map⇑ (unblock• E) f g (Unblock x⇑) = Unblock (map⇑ E f g x⇑) hunk ./Semantics/Equivalence.agda 227 -small⇒big⟶⋆ (val n) ε = Val -small⇒big⟶⋆ throw ε = Throw -small⇒big⟶⋆ v (Red E r ◅ rs) = - map⇓ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶⋆ v rs) +small⇒big⟶⋆ (val n) ε = Val +small⇒big⟶⋆ throw ε = Throw +small⇒big⟶⋆ v (⟶ ◅ ⟶⋆) with ⟶⇒⟶E ⟶ +small⇒big⟶⋆ v (⟶ ◅ ⟶⋆) | Red E ⟶ʳ = + map⇓ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶⋆ v ⟶⋆) hunk ./Semantics/Equivalence.agda 241 --- small⇒big⟶∞ (Red E r ◅∞ rs) ~ --- map⇑ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶ʳ⇑ r) (small⇒big⟶∞ rs) +-- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) with ⟶⇒⟶E ⟶ +-- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) | Red E ⟶ʳ = +-- map⇑ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶ʳ⇑ ⟶ʳ) (small⇒big⟶∞ ⟶∞) hunk ./Semantics/Equivalence/Add.agda 18 -drop-run[•⊕-] : forall {t} {x x' y y' : Exprˢ t} -> - run (x ⊕ y) ≡ run (x' ⊕ y') -> x ≡ x' -drop-run[•⊕-] ≡-refl ~ ≡-refl - -helper₁ : forall {t} {y z : Exprˢ t} {m i} -> - z ⟶∞[ i ] -> z ≡ run (done (val m) ⊕ y) -> y ⟶∞[ i ] -helper₁ (Red • Val ◅∞ ⟶∞) () -helper₁ (Red • Throw ◅∞ ⟶∞) () -helper₁ (Red • Loop ◅∞ ⟶∞) () -helper₁ (Red • Add₁ ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₁ (Red • Add₂ ◅∞ ⟶∞) () -helper₁ (Red • Add₃ ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₁ (Red • Seqn₁ ◅∞ ⟶∞) () -helper₁ (Red • Seqn₂ ◅∞ ⟶∞) () -helper₁ (Red • Catch₁ ◅∞ ⟶∞) () -helper₁ (Red • Catch₂ ◅∞ ⟶∞) () -helper₁ (Red • Block ◅∞ ⟶∞) () -helper₁ (Red • Unblock ◅∞ ⟶∞) () -helper₁ (Red • (Int int) ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₁ (Red {j = j} {y = z} - (E •< |⊕| > y) r ◅∞ ⟶∞) eq ~ ⊥-elim (done↛ $ ≡-subst (\x -> x ⟶[ j ] E [ z ]) - (drop-run[•⊕-] eq) - (Red E r)) -helper₁ (Red (E •< |>>| > y) r ◅∞ ⟶∞) () -helper₁ (Red (E •< |catch| > y) r ◅∞ ⟶∞) () -helper₁ (Red (val m ⊕• E) r ◅∞ ⟶∞) ≡-refl ~ Red E r ◅∞ helper₁ ⟶∞ ≡-refl -helper₁ (Red (handler• E) r ◅∞ ⟶∞) () -helper₁ (Red (block• E) r ◅∞ ⟶∞) () -helper₁ (Red (unblock• E) r ◅∞ ⟶∞) () +helper₁ : forall {t} {y : Exprˢ t} {m i} -> + run (done (val m) ⊕ y) ⟶∞[ i ] -> y ⟶∞[ i ] +helper₁ (Red Add₁ ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₁ (Red Add₃ ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₁ (Addˡ ⟶ ◅∞ ⟶∞) ~ ⊥-elim (done↛ ⟶) +helper₁ (Addʳ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞ hunk ./Semantics/Equivalence/Add.agda 29 -helper₂ : forall {t} {x y u : Exprˢ t} {i} -> - u ⟶∞[ i ] -> u ≡ run (x ⊕ y) -> x ⟶⋆∞[ i ] Pred y i -helper₂ (Red • Val ◅∞ ⟶∞) () -helper₂ (Red • Throw ◅∞ ⟶∞) () -helper₂ (Red • Loop ◅∞ ⟶∞) () -helper₂ (Red • Add₁ ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₂ (Red • Add₂ ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₂ (Red • Add₃ ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₂ (Red • Seqn₁ ◅∞ ⟶∞) () -helper₂ (Red • Seqn₂ ◅∞ ⟶∞) () -helper₂ (Red • Catch₁ ◅∞ ⟶∞) () -helper₂ (Red • Catch₂ ◅∞ ⟶∞) () -helper₂ (Red • Block ◅∞ ⟶∞) () -helper₂ (Red • Unblock ◅∞ ⟶∞) () -helper₂ (Red • (Int int) ◅∞ ⟶∞) ≡-refl ~ ⊥-elim (done↛∞ ⟶∞) -helper₂ (Red (E •< |⊕| > y) r ◅∞ ⟶∞) ≡-refl ~ Red E r ◅∞ helper₂ ⟶∞ ≡-refl -helper₂ (Red (E •< |>>| > y) r ◅∞ ⟶∞) () -helper₂ (Red (E •< |catch| > y) r ◅∞ ⟶∞) () -helper₂ (Red (val m ⊕• E) r ◅∞ ⟶∞) ≡-refl ~ ε (m , ≡-refl , Red E r ◅∞ helper₁ ⟶∞ ≡-refl) -helper₂ (Red (handler• E) r ◅∞ ⟶∞) () -helper₂ (Red (block• E) r ◅∞ ⟶∞) () -helper₂ (Red (unblock• E) r ◅∞ ⟶∞) () +helper₂ : forall {t} {x y : Exprˢ t} {i} -> + run (x ⊕ y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i +helper₂ (Red Add₁ ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₂ (Red Add₂ ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₂ (Red Add₃ ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₂ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞) +helper₂ (Addˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₂ ⟶∞ +helper₂ (Addʳ ⟶ ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶ ◅∞ helper₁ ⟶∞) hunk ./Semantics/Equivalence/Add.agda 43 - map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₂ x⊕y⟶∞ ≡-refl)) + map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₂ x⊕y⟶∞)) hunk ./Semantics/SmallStep.agda 81 --- A variant of _<_>_. - -infix 8 _<_>'_ - -_<_>'_ : forall {t} -> Exprˢ t -> Op -> Exprˢ t -> Exprˢ' t -x < |⊕| >' y = x ⊕ y -x < |>>| >' y = x >> y -x < |catch| >' y = x catch y - hunk ./Semantics/SmallStep.agda 108 --- Reduction relation +-- The semantics hunk ./Semantics/SmallStep.agda 110 -infix 2 _⟶ʳ[_]_ _∶_⟶ʳ[_]_ +infix 2 _⟶ʳ[_]_ _∶_⟶ʳ[_]_ _⟶[_]_ _∶_⟶[_]_ + +-- Redexes and reducts. hunk ./Semantics/SmallStep.agda 136 ------------------------------------------------------------------------- --- Evaluation contexts - --- Evaluation contexts. Indexed on the status at the hole and the --- outermost status. - -infix 7 _•<_>_ val_⊕•_ - -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 - handler• : forall {i j} (E : EvalCtxt t i B) -> 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 - --- Filling holes. - -infix 9 _[_] - -_[_] : forall {t i j} -> EvalCtxt t i j -> Exprˢ t -> Exprˢ t -• [ y ] = y -(E •< op > x) [ y ] = run (E [ y ] < op >' x) -(val n ⊕• E) [ y ] = run (done (val n) ⊕ E [ y ]) -(handler• E) [ y ] = run (done throw catch E [ y ]) -(block• E) [ y ] = run (block (E [ y ])) -(unblock• E) [ y ] = run (unblock (E [ y ])) - --- Composition of evaluation contexts. - -infixr 10 _⊚_ +-- Structural rules. hunk ./Semantics/SmallStep.agda 138 -_⊚_ : 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₂) -handler• E₁ ⊚ E₂ = handler• (E₁ ⊚ E₂) -block• E₁ ⊚ E₂ = block• (E₁ ⊚ E₂) -unblock• E₁ ⊚ E₂ = unblock• (E₁ ⊚ E₂) - ------------------------------------------------------------------------- --- The semantics - --- Single-step evaluation. +mutual hunk ./Semantics/SmallStep.agda 140 -infix 2 _⟶[_]_ + private + _∶_⟶[_]_ : forall t -> Exprˢ t -> Status -> Exprˢ t -> Set + t ∶ e₁ ⟶[ i ] e₂ = e₁ ⟶[ i ] e₂ hunk ./Semantics/SmallStep.agda 144 -data _⟶[_]_ : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set where - Red : forall {t i j x y} - (E : EvalCtxt t i j) (r : x ⟶ʳ[ i ] y) -> - E [ x ] ⟶[ j ] E [ y ] + data _⟶[_]_ : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set where + Red : forall {t x x' i} (⟶ : x ⟶ʳ[ i ] x') -> t ∶ x ⟶[ i ] x' + Addˡ : forall {t x x' y i} (⟶ : x ⟶[ i ] x') -> t ∶ run (x ⊕ y) ⟶[ i ] run (x' ⊕ y) + Addʳ : forall {t m y y' i} (⟶ : y ⟶[ i ] y') -> t ∶ run (done (val m) ⊕ y) ⟶[ i ] run (done (val m) ⊕ y') + Seqnˡ : forall {t x x' y i} (⟶ : x ⟶[ i ] x') -> t ∶ run (x >> y) ⟶[ i ] run (x' >> y) + Catchˡ : forall {t x x' y i} (⟶ : x ⟶[ i ] x') -> t ∶ run (x catch y) ⟶[ i ] run (x' catch y) + Catchʳ : forall {t y y' i} (⟶ : y ⟶[ B ] y') -> t ∶ run (done throw catch y) ⟶[ i ] run (done throw catch y') + Blockˡ : forall {t x x' i} (⟶ : x ⟶[ B ] x') -> t ∶ run (block x) ⟶[ i ] run (block x') + Unblockˡ : forall {t x x' i} (⟶ : x ⟶[ U ] x') -> t ∶ run (unblock x) ⟶[ i ] run (unblock x') hunk ./Semantics/SmallStep.agda 180 ------------------------------------------------------------------------- --- Lemmas about evaluation contexts - -⊚-lemma : forall {t i j k} - (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} -> - E₁ ⊚ E₂ [ x ] ≡ E₁ [ E₂ [ x ] ] -⊚-lemma • E₂ = ≡-refl -⊚-lemma (E₁ •< op > y) E₂ = ≡-cong (\x -> run (x < op >' y)) (⊚-lemma E₁ E₂) -⊚-lemma (val n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (val n) ⊕ x)) (⊚-lemma E₁ E₂) -⊚-lemma (handler• E₁) E₂ = ≡-cong (\x -> run (done throw catch x)) (⊚-lemma E₁ E₂) -⊚-lemma (block• E₁) E₂ = ≡-cong (\x -> run (block x)) (⊚-lemma E₁ E₂) -⊚-lemma (unblock• E₁) E₂ = ≡-cong (\x -> run (unblock x)) (⊚-lemma E₁ E₂) - --- Lifting of reductions/reduction sequences. - -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⟶⋆ : forall {t i j x y} (E : EvalCtxt t i j) -> - x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ] -lift⟶⋆ E = gmap (\x -> E [ x ]) (lift⟶ E) - -lift⟶∞ : forall {t i j x} (E : EvalCtxt t i j) -> - x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ] -lift⟶∞ E = map∞ (\x -> E [ x ]) (lift⟶ E) - hunk ./Semantics/SmallStep.agda 214 -run⟶ (val n) = (, Red • Val) -run⟶ throw = (, Red • Throw) -run⟶ loop = (, Red • Loop) -run⟶ (run x ⊕ y) = map-Σ _ (lift⟶ (• •< |⊕| > y)) (run⟶ x) -run⟶ (done (val m) ⊕ run y) = map-Σ _ (lift⟶ (val m ⊕• •)) (run⟶ y) -run⟶ (done (val m) ⊕ done (val n)) = (, Red • Add₁) -run⟶ (done (val m) ⊕ done throw) = (, Red • Add₃) -run⟶ (done throw ⊕ y) = (, Red • Add₂) -run⟶ (run x >> y) = map-Σ _ (lift⟶ (• •< |>>| > y)) (run⟶ x) -run⟶ (done (val m) >> run x) = (, Red • Seqn₁) -run⟶ (done (val m) >> done v) = (, Red • Seqn₁) -run⟶ (done throw >> y) = (, Red • Seqn₂) -run⟶ (run x catch y) = map-Σ _ (lift⟶ (• •< |catch| > y)) (run⟶ x) -run⟶ (done (val m) catch y) = (, Red • Catch₁) -run⟶ (done throw catch run y) = map-Σ _ (lift⟶ (handler• •)) (run⟶ y) -run⟶ (done throw catch done v) = (, Red • Catch₂) -run⟶ (block (run x)) = map-Σ _ (lift⟶ (block• •)) (run⟶ x) -run⟶ (block (done v)) = (, Red • Block) -run⟶ (unblock (run x)) = map-Σ _ (lift⟶ (unblock• •)) (run⟶ x) -run⟶ (unblock (done v)) = (, Red • Unblock) +run⟶ (val n) = (, Red Val) +run⟶ throw = (, Red Throw) +run⟶ loop = (, Red Loop) +run⟶ (run x ⊕ y) = map-Σ _ Addˡ (run⟶ x) +run⟶ (done (val m) ⊕ run y) = map-Σ _ Addʳ (run⟶ y) +run⟶ (done (val m) ⊕ done (val n)) = (, Red Add₁) +run⟶ (done (val m) ⊕ done throw) = (, Red Add₃) +run⟶ (done throw ⊕ y) = (, Red Add₂) +run⟶ (run x >> y) = map-Σ _ Seqnˡ (run⟶ x) +run⟶ (done (val m) >> run x) = (, Red Seqn₁) +run⟶ (done (val m) >> done v) = (, Red Seqn₁) +run⟶ (done throw >> y) = (, Red Seqn₂) +run⟶ (run x catch y) = map-Σ _ Catchˡ (run⟶ x) +run⟶ (done (val m) catch y) = (, Red Catch₁) +run⟶ (done throw catch run y) = map-Σ _ Catchʳ (run⟶ y) +run⟶ (done throw catch done v) = (, Red Catch₂) +run⟶ (block (run x)) = map-Σ _ Blockˡ (run⟶ x) +run⟶ (block (done v)) = (, Red Block) +run⟶ (unblock (run x)) = map-Σ _ Unblockˡ (run⟶ x) +run⟶ (unblock (done v)) = (, Red Unblock) hunk ./Semantics/SmallStep.agda 238 -done↛ hyp = helper₁ hyp ≡-refl - where - helper₂ : forall {t} (x : Exprˢ t) {y v i} -> - x ⟶ʳ[ i ] y -> x ≢ done v - helper₂ (run x) _ () - helper₂ (done v) () _ - - helper₁ : forall {t} {x y : Exprˢ t} {v i} -> - x ⟶[ i ] y -> x ≢ done v - helper₁ (Red • r) eq = helper₂ _ r eq - helper₁ (Red (E •< op > y) r) () - helper₁ (Red (val m ⊕• E) r) () - helper₁ (Red (handler• E) r) () - helper₁ (Red (block• E) r) () - helper₁ (Red (unblock• E) r) () +done↛ (Red ()) hunk ./Semantics/SmallStep.agda 243 -done↛∞ (v⟶y ◅∞ y⟶∞) = done↛ v⟶y +done↛∞ (Red () ◅∞ ⟶∞) addfile ./Semantics/SmallStep/EvalCtxt.agda hunk ./Semantics/SmallStep/EvalCtxt.agda 1 +------------------------------------------------------------------------ +-- Evaluation contexts +------------------------------------------------------------------------ + +-- The evaluation contexts are not part of the definition of the +-- semantics, they are just available as a convenience. + +module Semantics.SmallStep.EvalCtxt where + +open import Syntax +open import Infinite +open import Semantics.SmallStep + +open import Data.Nat +open import Data.Star +open import Relation.Binary.PropositionalEquality + +------------------------------------------------------------------------ +-- Evaluation contexts + +infix 7 val_⊕•_ +infixl 7 _•⊕_ +infixl 6 _•catch_ +infixl 5 _•>>_ + +-- The evaluation contexts are indexed on the status at the hole and +-- the outermost status (see lift⟶ below). + +data EvalCtxt t : Status -> Status -> Set where + • : forall {i} -> EvalCtxt t i i + _•⊕_ : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j + _•>>_ : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j + _•catch_ : forall {i j} (E : EvalCtxt t i j) (y : Exprˢ t) -> EvalCtxt t i j + val_⊕•_ : forall {i j} (m : ℕ) (E : EvalCtxt t i j) -> EvalCtxt t i j + handler• : forall {i j} (E : EvalCtxt t i B) -> 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 + +-- Filling holes. + +infix 9 _[_] + +_[_] : forall {t i j} -> EvalCtxt t i j -> Exprˢ t -> Exprˢ t +• [ y ] = y +(E •⊕ x) [ y ] = run (E [ y ] ⊕ x) +(E •>> x) [ y ] = run (E [ y ] >> x) +(E •catch x) [ y ] = run (E [ y ] catch x) +(val n ⊕• E) [ y ] = run (done (val n) ⊕ E [ y ]) +(handler• E) [ y ] = run (done throw catch E [ y ]) +(block• E) [ y ] = run (block (E [ y ])) +(unblock• E) [ y ] = run (unblock (E [ y ])) + +------------------------------------------------------------------------ +-- Lifting of reductions/reduction sequences + +lift⟶ : forall {t i j x y} (E : EvalCtxt t i j) -> + x ⟶[ i ] y -> E [ x ] ⟶[ j ] E [ y ] +lift⟶ • ⟶ = ⟶ +lift⟶ (E •⊕ y) ⟶ = Addˡ (lift⟶ E ⟶) +lift⟶ (E •>> y) ⟶ = Seqnˡ (lift⟶ E ⟶) +lift⟶ (E •catch y) ⟶ = Catchˡ (lift⟶ E ⟶) +lift⟶ (val m ⊕• E) ⟶ = Addʳ (lift⟶ E ⟶) +lift⟶ (handler• E) ⟶ = Catchʳ (lift⟶ E ⟶) +lift⟶ (block• E) ⟶ = Blockˡ (lift⟶ E ⟶) +lift⟶ (unblock• E) ⟶ = Unblockˡ (lift⟶ E ⟶) + +lift⟶⋆ : forall {t i j x y} (E : EvalCtxt t i j) -> + x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ] +lift⟶⋆ E = gmap (\x -> E [ x ]) (lift⟶ E) + +lift⟶∞ : forall {t i j x} (E : EvalCtxt t i j) -> + x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ] +lift⟶∞ E = map∞ (\x -> E [ x ]) (lift⟶ E) + +------------------------------------------------------------------------ +-- Composition of evaluation contexts + +infixr 10 _⊚_ + +_⊚_ : forall {t i j k} -> + EvalCtxt t j k -> EvalCtxt t i j -> EvalCtxt t i k +• ⊚ E₂ = E₂ +(E₁ •⊕ y) ⊚ E₂ = (E₁ ⊚ E₂) •⊕ y +(E₁ •>> y) ⊚ E₂ = (E₁ ⊚ E₂) •>> y +(E₁ •catch y) ⊚ E₂ = (E₁ ⊚ E₂) •catch y +(val n ⊕• E₁) ⊚ E₂ = val n ⊕• (E₁ ⊚ E₂) +handler• E₁ ⊚ E₂ = handler• (E₁ ⊚ E₂) +block• E₁ ⊚ E₂ = block• (E₁ ⊚ E₂) +unblock• E₁ ⊚ E₂ = unblock• (E₁ ⊚ E₂) + +⊚-lemma : forall {t i j k} + (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} -> + E₁ ⊚ E₂ [ x ] ≡ E₁ [ E₂ [ x ] ] +⊚-lemma • E₂ = ≡-refl +⊚-lemma (E₁ •⊕ y) E₂ = ≡-cong (\x -> run (x ⊕ y) ) (⊚-lemma E₁ E₂) +⊚-lemma (E₁ •>> y) E₂ = ≡-cong (\x -> run (x >> y)) (⊚-lemma E₁ E₂) +⊚-lemma (E₁ •catch y) E₂ = ≡-cong (\x -> run (x catch y)) (⊚-lemma E₁ E₂) +⊚-lemma (val n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (val n) ⊕ x)) (⊚-lemma E₁ E₂) +⊚-lemma (handler• E₁) E₂ = ≡-cong (\x -> run (done throw catch x)) (⊚-lemma E₁ E₂) +⊚-lemma (block• E₁) E₂ = ≡-cong (\x -> run (block x)) (⊚-lemma E₁ E₂) +⊚-lemma (unblock• E₁) E₂ = ≡-cong (\x -> run (unblock x)) (⊚-lemma E₁ E₂) + +------------------------------------------------------------------------ +-- Another view of the small-step relation + +-- Every step can be decomposed into a reduction and an evaluation +-- context. + +infix 2 _⟶E[_]_ + +data _⟶E[_]_ {t} : Exprˢ t -> Status -> Exprˢ t -> Set where + Red : forall {x y i j} (E : EvalCtxt t i j) + (x⟶ʳy : x ⟶ʳ[ i ] y) -> E [ x ] ⟶E[ j ] E [ y ] + +-- The two views are equivalent: + +lift⟶E : forall {t i j x y} (E : EvalCtxt t i j) -> + x ⟶E[ i ] y -> E [ x ] ⟶E[ j ] E [ y ] +lift⟶E {j = j} E₁ (Red {x = x} {y = y} E₂ red) = + ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶E[ j ] y') (⊚-lemma E₁ E₂) + (≡-subst (\x' -> x' ⟶E[ j ] E₁ ⊚ E₂ [ y ]) (⊚-lemma E₁ E₂) + (Red (E₁ ⊚ E₂) red)) + +⟶⇒⟶E : forall {t i} {x y : Exprˢ t} -> + x ⟶[ i ] y -> x ⟶E[ i ] y +⟶⇒⟶E (Red ⟶) = Red • ⟶ +⟶⇒⟶E (Addˡ ⟶) = lift⟶E (• •⊕ _) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Addʳ ⟶) = lift⟶E (val _ ⊕• •) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Seqnˡ ⟶) = lift⟶E (• •>> _) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Catchˡ ⟶) = lift⟶E (• •catch _) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Catchʳ ⟶) = lift⟶E (handler• •) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Blockˡ ⟶) = lift⟶E (block• •) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Unblockˡ ⟶) = lift⟶E (unblock• •) (⟶⇒⟶E ⟶) + +⟶E⇒⟶ : forall {t i} {x y : Exprˢ t} -> + x ⟶E[ i ] y -> x ⟶[ i ] y +⟶E⇒⟶ (Red • x⟶ʳy) = Red x⟶ʳy +⟶E⇒⟶ (Red (E •⊕ y) x⟶ʳy) = lift⟶ (• •⊕ y) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (E •>> y) x⟶ʳy) = lift⟶ (• •>> y) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (E •catch y) x⟶ʳy) = lift⟶ (• •catch y) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (val m ⊕• E) x⟶ʳy) = lift⟶ (val m ⊕• •) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (handler• E) x⟶ʳy) = lift⟶ (handler• •) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (block• E) x⟶ʳy) = lift⟶ (block• •) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (unblock• E) x⟶ʳy) = lift⟶ (unblock• •) (⟶E⇒⟶ (Red E x⟶ʳy)) hunk ./Syntax.agda 8 -open import Data.Bool hunk ./Syntax.agda 57 --- "Higher-order" representation of binary operators. - -data Op : Set where - |⊕| : Op - |>>| : Op - |catch| : Op - --- Application. - -infix 8 _<_>_ - -_<_>_ : forall {t} -> Expr t -> Op -> Expr t -> Expr t -x < |⊕| > y = x ⊕ y -x < |>>| > y = x >> y -x < |catch| > y = x catch y -