[Tried adding an infinitely looping construct. Nils Anders Danielsson **20080521194124 + This code is unfinished. + I decided to include non-termination as one of the results of the big-step semantics. However, this seems to be a bad idea, for two reasons: 1) With a more complicated language it won't be possible to include non-termination in the inductive big-step relation. 2) Non-termination requires special treatment in many results anyway, so breaking out non-termination into a separate relation will (probably) be a simplification. ] hunk ./AlgebraicProperties.agda 14 -import Algebra.FunctionProperties as AlgProp; open AlgProp ≈-setoid +import Algebra.FunctionProperties as AlgProp +private + open module AP (t : Totality) = AlgProp (≈-setoid t) hunk ./AlgebraicProperties.agda 19 +open import Data.Empty hunk ./AlgebraicProperties.agda 24 -cast : forall {n₁ n₂ x i} -> +cast : forall {n₁ n₂ i t} {x : Expr t} -> hunk ./AlgebraicProperties.agda 35 -⊕-assoc : Associative _⊕_ +⊕-assoc : forall {t} -> Associative t _⊕_ hunk ./AlgebraicProperties.agda 60 -catch-assoc : Associative _catch_ -catch-assoc x y z = equal ⟶ ⟵ +catch-assoc : forall {t} -> Associative t _catch_ +catch-assoc _ _ _ = equal ⟶ ⟵ hunk ./AlgebraicProperties.agda 63 - ⟶ : (x catch y) catch z ⊑ x catch (y catch z) + ⟶ : forall {t} {x y z : Expr t} -> + (x catch y) catch z ⊑ x catch (y catch z) hunk ./AlgebraicProperties.agda 69 + ⟶ (Catch₃ (Catch₂ x↯ y↯)) = Catch₂ x↯ (Catch₃ y↯) + ⟶ (Catch₃ (Catch₃ x⇑)) = Catch₃ x⇑ hunk ./AlgebraicProperties.agda 73 - ⟵ : x catch (y catch z) ⊑ (x catch y) catch z + ⟵ : forall {t} {x y z : Expr t} -> + x catch (y catch z) ⊑ (x catch y) catch z hunk ./AlgebraicProperties.agda 78 + ⟵ (Catch₂ x↯ (Catch₃ y⇑)) = Catch₃ (Catch₂ x↯ y⇑) hunk ./AlgebraicProperties.agda 80 + ⟵ (Catch₃ x⇑) = Catch₃ (Catch₃ x⇑) hunk ./AlgebraicProperties.agda 85 ->>-assoc : Associative _>>_ +>>-assoc : forall {t} -> Associative t _>>_ hunk ./AlgebraicProperties.agda 104 -finally-assocʳ : - forall {x y z} -> (x finally y) finally z ⊑ x finally (y finally z) +finally-assocʳ : forall {t} {x y z : Expr t} -> + (x finally y) finally z ⊑ x finally (y finally z) hunk ./AlgebraicProperties.agda 113 +finally-assocʳ (Block (Seqn₂ (Catch₃ (Unblock (Block (Seqn₁ (Catch₁ x⇓) y⇑)))))) = + Block (Seqn₁ (Catch₁ x⇓) (Block (Seqn₂ (Catch₃ (Unblock (Bto· y⇑)))))) +finally-assocʳ (Block (Seqn₂ (Catch₃ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))))) +finally-assocʳ (Block (Seqn₂ (Catch₃ (Unblock (Block (Seqn₂ (Catch₂ _ (Seqn₁ _ ())))))))) +finally-assocʳ (Block (Seqn₂ (Catch₃ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₂ y⇑)))))))) = + Block (Seqn₂ (Catch₂ x↯ (Seqn₂ (Block (Seqn₂ (Catch₃ (Unblock (Bto· y⇑)))))))) +finally-assocʳ (Block (Seqn₂ (Catch₃ (Unblock (Block (Seqn₂ (Catch₃ x⇑))))))) = + Block (Seqn₂ (Catch₃ x⇑)) hunk ./AlgebraicProperties.agda 122 --- In a non-total setting _finally_ is not associative (c.f. +-- In a partial setting _finally_ is not associative (c.f. hunk ./AlgebraicProperties.agda 125 -¬finally-assoc : NonTotal -> ¬ Associative _finally_ -¬finally-assoc (¬⇓ x i ¬x⇓) assoc with assoc (val 0) (x catch val 0) (val 0) -... | equal _ f with f {i = i} (Block (Seqn₁ (Catch₁ (Unblock Val)) +¬finally-assoc : ¬ Associative partial _finally_ +¬finally-assoc assoc with assoc (val 0) (loop catch val 0) (val 0) +... | equal _ f with f {i = U} (Block (Seqn₁ (Catch₁ (Unblock Val)) hunk ./AlgebraicProperties.agda 130 -... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ x⇓))))) Val) = - ¬x⇓ (_ , Bto· x⇓) -... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ x↯ _))))) Val) = - ¬x⇓ (_ , Bto· x↯) +... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ ()))))) Val) +... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ () _))))) Val) hunk ./AlgebraicProperties.agda 137 -finally-assoc : Total -> Associative _finally_ -finally-assoc total x y z = equal finally-assocʳ ⟵ +finally-assoc : Associative total _finally_ +finally-assoc x y z = equal finally-assocʳ ⟵ hunk ./AlgebraicProperties.agda 145 - where y' = proj₂ (Uto·' total (_ , y)) + where y' = proj₂ (Uto·' (_ , y)) hunk ./AlgebraicProperties.agda 150 - ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Throw))) + ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) Throw)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Throw))) hunk ./AlgebraicProperties.agda 159 -⊕-comm : Total -> Commutative _⊕_ -⊕-comm total x y = equal (⟶ _ _) (⟶ _ _) +⊕-comm : Commutative total _⊕_ +⊕-comm x y = equal (⟶ _ _) (⟶ _ _) hunk ./AlgebraicProperties.agda 165 - ⟶ _ _ Int = Int - ⟶ _ _ (Add₃ x⇓ y↯) = Add₂ y↯ - ⟶ x y {i = i} (Add₂ x↯) with total y i - ⟶ x y {i = i} (Add₂ x↯) | returns y⇓ = Add₃ y⇓ x↯ - ⟶ x y {i = i} (Add₂ x↯) | throws y↯ = Add₂ y↯ + ⟶ _ _ Int = Int + ⟶ _ _ (Add₃ x⇓ y↯) = Add₂ y↯ + ⟶ x y {i = i} (Add₂ x↯) with defined y i + ⟶ x y {i = i} (Add₂ x↯) | returns y⇓ = Add₃ y⇓ x↯ + ⟶ x y {i = i} (Add₂ {r = throw} x↯) | throws y↯ = Add₂ y↯ hunk ./AlgebraicProperties.agda 173 --- _⊕_ is not commutative if the language is non-total. - -¬⊕-comm : NonTotal -> ¬ Commutative _⊕_ -¬⊕-comm (¬⇓ x i ¬x⇓) ⊕-comm with ⊕-comm throw x -¬⊕-comm (¬⇓ x i ¬x⇓) ⊕-comm | equal ⟵ ⟶ = helper (⟵ (Add₂ Throw)) - where - ¬x⇓B : ¬ Σ₀ (\v -> x ⇓[ B ] v) - ¬x⇓B (v , x⇓) = ¬x⇓ (v , Bto· x⇓) +-- _⊕_ is not commutative if the language is partial. hunk ./AlgebraicProperties.agda 175 - helper : ¬ (x ⊕ throw ⇓[ B ] throw) - helper (Add₂ x↯) = ¬x⇓B (throw , x↯) - helper (Add₃ x⇓ _) = ¬x⇓B (_ , x⇓) +¬⊕-comm : ¬ Commutative partial _⊕_ +¬⊕-comm ⊕-comm with ⊕-comm throw loop +¬⊕-comm ⊕-comm | equal ⟵ ⟶ with ⟵ {i = B} (Add₂ Throw) +... | Add₂ () +... | Add₃ () _ hunk ./CompilerCorrectness.agda 13 +open import Data.Unit hunk ./CompilerCorrectness.agda 18 +import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness.agda 29 -start : Expr -> Status -> State +start : forall {t} -> Expr t -> Status -> State hunk ./CompilerCorrectness.agda 40 -data Matches (e : Expr) (i : Status) : State -> Set where +data Matches {t : _} (e : Expr t) (i : Status) : State -> Set where hunk ./CompilerCorrectness.agda 46 --- starting one (according to _⇓[_]_). +-- starting one (according to _⇓[_]_). Furthermore, if no final state +-- is reached, then the original expression can loop. hunk ./CompilerCorrectness.agda 49 -Sound : Expr -> Status -> Set -Sound e i = forall {c} -> start e i ⟶⋆ c -> Final c -> Matches e i c +Sound₁ : forall {t} -> Expr t -> Status -> Set +Sound₁ e i = forall {c} -> start e i ⟶⋆ c -> Final c -> Matches e i c + +Sound₂ : Expr partial -> Status -> Set +Sound₂ e i = start e i ⟶∞ -> e ⇑[ i ] + +Sound : forall t -> Expr t -> Status -> Set +Sound total e i = Sound₁ e i +Sound partial e i = Sound₁ e i × Sound₂ e i hunk ./CompilerCorrectness.agda 62 -Complete₁ : Expr -> Status -> Set +Complete₁ : forall {t} -> Expr t -> Status -> Set hunk ./CompilerCorrectness.agda 65 --- The second part of completeness: If the program must terminate --- (vacuously true for the current language), then some final state --- _will_ be reached. - --- Note that this result actually implies soundness (under some mild --- extra assumptions), see CompilerCorrectness.Soundness. +-- The second part of completeness: If the program can fail to +-- terminate, then the VM can also fail to terminate. + +Complete₂ : Expr partial -> Status -> Set +Complete₂ e i = e ⇑[ i ] -> start e i ⟶∞ + +-- The third part of completeness: If the program must terminate, +-- then some final state _will_ be reached. hunk ./CompilerCorrectness.agda 74 -Complete₂ : Expr -> Status -> Set -Complete₂ e i = start e i ◁ Matches e i +DoesNotLoop : forall t -> Expr t -> Status -> Set +DoesNotLoop total e i = ⊤ +DoesNotLoop partial e i = ¬ e ⇑[ i ] + +Complete₃ : forall t -> Expr t -> Status -> Set +Complete₃ t e i = DoesNotLoop t e i -> start e i ◁ Matches e i + +-- Completeness. + +Complete : forall t -> Expr t -> Status -> Set +Complete total e i = Complete₁ e i × Complete₃ total e i +Complete partial e i = Complete₁ e i × Complete₂ e i × + Complete₃ partial e i hunk ./CompilerCorrectness.agda 90 -CompilerCorrect : Expr -> Status -> Set -CompilerCorrect e i = Sound e i × Complete₁ e i × Complete₂ e i +CompilerCorrect : forall t -> Expr t -> Status -> Set +CompilerCorrect t e i = Sound t e i × Complete t e i hunk ./CompilerCorrectness/Completeness1.agda 2 --- The first part of the completeness proof +-- The first and second part of the completeness proof hunk ./CompilerCorrectness/Completeness1.agda 10 +import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness/Completeness1.agda 20 -[]≢∷ : forall {x xs} -> [] ≢ x ∷ xs +[]≢∷ : forall {a} {x : a} {xs} -> [] ≢ x ∷ xs hunk ./CompilerCorrectness/Completeness1.agda 25 -code-nonempty : forall e ops -> [] ≢ comp e ops +code-nonempty : forall {t} (e : Expr t) ops -> [] ≢ comp e ops hunk ./CompilerCorrectness/Completeness1.agda 33 +code-nonempty loop ops = []≢∷ hunk ./CompilerCorrectness/Completeness1.agda 36 --- The first part of the completeness proof +-- The first and second part of the completeness proof hunk ./CompilerCorrectness/Completeness1.agda 40 - complete⇓ : forall {e ops i s n} -> + complete⇓ : forall {t} {e : Expr t} {ops i s n} -> hunk ./CompilerCorrectness/Completeness1.agda 42 - Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟨ ops , i , val n ∷ s ⟩ + ⟨ comp e ops , i , s ⟩ ⟶⋆ ⟨ ops , i , val n ∷ s ⟩ hunk ./CompilerCorrectness/Completeness1.agda 51 - complete↯ : forall {e ops i s} -> - e ↯[ i ] -> Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟪ i , s ⟫ + complete↯ : forall {t} {e : Expr t} {ops i s} -> + e ↯[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶⋆ ⟪ i , s ⟫ hunk ./CompilerCorrectness/Completeness1.agda 61 - complete↯ {e} {ops} {s = s} Int with inspect (comp e ops) + complete↯ {e = e} {ops} {s = s} Int with inspect (comp e ops) hunk ./CompilerCorrectness/Completeness1.agda 67 -complete₁ : forall e {i} -> Complete₁ e i + complete⇑ : forall {e ops i s} -> + e ⇑[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶∞ + complete⇑ (Add₂ x) = complete⇑ x + complete⇑ (Add₃ x y) = complete⇓ x ◅◅∞ complete⇑ y + complete⇑ (Seqn₁ x y) = complete⇓ x ◅◅∞ pop ◅∞ complete⇑ y + complete⇑ (Seqn₂ x) = complete⇑ x + complete⇑ (Catch₂ x y) = mark ◅∞ complete↯ x ◅◅∞ han ◅∞ complete⇑ y + complete⇑ (Catch₃ x) = mark ◅∞ complete⇑ x + complete⇑ (Block x) = set ◅∞ complete⇑ x + complete⇑ (Unblock x) = set ◅∞ complete⇑ x + complete⇑ Loop = loop loops + +complete₁ : forall {t} (e : Expr t) {i} -> Complete₁ e i hunk ./CompilerCorrectness/Completeness1.agda 83 +complete₂ : forall e {i} -> Complete₂ e i +complete₂ _ = complete⇑ + hunk ./CompilerCorrectness/Completeness2.agda 10 +open import CompilerCorrectness.DoesNotLoopLemmas hunk ./CompilerCorrectness/Completeness2.agda 15 +open import Data.Empty hunk ./CompilerCorrectness/Completeness2.agda 20 -data Matches⁺ (ops : Code) (s : Stack) (e : Expr) (i : Status) +data Matches⁺ (ops : Code) (s : Stack) {t : _} (e : Expr t) (i : Status) hunk ./CompilerCorrectness/Completeness2.agda 28 -Matches⁺⇒Matches : forall {e i} -> Matches⁺ [] [] e i ⊆ Matches e i +Matches⁺⇒Matches : forall {t} {e : Expr t} {i} -> + Matches⁺ [] [] e i ⊆ Matches e i hunk ./CompilerCorrectness/Completeness2.agda 35 -bar-theorem : forall e {ops i s} -> +bar-theorem : forall t (e : Expr t) {ops i s} -> + DoesNotLoop t e i -> hunk ./CompilerCorrectness/Completeness2.agda 38 -bar-theorem (val n) = via (_ , push) helper +bar-theorem t (val n) ¬⇑ = via (_ , push) helper hunk ./CompilerCorrectness/Completeness2.agda 41 - ⟨ push n ∷ ops , i , s ⟩ ⟶ y -> y ◁ Matches⁺ ops s (val n) i + ⟨ push n ∷ ops , i , s ⟩ ⟶ y -> + y ◁ Matches⁺ ops s {t = t} (val n) i hunk ./CompilerCorrectness/Completeness2.agda 46 -bar-theorem throw = via (_ , throw) helper +bar-theorem t throw ¬⇑ = via (_ , throw) helper hunk ./CompilerCorrectness/Completeness2.agda 49 - ⟨ throw ∷ ops , i , s ⟩ ⟶ y -> y ◁ Matches⁺ ops s throw i + ⟨ throw ∷ ops , i , s ⟩ ⟶ y -> + y ◁ Matches⁺ ops s {t = t} throw i hunk ./CompilerCorrectness/Completeness2.agda 54 -bar-theorem (x ⊕ y) = ◁-trans (bar-theorem x) helper₁ +bar-theorem t (x ⊕ y) ¬⇑ = ◁-trans (bar-theorem t x (dnl-⊕ˡ t ¬⇑)) + (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 88 + DoesNotLoop t (x ⊕ y) i -> hunk ./CompilerCorrectness/Completeness2.agda 91 - helper₁ (throws x↯) = directly (throws (Add₂ x↯)) - helper₁ (returns x⇓) = ◁-trans (bar-theorem y) (helper₂ x⇓) + helper₁ _ (throws x↯) = directly (throws (Add₂ x↯)) + helper₁ ¬⇑ (returns x⇓) = ◁-trans (bar-theorem t y (dnl-⊕ʳ t ¬⇑ x⇓)) + (helper₂ x⇓) hunk ./CompilerCorrectness/Completeness2.agda 95 -bar-theorem (x >> y) = ◁-trans (bar-theorem x) helper₁ +bar-theorem t (x >> y) ¬⇑ = ◁-trans (bar-theorem t x (dnl->>ˡ t ¬⇑)) + (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 111 - x ⇓[ i ] val m -> + DoesNotLoop t (x >> y) i -> x ⇓[ i ] val m -> hunk ./CompilerCorrectness/Completeness2.agda 114 - helper₂ x⇓ pop = ◁-trans (bar-theorem y) (helper₃ x⇓) - helper₂ _ interrupt = via (_ , val) helper₄ + helper₂ ¬⇑ x⇓ pop = ◁-trans (bar-theorem t y (dnl->>ʳ t ¬⇑ x⇓)) + (helper₃ x⇓) + helper₂ _ _ interrupt = via (_ , val) helper₄ hunk ./CompilerCorrectness/Completeness2.agda 119 + DoesNotLoop t (x >> y) i -> hunk ./CompilerCorrectness/Completeness2.agda 122 - helper₁ (throws x↯) = directly (throws (Seqn₂ x↯)) - helper₁ (returns x⇓) = via (_ , pop) (helper₂ x⇓) + helper₁ _ (throws x↯) = directly (throws (Seqn₂ x↯)) + helper₁ ¬⇑ (returns x⇓) = via (_ , pop) (helper₂ ¬⇑ x⇓) hunk ./CompilerCorrectness/Completeness2.agda 125 -bar-theorem (x catch y) = via (_ , mark) helper₁ +bar-theorem t (x catch y) ¬⇑ = via (_ , mark) (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 135 - x ↯[ i ] -> + DoesNotLoop t (x catch y) i -> x ↯[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 138 - helper₆ x↯ han = ◁-trans (bar-theorem y) (helper₇ x↯) + helper₆ ¬⇑ x↯ han = ◁-trans (bar-theorem t y (dnl-catchʳ t ¬⇑ x↯)) + (helper₇ x↯) hunk ./CompilerCorrectness/Completeness2.agda 142 - x ↯[ i ] -> + DoesNotLoop t (x catch y) i -> x ↯[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 145 - helper₅ x↯ = via (_ , han) (helper₆ x↯) + helper₅ ¬⇑ x↯ = via (_ , han) (helper₆ ¬⇑ x↯) hunk ./CompilerCorrectness/Completeness2.agda 148 + DoesNotLoop t (x catch y) U -> hunk ./CompilerCorrectness/Completeness2.agda 151 - helper₄ val = helper₅ Int + helper₄ ¬⇑ val = helper₅ ¬⇑ Int hunk ./CompilerCorrectness/Completeness2.agda 154 - x ⇓[ i ] val m -> + DoesNotLoop t (x catch y) i -> x ⇓[ i ] val m -> hunk ./CompilerCorrectness/Completeness2.agda 157 - helper₃ x⇓ unmark = directly (returns (Catch₁ x⇓)) - helper₃ _ interrupt = via (_ , val) helper₄ + helper₃ _ x⇓ unmark = directly (returns (Catch₁ x⇓)) + helper₃ ¬⇑ _ interrupt = via (_ , val) (helper₄ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 161 + DoesNotLoop t (x catch y) i -> hunk ./CompilerCorrectness/Completeness2.agda 164 - helper₂ (returns x⇓) = via (_ , unmark) (helper₃ x⇓) - helper₂ (throws x↯) = helper₅ x↯ + helper₂ ¬⇑ (returns x⇓) = via (_ , unmark) (helper₃ ¬⇑ x⇓) + helper₂ ¬⇑ (throws x↯) = helper₅ ¬⇑ x↯ hunk ./CompilerCorrectness/Completeness2.agda 168 + DoesNotLoop t (x catch y) i -> hunk ./CompilerCorrectness/Completeness2.agda 171 - helper₁ mark = ◁-trans (bar-theorem x) helper₂ - helper₁ interrupt = directly (throws Int) + helper₁ ¬⇑ mark = ◁-trans (bar-theorem t x (dnl-catchˡ t ¬⇑)) + (helper₂ ¬⇑) + helper₁ _ interrupt = directly (throws Int) hunk ./CompilerCorrectness/Completeness2.agda 175 -bar-theorem (block x) = via (_ , set) helper₁ +bar-theorem t (block x) ¬⇑ = via (_ , set) helper₁ hunk ./CompilerCorrectness/Completeness2.agda 198 - helper₁ set = ◁-trans (bar-theorem x) helper₂ + helper₁ set = ◁-trans (bar-theorem t x (dnl-block t ¬⇑)) + helper₂ hunk ./CompilerCorrectness/Completeness2.agda 202 -bar-theorem (unblock x) = via (_ , set) helper₁ +bar-theorem t (unblock x) ¬⇑ = via (_ , set) helper₁ hunk ./CompilerCorrectness/Completeness2.agda 236 - helper₁ set = ◁-trans (bar-theorem x) helper₂ + helper₁ set = ◁-trans (bar-theorem t x (dnl-unblock t ¬⇑)) + helper₂ hunk ./CompilerCorrectness/Completeness2.agda 240 --- The second part of the completeness proof. +bar-theorem partial loop ¬⇑ = ⊥-elim (¬⇑ Loop) + +-- The third part of the completeness proof. hunk ./CompilerCorrectness/Completeness2.agda 244 -complete₂ : forall e {i} -> Complete₂ e i -complete₂ e = ◁-map Matches⁺⇒Matches (bar-theorem e) +complete₃ : forall {t} e {i} -> Complete₃ t e i +complete₃ e ¬⇑ = ◁-map Matches⁺⇒Matches (bar-theorem _ e ¬⇑) addfile ./CompilerCorrectness/DoesNotLoopLemmas.agda hunk ./CompilerCorrectness/DoesNotLoopLemmas.agda 1 +------------------------------------------------------------------------ +-- Boring lemmas about DoesNotLoop +------------------------------------------------------------------------ + +module CompilerCorrectness.DoesNotLoopLemmas where + +open import Language +open import CompilerCorrectness + +dnl-⊕ˡ : forall t {x y i} -> + DoesNotLoop t (x ⊕ y) i -> DoesNotLoop t x i +dnl-⊕ˡ total _ = _ +dnl-⊕ˡ partial ¬⇑ = \x⇑ -> ¬⇑ (Add₂ x⇑) + +dnl-⊕ʳ : forall t {x y i n} -> + DoesNotLoop t (x ⊕ y) i -> x ⇓[ i ] val n -> DoesNotLoop t y i +dnl-⊕ʳ total _ _ = _ +dnl-⊕ʳ partial ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Add₃ x⇓ y⇑) + +dnl->>ˡ : forall t {x y i} -> + DoesNotLoop t (x >> y) i -> DoesNotLoop t x i +dnl->>ˡ total _ = _ +dnl->>ˡ partial ¬⇑ = \x⇑ -> ¬⇑ (Seqn₂ x⇑) + +dnl->>ʳ : forall t {x y i n} -> + DoesNotLoop t (x >> y) i -> x ⇓[ i ] val n -> + DoesNotLoop t y i +dnl->>ʳ total _ _ = _ +dnl->>ʳ partial ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Seqn₁ x⇓ y⇑) + +dnl-catchˡ : forall t {x y i} -> + DoesNotLoop t (x catch y) i -> DoesNotLoop t x i +dnl-catchˡ total _ = _ +dnl-catchˡ partial ¬⇑ = \x⇑ -> ¬⇑ (Catch₃ x⇑) + +dnl-catchʳ : forall t {x y i} -> + DoesNotLoop t (x catch y) i -> x ↯[ i ] -> + DoesNotLoop t y i +dnl-catchʳ total _ _ = _ +dnl-catchʳ partial ¬⇑ x↯ = \y⇑ -> ¬⇑ (Catch₂ x↯ y⇑) + +dnl-block : forall t {x i} -> + DoesNotLoop t (block x) i -> DoesNotLoop t x B +dnl-block total _ = _ +dnl-block partial ¬⇑ = \x⇑ -> ¬⇑ (Block x⇑) + +dnl-unblock : forall t {x i} -> + DoesNotLoop t (unblock x) i -> DoesNotLoop t x U +dnl-unblock total _ = _ +dnl-unblock partial ¬⇑ = \x⇑ -> ¬⇑ (Unblock x⇑) hunk ./CompilerCorrectness/Soundness.agda 8 +open import Language hunk ./CompilerCorrectness/Soundness.agda 19 -matches-final : forall {e i c} -> Matches e i c -> ¬ c ⟶ +matches-final : forall {t e i c} -> Matches {t} e i c -> ¬ c ⟶ hunk ./CompilerCorrectness/Soundness.agda 27 --- Soundness. Depends crucially on the bar theorem (complete₂). +-- The first part of soundness. Depends crucially on the bar theorem +-- (complete₂). hunk ./CompilerCorrectness/Soundness.agda 30 -sound : forall e {i} -> Sound e i -sound e r f = bar-lemma matches-final (complete₂ e) r (final-final f) +sound₁ : forall {t} (e : Expr t) {i} -> Sound₁ e i +sound₁ e r f = bar-lemma matches-final (complete₃ e {! !}) r (final-final f) + +-- Soundness. + +sound : forall t e {i} -> Sound t e i +sound total e = sound₁ e +sound partial e = ((\{_} -> sound₁ e) , {! !}) hunk ./Equivalence.agda 17 -_⊑_ : Expr -> Expr -> Set +_⊑_ : forall {t} -> Expr t -> Expr t -> Set hunk ./Equivalence.agda 27 -data _≈_ (x y : Expr) : Set where +data _≈_ {t : Totality} (x y : Expr t) : Set where hunk ./Equivalence.agda 32 -⊑-preorder : Preorder -⊑-preorder = record - { carrier = Expr +⊑-preorder : Totality -> Preorder +⊑-preorder t = record + { carrier = Expr t hunk ./Equivalence.agda 53 -≈-setoid : Setoid -≈-setoid = record - { carrier = Expr +≈-setoid : Totality -> Setoid +≈-setoid t = record + { carrier = Expr t hunk ./Everything.agda 20 --- The bar relation, use to state compiler correctness. +-- The bar relation, used to state compiler correctness. hunk ./Everything.agda 24 +-- Infinite transition sequences, used to state compiler correctness. + +import Infinite + hunk ./Everything.agda 34 -import CompilerCorrectness.Soundness hunk ./Everything.agda 35 +import CompilerCorrectness.DoesNotLoopLemmas hunk ./Everything.agda 37 +import CompilerCorrectness.Soundness addfile ./Infinite.agda hunk ./Infinite.agda 1 +------------------------------------------------------------------------ +-- Infinite transition sequences +------------------------------------------------------------------------ + +open import Relation.Binary + +module Infinite {S : Set} (_⟶_ : Rel S) where + +open import Data.Star +open import Data.Product +open import Data.Nat +open import Data.Function + +infix 4 _⟶∞ + +-- x ⟶∞ means that there is an infinite transition sequence starting +-- at x. + +_⟶∞ : S -> Set +x ⟶∞ = Σ (ℕ -> S) \seq -> + (x ⟨ Star _⟶_ ⟩₁ seq 0) + × + (forall n -> seq n ⟶ seq (suc n)) + +-- Some lemmas. + +_loops : forall {x} -> x ⟶ x -> x ⟶∞ +_loops {x} x⟶x = (const x , ε , const x⟶x) + +infixr 5 _◅∞_ _◅◅∞_ + +_◅∞_ : forall {x y} -> x ⟶ y -> y ⟶∞ -> x ⟶∞ +x⟶y ◅∞ (seq , y⟶⋆z , step) = (seq , x⟶y ◅ y⟶⋆z , step) + +_◅◅∞_ : forall {x y} -> x ⟨ Star _⟶_ ⟩₁ y -> y ⟶∞ -> x ⟶∞ +x⟶⋆y ◅◅∞ (seq , y⟶⋆z , step) = (seq , x⟶⋆y ◅◅ y⟶⋆z , step) hunk ./Language.agda 6 --- (Hutton/Wright). +-- (Hutton/Wright), but modified by me. hunk ./Language.agda 20 -data Expr : Set where - val : ℕ -> Expr - throw : Expr - _⊕_ : Expr -> Expr -> Expr - _>>_ : Expr -> Expr -> Expr - _catch_ : Expr -> Expr -> Expr - block : Expr -> Expr - unblock : Expr -> Expr +-- Is the language total? hunk ./Language.agda 22 -_finally_ : Expr -> Expr -> Expr +data Totality : Set where + total : Totality + partial : Totality + +-- Expressions. + +data Expr : Totality -> Set where + val : forall {t} -> ℕ -> Expr t + throw : forall {t} -> Expr t + _⊕_ : forall {t} -> Expr t -> Expr t -> Expr t + _>>_ : forall {t} -> Expr t -> Expr t -> Expr t + _catch_ : forall {t} -> Expr t -> Expr t -> Expr t + block : forall {t} -> Expr t -> Expr t + unblock : forall {t} -> Expr t -> Expr t + loop : Expr partial + +_finally_ : forall {t} -> Expr t -> Expr t -> Expr t hunk ./Language.agda 44 -infix 3 _⇓[_]_ _⇓[_] _↯[_] +infix 3 _⇓[_]_ _⇓[_] _↯[_] _⇑[_] hunk ./Language.agda 50 -data Value : Set where - val : ℕ -> Value - throw : Value +-- The reason for program failure. + +data Reason : Totality -> Set where + throw : forall {t} -> Reason t + loop : Reason partial hunk ./Language.agda 56 -⌜_⌝ : Value -> Expr -⌜ val n ⌝ = val n -⌜ throw ⌝ = throw +-- Values. hunk ./Language.agda 58 -data _⇓[_]_ : Expr -> Status -> Value -> Set where - Val : forall {n i} -> val n ⇓[ i ] val n - Throw : forall {i} -> throw ⇓[ i ] throw - Add₁ : forall {x y m n i} -> +data Value (t : Totality) : Set where + val : ℕ -> Value t + fail : Reason t -> Value t + +⌜_⌝ : forall {t} -> Value t -> Expr t +⌜ val n ⌝ = val n +⌜ fail throw ⌝ = throw +⌜ fail loop ⌝ = loop + +data _⇓[_]_ : forall {t} -> Expr t -> Status -> Value t -> Set where + Val : forall {t n i} -> val {t = t} n ⇓[ i ] val n + Throw : forall {t i} -> throw {t = t} ⇓[ i ] fail throw + Add₁ : forall {t} {x y : Expr t} {m n i} -> hunk ./Language.agda 73 - Add₂ : forall {x y i} -> - x ⇓[ i ] throw -> x ⊕ y ⇓[ i ] throw - Add₃ : forall {x y m i} -> - x ⇓[ i ] val m -> y ⇓[ i ] throw -> x ⊕ y ⇓[ i ] throw - Seqn₁ : forall {x y m v i} -> + Add₂ : forall {t} {x y : Expr t} {i r} -> + x ⇓[ i ] fail r -> x ⊕ y ⇓[ i ] fail r + Add₃ : forall {t} {x y : Expr t} {m i r} -> + x ⇓[ i ] val m -> y ⇓[ i ] fail r -> x ⊕ y ⇓[ i ] fail r + Seqn₁ : forall {t} {x y : Expr t} {m v i} -> hunk ./Language.agda 79 - Seqn₂ : forall {x y i} -> - x ⇓[ i ] throw -> x >> y ⇓[ i ] throw - Catch₁ : forall {x y m i} -> + Seqn₂ : forall {t} {x y : Expr t} {i r} -> + x ⇓[ i ] fail r -> x >> y ⇓[ i ] fail r + Catch₁ : forall {t} {x y : Expr t} {m i} -> hunk ./Language.agda 83 - Catch₂ : forall {x y v i} -> - x ⇓[ i ] throw -> y ⇓[ i ] v -> x catch y ⇓[ i ] v - Int : forall {x} -> x ⇓[ U ] throw - Block : forall {x v i} -> + Catch₂ : forall {t} {x y : Expr t} {v i} -> + x ⇓[ i ] fail throw -> y ⇓[ i ] v -> x catch y ⇓[ i ] v + Catch₃ : forall {x y} {i} -> + x ⇓[ i ] fail loop -> x catch y ⇓[ i ] fail loop + Int : forall {t} {x : Expr t} -> x ⇓[ U ] fail throw + Block : forall {t} {x : Expr t} {v i} -> hunk ./Language.agda 90 - Unblock : forall {x v i} -> + Unblock : forall {t} {x : Expr t} {v i} -> hunk ./Language.agda 92 + Loop : forall {i} -> loop ⇓[ i ] fail loop hunk ./Language.agda 96 -_⇓[_] : Expr -> Status -> Set +_⇓[_] : forall {t} -> Expr t -> Status -> Set hunk ./Language.agda 99 -_↯[_] : Expr -> Status -> Set -x ↯[ i ] = x ⇓[ i ] throw +_↯[_] : forall {t} -> Expr t -> Status -> Set +x ↯[ i ] = x ⇓[ i ] fail throw + +_⇑[_] : Expr partial -> Status -> Set +x ⇑[ i ] = x ⇓[ i ] fail loop hunk ./SmallStep.agda 16 -data _⟶ʳ[_]_ : Expr -> Status -> Expr -> Set where - Add₁ : forall {i m n} -> val m ⊕ val n ⟶ʳ[ i ] val (m + n) - Add₂ : forall {i y} -> throw ⊕ y ⟶ʳ[ i ] throw - Add₃ : forall {i m} -> val m ⊕ throw ⟶ʳ[ i ] throw - Seqn₁ : forall {i m y} -> val m >> y ⟶ʳ[ i ] y - Seqn₂ : forall {i y} -> throw >> y ⟶ʳ[ i ] throw - Catch₁ : forall {i m y} -> val m catch y ⟶ʳ[ i ] val m - Catch₂ : forall {i y} -> throw catch y ⟶ʳ[ i ] y - Int : forall {x} -> x ⟶ʳ[ U ] throw - Block : forall {i v} -> block ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ - Unblock : forall {i v} -> unblock ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ +data _⟶ʳ[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set where + Add₁ : forall {t i m n} -> + val m ⊕ val n ⟶ʳ[ i ] val {t = t} (m + n) + Add₂ : forall {t i r} {y : Expr t} -> fail r ⊕ y ⟶ʳ[ i ] fail r + Add₃ : forall {t i m} {r : Reason t} -> + val m ⊕ fail r ⟶ʳ[ i ] fail r + Seqn₁ : forall {t i m} {y : Expr t} -> val m >> y ⟶ʳ[ i ] y + Seqn₂ : forall {t i r} {y : Expr t} -> fail r >> y ⟶ʳ[ i ] fail r + Catch₁ : forall {t i m} {y : Expr t} -> val m catch y ⟶ʳ[ i ] val m + Catch₂ : forall {t i} {y : Expr t} -> fail throw catch y ⟶ʳ[ i ] y + Catch₃ : forall {i y} -> fail loop catch y ⟶ʳ[ i ] fail loop catch y + Int : forall {t} {x : Expr t} -> x ⟶ʳ[ U ] fail throw + Block : forall {t i} {v : Value t} -> block ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ + Unblock : forall {t i} {v : Value t} -> unblock ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ + Loop : forall {i} -> fail loop ⟶ʳ[ i ] fail loop hunk ./SmallStep.agda 46 -_⟨_⟩_ : Expr -> Op -> Expr -> Expr +_⟨_⟩_ : forall {t} -> Expr t -> Op -> Expr t -> Expr t hunk ./SmallStep.agda 54 -data EvalCtxt : Status -> Status -> Set where - • : forall {i} -> EvalCtxt i i - _•[_]_ : forall {i j} -> EvalCtxt i j -> Op -> Expr -> EvalCtxt i j - _[_]•_ : forall {i j} -> Value -> Op -> EvalCtxt i j -> EvalCtxt i j - block• : forall {i j} -> EvalCtxt i B -> EvalCtxt i j - unblock• : forall {i j} -> EvalCtxt i U -> EvalCtxt i j +data EvalCtxt (t : Totality) : Status -> Status -> Set where + • : forall {i} -> EvalCtxt t i i + _•[_]_ : forall {i j} -> + EvalCtxt t i j -> Op -> Expr t -> EvalCtxt t i j + _[_]•_ : forall {i j} -> + Value t -> Op -> EvalCtxt t i j -> EvalCtxt t i j + block• : forall {i j} -> EvalCtxt t i B -> EvalCtxt t i j + unblock• : forall {i j} -> EvalCtxt t i U -> EvalCtxt t i j hunk ./SmallStep.agda 67 -_[_] : forall {i j} -> EvalCtxt i j -> Expr -> Expr +_[_] : forall {t i j} -> EvalCtxt t i j -> Expr t -> Expr t hunk ./SmallStep.agda 79 -data _⟶[_]_ : Expr -> Status -> Expr -> Set where - reduction : forall {i j x y} (E : EvalCtxt i j) -> +data _⟶[_]_ {t : Totality} : Expr t -> Status -> Expr t -> Set where + reduction : forall {i j x y} (E : EvalCtxt t i j) -> hunk ./SmallStep.agda 92 -_⟶⋆[_]_ : Expr -> Status -> Expr -> Set +_⟶⋆[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set hunk ./SmallStep.agda 95 -module ⟶-Reasoning {i : Status} = StarReasoning (\x y -> _⟶[_]_ x i y) +module ⟶-Reasoning {t : Totality} {i : Status} = + StarReasoning (\x y -> _⟶[_]_ {t} x i y) hunk ./SmallStep.agda 106 -_∘_ : forall {i j k} -> EvalCtxt j k -> EvalCtxt i j -> EvalCtxt i k +_∘_ : forall {t i j k} -> + EvalCtxt t j k -> EvalCtxt t i j -> EvalCtxt t i k hunk ./SmallStep.agda 114 -∘-lemma : forall {i j k} (E₁ : EvalCtxt j k) (E₂ : EvalCtxt i j) {x} -> +∘-lemma : forall {t i j k} + (E₁ : EvalCtxt t j k) (E₂ : EvalCtxt t i j) {x} -> hunk ./SmallStep.agda 125 -lift⟶ : forall {i j x y} (E : EvalCtxt i j) -> +lift⟶ : forall {t i j x y} (E : EvalCtxt t i j) -> hunk ./SmallStep.agda 134 -lift : forall {x i j y} (E : EvalCtxt i j) -> +lift : forall {t x i j y} (E : EvalCtxt t i j) -> hunk ./SmallStep.agda 140 -complete : forall {e i v} -> e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝ -complete (Val {n}) = begin val n ∎ -complete Throw = begin throw ∎ -complete (Add₁ {x} {y} {m} {n} x⇓ y⇓) = begin +complete : forall {t} {e : Expr t} {i v} -> + e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝ +complete (Val {n = n}) = begin val n ∎ +complete (Fail {r = r}) = begin fail r ∎ +complete (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin hunk ./SmallStep.agda 153 -complete (Add₂ {x} {y} x↯) = begin +complete (Add₂ {x = x} {y} {r = r} x↯) = begin hunk ./SmallStep.agda 156 - throw ⊕ y + fail r ⊕ y hunk ./SmallStep.agda 158 - throw + fail r hunk ./SmallStep.agda 160 -complete (Add₃ {x} {y} {m} x⇓ y↯) = begin +complete (Add₃ {x = x} {y} {m} {r = r} x⇓ y↯) = begin hunk ./SmallStep.agda 165 - val m ⊕ throw + val m ⊕ fail r hunk ./SmallStep.agda 167 - throw + fail r hunk ./SmallStep.agda 169 -complete (Seqn₁ {x} {y} {m} {v} x⇓ y⇒) = begin +complete (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin hunk ./SmallStep.agda 178 -complete (Seqn₂ {x} {y} x↯) = begin +complete (Seqn₂ {x = x} {y} {r = r} x↯) = begin hunk ./SmallStep.agda 181 - throw >> y + fail r >> y hunk ./SmallStep.agda 183 - throw + fail r hunk ./SmallStep.agda 185 -complete (Catch₁ {x} {y} {m} x⇓) = begin +complete (Catch₁ {x = x} {y} {m} x⇓) = begin hunk ./SmallStep.agda 192 -complete (Catch₂ {x} {y} {v} x↯ y⇒) = begin +complete (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin hunk ./SmallStep.agda 195 - throw catch y + fail throw catch y hunk ./SmallStep.agda 201 -complete (Int {x}) = begin +complete (Catch₃ {x = x} {y} x⇑) = begin + x catch y + ⟶⋆⟨ lift (• •[ catch′ ] y) (complete x⇑) ⟩ + fail loop catch y + ⟶⟨ {! !} ⟩ + fail loop + ∎ +complete (Int {x = x}) = begin hunk ./SmallStep.agda 211 - throw + fail throw hunk ./SmallStep.agda 213 -complete (Block {x} {v} x⇒) = begin +complete (Block {x = x} {v} x⇒) = begin hunk ./SmallStep.agda 220 -complete (Unblock {x} {v} x⇒) = begin +complete (Unblock {x = x} {v} x⇒) = begin hunk ./SmallStep.agda 228 --- Soundness. +-- -- Soundness. hunk ./SmallStep.agda 230 -sound⟶ʳ : forall {e₁ e₂ i v} -> - e₁ ⟶ʳ[ i ] e₂ -> e₂ ⇓[ i ] v -> e₁ ⇓[ i ] v -sound⟶ʳ Add₁ Val = Add₁ Val Val -sound⟶ʳ Add₁ Int = Int -sound⟶ʳ Add₂ Throw = Add₂ Throw -sound⟶ʳ Add₂ Int = Int -sound⟶ʳ Add₃ Throw = Add₃ Val Throw -sound⟶ʳ Add₃ Int = Int -sound⟶ʳ Seqn₁ ⇓ = Seqn₁ Val ⇓ -sound⟶ʳ Seqn₂ Throw = Seqn₂ Throw -sound⟶ʳ Seqn₂ Int = Int -sound⟶ʳ Catch₁ Val = Catch₁ Val -sound⟶ʳ Catch₁ Int = Int -sound⟶ʳ Catch₂ ⇓ = Catch₂ Throw ⇓ -sound⟶ʳ Int Throw = Int -sound⟶ʳ Int Int = Int -sound⟶ʳ (Block {i} {val n}) Val = Block Val -sound⟶ʳ (Block .{U} {val n}) Int = Int -sound⟶ʳ (Block {i} {throw}) Throw = Block Throw -sound⟶ʳ (Block .{U} {throw}) Int = Int -sound⟶ʳ (Unblock {i} {val n}) Val = Unblock Val -sound⟶ʳ (Unblock .{U} {val n}) Int = Int -sound⟶ʳ (Unblock {i} {throw}) Throw = Unblock Throw -sound⟶ʳ (Unblock .{U} {throw}) Int = Int +-- sound⟶ʳ : forall {e₁ e₂ i v} -> +-- e₁ ⟶ʳ[ i ] e₂ -> e₂ ⇓[ i ] v -> e₁ ⇓[ i ] v +-- sound⟶ʳ Add₁ Val = Add₁ Val Val +-- sound⟶ʳ Add₁ Int = Int +-- sound⟶ʳ Add₂ Throw = Add₂ Throw +-- sound⟶ʳ Add₂ Int = Int +-- sound⟶ʳ Add₃ Throw = Add₃ Val Throw +-- sound⟶ʳ Add₃ Int = Int +-- sound⟶ʳ Seqn₁ ⇓ = Seqn₁ Val ⇓ +-- sound⟶ʳ Seqn₂ Throw = Seqn₂ Throw +-- sound⟶ʳ Seqn₂ Int = Int +-- sound⟶ʳ Catch₁ Val = Catch₁ Val +-- sound⟶ʳ Catch₁ Int = Int +-- sound⟶ʳ Catch₂ ⇓ = Catch₂ Throw ⇓ +-- sound⟶ʳ Int Throw = Int +-- sound⟶ʳ Int Int = Int +-- sound⟶ʳ (Block {i} {val n}) Val = Block Val +-- sound⟶ʳ (Block .{U} {val n}) Int = Int +-- sound⟶ʳ (Block {i} {throw}) Throw = Block Throw +-- sound⟶ʳ (Block .{U} {throw}) Int = Int +-- sound⟶ʳ (Unblock {i} {val n}) Val = Unblock Val +-- sound⟶ʳ (Unblock .{U} {val n}) Int = Int +-- sound⟶ʳ (Unblock {i} {throw}) Throw = Unblock Throw +-- sound⟶ʳ (Unblock .{U} {throw}) Int = Int hunk ./SmallStep.agda 255 -sound⟶ : forall {i j} (E : EvalCtxt i j) {e₁ e₂ v} -> - e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⇓[ j ] v -> E [ e₁ ] ⇓[ j ] v -sound⟶ • r ⇒ = sound⟶ʳ r ⇒ -sound⟶ (E •[ ⊕′ ] y) r (Add₁ ⇓₁ ⇓₂) = Add₁ (sound⟶ E r ⇓₁) ⇓₂ -sound⟶ (E •[ ⊕′ ] y) r (Add₂ ↯₁) = Add₂ (sound⟶ E r ↯₁) -sound⟶ (E •[ ⊕′ ] y) r (Add₃ ⇓₁ ↯₂) = Add₃ (sound⟶ E r ⇓₁) ↯₂ -sound⟶ (E •[ ⊕′ ] y) r Int = Int -sound⟶ (E •[ >>′ ] y) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ (sound⟶ E r ⇓₁) ⇒₂ -sound⟶ (E •[ >>′ ] y) r (Seqn₂ ↯₁) = Seqn₂ (sound⟶ E r ↯₁) -sound⟶ (E •[ >>′ ] y) r Int = Int -sound⟶ (E •[ catch′ ] y) r (Catch₁ ⇓₁) = Catch₁ (sound⟶ E r ⇓₁) -sound⟶ (E •[ catch′ ] y) r (Catch₂ ↯₁ ⇒₂) = Catch₂ (sound⟶ E r ↯₁) ⇒₂ -sound⟶ (E •[ catch′ ] y) r Int = Int -sound⟶ (v [ ⊕′ ]• E) r (Add₁ ⇓₁ ⇓₂) = Add₁ ⇓₁ (sound⟶ E r ⇓₂) -sound⟶ (v [ ⊕′ ]• E) r (Add₂ ↯₁) = Add₂ ↯₁ -sound⟶ (v [ ⊕′ ]• E) r (Add₃ ⇓₁ ↯₂) = Add₃ ⇓₁ (sound⟶ E r ↯₂) -sound⟶ (v [ ⊕′ ]• E) r Int = Int -sound⟶ (v [ >>′ ]• E) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ ⇓₁ (sound⟶ E r ⇒₂) -sound⟶ (v [ >>′ ]• E) r (Seqn₂ ↯₁) = Seqn₂ ↯₁ -sound⟶ (v [ >>′ ]• E) r Int = Int -sound⟶ (v [ catch′ ]• E) r (Catch₁ ⇓₁) = Catch₁ ⇓₁ -sound⟶ (v [ catch′ ]• E) r (Catch₂ ↯₁ ⇒₂) = Catch₂ ↯₁ (sound⟶ E r ⇒₂) -sound⟶ (v [ catch′ ]• E) r Int = Int -sound⟶ (block• E) r Int = Int -sound⟶ (block• E) r (Block ⇒) = Block (sound⟶ E r ⇒) -sound⟶ (unblock• E) r Int = Int -sound⟶ (unblock• E) r (Unblock ⇒) = Unblock (sound⟶ E r ⇒) +-- sound⟶ : forall {i j} (E : EvalCtxt i j) {e₁ e₂ v} -> +-- e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⇓[ j ] v -> E [ e₁ ] ⇓[ j ] v +-- sound⟶ • r ⇒ = sound⟶ʳ r ⇒ +-- sound⟶ (E •[ ⊕′ ] y) r (Add₁ ⇓₁ ⇓₂) = Add₁ (sound⟶ E r ⇓₁) ⇓₂ +-- sound⟶ (E •[ ⊕′ ] y) r (Add₂ ↯₁) = Add₂ (sound⟶ E r ↯₁) +-- sound⟶ (E •[ ⊕′ ] y) r (Add₃ ⇓₁ ↯₂) = Add₃ (sound⟶ E r ⇓₁) ↯₂ +-- sound⟶ (E •[ ⊕′ ] y) r Int = Int +-- sound⟶ (E •[ >>′ ] y) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ (sound⟶ E r ⇓₁) ⇒₂ +-- sound⟶ (E •[ >>′ ] y) r (Seqn₂ ↯₁) = Seqn₂ (sound⟶ E r ↯₁) +-- sound⟶ (E •[ >>′ ] y) r Int = Int +-- sound⟶ (E •[ catch′ ] y) r (Catch₁ ⇓₁) = Catch₁ (sound⟶ E r ⇓₁) +-- sound⟶ (E •[ catch′ ] y) r (Catch₂ ↯₁ ⇒₂) = Catch₂ (sound⟶ E r ↯₁) ⇒₂ +-- sound⟶ (E •[ catch′ ] y) r Int = Int +-- sound⟶ (v [ ⊕′ ]• E) r (Add₁ ⇓₁ ⇓₂) = Add₁ ⇓₁ (sound⟶ E r ⇓₂) +-- sound⟶ (v [ ⊕′ ]• E) r (Add₂ ↯₁) = Add₂ ↯₁ +-- sound⟶ (v [ ⊕′ ]• E) r (Add₃ ⇓₁ ↯₂) = Add₃ ⇓₁ (sound⟶ E r ↯₂) +-- sound⟶ (v [ ⊕′ ]• E) r Int = Int +-- sound⟶ (v [ >>′ ]• E) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ ⇓₁ (sound⟶ E r ⇒₂) +-- sound⟶ (v [ >>′ ]• E) r (Seqn₂ ↯₁) = Seqn₂ ↯₁ +-- sound⟶ (v [ >>′ ]• E) r Int = Int +-- sound⟶ (v [ catch′ ]• E) r (Catch₁ ⇓₁) = Catch₁ ⇓₁ +-- sound⟶ (v [ catch′ ]• E) r (Catch₂ ↯₁ ⇒₂) = Catch₂ ↯₁ (sound⟶ E r ⇒₂) +-- sound⟶ (v [ catch′ ]• E) r Int = Int +-- sound⟶ (block• E) r Int = Int +-- sound⟶ (block• E) r (Block ⇒) = Block (sound⟶ E r ⇒) +-- sound⟶ (unblock• E) r Int = Int +-- sound⟶ (unblock• E) r (Unblock ⇒) = Unblock (sound⟶ E r ⇒) hunk ./SmallStep.agda 283 -sound : forall e i v -> e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v -sound .(⌜ val n ⌝) i (val n) ε = Val -sound .(⌜ throw ⌝) i throw ε = Throw -sound .(E [ x ]) i v (reduction {x = x} {y} E r ◅ rs) = - sound⟶ E r (sound (E [ y ]) i v rs) +-- sound : forall e i v -> e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v +-- sound .(⌜ val n ⌝) i (val n) ε = Val +-- sound .(⌜ throw ⌝) i throw ε = Throw +-- sound .(E [ x ]) i v (reduction {x = x} {y} E r ◅ rs) = +-- sound⟶ E r (sound (E [ y ]) i v rs) hunk ./StatusLemmas.agda 17 -Bto· : forall {x v i} -> x ⇓[ B ] v -> x ⇓[ i ] v -Bto· Val = Val -Bto· Throw = Throw -Bto· (Add₁ x⇓ y⇓) = Add₁ (Bto· x⇓) (Bto· y⇓) -Bto· (Add₂ x↯) = Add₂ (Bto· x↯) -Bto· (Add₃ x⇓ y↯) = Add₃ (Bto· x⇓) (Bto· y↯) -Bto· (Seqn₁ x⇓ y) = Seqn₁ (Bto· x⇓) (Bto· y) -Bto· (Seqn₂ x↯) = Seqn₂ (Bto· x↯) -Bto· (Catch₁ x⇓) = Catch₁ (Bto· x⇓) -Bto· (Catch₂ x↯ y) = Catch₂ (Bto· x↯) (Bto· y) -Bto· (Block x) = Block x -Bto· (Unblock x) = Unblock x +Bto· : forall {t} {x : Expr t} {v i} -> x ⇓[ B ] v -> x ⇓[ i ] v +Bto· Val = Val +Bto· Throw = Throw +Bto· (Add₁ x⇓ y⇓) = Add₁ (Bto· x⇓) (Bto· y⇓) +Bto· (Add₂ x↯) = Add₂ (Bto· x↯) +Bto· (Add₃ x⇓ y↯) = Add₃ (Bto· x⇓) (Bto· y↯) +Bto· (Seqn₁ x⇓ y⇒) = Seqn₁ (Bto· x⇓) (Bto· y⇒) +Bto· (Seqn₂ x↯) = Seqn₂ (Bto· x↯) +Bto· (Catch₁ x⇓) = Catch₁ (Bto· x⇓) +Bto· (Catch₂ x↯ y⇒) = Catch₂ (Bto· x↯) (Bto· y⇒) +Bto· (Catch₃ x⇑) = Catch₃ (Bto· x⇑) +Bto· (Block x) = Block x +Bto· (Unblock x) = Unblock x +Bto· Loop = Loop hunk ./StatusLemmas.agda 32 -·toU : forall {x v i} -> x ⇓[ i ] v -> x ⇓[ U ] v +·toU : forall {t} {x : Expr t} {v i} -> x ⇓[ i ] v -> x ⇓[ U ] v hunk ./StatusLemmas.agda 36 --- However, the other direction is not valid, not even when the end --- result is not exceptional. +-- However, the other direction is not valid, not even in a total +-- setting with a non-exceptional end result. hunk ./StatusLemmas.agda 39 -¬UtoB : ¬ (forall x {n} -> x ⇓[ U ] val n -> x ⇓[ B ] val n) +¬UtoB : ¬ (forall (x : Expr total) {n} -> + x ⇓[ U ] val n -> x ⇓[ B ] val n) hunk ./StatusLemmas.agda 45 --- Furthermore, under the assumption that some computation can fail to --- terminate the following even more limited variant is also invalid. +-- Furthermore, in a partial setting the following even more limited +-- variant is also invalid. hunk ./StatusLemmas.agda 48 -data NonTotal : Set where - ¬⇓ : forall x i -> ¬ Σ₀ (\v -> x ⇓[ i ] v) -> NonTotal +¬UtoB' : ¬ (forall (x : Expr partial) -> x ⇓[ U ] -> x ⇓[ B ]) +¬UtoB' UtoB' with UtoB' (loop catch val 0) (0 , Catch₂ Int Val) +... | (n , Catch₁ ()) +... | (n , Catch₂ () _) hunk ./StatusLemmas.agda 53 -¬UtoB' : NonTotal -> ¬ (forall x -> x ⇓[ U ] -> x ⇓[ B ]) -¬UtoB' (¬⇓ x i ¬x⇓) UtoB' with - UtoB' (x catch val 0) (0 , Catch₂ Int Val) -¬UtoB' (¬⇓ x i ¬x⇓) _ | (n , Catch₁ x⇓) = ¬x⇓ (_ , Bto· x⇓) -¬UtoB' (¬⇓ x i ¬x⇓) _ | (n , Catch₂ x⇓ _) = ¬x⇓ (_ , Bto· x⇓) +-- In a total setting the more limited variant is provable, though. hunk ./StatusLemmas.agda 55 --- If all computations can terminate, then the more limited variant is --- provable. However, this property may not be very interesting. The --- current language is obviously total, but it is intended to model --- partial languages. - -Uto·' : Total -> forall {x i} -> x ⇓[ U ] -> x ⇓[ i ] -Uto·' total (_ , x) = helper x +Uto·' : forall {x : Expr total} {i} -> x ⇓[ U ] -> x ⇓[ i ] +Uto·' (_ , x) = helper x hunk ./StatusLemmas.agda 58 - helper : forall {x i m} -> x ⇓[ U ] val m -> x ⇓[ i ] + helper : forall {x : Expr total} {i m} -> x ⇓[ U ] val m -> x ⇓[ i ] hunk ./StatusLemmas.agda 65 - helper {x catch y} {i} (Catch₂ x↯ y⇓) with total x i - ... | throws x↯' = map-Σ₂ (Catch₂ x↯') (helper y⇓) + helper {x catch y} {i} (Catch₂ x⇑ y⇓) with defined x i + ... | throws x⇑' = map-Σ₂ (Catch₂ x⇑') (helper y⇓) hunk ./StatusLemmas.agda 72 -block-unblockˡ : forall {x} -> x ⊑ block (unblock x) +block-unblockˡ : forall {t} {x : Expr t} -> x ⊑ block (unblock x) hunk ./StatusLemmas.agda 75 -block-unblockʳ : ¬ (forall x -> block (unblock x) ⊑ x) -block-unblockʳ bux⊑x with bux⊑x (val 0) {i = B} (Block (Unblock Int)) +block-unblockʳ : ¬ (forall t (x : Expr t) -> block (unblock x) ⊑ x) +block-unblockʳ bux⊑x + with bux⊑x total (val 0) {i = B} (Block (Unblock Int)) hunk ./StatusLemmas.agda 80 -unblock-blockˡ : ¬ (forall x -> x ⊑ unblock (block x)) +unblock-blockˡ : ¬ (forall t (x : Expr t) -> x ⊑ unblock (block x)) hunk ./StatusLemmas.agda 82 - with x⊑ubx (val 0 catch val 1) (Catch₂ Int Val) + with x⊑ubx total (val 0 catch val 1) (Catch₂ Int Val) hunk ./StatusLemmas.agda 86 -unblock-blockʳ : ¬ (forall x -> unblock (block x) ⊑ x) -unblock-blockʳ ubx⊑x with ubx⊑x (val 0) {i = B} (Unblock Int) +unblock-blockʳ : ¬ (forall t (x : Expr t) -> unblock (block x) ⊑ x) +unblock-blockʳ ubx⊑x with ubx⊑x total (val 0) {i = B} (Unblock Int) hunk ./Totality.agda 5 --- These lemmas are not used in other modules, since the language is --- intended (?) to be a simplified variant of a partial language (even --- though it is total). - hunk ./Totality.agda 13 --- The language is total. +-- Defined x i means that x can terminate (possibly exceptionally) +-- when run in exception status i. hunk ./Totality.agda 16 -data Defined (x : Expr) (i : Status) : Set where +data Defined {t : Totality} (x : Expr t) (i : Status) : Set where hunk ./Totality.agda 20 -Total : Set -Total = forall x i -> Defined x i +-- Partial expressions can sometimes be completely undefined. + +¬defined : ¬ (forall (x : Expr partial) i -> Defined x i) +¬defined defined with defined loop B +... | returns () +... | throws () + +-- The expressions denoted as "total" are always potentially +-- terminating. (Note that the "type system" ensures that total +-- expressions cannot loop.) hunk ./Totality.agda 31 -total : Total -total (val n) _ = returns Val -total throw _ = throws Throw -total (x ⊕ y) i with total x i | total y i +defined : forall (x : Expr total) i -> Defined x i +defined (val n) _ = returns Val +defined throw _ = throws Throw +defined (x ⊕ y) i with defined x i | defined y i hunk ./Totality.agda 38 -total (x >> y) i with total x i | total y i +defined (x >> y) i with defined x i | defined y i hunk ./Totality.agda 42 -total (x catch y) i with total x i | total y i +defined (x catch y) i with defined x i | defined y i hunk ./Totality.agda 46 -total (block x) _ with total x B +defined (block x) _ with defined x B hunk ./Totality.agda 49 -total (unblock x) _ with total x U +defined (unblock x) _ with defined x U hunk ./Totality.agda 56 - forall {x i} -> ¬ x ↯[ i ] -> Σ₀ \n -> x ⇓[ i ] val n -cannot-throw⇒can-return {x} {i} ¬x↯ with total x i + forall {x : Expr total} {i} -> + ¬ x ↯[ i ] -> Σ₀ \n -> x ⇓[ i ] val n +cannot-throw⇒can-return {x} {i} ¬x↯ with defined x i hunk ./Totality.agda 63 - forall {x i} -> ¬ Σ₀ (\n -> x ⇓[ i ] val n) -> x ↯[ i ] -cannot-return⇒can-throw {x} {i} ¬x⇓ with total x i + forall {x : Expr total} {i} -> + ¬ Σ₀ (\n -> x ⇓[ i ] val n) -> x ↯[ i ] +cannot-return⇒can-throw {x} {i} ¬x⇓ with defined x i hunk ./Totality.agda 69 --- We can be more precise than in "total" above. +-- We can be more precise than in "defined" above. hunk ./Totality.agda 71 -can-throw? : forall x i -> Dec (x ↯[ i ]) +can-throw? : forall (x : Expr total) i -> Dec (x ↯[ i ]) hunk ./Totality.agda 117 -can-return? : forall x i -> Dec (Σ₀ \n -> x ⇓[ i ] val n) +can-return? : forall (x : Expr total) i -> Dec (Σ₀ \n -> x ⇓[ i ] val n) hunk ./Totality.agda 164 --- Wraps up the results of the functions above. +-- Wraps up the results of some of the functions above. hunk ./Totality.agda 171 -decidable : forall x i -> (Σ₀ \n -> x ⇓[ i ] val n) Or (x ↯[ i ]) +decidable : forall (x : Expr total) i -> + (Σ₀ \n -> x ⇓[ i ] val n) Or (x ↯[ i ]) hunk ./Totality.agda 177 -decidable x i | no ¬x⇓ | no ¬x↯ with total x i +decidable x i | no ¬x⇓ | no ¬x↯ with defined x i hunk ./VirtualMachine.agda 30 + loop : Op hunk ./VirtualMachine.agda 70 + loop : forall {ops i s} -> + ⟨ loop ∷ ops , i , s ⟩ ⟶ ⟨ loop ∷ ops , i , s ⟩ hunk ./VirtualMachine.agda 89 -comp : Expr -> Code -> Code +comp : forall {t} -> Expr t -> Code -> Code hunk ./VirtualMachine.agda 97 +comp loop ops = loop ∷ ops