[Tried another approach to non-termination. Nils Anders Danielsson **20080610155140 + A separate big-step relation now encodes non-termination. This approach seems more promising, but some proofs are still unfinished. There are two main problems: 1) The inductive encoding of infinite transition sequences that I am using is quite awkward to work with. A coinductive encoding would probably be more natural. Fortunately Agda has recently (after I wrote most of the code in this patch) gained support for coinductive definitions. 2) The bar theorem does not imply soundness any more, since all I can prove now is that terms /which are guaranteed to terminate/ will reach some final state when run in the VM, and then the bar lemma does not apply. However, it may be possible to prove soundness directly by using the small-step semantics instead of the big-step one. ] move ./Language.agda ./Syntax.agda adddir ./Semantics move ./SmallStep.agda ./Semantics/SmallStep.agda hunk ./AlgebraicProperties.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep hunk ./AlgebraicProperties.agda 12 + hunk ./AlgebraicProperties.agda 20 +open import Data.Nat hunk ./AlgebraicProperties.agda 39 -⊕-assoc x y z = equal ⟶ ⟵ +⊕-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑ hunk ./AlgebraicProperties.agda 43 - ⟶ : (x ⊕ y) ⊕ z ⊑ x ⊕ (y ⊕ z) - ⟶ Int = Int - ⟶ (Add₃ (Add₁ x y) z) = Add₃ x (Add₃ y z) - ⟶ (Add₂ Int) = Int - ⟶ (Add₂ (Add₃ x y)) = Add₃ x (Add₂ y) - ⟶ (Add₂ (Add₂ x)) = Add₂ x - ⟶ {i = i} (Add₁ {n = n₃} (Add₁ {m = n₁} {n = n₂} x⇓ y⇓) z⇓) = - cast (≡-sym (assoc n₁ n₂ n₃)) (Add₁ x⇓ (Add₁ y⇓ z⇓)) + ⟶⇓ : (x ⊕ y) ⊕ z ⊑⇓ x ⊕ (y ⊕ z) + ⟶⇓ Int = Int + ⟶⇓ (Add₃ (Add₁ x y) z) = Add₃ x (Add₃ y z) + ⟶⇓ (Add₂ Int) = Int + ⟶⇓ (Add₂ (Add₃ x y)) = Add₃ x (Add₂ y) + ⟶⇓ (Add₂ (Add₂ x)) = Add₂ x + ⟶⇓ {i = i} (Add₁ {n = n₃} (Add₁ {m = n₁} {n = n₂} x⇓ y⇓) z⇓) = + cast (≡-sym (assoc n₁ n₂ n₃)) (Add₁ x⇓ (Add₁ y⇓ z⇓)) + + ⟵⇓ : x ⊕ (y ⊕ z) ⊑⇓ (x ⊕ y) ⊕ z + ⟵⇓ Int = Int + ⟵⇓ (Add₃ x Int) = Int + ⟵⇓ (Add₃ x (Add₂ y)) = Add₂ (Add₃ x y) + ⟵⇓ (Add₃ x (Add₃ y z)) = Add₃ (Add₁ x y) z + ⟵⇓ (Add₂ x) = Add₂ (Add₂ x) + ⟵⇓ {i = i} (Add₁ {m = n₁} x⇓ (Add₁ {m = n₂} {n = n₃} y⇓ z⇓)) = + cast (assoc n₁ n₂ n₃) (Add₁ (Add₁ x⇓ y⇓) z⇓) hunk ./AlgebraicProperties.agda 61 - ⟵ : x ⊕ (y ⊕ z) ⊑ (x ⊕ y) ⊕ z - ⟵ Int = Int - ⟵ (Add₃ x Int) = Int - ⟵ (Add₃ x (Add₂ y)) = Add₂ (Add₃ x y) - ⟵ (Add₃ x (Add₃ y z)) = Add₃ (Add₁ x y) z - ⟵ (Add₂ x) = Add₂ (Add₂ x) - ⟵ {i = i} (Add₁ {m = n₁} x⇓ (Add₁ {m = n₂} {n = n₃} y⇓ z⇓)) = - cast (assoc n₁ n₂ n₃) (Add₁ (Add₁ x⇓ y⇓) z⇓) + ⟶⇑ : (x ⊕ y) ⊕ z ⊑⇑ x ⊕ (y ⊕ z) + ⟶⇑ (Add₁ (Add₁ x⇑)) = Add₁ x⇑ + ⟶⇑ (Add₁ (Add₂ x↡ y⇑)) = Add₂ x↡ (Add₁ y⇑) + ⟶⇑ (Add₂ (._ , Add₁ x↡ y↡) z⇑) = Add₂ (_ , x↡) (Add₂ (_ , y↡) z⇑) + + ⟵⇑ : x ⊕ (y ⊕ z) ⊑⇑ (x ⊕ y) ⊕ z + ⟵⇑ (Add₁ x⇑) = Add₁ (Add₁ x⇑) + ⟵⇑ (Add₂ x↡ (Add₁ y⇑)) = Add₁ (Add₂ x↡ y⇑) + ⟵⇑ (Add₂ x↡ (Add₂ y↡ z⇑)) = Add₂ (zip-Σ _+_ Add₁ x↡ y↡) z⇑ hunk ./AlgebraicProperties.agda 74 -catch-assoc _ _ _ = equal ⟶ ⟵ +catch-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑ hunk ./AlgebraicProperties.agda 76 - ⟶ : forall {t} {x y z : Expr t} -> - (x catch y) catch z ⊑ x catch (y catch z) - ⟶ (Catch₁ (Catch₁ x⇓)) = Catch₁ x⇓ - ⟶ (Catch₁ (Catch₂ x↯ y⇓)) = Catch₂ x↯ (Catch₁ y⇓) - ⟶ (Catch₂ (Catch₂ x↯ y↯) z) = Catch₂ x↯ (Catch₂ y↯ z) - ⟶ (Catch₂ Int z) = Catch₂ Int (Catch₂ Int z) - ⟶ (Catch₃ (Catch₂ x↯ y↯)) = Catch₂ x↯ (Catch₃ y↯) - ⟶ (Catch₃ (Catch₃ x⇑)) = Catch₃ x⇑ - ⟶ Int = Int + ⟶⇓ : (x catch y) catch z ⊑⇓ x catch (y catch z) + ⟶⇓ (Catch₁ (Catch₁ x⇓)) = Catch₁ x⇓ + ⟶⇓ (Catch₁ (Catch₂ x↯ y⇓)) = Catch₂ x↯ (Catch₁ y⇓) + ⟶⇓ (Catch₂ (Catch₂ x↯ y↯) z) = Catch₂ x↯ (Catch₂ y↯ z) + ⟶⇓ (Catch₂ Int z) = Catch₂ Int (Catch₂ Int z) + ⟶⇓ Int = Int hunk ./AlgebraicProperties.agda 83 - ⟵ : forall {t} {x y z : Expr t} -> - x catch (y catch z) ⊑ (x catch y) catch z - ⟵ (Catch₁ x⇓) = Catch₁ (Catch₁ x⇓) - ⟵ (Catch₂ x↯ (Catch₁ y⇓)) = Catch₁ (Catch₂ x↯ y⇓) - ⟵ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z - ⟵ (Catch₂ x↯ (Catch₃ y⇑)) = Catch₃ (Catch₂ x↯ y⇑) - ⟵ (Catch₂ x↯ Int) = Int - ⟵ (Catch₃ x⇑) = Catch₃ (Catch₃ x⇑) - ⟵ Int = Int + ⟵⇓ : x catch (y catch z) ⊑⇓ (x catch y) catch z + ⟵⇓ (Catch₁ x⇓) = Catch₁ (Catch₁ x⇓) + ⟵⇓ (Catch₂ x↯ (Catch₁ y⇓)) = Catch₁ (Catch₂ x↯ y⇓) + ⟵⇓ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z + ⟵⇓ (Catch₂ x↯ Int) = Int + ⟵⇓ Int = Int + + ⟶⇑ : (x catch y) catch z ⊑⇑ x catch (y catch z) + ⟶⇑ (Catch₁ (Catch₁ x⇑)) = Catch₁ x⇑ + ⟶⇑ (Catch₁ (Catch₂ x↯ y⇑)) = Catch₂ x↯ (Catch₁ y⇑) + ⟶⇑ (Catch₂ (Catch₂ x↯ y↯) z⇑) = Catch₂ x↯ (Catch₂ y↯ z⇑) + ⟶⇑ (Catch₂ Int z⇑) = Catch₂ Int (Catch₂ Int z⇑) + + ⟵⇑ : x catch (y catch z) ⊑⇑ (x catch y) catch z + ⟵⇑ (Catch₁ x⇑) = Catch₁ (Catch₁ x⇑) + ⟵⇑ (Catch₂ x↯ (Catch₁ y⇑)) = Catch₁ (Catch₂ x↯ y⇑) + ⟵⇑ (Catch₂ x↯ (Catch₂ y↯ z⇑)) = Catch₂ (Catch₂ x↯ y↯) z⇑ hunk ./AlgebraicProperties.agda 104 ->>-assoc x y z = equal ⟶ ⟵ +>>-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑ hunk ./AlgebraicProperties.agda 106 - ⟶ : (x >> y) >> z ⊑ x >> (y >> z) - ⟶ (Seqn₁ (Seqn₁ x⇓ y⇓) z) = Seqn₁ x⇓ (Seqn₁ y⇓ z) - ⟶ (Seqn₂ (Seqn₁ x⇓ y↯)) = Seqn₁ x⇓ (Seqn₂ y↯) - ⟶ (Seqn₂ (Seqn₂ x↯)) = Seqn₂ x↯ - ⟶ (Seqn₂ Int) = Int - ⟶ Int = Int + ⟶⇓ : (x >> y) >> z ⊑⇓ x >> (y >> z) + ⟶⇓ (Seqn₁ (Seqn₁ x⇓ y⇓) z) = Seqn₁ x⇓ (Seqn₁ y⇓ z) + ⟶⇓ (Seqn₂ (Seqn₁ x⇓ y↯)) = Seqn₁ x⇓ (Seqn₂ y↯) + ⟶⇓ (Seqn₂ (Seqn₂ x↯)) = Seqn₂ x↯ + ⟶⇓ (Seqn₂ Int) = Int + ⟶⇓ Int = Int hunk ./AlgebraicProperties.agda 113 - ⟵ : x >> (y >> z) ⊑ (x >> y) >> z - ⟵ (Seqn₁ x⇓ (Seqn₁ y⇓ z)) = Seqn₁ (Seqn₁ x⇓ y⇓) z - ⟵ (Seqn₁ x⇓ (Seqn₂ y↯)) = Seqn₂ (Seqn₁ x⇓ y↯) - ⟵ (Seqn₁ x↯ Int) = Int - ⟵ (Seqn₂ x↯) = Seqn₂ (Seqn₂ x↯) - ⟵ Int = Int + ⟵⇓ : x >> (y >> z) ⊑⇓ (x >> y) >> z + ⟵⇓ (Seqn₁ x⇓ (Seqn₁ y⇓ z)) = Seqn₁ (Seqn₁ x⇓ y⇓) z + ⟵⇓ (Seqn₁ x⇓ (Seqn₂ y↯)) = Seqn₂ (Seqn₁ x⇓ y↯) + ⟵⇓ (Seqn₁ x↯ Int) = Int + ⟵⇓ (Seqn₂ x↯) = Seqn₂ (Seqn₂ x↯) + ⟵⇓ Int = Int + + ⟶⇑ : (x >> y) >> z ⊑⇑ x >> (y >> z) + ⟶⇑ (Seqn₁ (Seqn₁ x⇑)) = Seqn₁ x⇑ + ⟶⇑ (Seqn₁ (Seqn₂ x↡ y⇑)) = Seqn₂ x↡ (Seqn₁ y⇑) + ⟶⇑ (Seqn₂ (_ , Seqn₁ x↡ y↡) z⇑) = Seqn₂ (_ , x↡) (Seqn₂ (_ , y↡) z⇑) + + ⟵⇑ : x >> (y >> z) ⊑⇑ (x >> y) >> z + ⟵⇑ (Seqn₁ x⇑) = Seqn₁ (Seqn₁ x⇑) + ⟵⇑ (Seqn₂ x↡ (Seqn₁ y⇑)) = Seqn₁ (Seqn₂ x↡ y⇑) + ⟵⇑ (Seqn₂ x↡ (Seqn₂ y↡ z⇑)) = Seqn₂ (zip-Σ (\u v -> v) Seqn₁ x↡ y↡) z⇑ hunk ./AlgebraicProperties.agda 132 -finally-assocʳ : forall {t} {x y z : Expr t} -> +finally-assocʳ : forall {t} (x y z : Expr t) -> hunk ./AlgebraicProperties.agda 134 -finally-assocʳ Int = Int -finally-assocʳ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x) y)))) z)) = - Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock (Bto· y))) z))) -finally-assocʳ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)) -finally-assocʳ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) -finally-assocʳ (Block (Seqn₂ (Catch₂ _ zt))) = - Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ (Block (Seqn₂ (Catch₂ (Unblock Int) zt)))))) -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⇑)) +finally-assocʳ x y z = record { ⇓ = ⇓; ⇑ = ⇑ } + where + ⇓ : (x finally y) finally z ⊑⇓ x finally (y finally z) + ⇓ Int = Int + ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇒)) = + Block (Seqn₁ (Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇓ y↡))) z⇒))) + ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)) + ⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) + ⇓ (Block (Seqn₂ (Catch₂ _ z↯))) = + Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ (Block (Seqn₂ (Catch₂ (Unblock Int) z↯)))))) + + ⇑ : (x finally y) finally z ⊑⇑ x finally (y finally z) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x⇑))))))) = + Block (Seqn₁ (Catch₁ x⇑)) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ x↯ (Seqn₁ y⇑)))))))) = + Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑)))))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₁ x↡) y⇑)))))) = + Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑)))))) + ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _)))))) + ⇑ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑)))) = + Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑))))))) + ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))) + ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↯))) (Seqn₁ z⇑)))) = + Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑))))) + ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))) _))) + ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₁ y↡ _))))) (Seqn₁ z⇑)))) = + Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑))))) + ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₂ y↯))))) (Seqn₁ z⇑)))) = + Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑))))))) + ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇑)) = + Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑))) + ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)) + ⇑ (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _)) hunk ./AlgebraicProperties.agda 173 -¬finally-assoc assoc with assoc (val 0) (loop catch val 0) (val 0) -... | equal _ f with f {i = U} (Block (Seqn₁ (Catch₁ (Unblock Val)) - (Block (Seqn₁ (Catch₁ (Unblock (Catch₂ Int Val))) - Val)))) +¬finally-assoc assoc + with _⊑_.⇓ (_≈_.⊒ (assoc (val 0) (loop catch val 0) (val 0))) + {i = U} + (Block (Seqn₁ (Catch₁ (Unblock Val)) + (Block (Seqn₁ (Catch₁ (Unblock (Catch₂ Int Val))) + Val)))) hunk ./AlgebraicProperties.agda 187 -finally-assoc x y z = equal finally-assocʳ ⟵ +finally-assoc x y z = record { ⊑ = finally-assocʳ x y z + ; ⊒ = record { ⇓ = ⟵⇓; ⇑ = ⟵⇑ } } hunk ./AlgebraicProperties.agda 190 - ⟵ : x finally (y finally z) ⊑ (x finally y) finally z - ⟵ Int = Int + ⟵⇓ : x finally (y finally z) ⊑⇓ (x finally y) finally z + ⟵⇓ Int = Int hunk ./AlgebraicProperties.agda 193 - ⟵ (Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock y)) z)))) = + ⟵⇓ (Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock y)) z)))) = hunk ./AlgebraicProperties.agda 196 - ⟵ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) - ⟵ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₂ (Catch₂ _ z↯))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) - ⟵ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) + ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) + ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₂ (Catch₂ _ z↯))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) + ⟵⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) + + ⟵⇓ (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))) + ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₂ (Catch₂ _ z↯))))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) hunk ./AlgebraicProperties.agda 204 - ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) Throw)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Throw))) - ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₁ _ z)))))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ z))) - ⟵ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₂ (Catch₂ _ z↯))))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) + ⟵⇑ : x finally (y finally z) ⊑⇑ (x finally y) finally z + ⟵⇑ ⇑ = ⊥-elim (¬undefined _ ⇑) hunk ./AlgebraicProperties.agda 213 -⊕-comm x y = equal (⟶ _ _) (⟶ _ _) +⊕-comm x y = is-≈ (⟶⇓ _) (⟶⇓ _) ⟶⇑ ⟶⇑ hunk ./AlgebraicProperties.agda 217 - ⟶ : forall x y -> x ⊕ y ⊑ y ⊕ x - ⟶ _ _ 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↯ - ⟶ x y {i = i} (Add₁ {m = m} {n = n} x⇓ y⇓) = + ⟶⇓ : forall {x} y -> x ⊕ y ⊑⇓ y ⊕ x + ⟶⇓ _ Int = Int + ⟶⇓ _ (Add₃ x⇓ y↯) = Add₂ y↯ + ⟶⇓ y {i = i} (Add₂ x↯) with defined y i + ⟶⇓ _ (Add₂ x↯) | (val _ , y⇓) = Add₃ y⇓ x↯ + ⟶⇓ _ (Add₂ x↯) | (throw , y↯) = Add₂ y↯ + ⟶⇓ _ (Add₁ {m = m} {n = n} x⇓ y⇓) = hunk ./AlgebraicProperties.agda 226 + ⟶⇑ : {x y : Expr total} -> x ⊕ y ⊑⇑ y ⊕ x + ⟶⇑ ⇑ = ⊥-elim (¬undefined _ ⇑) + hunk ./AlgebraicProperties.agda 232 -¬⊕-comm ⊕-comm with ⊕-comm throw loop -¬⊕-comm ⊕-comm | equal ⟵ ⟶ with ⟵ {i = B} (Add₂ Throw) +¬⊕-comm ⊕-comm + with _⊑_.⇓ (_≈_.⊑ (⊕-comm throw loop)) {i = B} (Add₂ Throw) hunk ./Bar.agda 10 +open import Data.Sum hunk ./CompilerCorrectness.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep hunk ./CompilerCorrectness.agda 10 +import Bar; open Bar _⟶_ +import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness.agda 18 -open import Relation.Unary -open import Relation.Binary.PropositionalEquality -import Bar; open Bar _⟶_ -import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness.agda 26 --- Starting states. - -start : forall {t} -> Expr t -> Status -> State -start e i = ⟨ comp e [] , i , [] ⟩ - --- Final states. - -data Final : State -> Set where - returns : forall i s -> Final ⟨ [] , i , s ⟩ - throws : forall i -> Final ⟪ i , [] ⟫ - hunk ./CompilerCorrectness.agda 40 -Sound₂ : Expr partial -> Status -> Set +Sound₂ : forall {t} -> Expr t -> Status -> Set hunk ./CompilerCorrectness.agda 43 -Sound : forall t -> Expr t -> Status -> Set -Sound total e i = Sound₁ e i -Sound partial e i = Sound₁ e i × Sound₂ e i +Sound : forall {t} -> Expr t -> Status -> Set +Sound e i = Sound₁ e i × Sound₂ e i hunk ./CompilerCorrectness.agda 55 -Complete₂ : Expr partial -> Status -> Set +Complete₂ : forall {t} -> Expr t -> Status -> Set hunk ./CompilerCorrectness.agda 61 -DoesNotLoop : forall t -> Expr t -> Status -> Set -DoesNotLoop total e i = ⊤ -DoesNotLoop partial e i = ¬ e ⇑[ i ] +-- Note that this result actually implies Sound₁, if restricted to +-- total input (see Bar.bar-lemma). hunk ./CompilerCorrectness.agda 64 -Complete₃ : forall t -> Expr t -> Status -> Set -Complete₃ t e i = DoesNotLoop t e i -> start e i ◁ Matches e i +Complete₃ : forall {t} -> Expr t -> Status -> Set +Complete₃ e i = ¬ e ⇑[ i ] -> start e i ◁ Matches e i hunk ./CompilerCorrectness.agda 69 -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 +Complete : forall {t} -> Expr t -> Status -> Set +Complete e i = Complete₁ e i × Complete₂ e i × Complete₃ e i hunk ./CompilerCorrectness.agda 74 -CompilerCorrect : forall t -> Expr t -> Status -> Set -CompilerCorrect t e i = Sound t e i × Complete t e i +CompilerCorrect : forall {t} -> Expr t -> Status -> Set +CompilerCorrect e i = Sound e i × Complete e i hunk ./CompilerCorrectness/Completeness1.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep hunk ./CompilerCorrectness/Completeness1.agda 16 +open import Data.Product hunk ./CompilerCorrectness/Completeness1.agda 69 - 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 - hunk ./CompilerCorrectness/Completeness1.agda 73 -complete₂ : forall e {i} -> Complete₂ e i -complete₂ _ = complete⇑ +complete⇑ : forall {t} {e : Expr t} {ops i s} -> + e ⇑[ i ] -> ⟨ comp e ops , i , s ⟩ ⟶∞ +complete⇑ Loop = loop loops +complete⇑ (Add₁ x) = complete⇑ x +complete⇑ (Add₂ x y) = complete⇓ (proj₂ x) ◅◅∞ complete⇑ y +complete⇑ (Seqn₁ x) = complete⇑ x +complete⇑ (Seqn₂ x y) = complete⇓ (proj₂ x) ◅◅∞ pop ◅∞ complete⇑ y +complete⇑ (Catch₁ x) = mark ◅∞ complete⇑ x +complete⇑ (Catch₂ x y) = mark ◅∞ complete↯ x ◅◅∞ han ◅∞ complete⇑ y +complete⇑ (Block x) = set ◅∞ complete⇑ x +complete⇑ (Unblock x) = set ◅∞ complete⇑ x + +complete₂ : forall {t} {e : Expr t} {i} -> Complete₂ e i +complete₂ = complete⇑ hunk ./CompilerCorrectness/Completeness2.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep hunk ./CompilerCorrectness/Completeness2.agda 11 -open import CompilerCorrectness.DoesNotLoopLemmas +open import Totality hunk ./CompilerCorrectness/Completeness2.agda 17 +open import Relation.Nullary hunk ./CompilerCorrectness/Completeness2.agda 37 -bar-theorem : forall t (e : Expr t) {ops i s} -> - DoesNotLoop t e i -> +bar-theorem : forall {t} (e : Expr t) {ops i s} -> + ¬ e ⇑[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 40 -bar-theorem t (val n) ¬⇑ = via (_ , push) helper +bar-theorem {t = t} (val n) ¬⇑ = via (_ , push) helper hunk ./CompilerCorrectness/Completeness2.agda 48 -bar-theorem t throw ¬⇑ = via (_ , throw) helper +bar-theorem {t = t} throw ¬⇑ = via (_ , throw) helper hunk ./CompilerCorrectness/Completeness2.agda 56 -bar-theorem t (x ⊕ y) ¬⇑ = ◁-trans (bar-theorem t x (dnl-⊕ˡ t ¬⇑)) - (helper₁ ¬⇑) +bar-theorem (x ⊕ y) ¬⇑ = ◁-trans (bar-theorem x (¬⇑-⊕ˡ ¬⇑)) + (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 90 - DoesNotLoop t (x ⊕ y) i -> + ¬ x ⊕ y ⇑[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 94 - helper₁ ¬⇑ (returns x⇓) = ◁-trans (bar-theorem t y (dnl-⊕ʳ t ¬⇑ x⇓)) + helper₁ ¬⇑ (returns x⇓) = ◁-trans (bar-theorem y (¬⇑-⊕ʳ ¬⇑ (_ , x⇓))) hunk ./CompilerCorrectness/Completeness2.agda 97 -bar-theorem t (x >> y) ¬⇑ = ◁-trans (bar-theorem t x (dnl->>ˡ t ¬⇑)) - (helper₁ ¬⇑) +bar-theorem (x >> y) ¬⇑ = ◁-trans (bar-theorem x (¬⇑->>ˡ ¬⇑)) + (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 113 - DoesNotLoop t (x >> y) i -> x ⇓[ i ] val m -> + ¬ x >> y ⇑[ i ] -> x ⇓[ i ] val m -> hunk ./CompilerCorrectness/Completeness2.agda 116 - helper₂ ¬⇑ x⇓ pop = ◁-trans (bar-theorem t y (dnl->>ʳ t ¬⇑ x⇓)) + helper₂ ¬⇑ x⇓ pop = ◁-trans (bar-theorem y (¬⇑->>ʳ ¬⇑ (_ , x⇓))) hunk ./CompilerCorrectness/Completeness2.agda 121 - DoesNotLoop t (x >> y) i -> + ¬ x >> y ⇑[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 127 -bar-theorem t (x catch y) ¬⇑ = via (_ , mark) (helper₁ ¬⇑) +bar-theorem (x catch y) ¬⇑ = via (_ , mark) (helper₁ ¬⇑) hunk ./CompilerCorrectness/Completeness2.agda 137 - DoesNotLoop t (x catch y) i -> x ↯[ i ] -> + ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 140 - helper₆ ¬⇑ x↯ han = ◁-trans (bar-theorem t y (dnl-catchʳ t ¬⇑ x↯)) + helper₆ ¬⇑ x↯ han = ◁-trans (bar-theorem y (¬⇑-catchʳ ¬⇑ x↯)) hunk ./CompilerCorrectness/Completeness2.agda 144 - DoesNotLoop t (x catch y) i -> x ↯[ i ] -> + ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 150 - DoesNotLoop t (x catch y) U -> + ¬ x catch y ⇑[ U ] -> hunk ./CompilerCorrectness/Completeness2.agda 156 - DoesNotLoop t (x catch y) i -> x ⇓[ i ] val m -> + ¬ x catch y ⇑[ i ] -> x ⇓[ i ] val m -> hunk ./CompilerCorrectness/Completeness2.agda 163 - DoesNotLoop t (x catch y) i -> + ¬ x catch y ⇑[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 170 - DoesNotLoop t (x catch y) i -> + ¬ x catch y ⇑[ i ] -> hunk ./CompilerCorrectness/Completeness2.agda 173 - helper₁ ¬⇑ mark = ◁-trans (bar-theorem t x (dnl-catchˡ t ¬⇑)) + helper₁ ¬⇑ mark = ◁-trans (bar-theorem x (¬⇑-catchˡ ¬⇑)) hunk ./CompilerCorrectness/Completeness2.agda 177 -bar-theorem t (block x) ¬⇑ = via (_ , set) helper₁ +bar-theorem (block x) ¬⇑ = via (_ , set) helper₁ hunk ./CompilerCorrectness/Completeness2.agda 200 - helper₁ set = ◁-trans (bar-theorem t x (dnl-block t ¬⇑)) + helper₁ set = ◁-trans (bar-theorem x (¬⇑-block ¬⇑)) hunk ./CompilerCorrectness/Completeness2.agda 204 -bar-theorem t (unblock x) ¬⇑ = via (_ , set) helper₁ +bar-theorem (unblock x) ¬⇑ = via (_ , set) helper₁ hunk ./CompilerCorrectness/Completeness2.agda 238 - helper₁ set = ◁-trans (bar-theorem t x (dnl-unblock t ¬⇑)) + helper₁ set = ◁-trans (bar-theorem x (¬⇑-unblock ¬⇑)) hunk ./CompilerCorrectness/Completeness2.agda 242 -bar-theorem partial loop ¬⇑ = ⊥-elim (¬⇑ Loop) +bar-theorem loop ¬⇑ = ⊥-elim (¬⇑ Loop) hunk ./CompilerCorrectness/Completeness2.agda 246 -complete₃ : forall {t} e {i} -> Complete₃ t e i -complete₃ e ¬⇑ = ◁-map Matches⁺⇒Matches (bar-theorem _ e ¬⇑) +complete₃ : forall {t} (e : Expr t) {i} -> Complete₃ e i +complete₃ e ¬⇑ = ◁-map Matches⁺⇒Matches (bar-theorem e ¬⇑) 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⇑) rmfile ./CompilerCorrectness/DoesNotLoopLemmas.agda hunk ./CompilerCorrectness/Proof.agda 7 +open import Syntax hunk ./CompilerCorrectness/Proof.agda 15 -correct : forall e {i} -> CompilerCorrect e i -correct e = ((\{_} -> sound e) , (\{_} -> complete₁ e) , complete₂ e) +correct : forall {t} (e : Expr t) {i} -> CompilerCorrect e i +correct e = (sound e , (\{_} -> complete₁ e) , complete₂ , complete₃ e) hunk ./CompilerCorrectness/Soundness.agda 8 -open import Language +open import Syntax +open import Semantics.SmallStep +open import Semantics.Equivalence hunk ./CompilerCorrectness/Soundness.agda 13 -open import CompilerCorrectness.Completeness2 -import Bar; open Bar _⟶_ +import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness/Soundness.agda 16 -open import Relation.Nullary hunk ./CompilerCorrectness/Soundness.agda 17 --- Some impossibility results. +-- The first part of soundness. hunk ./CompilerCorrectness/Soundness.agda 19 -matches-final : forall {t e i c} -> Matches {t} e i c -> ¬ c ⟶ -matches-final (returns _) (_ , ()) -matches-final (throws _) (_ , ()) +postulate + sound₁ : forall {t} (e : Expr t) {i} -> Sound₁ e i hunk ./CompilerCorrectness/Soundness.agda 22 -final-final : forall {c} -> Final c -> ¬ c ⟶ -final-final (returns _ _) (_ , ()) -final-final (throws _) (_ , ()) +-- The second part of soundness. hunk ./CompilerCorrectness/Soundness.agda 24 --- The first part of soundness. Depends crucially on the bar theorem --- (complete₂). +postulate + sound₂' : forall {t} (e : Expr t) {i} -> start e i ⟶∞ -> e ⟶∞[ i ] hunk ./CompilerCorrectness/Soundness.agda 27 -sound₁ : forall {t} (e : Expr t) {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 e⟶∞ = small⇒big⟶∞ e (sound₂' e e⟶∞) hunk ./CompilerCorrectness/Soundness.agda 32 -sound : forall t e {i} -> Sound t e i -sound total e = sound₁ e -sound partial e = ((\{_} -> sound₁ e) , {! !}) +sound : forall {t} (e : Expr t) {i} -> Sound e i +sound e = ((\{_} -> sound₁ e) , sound₂ e) hunk ./Equivalence.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep + hunk ./Equivalence.agda 13 +open import Data.Product hunk ./Equivalence.agda 15 -infix 3 _⊑_ _≈_ +infix 3 _⊑⇓_ _⊑⇑_ _⊑_ _≈_ hunk ./Equivalence.agda 20 -_⊑_ : forall {t} -> Expr t -> Expr t -> Set -x ⊑ y = forall {i v} -> x ⇓[ i ] v -> y ⇓[ i ] v +_⊑⇓_ : forall {t} -> Expr t -> Expr t -> Set +x ⊑⇓ y = forall {i v} -> x ⇓[ i ] v -> y ⇓[ i ] v + +_⊑⇑_ : forall {t} -> Expr t -> Expr t -> Set +x ⊑⇑ y = forall {i} -> x ⇑[ i ] -> y ⇑[ i ] + +record _⊑_ {t : Totality} (x y : Expr t) : Set where + field + ⇓ : x ⊑⇓ y + ⇑ : x ⊑⇑ y hunk ./Equivalence.agda 36 --- would not be associative (see FixitiesOK.catch-assoc). +-- would not be associative (see AlgebraicProperties.catch-assoc). + +record _≈_ {t : Totality} (x y : Expr t) : Set where + field + ⊒ : y ⊑ x + ⊑ : x ⊑ y hunk ./Equivalence.agda 43 -data _≈_ {t : Totality} (x y : Expr t) : Set where - equal : x ⊑ y -> y ⊑ x -> x ≈ y + open _⊑_ ⊒ public renaming (⇓ to ⊒⇓; ⇑ to ⊒⇑) + open _⊑_ ⊑ public renaming (⇓ to ⊑⇓; ⇑ to ⊑⇑) + +is-≈ : forall {t} {x y : Expr t} -> + x ⊑⇓ y -> y ⊑⇓ x -> x ⊑⇑ y -> y ⊑⇑ x -> x ≈ y +is-≈ x⊑⇓y y⊑⇓x x⊑⇑y y⊑⇑x = record + { ⊑ = record { ⇓ = x⊑⇓y; ⇑ = x⊑⇑y } + ; ⊒ = record { ⇓ = y⊑⇓x; ⇑ = y⊑⇑x } + } hunk ./Equivalence.agda 69 - reflexive ≡-refl = id + reflexive ≡-refl = record { ⇓ = id; ⇑ = id } hunk ./Equivalence.agda 72 - trans ⟶₁ ⟶₂ = ⟶₂ ∘ ⟶₁ + trans x⊑y y⊑z = record { ⇓ = ⇓ y⊑z ∘ ⇓ x⊑y + ; ⇑ = ⇑ y⊑z ∘ ⇑ x⊑y } + where open _⊑_ hunk ./Equivalence.agda 83 - { refl = equal id id + { refl = record { ⊑ = P.refl; ⊒ = P.refl } hunk ./Equivalence.agda 89 + module P = Preorder (⊑-preorder t) + hunk ./Equivalence.agda 92 - sym (equal ⟶ ⟵) = equal ⟵ ⟶ + sym x≈y = record { ⊑ = ⊒ ; ⊒ = ⊑ } + where open _≈_ x≈y hunk ./Equivalence.agda 96 - trans (equal ⟶₁ ⟵₁) (equal ⟶₂ ⟵₂) = equal (⟶₂ ∘ ⟶₁) (⟵₁ ∘ ⟵₂) + trans x≈y y≈z = record { ⊑ = P.trans (⊑ x≈y) (⊑ y≈z) + ; ⊒ = P.trans (⊒ y≈z) (⊒ x≈y) } + where open _≈_ hunk ./Everything.agda 7 --- Syntax and a big-step semantics for a simple language with --- exceptions and interrupts (asynchronous exceptions). +-- The syntax of a simple language with exceptions and interrupts +-- (asynchronous exceptions). hunk ./Everything.agda 10 -import Language +import Syntax hunk ./Everything.agda 12 --- A small-step semantics, equivalent to the big-step one. +-- Big-step semantics. hunk ./Everything.agda 14 -import SmallStep +import Semantics.BigStep hunk ./Everything.agda 16 --- A virtual machine and a compiler. - -import VirtualMachine - --- The bar relation, used to state compiler correctness. - -import Bar - --- Infinite transition sequences, used to state compiler correctness. +-- Infinite transition sequences, used by the small-step semantics. hunk ./Everything.agda 20 --- Statement of compiler correctness. +-- Small-step semantics. hunk ./Everything.agda 22 -import CompilerCorrectness +import Semantics.SmallStep hunk ./Everything.agda 24 --- Proof of compiler correctness. +-- The two semantics are equivalent. hunk ./Everything.agda 26 -import CompilerCorrectness.Completeness1 -import CompilerCorrectness.DoesNotLoopLemmas -import CompilerCorrectness.Completeness2 -import CompilerCorrectness.Soundness -import CompilerCorrectness.Proof +import Semantics.Equivalence -- Currently contains postulate. hunk ./Everything.agda 28 --- Definition of equivalence between two expressions. +-- Definition of equivalence between two expressions. Uses the +-- big-step semantics. hunk ./Everything.agda 45 +-- A virtual machine and a compiler. + +import VirtualMachine + +-- The bar relation, used to state compiler correctness. + +import Bar + +-- Statement of compiler correctness. Uses the big-step semantics. + +import CompilerCorrectness + +-- Proof of compiler correctness. + +import CompilerCorrectness.Completeness1 +import CompilerCorrectness.Completeness2 +import CompilerCorrectness.Soundness -- Currently contains postulates. +import CompilerCorrectness.Proof + addfile ./README hunk ./README 1 +This project started out as a formalisation of "What is the meaning of +these constant interruptions?" by Hutton and Wright, but has since +grown. addfile ./Semantics/BigStep.agda hunk ./Semantics/BigStep.agda 1 +------------------------------------------------------------------------ +-- Big-step semantics +------------------------------------------------------------------------ + +module Semantics.BigStep where + +open import Syntax + +open import Data.Nat +open import Data.Product + +infix 3 _⇓[_]_ _⇓[_] _↡[_] _↯[_] _⇑[_] _∶_⇑[_] + +-- x ⇓[ i ] v means that x _can_ terminate with the value (or +-- exception) v. + +mutual + + _∶_⇓[_]_ : forall t -> Expr t -> Status -> Value -> Set + _ ∶ e ⇓[ i ] v = e ⇓[ i ] v + + data _⇓[_]_ : forall {t} -> Expr t -> Status -> Value -> Set where + 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 ⇓[ i ] val m -> y ⇓[ i ] val n -> t ∶ x ⊕ y ⇓[ i ] val (m + n) + Add₂ : forall {t x y i} -> x ⇓[ i ] throw -> t ∶ x ⊕ y ⇓[ i ] throw + Add₃ : forall {t x y m i} -> x ⇓[ i ] val m -> y ⇓[ i ] throw -> t ∶ x ⊕ y ⇓[ i ] throw + Seqn₁ : forall {t x y m v i} -> x ⇓[ i ] val m -> y ⇓[ i ] v -> t ∶ x >> y ⇓[ i ] v + Seqn₂ : forall {t x y i} -> x ⇓[ i ] throw -> t ∶ x >> y ⇓[ i ] throw + Catch₁ : forall {t x y m i} -> x ⇓[ i ] val m -> t ∶ x catch y ⇓[ i ] val m + Catch₂ : forall {t x y v i} -> x ⇓[ i ] throw -> y ⇓[ i ] v -> t ∶ x catch y ⇓[ i ] v + Int : forall {t x} -> t ∶ x ⇓[ U ] throw + Block : forall {t x v i} -> x ⇓[ B ] v -> t ∶ block x ⇓[ i ] v + Unblock : forall {t x v i} -> x ⇓[ U ] v -> t ∶ unblock x ⇓[ i ] v + +-- Short-hand notation. + +_⇓[_] : forall {t} -> Expr t -> Status -> Set +x ⇓[ i ] = Σ₀ \v -> x ⇓[ i ] v + +_↡[_] : forall {t} -> Expr t -> Status -> Set +x ↡[ i ] = Σ₀ \n -> x ⇓[ i ] val n + +_↯[_] : forall {t} -> Expr t -> Status -> Set +x ↯[ i ] = x ⇓[ i ] throw + +-- x ⇑[ i ] means that x _can_ fail to terminate. Note that the +-- natural definition of this type is coinductive. We get away with an +-- inductive type since the language is so simple. + +mutual + + private + _∶_⇑[_] : forall t -> Expr t -> Status -> Set + t ∶ e₁ ⇑[ i ] = e₁ ⇑[ i ] + + data _⇑[_] : forall {t} -> Expr t -> Status -> Set where + Loop : forall {i} -> loop ⇑[ i ] + Add₁ : forall {t x y i} -> x ⇑[ i ] -> t ∶ x ⊕ y ⇑[ i ] + Add₂ : forall {t x y i} -> x ↡[ i ] -> y ⇑[ i ] -> t ∶ x ⊕ y ⇑[ i ] + Seqn₁ : forall {t x y i} -> x ⇑[ i ] -> t ∶ x >> y ⇑[ i ] + Seqn₂ : forall {t x y i} -> x ↡[ i ] -> y ⇑[ i ] -> t ∶ x >> y ⇑[ i ] + Catch₁ : forall {t x y i} -> x ⇑[ i ] -> t ∶ x catch y ⇑[ i ] + Catch₂ : forall {t x y i} -> x ↯[ i ] -> y ⇑[ i ] -> t ∶ x catch y ⇑[ i ] + Block : forall {t x i} -> x ⇑[ B ] -> t ∶ block x ⇑[ i ] + Unblock : forall {t x i} -> x ⇑[ U ] -> t ∶ unblock x ⇑[ i ] addfile ./Semantics/Equivalence.agda hunk ./Semantics/Equivalence.agda 1 +------------------------------------------------------------------------ +-- The two semantics are equivalent +------------------------------------------------------------------------ + +module Semantics.Equivalence where + +open import Syntax +open import Semantics.BigStep +open import Semantics.SmallStep +open ⟶-Reasoning + +open import Data.Nat +open import Data.Star +open import Data.Product +open import Data.Empty + +------------------------------------------------------------------------ +-- Statement of equivalence + +record Big⇒Small : Set where + field + ⇓ : forall {t} {e : Expr t} {i v} -> + e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝ + + ⇑ : forall {t} {e : Expr t} {i} -> + e ⇑[ i ] -> e ⟶∞[ i ] + +record Small⇒Big : Set where + field + ⟶⋆ : forall {t} (e : Expr t) {i} v -> + e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v + + ⟶∞ : forall {t} (e : Expr t) {i} -> + e ⟶∞[ i ] -> e ⇑[ i ] + +------------------------------------------------------------------------ +-- Proof of Big⇒Small + +big⇒small⇓ : forall {t} {e : Expr t} {i v} -> + e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝ +big⇒small⇓ (Val {n = n}) = begin val n ∎ +big⇒small⇓ Throw = begin throw ∎ +big⇒small⇓ (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin + x ⊕ y + ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x⇓) ⟩ + val m ⊕ y + ⟶⋆⟨ lift⟶⋆ (val m [ |⊕| ]• •) (big⇒small⇓ y⇓) ⟩ + val m ⊕ val n + ⟶⟨ reduction • Add₁ ⟩ + val (m + n) + ∎ +big⇒small⇓ (Add₂ {x = x} {y} x↯) = begin + x ⊕ y + ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x↯) ⟩ + throw ⊕ y + ⟶⟨ reduction • Add₂ ⟩ + throw + ∎ +big⇒small⇓ (Add₃ {x = x} {y} {m} x⇓ y↯) = begin + x ⊕ y + ⟶⋆⟨ lift⟶⋆ (• •[ |⊕| ] y) (big⇒small⇓ x⇓) ⟩ + val m ⊕ y + ⟶⋆⟨ lift⟶⋆ (val m [ |⊕| ]• •) (big⇒small⇓ y↯) ⟩ + val m ⊕ throw + ⟶⟨ reduction • Add₃ ⟩ + throw + ∎ +big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin + x >> y + ⟶⋆⟨ lift⟶⋆ (• •[ |>>| ] y) (big⇒small⇓ x⇓) ⟩ + val m >> y + ⟶⟨ reduction • Seqn₁ ⟩ + y + ⟶⋆⟨ big⇒small⇓ y⇒ ⟩ + ⌜ v ⌝ + ∎ +big⇒small⇓ (Seqn₂ {x = x} {y} x↯) = begin + x >> y + ⟶⋆⟨ lift⟶⋆ (• •[ |>>| ] y) (big⇒small⇓ x↯) ⟩ + throw >> y + ⟶⟨ reduction • Seqn₂ ⟩ + throw + ∎ +big⇒small⇓ (Catch₁ {x = x} {y} {m} x⇓) = begin + x catch y + ⟶⋆⟨ lift⟶⋆ (• •[ |catch| ] y) (big⇒small⇓ x⇓) ⟩ + val m catch y + ⟶⟨ reduction • Catch₁ ⟩ + val m + ∎ +big⇒small⇓ (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin + x catch y + ⟶⋆⟨ lift⟶⋆ (• •[ |catch| ] y) (big⇒small⇓ x↯) ⟩ + throw catch y + ⟶⟨ reduction • Catch₂ ⟩ + y + ⟶⋆⟨ big⇒small⇓ y⇒ ⟩ + ⌜ v ⌝ + ∎ +big⇒small⇓ (Int {x = x}) = begin + x + ⟶⟨ reduction • Int ⟩ + throw + ∎ +big⇒small⇓ (Block {x = x} {v} x⇒) = begin + block x + ⟶⋆⟨ lift⟶⋆ (block• •) (big⇒small⇓ x⇒) ⟩ + block ⌜ v ⌝ + ⟶⟨ reduction • Block ⟩ + ⌜ v ⌝ + ∎ +big⇒small⇓ (Unblock {x = x} {v} x⇒) = begin + unblock x + ⟶⋆⟨ lift⟶⋆ (unblock• •) (big⇒small⇓ x⇒) ⟩ + unblock ⌜ v ⌝ + ⟶⟨ reduction • Unblock ⟩ + ⌜ v ⌝ + ∎ + +big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> e ⟶∞[ i ] +big⇒small⇑ Loop = reduction • Loop loops +big⇒small⇑ (Add₁ x⇑) = lift⟶∞ (• •[ |⊕| ] _) (big⇒small⇑ x⇑) +big⇒small⇑ (Add₂ (_ , x⇓) y⇑) = lift⟶⋆ (• •[ |⊕| ] _) (big⇒small⇓ x⇓) + ◅◅∞ + lift⟶∞ (_ [ |⊕| ]• •) (big⇒small⇑ y⇑) +big⇒small⇑ (Seqn₁ x⇑) = lift⟶∞ (• •[ |>>| ] _) (big⇒small⇑ x⇑) +big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) = lift⟶⋆ (• •[ |>>| ] _) (big⇒small⇓ x⇓) + ◅◅∞ + lift⟶∞ (_ [ |>>| ]• •) (big⇒small⇑ y⇑) +big⇒small⇑ (Catch₁ x⇑) = lift⟶∞ (• •[ |catch| ] _) (big⇒small⇑ x⇑) +big⇒small⇑ (Catch₂ x↯ y⇑) = lift⟶⋆ (• •[ |catch| ] _) (big⇒small⇓ x↯) + ◅◅∞ + lift⟶∞ (_ [ |catch| ]• •) (big⇒small⇑ y⇑) +big⇒small⇑ (Block x⇑) = lift⟶∞ (block• •) (big⇒small⇑ x⇑) +big⇒small⇑ (Unblock x⇑) = lift⟶∞ (unblock• •) (big⇒small⇑ x⇑) + +big⇒small : Big⇒Small +big⇒small = record { ⇓ = big⇒small⇓; ⇑ = big⇒small⇑ } + +------------------------------------------------------------------------ +-- Proof of Small⇒Big + +small⇒big⟶ʳ : forall {t} {e₁ e₂ : Expr t} {i v} -> + e₁ ⟶ʳ[ i ] e₂ -> e₂ ⇓[ i ] v -> e₁ ⇓[ i ] v +small⇒big⟶ʳ Loop Int = Int +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₂ ⇓ = Catch₂ Throw ⇓ +small⇒big⟶ʳ Int Throw = Int +small⇒big⟶ʳ Int Int = Int +small⇒big⟶ʳ (Block {i = i} {val n}) Val = Block Val +small⇒big⟶ʳ (Block .{i = U} {val n}) Int = Int +small⇒big⟶ʳ (Block {i = i} {throw}) Throw = Block Throw +small⇒big⟶ʳ (Block .{i = U} {throw}) Int = Int +small⇒big⟶ʳ (Unblock {i = i} {val n}) Val = Unblock Val +small⇒big⟶ʳ (Unblock .{i = U} {val n}) Int = Int +small⇒big⟶ʳ (Unblock {i = i} {throw}) Throw = Unblock Throw +small⇒big⟶ʳ (Unblock .{i = U} {throw}) Int = Int + +small⇒big⟶ : forall {i j t} (E : EvalCtxt t i j) {e₁ e₂ v} -> + e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⇓[ j ] v -> E [ e₁ ] ⇓[ j ] v +small⇒big⟶ • r ⇒ = small⇒big⟶ʳ r ⇒ +small⇒big⟶ (E •[ |⊕| ] y) r (Add₁ ⇓₁ ⇓₂) = Add₁ (small⇒big⟶ E r ⇓₁) ⇓₂ +small⇒big⟶ (E •[ |⊕| ] y) r (Add₂ ↯₁) = Add₂ (small⇒big⟶ E r ↯₁) +small⇒big⟶ (E •[ |⊕| ] y) r (Add₃ ⇓₁ ↯₂) = Add₃ (small⇒big⟶ E r ⇓₁) ↯₂ +small⇒big⟶ (E •[ |⊕| ] y) r Int = Int +small⇒big⟶ (E •[ |>>| ] y) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ (small⇒big⟶ E r ⇓₁) ⇒₂ +small⇒big⟶ (E •[ |>>| ] y) r (Seqn₂ ↯₁) = Seqn₂ (small⇒big⟶ E r ↯₁) +small⇒big⟶ (E •[ |>>| ] y) r Int = Int +small⇒big⟶ (E •[ |catch| ] y) r (Catch₁ ⇓₁) = Catch₁ (small⇒big⟶ E r ⇓₁) +small⇒big⟶ (E •[ |catch| ] y) r (Catch₂ ↯₁ ⇒₂) = Catch₂ (small⇒big⟶ E r ↯₁) ⇒₂ +small⇒big⟶ (E •[ |catch| ] y) r Int = Int +small⇒big⟶ (v [ |⊕| ]• E) r (Add₁ ⇓₁ ⇓₂) = Add₁ ⇓₁ (small⇒big⟶ E r ⇓₂) +small⇒big⟶ (v [ |⊕| ]• E) r (Add₂ ↯₁) = Add₂ ↯₁ +small⇒big⟶ (v [ |⊕| ]• E) r (Add₃ ⇓₁ ↯₂) = Add₃ ⇓₁ (small⇒big⟶ E r ↯₂) +small⇒big⟶ (v [ |⊕| ]• E) r Int = Int +small⇒big⟶ (v [ |>>| ]• E) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ ⇓₁ (small⇒big⟶ E r ⇒₂) +small⇒big⟶ (v [ |>>| ]• E) r (Seqn₂ ↯₁) = Seqn₂ ↯₁ +small⇒big⟶ (v [ |>>| ]• E) r Int = Int +small⇒big⟶ (v [ |catch| ]• E) r (Catch₁ ⇓₁) = Catch₁ ⇓₁ +small⇒big⟶ (v [ |catch| ]• E) r (Catch₂ ↯₁ ⇒₂) = Catch₂ ↯₁ (small⇒big⟶ E r ⇒₂) +small⇒big⟶ (v [ |catch| ]• E) r Int = Int +small⇒big⟶ (block• E) r Int = Int +small⇒big⟶ (block• E) r (Block ⇒) = Block (small⇒big⟶ E r ⇒) +small⇒big⟶ (unblock• E) r Int = Int +small⇒big⟶ (unblock• E) r (Unblock ⇒) = Unblock (small⇒big⟶ E r ⇒) + +small⇒big⟶⋆ : forall {t} (e : Expr t) {i} v -> + e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v +small⇒big⟶⋆ .(⌜ val n ⌝) (val n) ε = Val +small⇒big⟶⋆ .(⌜ throw ⌝) throw ε = Throw +small⇒big⟶⋆ .(E [ x ]) v (reduction {x = x} {y} E r ◅ rs) = + small⇒big⟶ E r (small⇒big⟶⋆ (E [ y ]) v rs) + +postulate + small⇒big⟶∞ : forall {t} (e : Expr t) {i} -> e ⟶∞[ i ] -> e ⇑[ i ] +-- small⇒big⟶∞ (val x) ⟶∞ = ⊥-elim {! !} +-- small⇒big⟶∞ throw ⟶∞ = ⊥-elim {! !} +-- small⇒big⟶∞ loop ⟶∞ = Loop +-- small⇒big⟶∞ (x ⊕ y) ⟶∞ = {! !} +-- small⇒big⟶∞ (x >> y) ⟶∞ = {! !} +-- small⇒big⟶∞ (x catch y) ⟶∞ = {! !} +-- small⇒big⟶∞ (block x) ⟶∞ = {! !} +-- small⇒big⟶∞ (unblock x) ⟶∞ = {! !} + +small⇒big : Small⇒Big +small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ } hunk ./Semantics/SmallStep.agda 2 --- A small-step semantics for the language +-- Small-step semantics hunk ./Semantics/SmallStep.agda 11 -module SmallStep where +module Semantics.SmallStep where + +open import Syntax +import Infinite hunk ./Semantics/SmallStep.agda 16 -open import Language hunk ./Semantics/SmallStep.agda 17 +open import Data.Star +open import Data.Product hunk ./Semantics/SmallStep.agda 24 -infix 3 _⟶ʳ[_]_ - -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 - ------------------------------------------------------------------------- --- Evaluation contexts +infix 3 _⟶ʳ[_]_ _∶_⟶ʳ[_]_ hunk ./Semantics/SmallStep.agda 26 -infix 8 _•[_]_ _[_]•_ _⟨_⟩_ +mutual hunk ./Semantics/SmallStep.agda 28 --- "Higher-order" representation of binary operators. + private + _∶_⟶ʳ[_]_ : forall t -> Expr t -> Status -> Expr t -> Set + t ∶ e₁ ⟶ʳ[ i ] e₂ = e₁ ⟶ʳ[ i ] e₂ hunk ./Semantics/SmallStep.agda 32 -data Op : Set where - ⊕′ : Op - >>′ : Op - catch′ : Op + data _⟶ʳ[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set where + Loop : forall {i} -> loop ⟶ʳ[ i ] loop + Add₁ : forall {t i m n} -> t ∶ val m ⊕ val n ⟶ʳ[ i ] val (m + n) + Add₂ : forall {t i y} -> t ∶ throw ⊕ y ⟶ʳ[ i ] throw + Add₃ : forall {t i m} -> t ∶ val m ⊕ throw ⟶ʳ[ i ] throw + Seqn₁ : forall {t i m y} -> t ∶ val m >> y ⟶ʳ[ i ] y + Seqn₂ : forall {t i y} -> t ∶ throw >> y ⟶ʳ[ i ] throw + Catch₁ : forall {t i m y} -> t ∶ val m catch y ⟶ʳ[ i ] val m + Catch₂ : forall {t i y} -> t ∶ throw catch y ⟶ʳ[ i ] y + Int : forall {t x} -> t ∶ x ⟶ʳ[ U ] throw + Block : forall {t i v} -> t ∶ block ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ + Unblock : forall {t i v} -> t ∶ unblock ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ hunk ./Semantics/SmallStep.agda 45 --- Application. +------------------------------------------------------------------------ +-- Evaluation contexts hunk ./Semantics/SmallStep.agda 48 -_⟨_⟩_ : forall {t} -> Expr t -> Op -> Expr t -> Expr t -x ⟨ ⊕′ ⟩ y = x ⊕ y -x ⟨ >>′ ⟩ y = x >> y -x ⟨ catch′ ⟩ y = x catch y +infix 8 _•[_]_ _[_]•_ hunk ./Semantics/SmallStep.agda 58 - Value t -> Op -> EvalCtxt t i j -> EvalCtxt t i j + Value -> Op -> EvalCtxt t i j -> EvalCtxt t i j hunk ./Semantics/SmallStep.agda 68 -(E •[ op ] x) [ y ] = E [ y ] ⟨ op ⟩ x -(v [ op ]• E) [ y ] = ⌜ v ⌝ ⟨ op ⟩ E [ y ] +(E •[ op ] x) [ y ] = E [ y ] < op > x +(v [ op ]• E) [ y ] = ⌜ v ⌝ < op > E [ y ] hunk ./Semantics/SmallStep.agda 74 --- Single-step evaluation +-- The semantics + +-- Single-step evaluation. hunk ./Semantics/SmallStep.agda 84 ------------------------------------------------------------------------- --- Small-step semantics - hunk ./Semantics/SmallStep.agda 86 -open import Data.Star - hunk ./Semantics/SmallStep.agda 93 -open ⟶-Reasoning + +-- Infinite reduction sequences. + +private + module Infinite⟶ {t : Totality} {i : Status} = + Infinite (\x y -> _⟶[_]_ {t} x i y) +open Infinite⟶ public hiding (_⟶∞) + +infix 3 _⟶∞[_] + +_⟶∞[_] : forall {t} -> Expr t -> Status -> Set +e ⟶∞[ i ] = Infinite⟶._⟶∞ {i = i} e hunk ./Semantics/SmallStep.agda 107 --- Equivalence to the big-step semantics +-- Some utility functions/lemmas hunk ./Semantics/SmallStep.agda 125 -∘-lemma (E₁ •[ op ] y) E₂ = ≡-cong (\x -> x ⟨ op ⟩ y) (∘-lemma E₁ E₂) -∘-lemma (v [ op ]• E₁) E₂ = ≡-cong (_⟨_⟩_ ⌜ v ⌝ op) (∘-lemma E₁ E₂) +∘-lemma (E₁ •[ op ] y) E₂ = ≡-cong (\x -> x < op > y) (∘-lemma E₁ E₂) +∘-lemma (v [ op ]• E₁) E₂ = ≡-cong (_<_>_ ⌜ v ⌝ op) (∘-lemma E₁ E₂) hunk ./Semantics/SmallStep.agda 130 --- Lifting of reductions. +-- Lifting of reductions/reduction sequences. hunk ./Semantics/SmallStep.agda 139 --- Lifting of reduction sequences. - -lift : forall {t x i j y} (E : EvalCtxt t i j) -> - x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ] -lift E r = gmap (\x -> E [ x ]) (lift⟶ E) r - --- Completeness. - -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 - x ⊕ y - ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x⇓) ⟩ - val m ⊕ y - ⟶⋆⟨ lift (val m [ ⊕′ ]• •) (complete y⇓) ⟩ - val m ⊕ val n - ⟶⟨ reduction • Add₁ ⟩ - val (m + n) - ∎ -complete (Add₂ {x = x} {y} {r = r} x↯) = begin - x ⊕ y - ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x↯) ⟩ - fail r ⊕ y - ⟶⟨ reduction • Add₂ ⟩ - fail r - ∎ -complete (Add₃ {x = x} {y} {m} {r = r} x⇓ y↯) = begin - x ⊕ y - ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x⇓) ⟩ - val m ⊕ y - ⟶⋆⟨ lift (val m [ ⊕′ ]• •) (complete y↯) ⟩ - val m ⊕ fail r - ⟶⟨ reduction • Add₃ ⟩ - fail r - ∎ -complete (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin - x >> y - ⟶⋆⟨ lift (• •[ >>′ ] y) (complete x⇓) ⟩ - val m >> y - ⟶⟨ reduction • Seqn₁ ⟩ - y - ⟶⋆⟨ complete y⇒ ⟩ - ⌜ v ⌝ - ∎ -complete (Seqn₂ {x = x} {y} {r = r} x↯) = begin - x >> y - ⟶⋆⟨ lift (• •[ >>′ ] y) (complete x↯) ⟩ - fail r >> y - ⟶⟨ reduction • Seqn₂ ⟩ - fail r - ∎ -complete (Catch₁ {x = x} {y} {m} x⇓) = begin - x catch y - ⟶⋆⟨ lift (• •[ catch′ ] y) (complete x⇓) ⟩ - val m catch y - ⟶⟨ reduction • Catch₁ ⟩ - val m - ∎ -complete (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin - x catch y - ⟶⋆⟨ lift (• •[ catch′ ] y) (complete x↯) ⟩ - fail throw catch y - ⟶⟨ reduction • Catch₂ ⟩ - y - ⟶⋆⟨ complete y⇒ ⟩ - ⌜ v ⌝ - ∎ -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 - x - ⟶⟨ reduction • Int ⟩ - fail throw - ∎ -complete (Block {x = x} {v} x⇒) = begin - block x - ⟶⋆⟨ lift (block• •) (complete x⇒) ⟩ - block ⌜ v ⌝ - ⟶⟨ reduction • Block ⟩ - ⌜ v ⌝ - ∎ -complete (Unblock {x = x} {v} x⇒) = begin - unblock x - ⟶⋆⟨ lift (unblock• •) (complete x⇒) ⟩ - unblock ⌜ v ⌝ - ⟶⟨ reduction • Unblock ⟩ - ⌜ v ⌝ - ∎ - --- -- Soundness. - --- 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 {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 ⇒) +lift⟶⋆ : forall {t x i j y} (E : EvalCtxt t i j) -> + x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ] +lift⟶⋆ E r = gmap (\x -> E [ x ]) (lift⟶ E) r hunk ./Semantics/SmallStep.agda 143 --- 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) +lift⟶∞ : forall {t x i j} (E : EvalCtxt t i j) -> + x ⟶∞[ i ] -> E [ x ] ⟶∞[ j ] +lift⟶∞ E (seq , x⟶⋆y , step) = + ((\n -> E [ seq n ]) , lift⟶⋆ E x⟶⋆y , \n -> lift⟶ E (step n)) hunk ./StatusLemmas.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep hunk ./StatusLemmas.agda 18 -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 +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·⇓ (Block x) = Block x +Bto·⇓ (Unblock x) = Unblock x hunk ./StatusLemmas.agda 31 -·toU : forall {t} {x : Expr t} {v i} -> x ⇓[ i ] v -> x ⇓[ U ] v -·toU {i = B} x = Bto· x -·toU {i = U} x = x +·toU⇓ : forall {t} {x : Expr t} {v i} -> x ⇓[ i ] v -> x ⇓[ U ] v +·toU⇓ {i = B} x = Bto·⇓ x +·toU⇓ {i = U} x = x + +Bto·⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ B ] -> x ⇑[ i ] +Bto·⇑ Loop = Loop +Bto·⇑ (Add₁ x⇑) = Add₁ (Bto·⇑ x⇑) +Bto·⇑ (Add₂ (_ , x⇓) y⇑) = Add₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑) +Bto·⇑ (Seqn₁ x⇑) = Seqn₁ (Bto·⇑ x⇑) +Bto·⇑ (Seqn₂ (_ , x⇓) y⇑) = Seqn₂ (_ , Bto·⇓ x⇓) (Bto·⇑ y⇑) +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⇑ + +·toU⇑ : forall {t} {x : Expr t} {i} -> x ⇑[ i ] -> x ⇑[ U ] +·toU⇑ {i = B} x = Bto·⇑ x +·toU⇑ {i = U} x = x hunk ./StatusLemmas.agda 54 - x ⇓[ U ] val n -> x ⇓[ B ] val n) + x ⇓[ U ] val n -> x ⇓[ B ] val n) hunk ./StatusLemmas.agda 62 -¬UtoB' : ¬ (forall (x : Expr partial) -> x ⇓[ U ] -> x ⇓[ B ]) +¬UtoB' : ¬ (forall (x : Expr partial) -> x ↡[ U ] -> x ↡[ B ]) hunk ./StatusLemmas.agda 69 -Uto·' : forall {x : Expr total} {i} -> x ⇓[ U ] -> x ⇓[ i ] +Uto·' : forall {x : Expr total} {i} -> x ↡[ U ] -> x ↡[ i ] hunk ./StatusLemmas.agda 72 - helper : forall {x : Expr total} {i m} -> x ⇓[ U ] val m -> x ⇓[ i ] + helper : forall {x : Expr total} {i m} -> x ⇓[ U ] val m -> x ↡[ i ] hunk ./StatusLemmas.agda 80 - ... | throws x⇑' = map-Σ₂ (Catch₂ x⇑') (helper y⇓) - ... | returns x⇓ = (_ , Catch₁ x⇓) + ... | (throw , x⇑') = map-Σ₂ (Catch₂ x⇑') (helper y⇓) + ... | (val n , x⇓) = (n , Catch₁ x⇓) hunk ./StatusLemmas.agda 87 -block-unblockˡ x = Block (Unblock (·toU x)) +block-unblockˡ = record { ⇓ = \x -> Block (Unblock (·toU⇓ x)) + ; ⇑ = \x -> Block (Unblock (·toU⇑ x)) + } hunk ./StatusLemmas.agda 93 - with bux⊑x total (val 0) {i = B} (Block (Unblock Int)) + with _⊑_.⇓ (bux⊑x total (val 0)) {i = B} (Block (Unblock Int)) hunk ./StatusLemmas.agda 98 - with x⊑ubx total (val 0 catch val 1) (Catch₂ Int Val) + with _⊑_.⇓ (x⊑ubx total (val 0 catch val 1)) (Catch₂ Int Val) hunk ./StatusLemmas.agda 103 -unblock-blockʳ ubx⊑x with ubx⊑x total (val 0) {i = B} (Unblock Int) +unblock-blockʳ ubx⊑x + with _⊑_.⇓ (ubx⊑x total (val 0)) {i = B} (Unblock Int) hunk ./Syntax.agda 5 --- Taken from "What is the meaning of these constant interruptions?" --- (Hutton/Wright), but modified by me. - -module Language where +module Syntax where hunk ./Syntax.agda 8 -open import Data.Product hunk ./Syntax.agda 27 + loop : Expr partial hunk ./Syntax.agda 33 - loop : Expr partial hunk ./Syntax.agda 37 +-- Values. + +data Value : Set where + val : ℕ -> Value + throw : Value + +⌜_⌝ : forall {t} -> Value -> Expr t +⌜ val n ⌝ = val n +⌜ throw ⌝ = throw + hunk ./Syntax.agda 48 --- Semantics +-- Some other syntactic bits and pieces hunk ./Syntax.agda 50 -infix 3 _⇓[_]_ _⇓[_] _↯[_] _⇑[_] +-- Are interrupts blocked (B) or not (U)? hunk ./Syntax.agda 56 --- The reason for program failure. - -data Reason : Totality -> Set where - throw : forall {t} -> Reason t - loop : Reason partial - --- Values. - -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} -> - x ⇓[ i ] val m -> y ⇓[ i ] val n -> - x ⊕ y ⇓[ i ] val (m + n) - 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} -> - x ⇓[ i ] val m -> y ⇓[ i ] v -> x >> y ⇓[ i ] v - 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} -> - x ⇓[ i ] val m -> x catch y ⇓[ i ] val m - 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} -> - x ⇓[ B ] v -> block x ⇓[ i ] v - Unblock : forall {t} {x : Expr t} {v i} -> - x ⇓[ U ] v -> unblock x ⇓[ i ] v - Loop : forall {i} -> loop ⇓[ i ] fail loop +-- "Higher-order" representation of binary operators. hunk ./Syntax.agda 58 --- Short-hand notation. +data Op : Set where + |⊕| : Op + |>>| : Op + |catch| : Op hunk ./Syntax.agda 63 -_⇓[_] : forall {t} -> Expr t -> Status -> Set -x ⇓[ i ] = Σ ℕ \n -> x ⇓[ i ] val n +-- Application. hunk ./Syntax.agda 65 -_↯[_] : forall {t} -> Expr t -> Status -> Set -x ↯[ i ] = x ⇓[ i ] fail throw +infix 8 _<_>_ hunk ./Syntax.agda 67 -_⇑[_] : Expr partial -> Status -> Set -x ⇑[ i ] = x ⇓[ i ] fail loop +_<_>_ : forall {t} -> Expr t -> Op -> Expr t -> Expr t +x < |⊕| > y = x ⊕ y +x < |>>| > y = x >> y +x < |catch| > y = x catch y hunk ./Totality.agda 7 -open import Language +open import Syntax +open import Semantics.BigStep + hunk ./Totality.agda 15 --- Defined x i means that x can terminate (possibly exceptionally) --- when run in exception status i. - -data Defined {t : Totality} (x : Expr t) (i : Status) : Set where - returns : forall {n} -> x ⇓[ i ] val n -> Defined x i - throws : x ↯[ i ] -> Defined x i - hunk ./Totality.agda 17 -¬defined : ¬ (forall (x : Expr partial) i -> Defined x i) -¬defined defined with defined loop B -... | returns () -... | throws () +¬defined : ¬ (forall (x : Expr partial) i -> x ⇓[ i ]) +¬defined ⇓ with ⇓ loop B +... | (_ , ()) hunk ./Totality.agda 21 --- The expressions denoted as "total" are always potentially --- terminating. (Note that the "type system" ensures that total --- expressions cannot loop.) +-- The expressions denoted as total are always potentially +-- terminating... hunk ./Totality.agda 24 -defined : forall (x : Expr total) i -> Defined x i -defined (val n) _ = returns Val -defined throw _ = throws Throw +defined : forall (x : Expr total) i -> x ⇓[ i ] +defined (val n) _ = (_ , Val) +defined throw _ = (_ , Throw) hunk ./Totality.agda 28 -... | returns x⇓ | returns y⇓ = returns (Add₁ x⇓ y⇓) -... | returns x⇓ | throws y↯ = throws (Add₃ x⇓ y↯) -... | throws x⇓ | _ = throws (Add₂ x⇓) +... | (val _ , x⇓) | (val _ , y⇓) = (_ , Add₁ x⇓ y⇓) +... | (val _ , x⇓) | (throw , y↯) = (_ , Add₃ x⇓ y↯) +... | (throw , x↯) | _ = (_ , Add₂ x↯) hunk ./Totality.agda 32 -... | returns x⇓ | returns y⇓ = returns (Seqn₁ x⇓ y⇓) -... | returns x⇓ | throws y↯ = throws (Seqn₁ x⇓ y↯) -... | throws x⇓ | _ = throws (Seqn₂ x⇓) +... | (val _ , x⇓) | (val _ , y⇓) = (_ , Seqn₁ x⇓ y⇓) +... | (val _ , x⇓) | (throw , y↯) = (_ , Seqn₁ x⇓ y↯) +... | (throw , x↯) | _ = (_ , Seqn₂ x↯) hunk ./Totality.agda 36 -... | returns x⇓ | _ = returns (Catch₁ x⇓) -... | throws x↯ | returns y⇓ = returns (Catch₂ x↯ y⇓) -... | throws x↯ | throws y↯ = throws (Catch₂ x↯ y↯) -defined (block x) _ with defined x B -... | returns x⇓ = returns (Block x⇓) -... | throws x↯ = throws (Block x↯) -defined (unblock x) _ with defined x U -... | returns x⇓ = returns (Unblock x⇓) -... | throws x↯ = throws (Unblock x↯) +... | (val _ , x⇓) | _ = (_ , Catch₁ x⇓) +... | (throw , x↯) | (val _ , y⇓) = (_ , Catch₂ x↯ y⇓) +... | (throw , x↯) | (throw , y↯) = (_ , Catch₂ x↯ y↯) +defined (block x) _ = map-Σ₂ Block (defined x B) +defined (unblock x) _ = map-Σ₂ Unblock (defined x U) + +-- ...and never non-terminating. + +¬undefined : forall (x : Expr total) {i} -> ¬ x ⇑[ i ] +¬undefined (val n) () +¬undefined throw () +¬undefined (x ⊕ y) (Add₁ x⇑) = ¬undefined x x⇑ +¬undefined (x ⊕ y) (Add₂ x⇓ y⇑) = ¬undefined y y⇑ +¬undefined (x >> y) (Seqn₁ x⇑) = ¬undefined x x⇑ +¬undefined (x >> y) (Seqn₂ x⇓ y⇑) = ¬undefined y y⇑ +¬undefined (x catch y) (Catch₁ x⇑) = ¬undefined x x⇑ +¬undefined (x catch y) (Catch₂ x↯ y⇑) = ¬undefined y y⇑ +¬undefined (block x) (Block x⇑) = ¬undefined x x⇑ +¬undefined (unblock x) (Unblock x⇑) = ¬undefined x x⇑ hunk ./Totality.agda 58 -cannot-throw⇒can-return : - forall {x : Expr total} {i} -> - ¬ x ↯[ i ] -> Σ₀ \n -> x ⇓[ i ] val n +cannot-throw⇒can-return : forall {x : Expr total} {i} -> + ¬ x ↯[ i ] -> x ↡[ i ] hunk ./Totality.agda 61 -... | returns x⇓ = (_ , x⇓) -... | throws x↯ = ⊥-elim (¬x↯ x↯) +... | (val n , x↡) = (n , x↡) +... | (throw , x↯) = ⊥-elim (¬x↯ x↯) hunk ./Totality.agda 64 -cannot-return⇒can-throw : - forall {x : Expr total} {i} -> - ¬ Σ₀ (\n -> x ⇓[ i ] val n) -> x ↯[ i ] -cannot-return⇒can-throw {x} {i} ¬x⇓ with defined x i -... | returns x⇓ = ⊥-elim (¬x⇓ (_ , x⇓)) -... | throws x↯ = x↯ +cannot-return⇒can-throw : forall {x : Expr total} {i} -> + ¬ x ↡[ i ] -> x ↯[ i ] +cannot-return⇒can-throw {x} {i} ¬x↡ with defined x i +... | (val n , x↡) = ⊥-elim (¬x↡ (n , x↡)) +... | (throw , x↯) = x↯ hunk ./Totality.agda 118 -can-return? : forall (x : Expr total) i -> Dec (Σ₀ \n -> x ⇓[ i ] val n) +can-return? : forall (x : Expr total) i -> Dec (x ↡[ i ]) hunk ./Totality.agda 122 - helper : ¬ Σ₀ \n -> throw ⇓[ i ] val n + helper : ¬ throw ↡[ i ] hunk ./Totality.agda 128 - helper : ¬ Σ₀ \n -> x ⊕ y ⇓[ i ] val n + helper : ¬ x ⊕ y ↡[ i ] hunk ./Totality.agda 132 - helper : ¬ Σ₀ \n -> x ⊕ y ⇓[ i ] val n + helper : ¬ x ⊕ y ↡[ i ] hunk ./Totality.agda 138 - helper : ¬ Σ₀ \n -> x >> y ⇓[ i ] val n + helper : ¬ x >> y ↡[ i ] hunk ./Totality.agda 142 - helper : ¬ Σ₀ \n -> x >> y ⇓[ i ] val n + helper : ¬ x >> y ↡[ i ] hunk ./Totality.agda 149 - helper : ¬ Σ₀ \n -> x catch y ⇓[ i ] val n + helper : ¬ x catch y ↡[ i ] hunk ./Totality.agda 156 - helper : ¬ Σ₀ \n -> block x ⇓[ i ] val n + helper : ¬ block x ↡[ i ] hunk ./Totality.agda 162 - helper : ¬ Σ₀ \n -> unblock x ⇓[ i ] val n + helper : ¬ unblock x ↡[ i ] hunk ./Totality.agda 172 -decidable : forall (x : Expr total) i -> - (Σ₀ \n -> x ⇓[ i ] val n) Or (x ↯[ i ]) +decidable : forall (x : Expr total) i -> (x ↡[ i ]) Or (x ↯[ i ]) hunk ./Totality.agda 174 -decidable x i | yes x⇓ | yes x↯ = both x⇓ x↯ -decidable x i | yes x⇓ | no ¬x↯ = first x⇓ ¬x↯ -decidable x i | no ¬x⇓ | yes x↯ = second ¬x⇓ x↯ -decidable x i | no ¬x⇓ | no ¬x↯ with defined x i -decidable x i | no ¬x⇓ | no ¬x↯ | returns x⇓ = ⊥-elim (¬x⇓ (_ , x⇓)) -decidable x i | no ¬x⇓ | no ¬x↯ | throws x↯ = ⊥-elim (¬x↯ x↯) +decidable x i | yes x↡ | yes x↯ = both x↡ x↯ +decidable x i | yes x↡ | no ¬x↯ = first x↡ ¬x↯ +decidable x i | no ¬x↡ | yes x↯ = second ¬x↡ x↯ +decidable x i | no ¬x↡ | no ¬x↯ with defined x i +decidable x i | no ¬x↡ | no ¬x↯ | (val n , x↡) = ⊥-elim (¬x↡ (n , x↡)) +decidable x i | no ¬x↡ | no ¬x↯ | (throw , x↯) = ⊥-elim (¬x↯ x↯) hunk ./Totality.agda 185 +-- Finally some boring lemmas related to the absence of +-- non-termination. + +¬⇑-⊕ˡ : forall {t} {x y : Expr t} {i} -> + ¬ x ⊕ y ⇑[ i ] -> ¬ x ⇑[ i ] +¬⇑-⊕ˡ ¬⇑ = \x⇑ -> ¬⇑ (Add₁ x⇑) + +¬⇑-⊕ʳ : forall {t} {x y : Expr t} {i} -> + ¬ x ⊕ y ⇑[ i ] -> x ↡[ i ] -> ¬ y ⇑[ i ] +¬⇑-⊕ʳ ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Add₂ x⇓ y⇑) + +¬⇑->>ˡ : forall {t} {x y : Expr t} {i} -> + ¬ x >> y ⇑[ i ] -> ¬ x ⇑[ i ] +¬⇑->>ˡ ¬⇑ = \x⇑ -> ¬⇑ (Seqn₁ x⇑) + +¬⇑->>ʳ : forall {t} {x y : Expr t} {i} -> + ¬ x >> y ⇑[ i ] -> x ↡[ i ] -> ¬ y ⇑[ i ] +¬⇑->>ʳ ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Seqn₂ x⇓ y⇑) + +¬⇑-catchˡ : forall {t} {x y : Expr t} {i} -> + ¬ x catch y ⇑[ i ] -> ¬ x ⇑[ i ] +¬⇑-catchˡ ¬⇑ = \x⇑ -> ¬⇑ (Catch₁ x⇑) + +¬⇑-catchʳ : forall {t} {x y : Expr t} {i} -> + ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> ¬ y ⇑[ i ] +¬⇑-catchʳ ¬⇑ x↯ = \y⇑ -> ¬⇑ (Catch₂ x↯ y⇑) + +¬⇑-block : forall {t} {x : Expr t} {i} -> + ¬ block x ⇑[ i ] -> ¬ x ⇑[ B ] +¬⇑-block ¬⇑ = \x⇑ -> ¬⇑ (Block x⇑) + +¬⇑-unblock : forall {t} {x : Expr t} {i} -> + ¬ unblock x ⇑[ i ] -> ¬ x ⇑[ U ] +¬⇑-unblock ¬⇑ = \x⇑ -> ¬⇑ (Unblock x⇑) + hunk ./VirtualMachine.agda 7 -open import Language +open import Syntax + hunk ./VirtualMachine.agda 20 - -- A virtual machine code snippet is a list of operations. + -- A virtual machine code snippet is a list of instructions. hunk ./VirtualMachine.agda 22 - data Op : Set where - push : ℕ -> Op - throw : Op - add : Op - pop : Op - mark : Code -> Op - unmark : Op - set : Status -> Op - reset : Op - loop : Op + data Inst : Set where + push : ℕ -> Inst + throw : Inst + loop : Inst + add : Inst + pop : Inst + mark : Code -> Inst + unmark : Inst + set : Status -> Inst + reset : Inst hunk ./VirtualMachine.agda 34 - Code = [ Op ] + Code = [ Inst ] hunk ./VirtualMachine.agda 57 + loop : forall {ops i s} -> + ⟨ loop ∷ ops , i , s ⟩ ⟶ ⟨ loop ∷ ops , i , s ⟩ hunk ./VirtualMachine.agda 73 - loop : forall {ops i s} -> - ⟨ loop ∷ ops , i , s ⟩ ⟶ ⟨ loop ∷ ops , i , s ⟩ hunk ./VirtualMachine.agda 93 +comp loop ops = loop ∷ ops hunk ./VirtualMachine.agda 99 -comp loop ops = loop ∷ ops + +-- Starting states for the virtual machine. + +start : forall {t} -> Expr t -> Status -> State +start e i = ⟨ comp e [] , i , [] ⟩ + +-- Final states. + +data Final : State -> Set where + returns : forall i s -> Final ⟨ [] , i , s ⟩ + throws : forall i -> Final ⟪ i , [] ⟫