[Simplified some things by replacing the constructors val and throw with ⌜_⌝. Nils Anders Danielsson **20080624201229] hunk ./AlgebraicProperties.agda 28 - n₁ ≡ n₂ -> x ⇓[ i ] val n₁ -> x ⇓[ i ] val n₂ + n₁ ≡ n₂ -> x ⇓[ i ] nat n₁ -> x ⇓[ i ] nat n₂ hunk ./AlgebraicProperties.agda 91 -¬catch-assoc assoc with _⊑_.⇓ (_≈_.⊑ (assoc throw (val 0) (val 1))) - {i = U} (Catch₂ Int Val) +¬catch-assoc assoc + with _⊑_.⇓ (_≈_.⊑ (assoc ⌜ throw ⌝ ⌜ nat 0 ⌝ ⌜ nat 1 ⌝)) + {i = U} (Catch₂ Int Val) hunk ./AlgebraicProperties.agda 171 - with _⊑_.⇓ (_≈_.⊒ (assoc (val 0) (loop catch val 0) (val 0))) + with _⊑_.⇓ (_≈_.⊒ (assoc ⌜ nat 0 ⌝ (loop catch ⌜ nat 0 ⌝) ⌜ nat 0 ⌝)) hunk ./AlgebraicProperties.agda 197 - ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Throw))) + ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Val))) hunk ./AlgebraicProperties.agda 218 - ⟶⇓ _ (Add₂ x↯) | (val _ , y⇓) = Add₃ y⇓ x↯ + ⟶⇓ _ (Add₂ x↯) | (nat _ , y⇓) = Add₃ y⇓ x↯ hunk ./AlgebraicProperties.agda 230 - with _⊑_.⇓ (_≈_.⊑ (⊕-comm throw loop)) {i = B} (Add₂ Throw) + with _⊑_.⇓ (_≈_.⊑ (⊕-comm ⌜ throw ⌝ loop)) {i = B} (Add₂ Val) hunk ./CompilerCorrectness/BarTheorem.agda 24 - e ⇓[ i ] val n -> Matches⁺ ops s e i ⟨ ops , i , val n ∷ s ⟩ + e ⇓[ i ] nat n -> Matches⁺ ops s e i ⟨ ops , i , nat n ∷ s ⟩ hunk ./CompilerCorrectness/BarTheorem.agda 53 -bar-thm {t = t} (val n) κ ~ via (_ , push) (helper₁ κ) +bar-thm {t = t} ⌜ nat n ⌝ κ ~ via (_ , push) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 56 - Cont (Matches⁺ ops s (val {t = t} n) i) P -> + Cont (Matches⁺ ops s {t} ⌜ nat n ⌝ i) P -> hunk ./CompilerCorrectness/BarTheorem.agda 61 -bar-thm {t = t} throw κ ~ via (_ , throw) (helper₁ κ) +bar-thm {t = t} ⌜ throw ⌝ κ ~ via (_ , throw) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 64 - Cont (Matches⁺ ops s (throw {t = t}) i) P -> + Cont (Matches⁺ ops s {t} ⌜ throw ⌝ i) P -> hunk ./CompilerCorrectness/BarTheorem.agda 66 - helper₁ κ throw ~ κ (throws Throw) + helper₁ κ throw ~ κ (throws Val) hunk ./CompilerCorrectness/BarTheorem.agda 73 - Cont⟶ ⟪ U , val m ∷ s ⟫ P - helper₆ κ val ~ κ (throws Int) + Cont⟶ ⟪ U , nat m ∷ s ⟫ P + helper₆ κ nat ~ κ (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 78 - Cont⟶ ⟪ U , val n ∷ val m ∷ s ⟫ P - helper₅ κ val ~ via (_ , val) (helper₆ κ) + Cont⟶ ⟪ U , nat n ∷ nat m ∷ s ⟫ P + helper₅ κ nat ~ via (_ , nat) (helper₆ κ) hunk ./CompilerCorrectness/BarTheorem.agda 83 - x ⇓[ i ] val m -> y ↯[ i ] -> - Cont⟶ ⟪ i , val m ∷ s ⟫ P - helper₄ κ x⇓ y↯ val ~ κ (throws (Add₃ x⇓ y↯)) + x ⇓[ i ] nat m -> y ↯[ i ] -> + Cont⟶ ⟪ i , nat m ∷ s ⟫ P + helper₄ κ x⇓ y↯ nat ~ κ (throws (Add₃ x⇓ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 89 - x ⇓[ i ] val m -> y ⇓[ i ] val n -> - Cont⟶ ⟨ add ∷ ops , i , val n ∷ val m ∷ s ⟩ P + x ⇓[ i ] nat m -> y ⇓[ i ] nat n -> + Cont⟶ ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 92 - helper₃ κ _ _ interrupt ~ via (_ , val) (helper₅ κ) + helper₃ κ _ _ interrupt ~ via (_ , nat) (helper₅ κ) hunk ./CompilerCorrectness/BarTheorem.agda 96 - x ⇓[ i ] val m -> - Cont (Matches⁺ (add ∷ ops) (val m ∷ s) y i) P + x ⇓[ i ] nat m -> + Cont (Matches⁺ (add ∷ ops) (nat m ∷ s) y i) P hunk ./CompilerCorrectness/BarTheorem.agda 99 - helper₂ κ x⇓ (throws y↯) ~ via (_ , val) (helper₄ κ x⇓ y↯) + helper₂ κ x⇓ (throws y↯) ~ via (_ , nat) (helper₄ κ x⇓ y↯) hunk ./CompilerCorrectness/BarTheorem.agda 111 - Cont⟶ ⟪ U , val m ∷ s ⟫ P - helper₄ κ val ~ κ (throws Int) + Cont⟶ ⟪ U , nat m ∷ s ⟫ P + helper₄ κ nat ~ κ (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 116 - x ⇓[ i ] val m -> + x ⇓[ i ] nat m -> hunk ./CompilerCorrectness/BarTheorem.agda 123 - x ⇓[ i ] val m -> - Cont⟶ ⟨ pop ∷ comp y ops , i , val m ∷ s ⟩ P + x ⇓[ i ] nat m -> + Cont⟶ ⟨ pop ∷ comp y ops , i , nat m ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 126 - helper₂ κ _ interrupt ~ via (_ , val) (helper₄ κ) + helper₂ κ _ interrupt ~ via (_ , nat) (helper₄ κ) hunk ./CompilerCorrectness/BarTheorem.agda 144 - x ↯[ i ] -> y ⇓[ B ] val n -> - Cont⟶ ⟨ reset ∷ ops , B , val n ∷ int i ∷ s ⟩ P + x ↯[ i ] -> y ⇓[ B ] nat n -> + Cont⟶ ⟨ reset ∷ ops , B , nat n ∷ int i ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 169 - Cont⟶ ⟪ U , val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ P - helper₄ κ val ~ helper₅ κ Int + Cont⟶ ⟪ U , nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ P + helper₄ κ nat ~ helper₅ κ Int hunk ./CompilerCorrectness/BarTheorem.agda 174 - x ⇓[ i ] val m -> + x ⇓[ i ] nat m -> hunk ./CompilerCorrectness/BarTheorem.agda 176 - val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ P + nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 178 - helper₃ κ _ interrupt ~ via (_ , val) (helper₄ κ) + helper₃ κ _ interrupt ~ via (_ , nat) (helper₄ κ) hunk ./CompilerCorrectness/BarTheorem.agda 204 - x ⇓[ B ] val m -> - Cont⟶ ⟨ reset ∷ ops , B , val m ∷ int i ∷ s ⟩ P + x ⇓[ B ] nat m -> + Cont⟶ ⟨ reset ∷ ops , B , nat m ∷ int i ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 236 - Cont⟶ ⟪ U , val m ∷ int i ∷ s ⟫ P - helper₄ κ val ~ helper₅ κ Int + Cont⟶ ⟪ U , nat m ∷ int i ∷ s ⟫ P + helper₄ κ nat ~ helper₅ κ Int hunk ./CompilerCorrectness/BarTheorem.agda 241 - x ⇓[ U ] val m -> - Cont⟶ ⟨ reset ∷ ops , U , val m ∷ int i ∷ s ⟩ P + x ⇓[ U ] nat m -> + Cont⟶ ⟨ reset ∷ ops , U , nat m ∷ int i ∷ s ⟩ P hunk ./CompilerCorrectness/BarTheorem.agda 244 - helper₃ κ _ interrupt ~ via (_ , val) (helper₄ κ) + helper₃ κ _ interrupt ~ via (_ , nat) (helper₄ κ) hunk ./CompilerCorrectness/Completeness.agda 28 -code-nonempty (val n) ops = []≢∷ -code-nonempty throw ops = []≢∷ +code-nonempty ⌜ nat n ⌝ ops = []≢∷ +code-nonempty ⌜ throw ⌝ ops = []≢∷ hunk ./CompilerCorrectness/Completeness.agda 43 - e ⇓[ i ] val n -> - ⟨ comp e ops , i , s ⟩ ⟶⋆ ⟨ ops , i , val n ∷ s ⟩ + e ⇓[ i ] nat n -> + ⟨ comp e ops , i , s ⟩ ⟶⋆ ⟨ ops , i , nat n ∷ s ⟩ hunk ./CompilerCorrectness/Completeness.agda 56 - complete↯ Throw = throw ◅ ε + complete↯ Val = throw ◅ ε hunk ./CompilerCorrectness/Completeness.agda 58 - complete↯ (Add₃ x y) = complete⇓ x ◅◅ complete↯ y ◅◅ val ◅ ε + complete↯ (Add₃ x y) = complete⇓ x ◅◅ complete↯ y ◅◅ nat ◅ ε hunk ./CompilerCorrectness.agda 35 - e ⇓[ i ] val n -> Matches e i ⟨ [] , i , val n ∷ [] ⟩ + e ⇓[ i ] nat n -> Matches e i ⟨ [] , i , nat n ∷ [] ⟩ hunk ./Semantics/BigStep.agda 24 - Val : forall {t n i} -> t ∶ val n ⇓[ i ] val n - Throw : forall {t i} -> t ∶ throw ⇓[ i ] throw - Add₁ : forall {t x y m n i} (x↡ : x ⇓[ i ] val m) (y↡ : y ⇓[ i ] val n) -> t ∶ x ⊕ y ⇓[ i ] val (m + n) + Val : forall {t v i} -> t ∶ ⌜ v ⌝ ⇓[ i ] v + Add₁ : forall {t x y m n i} (x↡ : x ⇓[ i ] nat m) (y↡ : y ⇓[ i ] nat n) -> t ∶ x ⊕ y ⇓[ i ] nat (m + n) hunk ./Semantics/BigStep.agda 27 - Add₃ : forall {t x y m i} (x↡ : x ⇓[ i ] val m) (y↯ : y ⇓[ i ] throw) -> t ∶ x ⊕ y ⇓[ i ] throw - Seqn₁ : forall {t x y m v i} (x↡ : x ⇓[ i ] val m) (y⇓ : y ⇓[ i ] v) -> t ∶ x >> y ⇓[ i ] v + Add₃ : forall {t x y m i} (x↡ : x ⇓[ i ] nat m) (y↯ : y ⇓[ i ] throw) -> t ∶ x ⊕ y ⇓[ i ] throw + Seqn₁ : forall {t x y m v i} (x↡ : x ⇓[ i ] nat m) (y⇓ : y ⇓[ i ] v) -> t ∶ x >> y ⇓[ i ] v hunk ./Semantics/BigStep.agda 30 - Catch₁ : forall {t x y m i} (x↡ : x ⇓[ i ] val m) -> t ∶ x catch y ⇓[ i ] val m + Catch₁ : forall {t x y m i} (x↡ : x ⇓[ i ] nat m) -> t ∶ x catch y ⇓[ i ] nat m hunk ./Semantics/BigStep.agda 42 -x ↡[ i ] = ∃ \n -> x ⇓[ i ] val n +x ↡[ i ] = ∃ \n -> x ⇓[ i ] nat n hunk ./Semantics/Equivalence/Lemmas.agda 21 - run (done (val m) ⊕ y) ⟶∞[ i ] -> y ⟶∞[ i ] + run (done (nat m) ⊕ y) ⟶∞[ i ] -> y ⟶∞[ i ] hunk ./Semantics/Equivalence/Lemmas.agda 29 - Pred y i = \x -> ∃ \n -> x ≡ done (val n) × y ⟶∞[ i ] + Pred y i = \x -> ∃ \n -> x ≡ done (nat n) × y ⟶∞[ i ] hunk ./Semantics/Equivalence/Lemmas.agda 43 - (∃ \n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ])) + (∃ \n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ])) hunk ./Semantics/Equivalence/Lemmas.agda 48 - helper (inj₁ (.(done (val n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞) + helper (inj₁ (.(done (nat n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞) hunk ./Semantics/Equivalence/Lemmas.agda 54 - Pred y i = \x -> ∃ \n -> x ≡ done (val n) × y ⟶∞[ i ] + Pred y i = \x -> ∃ \n -> x ≡ done (nat n) × y ⟶∞[ i ] hunk ./Semantics/Equivalence/Lemmas.agda 66 - (∃ \n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ])) + (∃ \n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ])) hunk ./Semantics/Equivalence/Lemmas.agda 71 - helper (inj₁ (.(done (val n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞) + helper (inj₁ (.(done (nat n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞) hunk ./Semantics/Equivalence.agda 36 - ⟶⋆ : forall {t} {e : Exprˢ t} {i} v -> + ⟶⋆ : forall {t} {e : Exprˢ t} {i v} -> hunk ./Semantics/Equivalence.agda 47 -big⇒small⇓ (Val {n = n}) = begin - run (val n) ⟶⟨ Red Val ⟩ - done (val n) ∎ -big⇒small⇓ Throw = begin - run throw ⟶⟨ Red Throw ⟩ - done throw ∎ +big⇒small⇓ (Val {v = v}) = begin + run ⌜ v ⌝ ⟶⟨ Red Val ⟩ + done v ∎ hunk ./Semantics/Equivalence.agda 52 - run (done (val m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (val m ⊕• •) (big⇒small⇓ y⇓) ⟩ - run (done (val m) ⊕ done (val n)) ⟶⟨ Red Add₁ ⟩ - done (val (m + n)) ∎ + run (done (nat m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y⇓) ⟩ + run (done (nat m) ⊕ done (nat n)) ⟶⟨ Red Add₁ ⟩ + done (nat (m + n)) ∎ hunk ./Semantics/Equivalence.agda 61 - run (done (val m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (val m ⊕• •) (big⇒small⇓ y↯) ⟩ - run (done (val m) ⊕ done throw) ⟶⟨ Red Add₃ ⟩ + run (done (nat m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y↯) ⟩ + run (done (nat m) ⊕ done throw) ⟶⟨ Red Add₃ ⟩ hunk ./Semantics/Equivalence.agda 66 - run (done (val m) >> y ˢ) ⟶⟨ Red Seqn₁ ⟩ + run (done (nat m) >> y ˢ) ⟶⟨ Red Seqn₁ ⟩ hunk ./Semantics/Equivalence.agda 75 - run (done (val m) catch y ˢ) ⟶⟨ Red Catch₁ ⟩ - done (val m) ∎ + run (done (nat m) catch y ˢ) ⟶⟨ Red Catch₁ ⟩ + done (nat m) ∎ hunk ./Semantics/Equivalence.agda 99 - lift⟶∞ (val _ ⊕• •) (big⇒small⇑ y⇑) + lift⟶∞ (nat _ ⊕• •) (big⇒small⇑ y⇑) hunk ./Semantics/Equivalence.agda 136 -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⇓ (nat m ⊕• E) f (Add₁ x↡ y↡) = Add₁ x↡ (map⇓ E f y↡) +map⇓ (nat m ⊕• E) f (Add₂ x↯) = Add₂ x↯ +map⇓ (nat m ⊕• E) f (Add₃ x↡ y↯) = Add₃ x↡ (map⇓ E f y↯) +map⇓ (nat m ⊕• E) f Int = Int hunk ./Semantics/Equivalence.agda 159 -map⇑ (val m ⊕• E) f g (Add₁ ()) -map⇑ (val m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) +map⇑ (nat m ⊕• E) f g (Add₁ ()) +map⇑ (nat m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) hunk ./Semantics/Equivalence.agda 171 -small⇒big⟶ʳ⇓ Val ⇓ = ⇓ -small⇒big⟶ʳ⇓ Throw ⇓ = ⇓ -small⇒big⟶ʳ⇓ Loop ⇓ = ⇓ -small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val -small⇒big⟶ʳ⇓ Add₁ Int = Int -small⇒big⟶ʳ⇓ Add₂ Throw = Add₂ Throw -small⇒big⟶ʳ⇓ Add₂ Int = Int -small⇒big⟶ʳ⇓ Add₃ Throw = Add₃ Val Throw -small⇒big⟶ʳ⇓ Add₃ Int = Int -small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ -small⇒big⟶ʳ⇓ Seqn₂ Throw = Seqn₂ Throw -small⇒big⟶ʳ⇓ Seqn₂ Int = Int -small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val -small⇒big⟶ʳ⇓ Catch₁ Int = Int -small⇒big⟶ʳ⇓ (Catch₂ {v = val n}) Val = Catch₂ Throw Val -small⇒big⟶ʳ⇓ (Catch₂ {v = val n}) Int = Int -small⇒big⟶ʳ⇓ (Catch₂ {v = throw}) Throw = Catch₂ Throw Throw -small⇒big⟶ʳ⇓ (Catch₂ {v = throw}) Int = Int -small⇒big⟶ʳ⇓ (Block {v = val n}) Val = Block Val -small⇒big⟶ʳ⇓ (Block {v = val n}) Int = Int -small⇒big⟶ʳ⇓ (Block {v = throw}) Throw = Block Throw -small⇒big⟶ʳ⇓ (Block {v = throw}) Int = Int -small⇒big⟶ʳ⇓ (Unblock {v = val n}) Val = Unblock Val -small⇒big⟶ʳ⇓ (Unblock {v = val n}) Int = Int -small⇒big⟶ʳ⇓ (Unblock {v = throw}) Throw = Unblock Throw -small⇒big⟶ʳ⇓ (Unblock {v = throw}) Int = Int -small⇒big⟶ʳ⇓ (Int int) Throw = Int -small⇒big⟶ʳ⇓ (Int int) Int = Int +small⇒big⟶ʳ⇓ Val ⇓ = ⇓ +small⇒big⟶ʳ⇓ Loop ⇓ = ⇓ +small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val +small⇒big⟶ʳ⇓ Add₁ Int = Int +small⇒big⟶ʳ⇓ Add₂ Val = Add₂ Val +small⇒big⟶ʳ⇓ Add₂ Int = Int +small⇒big⟶ʳ⇓ Add₃ Val = Add₃ Val Val +small⇒big⟶ʳ⇓ Add₃ Int = Int +small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ +small⇒big⟶ʳ⇓ Seqn₂ Val = Seqn₂ Val +small⇒big⟶ʳ⇓ Seqn₂ Int = Int +small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val +small⇒big⟶ʳ⇓ Catch₁ Int = Int +small⇒big⟶ʳ⇓ Catch₂ Val = Catch₂ Val Val +small⇒big⟶ʳ⇓ Catch₂ Int = Int +small⇒big⟶ʳ⇓ Block Val = Block Val +small⇒big⟶ʳ⇓ Block Int = Int +small⇒big⟶ʳ⇓ Unblock Val = Unblock Val +small⇒big⟶ʳ⇓ Unblock Int = Int +small⇒big⟶ʳ⇓ (Int int) Val = Int +small⇒big⟶ʳ⇓ (Int int) Int = Int hunk ./Semantics/Equivalence.agda 195 -small⇒big⟶ʳ⇑ Val () -small⇒big⟶ʳ⇑ Throw () -small⇒big⟶ʳ⇑ Loop ⇑ = Loop ⇑ -small⇒big⟶ʳ⇑ Add₁ () -small⇒big⟶ʳ⇑ Add₂ () -small⇒big⟶ʳ⇑ Add₃ () -small⇒big⟶ʳ⇑ Seqn₁ ⇑ = Seqn₂ (_ , Val) ⇑ -small⇒big⟶ʳ⇑ Seqn₂ () -small⇒big⟶ʳ⇑ Catch₁ () -small⇒big⟶ʳ⇑ (Catch₂ {v = val n}) () -small⇒big⟶ʳ⇑ (Catch₂ {v = throw}) () -small⇒big⟶ʳ⇑ (Block {v = val n}) () -small⇒big⟶ʳ⇑ (Block {v = throw}) () -small⇒big⟶ʳ⇑ (Unblock {v = val n}) () -small⇒big⟶ʳ⇑ (Unblock {v = throw}) () -small⇒big⟶ʳ⇑ (Int int) () +small⇒big⟶ʳ⇑ Val () +small⇒big⟶ʳ⇑ Loop ⇑ = Loop ⇑ +small⇒big⟶ʳ⇑ Add₁ () +small⇒big⟶ʳ⇑ Add₂ () +small⇒big⟶ʳ⇑ Add₃ () +small⇒big⟶ʳ⇑ Seqn₁ ⇑ = Seqn₂ (_ , Val) ⇑ +small⇒big⟶ʳ⇑ Seqn₂ () +small⇒big⟶ʳ⇑ Catch₁ () +small⇒big⟶ʳ⇑ Catch₂ () +small⇒big⟶ʳ⇑ Block () +small⇒big⟶ʳ⇑ Unblock () +small⇒big⟶ʳ⇑ (Int int) () hunk ./Semantics/Equivalence.agda 211 -small⇒big⟶⋆ : forall {t} {e : Exprˢ t} {i} v -> +small⇒big⟶⋆ : forall {t} {e : Exprˢ t} {i v} -> hunk ./Semantics/Equivalence.agda 213 -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 ⟶⋆) +small⇒big⟶⋆ ε = Val +small⇒big⟶⋆ (⟶ ◅ ⟶⋆) with ⟶⇒⟶E ⟶ +small⇒big⟶⋆ (⟶ ◅ ⟶⋆) | Red E ⟶ʳ = + map⇓ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶⋆ ⟶⋆) hunk ./Semantics/Equivalence.agda 239 -small⇒big⟶∞ (run (val n)) i (Red Val ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) -small⇒big⟶∞ (run (val n)) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) -small⇒big⟶∞ (run throw) i (Red Throw ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) -small⇒big⟶∞ (run throw) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) +small⇒big⟶∞ (run ⌜ v ⌝) i (Red Val ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) +small⇒big⟶∞ (run ⌜ v ⌝) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) hunk ./Semantics/Equivalence.agda 244 - helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ]) -> ⊥ + helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) -> ⊥ hunk ./Semantics/Equivalence.agda 246 - helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Add₂ (n , small⇒big⟶⋆ (val n) x⟶⋆n)) + helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Add₂ (n , small⇒big⟶⋆ x⟶⋆n)) hunk ./Semantics/Equivalence.agda 249 - helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (val n)) × y ⟶∞[ i ]) -> ⊥ + helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) -> ⊥ hunk ./Semantics/Equivalence.agda 251 - helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Seqn₂ (n , small⇒big⟶⋆ (val n) x⟶⋆n)) + helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Seqn₂ (n , small⇒big⟶⋆ x⟶⋆n)) hunk ./Semantics/Equivalence.agda 256 - helper (inj₂ (x⟶⋆↯ , y⟶∞)) = small⇒big⟶∞ y B y⟶∞ (¬⇑ ∘ Catch₂ (small⇒big⟶⋆ throw x⟶⋆↯)) + helper (inj₂ (x⟶⋆↯ , y⟶∞)) = small⇒big⟶∞ y B y⟶∞ (¬⇑ ∘ Catch₂ (small⇒big⟶⋆ x⟶⋆↯)) hunk ./Semantics/SmallStep/EvalCtxt.agda 21 -infix 7 val_⊕•_ +infix 7 nat_⊕•_ hunk ./Semantics/SmallStep/EvalCtxt.agda 34 - val_⊕•_ : forall {i j} (m : ℕ) (E : EvalCtxt t i j) -> EvalCtxt t i j + nat_⊕•_ : forall {i j} (m : ℕ) (E : EvalCtxt t i j) -> EvalCtxt t i j hunk ./Semantics/SmallStep/EvalCtxt.agda 48 -(val n ⊕• E) [ y ] = run (done (val n) ⊕ E [ y ]) +(nat n ⊕• E) [ y ] = run (done (nat n) ⊕ E [ y ]) hunk ./Semantics/SmallStep/EvalCtxt.agda 62 -lift⟶ (val m ⊕• E) ⟶ = Addʳ (lift⟶ E ⟶) +lift⟶ (nat m ⊕• E) ⟶ = Addʳ (lift⟶ E ⟶) hunk ./Semantics/SmallStep/EvalCtxt.agda 86 -(val n ⊕• E₁) ⊚ E₂ = val n ⊕• (E₁ ⊚ E₂) +(nat n ⊕• E₁) ⊚ E₂ = nat n ⊕• (E₁ ⊚ E₂) hunk ./Semantics/SmallStep/EvalCtxt.agda 98 -⊚-lemma (val n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (val n) ⊕ x)) (⊚-lemma E₁ E₂) +⊚-lemma (nat n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (nat n) ⊕ x)) (⊚-lemma E₁ E₂) hunk ./Semantics/SmallStep/EvalCtxt.agda 128 -⟶⇒⟶E (Addʳ ⟶) = lift⟶E (val _ ⊕• •) (⟶⇒⟶E ⟶) +⟶⇒⟶E (Addʳ ⟶) = lift⟶E (nat _ ⊕• •) (⟶⇒⟶E ⟶) hunk ./Semantics/SmallStep/EvalCtxt.agda 141 -⟶E⇒⟶ (Red (val m ⊕• E) x⟶ʳy) = lift⟶ (val m ⊕• •) (⟶E⇒⟶ (Red E x⟶ʳy)) +⟶E⇒⟶ (Red (nat m ⊕• E) x⟶ʳy) = lift⟶ (nat m ⊕• •) (⟶E⇒⟶ (Red E x⟶ʳy)) hunk ./Semantics/SmallStep/StepGroups.agda 34 - size' (val n) = 0 - size' throw = 0 + size' ⌜ v ⌝ = 0 hunk ./Semantics/SmallStep/StepGroups.agda 48 -size-lemma (val m ⊕• E) gt = s≤s (size-lemma E gt) +size-lemma (nat m ⊕• E) gt = s≤s (size-lemma E gt) hunk ./Semantics/SmallStep/StepGroups.agda 84 -size-decreasesʳ Throw _ = s≤s z≤n hunk ./Semantics/SmallStep.agda 33 - val : forall {t} (n : ℕ) -> Exprˢ' t - throw : forall {t} -> Exprˢ' t + ⌜_⌝ : forall {t} (v : Value) -> Exprˢ' t hunk ./Semantics/SmallStep.agda 51 - val n ˢ' = val n - throw ˢ' = throw + ⌜ v ⌝ ˢ' = ⌜ v ⌝ hunk ./Semantics/SmallStep.agda 70 - val n ˢ'⁻¹ = val n - throw ˢ'⁻¹ = throw + ⌜ v ⌝ ˢ'⁻¹ = ⌜ v ⌝ hunk ./Semantics/SmallStep.agda 88 - interruptible (done (val n)) = true + interruptible (done (nat n)) = true hunk ./Semantics/SmallStep.agda 92 - interruptible' (val n) = true - interruptible' throw = true + interruptible' ⌜ v ⌝ = true hunk ./Semantics/SmallStep.agda 117 - Val : forall {t i m} -> t ∶ run (val m) ⟶ʳ[ i ] done (val m) - Throw : forall {t i} -> t ∶ run throw ⟶ʳ[ i ] done throw + Val : forall {t i v} -> t ∶ run ⌜ v ⌝ ⟶ʳ[ i ] done v hunk ./Semantics/SmallStep.agda 119 - Add₁ : forall {t i m n} -> t ∶ run (done (val m) ⊕ done (val n)) ⟶ʳ[ i ] done (val (m + n)) + Add₁ : forall {t i m n} -> t ∶ run (done (nat m) ⊕ done (nat n)) ⟶ʳ[ i ] done (nat (m + n)) hunk ./Semantics/SmallStep.agda 121 - Add₃ : forall {t i m} -> t ∶ run (done (val m) ⊕ done throw) ⟶ʳ[ i ] done throw - Seqn₁ : forall {t i m y} -> t ∶ run (done (val m) >> y) ⟶ʳ[ i ] y + Add₃ : forall {t i m} -> t ∶ run (done (nat m) ⊕ done throw) ⟶ʳ[ i ] done throw + Seqn₁ : forall {t i m y} -> t ∶ run (done (nat m) >> y) ⟶ʳ[ i ] y hunk ./Semantics/SmallStep.agda 124 - Catch₁ : forall {t i m y} -> t ∶ run (done (val m) catch y) ⟶ʳ[ i ] done (val m) + Catch₁ : forall {t i m y} -> t ∶ run (done (nat m) catch y) ⟶ʳ[ i ] done (nat m) hunk ./Semantics/SmallStep.agda 142 - Addʳ : forall {t m y y' i} (⟶ : y ⟶[ i ] y') -> t ∶ run (done (val m) ⊕ y) ⟶[ i ] run (done (val m) ⊕ y') + Addʳ : forall {t m y y' i} (⟶ : y ⟶[ i ] y') -> t ∶ run (done (nat m) ⊕ y) ⟶[ i ] run (done (nat m) ⊕ y') hunk ./Semantics/SmallStep.agda 181 -val n ˢ-interruptible = _ -throw ˢ-interruptible = _ +⌜ v ⌝ ˢ-interruptible = _ hunk ./Semantics/SmallStep.agda 192 -left-inverse (val n) = ≡-refl -left-inverse throw = ≡-refl +left-inverse ⌜ v ⌝ = ≡-refl hunk ./Semantics/SmallStep.agda 207 -run⟶ (val n) = (, Red Val) -run⟶ throw = (, Red Throw) +run⟶ ⌜ v ⌝ = (, Red Val) hunk ./Semantics/SmallStep.agda 210 -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 (nat m) ⊕ run y) = map-Σ _ Addʳ (run⟶ y) +run⟶ (done (nat m) ⊕ done (nat n)) = (, Red Add₁) +run⟶ (done (nat m) ⊕ done throw) = (, Red Add₃) hunk ./Semantics/SmallStep.agda 215 -run⟶ (done (val m) >> run x) = (, Red Seqn₁) -run⟶ (done (val m) >> done v) = (, Red Seqn₁) +run⟶ (done (nat m) >> run x) = (, Red Seqn₁) +run⟶ (done (nat m) >> done v) = (, Red Seqn₁) hunk ./Semantics/SmallStep.agda 219 -run⟶ (done (val m) catch y) = (, Red Catch₁) +run⟶ (done (nat m) catch y) = (, Red Catch₁) hunk ./StatusLemmas.agda 20 -Bto·⇓ Throw = Throw hunk ./StatusLemmas.agda 53 - x ⇓[ U ] val n -> x ⇓[ B ] val n) -¬UtoB UtoB with UtoB (val 0 catch val 1) (Catch₂ Int Val) + x ⇓[ U ] nat n -> x ⇓[ B ] nat n) +¬UtoB UtoB with UtoB (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝) (Catch₂ Int Val) hunk ./StatusLemmas.agda 62 -¬UtoB' UtoB' with UtoB' (loop catch val 0) (0 , Catch₂ Int Val) +¬UtoB' UtoB' with UtoB' (loop catch ⌜ nat 0 ⌝) (0 , Catch₂ Int Val) hunk ./StatusLemmas.agda 71 - helper : forall {x : Expr total} {i m} -> x ⇓[ U ] val m -> x ↡[ i ] + helper : forall {x : Expr total} {i m} -> x ⇓[ U ] nat m -> x ↡[ i ] hunk ./StatusLemmas.agda 80 - ... | (val n , x⇓) = (n , Catch₁ x⇓) + ... | (nat n , x⇓) = (n , Catch₁ x⇓) hunk ./StatusLemmas.agda 92 - with _⊑_.⇓ (bux⊑x total (val 0)) {i = B} (Block (Unblock Int)) + with _⊑_.⇓ (bux⊑x total ⌜ nat 0 ⌝) {i = B} (Block (Unblock Int)) hunk ./StatusLemmas.agda 97 - with _⊑_.⇓ (x⊑ubx total (val 0 catch val 1)) (Catch₂ Int Val) + with _⊑_.⇓ (x⊑ubx total (⌜ nat 0 ⌝ catch ⌜ nat 1 ⌝)) (Catch₂ Int Val) hunk ./StatusLemmas.agda 103 - with _⊑_.⇓ (ubx⊑x total (val 0)) {i = B} (Unblock Int) + with _⊑_.⇓ (ubx⊑x total ⌜ nat 0 ⌝) {i = B} (Unblock Int) hunk ./Syntax.agda 23 +-- Values. + +data Value : Set where + nat : (n : ℕ) -> Value + throw : Value + hunk ./Syntax.agda 32 - val : forall {t} (n : ℕ) -> Expr t - throw : forall {t} -> Expr t + ⌜_⌝ : forall {t} (v : Value) -> Expr t hunk ./Syntax.agda 41 -x finally y = block (unblock x catch (y >> throw) >> y) - --- Values. - -data Value : Set where - val : (n : ℕ) -> Value - throw : Value - -⌜_⌝ : forall {t} -> Value -> Expr t -⌜ val n ⌝ = val n -⌜ throw ⌝ = throw +x finally y = block (unblock x catch (y >> ⌜ throw ⌝) >> y) hunk ./Totality.agda 25 -defined (val n) _ = (_ , Val) -defined throw _ = (_ , Throw) +defined ⌜ v ⌝ _ = (_ , Val) hunk ./Totality.agda 27 -... | (val _ , x⇓) | (val _ , y⇓) = (_ , Add₁ x⇓ y⇓) -... | (val _ , x⇓) | (throw , y↯) = (_ , Add₃ x⇓ y↯) +... | (nat _ , x⇓) | (nat _ , y⇓) = (_ , Add₁ x⇓ y⇓) +... | (nat _ , x⇓) | (throw , y↯) = (_ , Add₃ x⇓ y↯) hunk ./Totality.agda 31 -... | (val _ , x⇓) | (val _ , y⇓) = (_ , Seqn₁ x⇓ y⇓) -... | (val _ , x⇓) | (throw , y↯) = (_ , Seqn₁ x⇓ y↯) +... | (nat _ , x⇓) | (nat _ , y⇓) = (_ , Seqn₁ x⇓ y⇓) +... | (nat _ , x⇓) | (throw , y↯) = (_ , Seqn₁ x⇓ y↯) hunk ./Totality.agda 35 -... | (val _ , x⇓) | _ = (_ , Catch₁ x⇓) -... | (throw , x↯) | (val _ , y⇓) = (_ , Catch₂ x↯ y⇓) +... | (nat _ , x⇓) | _ = (_ , Catch₁ x⇓) +... | (throw , x↯) | (nat _ , y⇓) = (_ , Catch₂ x↯ y⇓) hunk ./Totality.agda 44 -¬undefined (val n) () -¬undefined throw () +¬undefined ⌜ v ⌝ () hunk ./Totality.agda 59 -... | (val n , x↡) = (n , x↡) +... | (nat n , x↡) = (n , x↡) hunk ./Totality.agda 65 -... | (val n , x↡) = ⊥-elim (¬x↡ (n , x↡)) +... | (nat n , x↡) = ⊥-elim (¬x↡ (n , x↡)) hunk ./Totality.agda 71 -can-throw? _ U = yes Int -can-throw? (val n) B = no helper +can-throw? _ U = yes Int +can-throw? ⌜ nat m ⌝ B = no helper hunk ./Totality.agda 74 - helper : ¬ val n ↯[ B ] + helper : ¬ ⌜ nat m ⌝ ↯[ B ] hunk ./Totality.agda 76 -can-throw? throw B = yes Throw +can-throw? ⌜ throw ⌝ B = yes Val hunk ./Totality.agda 117 -can-return? (val m) i = yes (m , Val) -can-return? throw i = no helper +can-return? ⌜ nat m ⌝ i = yes (m , Val) +can-return? ⌜ throw ⌝ i = no helper hunk ./Totality.agda 120 - helper : ¬ throw ↡[ i ] + helper : ¬ ⌜ throw ⌝ ↡[ i ] hunk ./Totality.agda 176 -decidable x i | no ¬x↡ | no ¬x↯ | (val n , x↡) = ⊥-elim (¬x↡ (n , x↡)) +decidable x i | no ¬x↡ | no ¬x↯ | (nat n , x↡) = ⊥-elim (¬x↡ (n , x↡)) hunk ./VirtualMachine.agda 39 - val : ℕ -> Item + nat : ℕ -> Item hunk ./VirtualMachine.agda 54 - ⟨ push n ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , val n ∷ s ⟩ + ⟨ push n ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , nat n ∷ s ⟩ hunk ./VirtualMachine.agda 60 - ⟨ add ∷ ops , i , val n ∷ val m ∷ s ⟩ ⟶ - ⟨ ops , i , val (m + n) ∷ s ⟩ + ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶ + ⟨ ops , i , nat (m + n) ∷ s ⟩ hunk ./VirtualMachine.agda 63 - ⟨ pop ∷ ops , i , val n ∷ s ⟩ ⟶ ⟨ ops , i , s ⟩ + ⟨ pop ∷ ops , i , nat n ∷ s ⟩ ⟶ ⟨ ops , i , s ⟩ hunk ./VirtualMachine.agda 77 - val : forall {i n s} -> - ⟪ i , val n ∷ s ⟫ ⟶ ⟪ i , s ⟫ + nat : forall {i n s} -> + ⟪ i , nat n ∷ s ⟫ ⟶ ⟪ i , s ⟫ hunk ./VirtualMachine.agda 91 -comp (val n) ops = push n ∷ ops -comp throw ops = throw ∷ ops +comp ⌜ nat n ⌝ ops = push n ∷ ops +comp ⌜ throw ⌝ ops = throw ∷ ops