[Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20091015185044 Ignore-this: c08f14565bc6243c0d276d60b456cb79 ] hunk ./ApplicationBased.agda 67 - ≡⟨ ≡-cong₂ _∸_ (proof (eval e₁)) (proof (eval e₂)) ⟩ + ≡⟨ cong₂ _∸_ (proof (eval e₁)) (proof (eval e₂)) ⟩ hunk ./ApplicationBased.agda 69 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./ApplicationBased.agda 144 - execOK ε s = ≡-refl + execOK ε s = refl hunk ./ApplicationBased.agda 172 - correct e = ≡-refl + correct e = refl hunk ./DanvyFirstAttempt.agda 22 - infix 50 λ_ - infixr 30 _→_ + infix 50 ƛ_ + infixr 30 _⟶_ hunk ./DanvyFirstAttempt.agda 31 - _→_ : Ty -> Ty -> Ty + _⟶_ : Ty -> Ty -> Ty hunk ./DanvyFirstAttempt.agda 53 - λ_ : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ → τ - _·_ : forall {Γ σ τ} -> Γ ⊢ σ → τ -> Γ ⊢ σ -> Γ ⊢ τ + ƛ_ : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⟶ τ + _·_ : forall {Γ σ τ} -> Γ ⊢ σ ⟶ τ -> Γ ⊢ σ -> Γ ⊢ τ hunk ./DanvyFirstAttempt.agda 60 - ⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆ + ⟦ σ ⟶ τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆ hunk ./DanvyFirstAttempt.agda 83 - ⟦ λ t ⟧ ρ = \v -> ⟦ t ⟧ (ρ ▷ v) + ⟦ ƛ t ⟧ ρ = \v -> ⟦ t ⟧ (ρ ▷ v) hunk ./DanvyFirstAttempt.agda 101 - Λ_ : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ) + Λ_ : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ ⟶ τ) hunk ./DanvyFirstAttempt.agda 104 - _⊙_ : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ + _⊙_ : forall {Γ σ τ} -> Dom Γ (σ ⟶ τ) -> Dom Γ σ -> Dom Γ τ hunk ./DanvyFirstAttempt.agda 114 - ⟦ λ t ⟧'P = ▷ begin + ⟦ ƛ t ⟧'P = ▷ begin hunk ./DanvyFirstAttempt.agda 116 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./DanvyFirstAttempt.agda 121 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./DanvyFirstAttempt.agda 138 - Λ_ : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ) - _⊙_ : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ + Λ_ : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ ⟶ τ) + _⊙_ : forall {Γ σ τ} -> Dom Γ (σ ⟶ τ) -> Dom Γ σ -> Dom Γ τ hunk ./DanvyFirstAttempt.agda 143 - ⟦ λ t ⟧ = Λ ⟦ t ⟧ + ⟦ ƛ t ⟧ = Λ ⟦ t ⟧ hunk ./DanvyFirstAttempt.agda 159 - eval-correct (var x) = ≡-refl - eval-correct (λ t) = ≡-cong Step₁.Λ_ (eval-correct t) + eval-correct (var x) = refl + eval-correct (ƛ t) = cong Step₁.Λ_ (eval-correct t) hunk ./DanvyFirstAttempt.agda 162 - ≡-cong₂ Step₁._⊙_ (eval-correct t₁) (eval-correct t₂) + cong₂ Step₁._⊙_ (eval-correct t₁) (eval-correct t₂) hunk ./DanvyFirstAttempt.agda 170 - ; Λ_ = λ_ + ; Λ_ = ƛ_ hunk ./DanvyFirstAttempt.agda 179 - term-uninteresting (var x) = ≡-refl - term-uninteresting (λ t) = ≡-cong λ_ (term-uninteresting t) + term-uninteresting (var x) = refl + term-uninteresting (ƛ t) = cong ƛ_ (term-uninteresting t) hunk ./DanvyFirstAttempt.agda 182 - ≡-cong₂ _·_ (term-uninteresting t₁) (term-uninteresting t₂) + cong₂ _·_ (term-uninteresting t₁) (term-uninteresting t₂) hunk ./Exceptions.agda 20 - (≡-ext : forall {a b : Set} {f g : a -> b} -> - (forall x -> f x ≡ g x) -> f ≡ g) + (ext : forall {a b : Set} {f g : a -> b} -> + (forall x -> f x ≡ g x) -> f ≡ g) hunk ./Exceptions.agda 25 -open import Data.Maybe +open import Data.Maybe as Maybe hunk ./Exceptions.agda 29 -open RawMonadPlus MaybeMonadPlus +open RawMonadPlus Maybe.monadPlus hunk ./Exceptions.agda 72 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Exceptions.agda 76 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Exceptions.agda 78 - ≡⟨ ≡-cong (eval e₁) - (≡-ext (\m -> proof (evalP e₂ - (\n -> c (pure _+_ ⊛ m ⊛ n))))) ⟩ + ≡⟨ cong (eval e₁) + (ext (\m -> proof (evalP e₂ + (\n -> c (pure _+_ ⊛ m ⊛ n))))) ⟩ hunk ./Exceptions.agda 86 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Exceptions.agda 90 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Exceptions.agda 92 - ≡⟨ ≡-cong (eval e₁) - (≡-ext (\m -> proof (evalP e₂ (\n -> c (m ∣ n))))) ⟩ + ≡⟨ cong (eval e₁) + (ext (\m -> proof (evalP e₂ (\n -> c (m ∣ n))))) ⟩ hunk ./Exceptions.agda 161 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Exceptions.agda 169 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./HuttonsRazor.agda 12 - (≡-ext : forall {a b : Set} {f g : a -> b} -> - (forall x -> f x ≡ g x) -> f ≡ g) + (ext : forall {a b : Set} {f g : a -> b} -> + (forall x -> f x ≡ g x) -> f ≡ g) hunk ./HuttonsRazor.agda 19 +open import Data.Star.Properties hunk ./HuttonsRazor.agda 71 - distrib s ε c₂ = ≡-refl + distrib s ε c₂ = refl hunk ./HuttonsRazor.agda 77 - thm1 s (val n) = ≡-refl + thm1 s (val n) = refl hunk ./HuttonsRazor.agda 82 - ≡⟨ ≡-cong ⟪ comp e₂ ◅◅ add ◅ ε ⟫ (thm1 s e₁) ⟩ + ≡⟨ cong ⟪ comp e₂ ◅◅ add ◅ ε ⟫ (thm1 s e₁) ⟩ hunk ./HuttonsRazor.agda 86 - ≡⟨ ≡-cong ⟪ add ◅ ε ⟫ (thm1 (↦ ⟦ e₁ ⟧ ◅ s) e₂) ⟩ + ≡⟨ cong ⟪ add ◅ ε ⟫ (thm1 (↦ ⟦ e₁ ⟧ ◅ s) e₂) ⟩ hunk ./HuttonsRazor.agda 97 - thm2 s (val n) ops = ≡-refl + thm2 s (val n) ops = refl hunk ./HuttonsRazor.agda 100 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./HuttonsRazor.agda 102 - ≡⟨ ≡-cong (\ops' -> ⟪ ops' ⟫ s) - (◅◅-assoc (comp e₁) (comp e₂ ◅◅ add ◅ ε) ops) ⟩ + ≡⟨ cong (\ops' -> ⟪ ops' ⟫ s) + (◅◅-assoc (comp e₁) (comp e₂ ◅◅ add ◅ ε) ops) ⟩ hunk ./HuttonsRazor.agda 105 - ≡⟨ ≡-cong (\s' -> ⟪ comp e₁ ◅◅ s' ⟫ s) - (◅◅-assoc (comp e₂) (add ◅ ε) ops) ⟩ + ≡⟨ cong (\s' -> ⟪ comp e₁ ◅◅ s' ⟫ s) + (◅◅-assoc (comp e₂) (add ◅ ε) ops) ⟩ hunk ./HuttonsRazor.agda 140 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./HuttonsRazor.agda 144 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./HuttonsRazor.agda 146 - ≡⟨ ≡-cong (eval e₁) - (≡-ext (\m -> proof (evalP e₂ (\n -> c (m + n))))) ⟩ + ≡⟨ cong (eval e₁) + (ext (\m -> proof (evalP e₂ (\n -> c (m + n))))) ⟩ hunk ./HuttonsRazor.agda 204 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./HuttonsRazor.agda 225 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./MultiComposition.agda 5 -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality as PropEq + using (_≡_; refl; sym; cong; cong₂) hunk ./MultiComposition.agda 10 - (≡-ext : forall {a b : Set} {f g : a -> b} -> - (forall x -> f x ≡ g x) -> f ≡ g) + (ext : forall {a b : Set} {f g : a -> b} -> + (forall x -> f x ≡ g x) -> f ≡ g) hunk ./MultiComposition.agda 14 -open ≡-Reasoning -open import Relation.Binary.PropositionalEquality1 +open PropEq.≡-Reasoning +open import Relation.Binary.HeterogeneousEquality as HetEq + using (_≅_; refl) +open import Relation.Binary.PropositionalEquality1 as PropEq₁ + using (_≡₁_; refl) renaming (subst to subst₁) hunk ./MultiComposition.agda 21 -open import Algebra.Structures +open import Algebra hunk ./MultiComposition.agda 23 +private + module CS = CommutativeSemiring Nat.commutativeSemiring hunk ./MultiComposition.agda 34 - infixr 5 _→_ + infixr 5 _⟶_ hunk ./MultiComposition.agda 36 - _→_ : Set -> Set - map : forall {a b} -> (a -> b) -> _→_ a -> _→_ b + _⟶_ : Set -> Set + map : forall {a b} -> (a -> b) -> _⟶_ a -> _⟶_ b hunk ./MultiComposition.agda 51 - { _→_ = \c -> c + { _⟶_ = \c -> c hunk ./MultiComposition.agda 53 - ; map-id = \a -> ≡-refl - ; map-∘ = \f g -> ≡-refl + ; map-id = \a -> refl + ; map-∘ = \f g -> refl hunk ./MultiComposition.agda 63 - { _→_ = \c -> a -> bs → c + { _⟶_ = \c -> a -> bs ⟶ c hunk ./MultiComposition.agda 65 - ; map-id = \a -> ≡-ext \k -> ≡-ext \x -> - ≡-cong (\h -> h (k x)) (map-id bs a) - ; map-∘ = \f g -> ≡-ext \k -> ≡-ext \x -> - ≡-cong (\h -> h (k x)) (map-∘ bs f g) + ; map-id = \a -> ext \k -> ext \x -> + cong (\h -> h (k x)) (map-id bs a) + ; map-∘ = \f g -> ext \k -> ext \x -> + cong (\h -> h (k x)) (map-∘ bs f g) hunk ./MultiComposition.agda 77 - { _→_ = \c -> as → bs → c + { _⟶_ = \c -> as ⟶ bs ⟶ c hunk ./MultiComposition.agda 81 - ≡⟨ ≡-cong (map as) (map-id bs a) ⟩ + ≡⟨ cong (map as) (map-id bs a) ⟩ hunk ./MultiComposition.agda 83 - ≡⟨ map-id as (bs → a) ⟩ + ≡⟨ map-id as (bs ⟶ a) ⟩ hunk ./MultiComposition.agda 88 - ≡⟨ ≡-cong (map as) (map-∘ bs f g) ⟩ + ≡⟨ cong (map as) (map-∘ bs f g) ⟩ hunk ./MultiComposition.agda 111 - (a -> b) -> (ts : TypeList) -> ts → a -> ts → b + (a -> b) -> (ts : TypeList) -> ts ⟶ a -> ts ⟶ b hunk ./MultiComposition.agda 118 - {g₁ g₂ : ts → a} -> g₁ ≡ g₂ -> + {g₁ g₂ : ts ⟶ a} -> g₁ ≡ g₂ -> hunk ./MultiComposition.agda 120 -eqf ⟪ ts ⟫-cong eqg = ≡-cong₂ (map ts) eqf eqg +eqf ⟪ ts ⟫-cong eqg = cong₂ (map ts) eqf eqg hunk ./MultiComposition.agda 125 - (f : a -> b) (g : (t ▻ ts₂) → a) (h : ts₁ → t) -> + (f : a -> b) (g : (t ▻ ts₂) ⟶ a) (h : ts₁ ⟶ t) -> hunk ./MultiComposition.agda 129 - ≡-cong (\F -> F h) (map-∘ ts₁ (map ts₂ f) g) + cong (\F -> F h) (map-∘ ts₁ (map ts₂ f) g) hunk ./MultiComposition.agda 136 -shift : forall {A B} n -> A ^ suc n → B ≡₁ A ^ n → (A -> B) -shift zero = ≡₁-refl -shift {A = A} (suc n) = ≡₁-cong (\t -> A -> t) (shift n) +shift : forall {A B} n -> A ^ suc n ⟶ B ≡₁ A ^ n ⟶ (A -> B) +shift zero = PropEq₁.refl +shift {A = A} (suc n) = PropEq₁.cong (\t -> A -> t) (shift n) hunk ./MultiComposition.agda 141 - (C -> A ^ suc n → B) ≡₁ (C -> A ^ n → (A -> B)) -shift' {C = C} n = ≡₁-cong (\t -> C -> t) (shift n) + (C -> A ^ suc n ⟶ B) ≡₁ (C -> A ^ n ⟶ (A -> B)) +shift' {C = C} n = PropEq₁.cong (\t -> C -> t) (shift n) hunk ./MultiComposition.agda 144 -merge : forall {A B} m n -> A ^ m → A ^ n → B ≡₁ A ^ (m + n) → B -merge zero n = ≡₁-refl -merge {A = A} (suc m) n = ≡₁-cong (\t -> A -> t) (merge m n) +merge : forall {A B} m n -> A ^ m ⟶ A ^ n ⟶ B ≡₁ A ^ (m + n) ⟶ B +merge zero n = PropEq₁.refl +merge {A = A} (suc m) n = PropEq₁.cong (\t -> A -> t) (merge m n) hunk ./MultiComposition.agda 148 -swap : forall {A B} m n -> A ^ (m + n) → B ≡₁ A ^ (n + m) → B -swap {A} {B} m n = ≡₀₁-cong (\i -> A ^ i → B) (+-comm m n) - where open IsCommutativeSemiring _ Nat.isCommutativeSemiring +swap : forall {A B} m n -> A ^ (m + n) ⟶ B ≡₁ A ^ (n + m) ⟶ B +swap {A} {B} m n = PropEq₁.cong₀₁ (\i -> A ^ i ⟶ B) (CS.+-comm m n) hunk ./MultiComposition.agda 153 -subst-commutes : forall {a b : Set1} x₁ x₂ y₁ y₂ - (F : a -> b -> Set) - (f : (x : a) -> F x y₁ -> F x y₂) - (g : F x₁ y₁) - (eq₁ : F x₁ y₁ ≡₁ F x₂ y₁) - (eq₂ : F x₁ y₂ ≡₁ F x₂ y₂) -> - f x₂ (≡₁-subst eq₁ g) ≡ ≡₁-subst eq₂ (f x₁ g) -subst-commutes ._ _ _ _ _ _ _ ≡₁-refl ≡₁-refl = ≡-refl +subst-commutes : {A B C : Set} + (f : A → B) (x : A) + (eq₂ : B ≡₁ C) + (eq₁ : (A → B) ≡₁ (A → C)) → + subst₁ eq₁ f x ≡ subst₁ eq₂ (f x) +subst-commutes f x refl refl = refl hunk ./MultiComposition.agda 169 - (eq₀ : b ≡₁ a ^ m → k) - (eq₁ : ana ≡₁ a ^ n → k) - (eq₂ : a ^ n → b ≡₁ anb) - (eq₃ : anb ≡₁ a ^ (m + n) → k) - (eq₄ : a ^ (m + n) → c ≡₁ amnc) - (eq₅ : (k -> b) ≡₁ (k -> a ^ m → k)) - (eq₆ : ana ≡₁ a ^ n → k) - (eq₇ : a ^ n → a ^ m → c ≡₁ amnc) -> - ≡₁-subst eq₄ (f ⟪ a ^ (m + n) ⟫ - ≡₁-subst eq₃ (≡₁-subst eq₂ - (g ⟪ a ^ n ⟫ ≡₁-subst eq₁ h))) ≡ - ≡₁-subst eq₇ ((f ⟪ k ▻ a ^ m ⟫ ≡₁-subst eq₅ g) - ⟪ a ^ n ⟫ ≡₁-subst eq₆ h) + (eq₀ : b ≡₁ a ^ m ⟶ k) + (eq₁ : ana ≡₁ a ^ n ⟶ k) + (eq₂ : a ^ n ⟶ b ≡₁ anb) + (eq₃ : anb ≡₁ a ^ (m + n) ⟶ k) + (eq₄ : a ^ (m + n) ⟶ c ≡₁ amnc) + (eq₅ : (k -> b) ≡₁ (k -> a ^ m ⟶ k)) + (eq₆ : ana ≡₁ a ^ n ⟶ k) + (eq₇ : a ^ n ⟶ a ^ m ⟶ c ≡₁ amnc) -> + subst₁ eq₄ (f ⟪ a ^ (m + n) ⟫ + subst₁ eq₃ (subst₁ eq₂ + (g ⟪ a ^ n ⟫ subst₁ eq₁ h))) ≡ + subst₁ eq₇ ((f ⟪ k ▻ a ^ m ⟫ subst₁ eq₅ g) + ⟪ a ^ n ⟫ subst₁ eq₆ h) hunk ./MultiComposition.agda 183 - ≡₁-refl ≡₁-refl ≡₁-refl eq₃ ≡₁-refl ≡₁-refl ≡₁-refl eq₇ = + refl refl refl eq₃ refl refl refl eq₇ = hunk ./MultiComposition.agda 185 - f ⟪ a ^ (m + n) ⟫ ≡₁-subst eq₃ (g ⟪ a ^ n ⟫ h) - ≡⟨ subst-commutes (a ^ n ▻▻ a ^ m) (a ^ (m + n)) _ _ - _→_ (_⟪_⟫_ f) (g ⟪ a ^ n ⟫ h) eq₃ eq₇ ⟩ - ≡₁-subst eq₇ (f ⟪ a ^ n ▻▻ a ^ m ⟫ (g ⟪ a ^ n ⟫ h)) - ≡⟨ ≡-cong (≡₁-subst eq₇) - (≡-sym $ right-assoc (a ^ n) (a ^ m) f g h) ⟩ - ≡₁-subst eq₇ ((f ⟪ k ▻ a ^ m ⟫ g) ⟪ a ^ n ⟫ h) + f ⟪ a ^ (m + n) ⟫ subst₁ eq₃ (g ⟪ a ^ n ⟫ h) + ≡⟨ lem₁ m n f (g ⟪ a ^ n ⟫ h) eq₃ eq₇ ⟩ + subst₁ eq₇ (f ⟪ a ^ n ▻▻ a ^ m ⟫ (g ⟪ a ^ n ⟫ h)) + ≡⟨ cong (subst₁ eq₇) (sym $ right-assoc (a ^ n) (a ^ m) f g h) ⟩ + subst₁ eq₇ ((f ⟪ k ▻ a ^ m ⟫ g) ⟪ a ^ n ⟫ h) hunk ./MultiComposition.agda 191 + where + lem₂ : ∀ {A B C} m n + (f : B → C) (g : A ^ n ⟶ A ^ m ⟶ B) + (eq₁ : A ^ n ⟶ A ^ m ⟶ B ≡₁ A ^ (n + m) ⟶ B) + (eq₂ : A ^ n ⟶ A ^ m ⟶ C ≡₁ A ^ (n + m) ⟶ C) → + f ⟪ A ^ (n + m) ⟫ subst₁ eq₁ g ≡ + subst₁ eq₂ (map (A ^ m) f ⟪ A ^ n ⟫ g) + lem₂ m zero f g refl refl = refl + lem₂ {A} m (suc n) f g eq₁ eq₂ = ext (λ x → begin + map (A ^ (n + m)) f (subst₁ eq₁ g x) + ≡⟨ cong (map (A ^ (n + m)) f) + (subst-commutes g x (merge n m) eq₁) ⟩ + map (A ^ (n + m)) f (subst₁ (merge n m) (g x)) + ≡⟨ lem₂ m n f (g x) (merge n m) (merge n m) ⟩ + subst₁ (merge n m) (map (A ^ n) (map (A ^ m) f) (g x)) + ≡⟨ sym (subst-commutes (map (A ^ n) (map (A ^ m) f) ∘ g) x + (merge n m) eq₂) ⟩ + subst₁ eq₂ (map (A ^ n) (map (A ^ m) f) ∘ g) x + ∎) + + lem₁ : ∀ {A B C} m n (f : B → C) (g : A ^ n ⟶ A ^ m ⟶ B) + (eq₁ : A ^ n ⟶ A ^ m ⟶ B ≡₁ A ^ (m + n) ⟶ B) + (eq₂ : A ^ n ⟶ A ^ m ⟶ C ≡₁ A ^ (m + n) ⟶ C) → + f ⟪ A ^ (m + n) ⟫ subst₁ eq₁ g ≡ + subst₁ eq₂ (map (A ^ m) f ⟪ A ^ n ⟫ g) + lem₁ m n f g eq₁ eq₂ with m + n | eq₁ | eq₂ | CS.+-comm m n + lem₁ m n f g eq₁ eq₂ | .(n + m) | eq₁′ | eq₂′ | refl = + lem₂ m n f g eq₁′ eq₂′ hunk ./MultiComposition.agda 227 - (k -> c) -> (k -> v ^ suc n → c) -> (k -> v ^ n → c) + (k -> c) -> (k -> v ^ suc n ⟶ c) -> (k -> v ^ n ⟶ c) hunk ./MultiComposition.agda 231 - cast = ≡₁-subst (shift' n) + cast = subst₁ (shift' n) hunk ./MultiComposition.agda 234 - ((v -> c) -> v ^ m → c) -> v ^ suc n → c -> v ^ (m + n) → c + ((v -> c) -> v ^ m ⟶ c) -> v ^ suc n ⟶ c -> v ^ (m + n) ⟶ c hunk ./MultiComposition.agda 237 - cast₁ = ≡₁-subst (shift n) - cast₂ = ≡₁-subst (≡₁-trans (merge n m) (swap n m)) + cast₁ = subst₁ (shift n) + cast₂ = subst₁ (PropEq₁.trans (merge n m) (swap n m)) hunk ./MultiComposition.agda 248 - (≡₁-trans (merge n (suc m)) (swap n (suc m))) + (PropEq₁.trans (merge n (suc m)) (swap n (suc m))) hunk ./MultiComposition.agda 250 - (≡₁-trans (merge (m + n) 0) (swap (m + n) 0)) + (PropEq₁.trans (merge (m + n) 0) (swap (m + n) 0)) hunk ./MultiComposition.agda 253 - (≡₁-trans (merge n m) (swap n m)) + (PropEq₁.trans (merge n m) (swap n m)) hunk ./NotStructurallyRecursive.agda 42 - eval (val n) c (suc s) eq = exec c n s (≡-cong pred eq) + eval (val n) c (suc s) eq = exec c n s (cong pred eq) hunk ./NotStructurallyRecursive.agda 50 - exec (ADD m c₁) n (suc s) eq = exec c₁ (m + n) s (≡-cong pred eq) + exec (ADD m c₁) n (suc s) eq = exec c₁ (m + n) s (cong pred eq) hunk ./NotStructurallyRecursive.agda 56 -run e = eval e STOP _ ≡-refl +run e = eval e STOP _ refl hunk ./NotStructurallyRecursive/Lemmas.agda 11 -open import Data.Fin using (#_) -open import Data.Vec hunk ./NotStructurallyRecursive/Lemmas.agda 14 -lemma₁ n₁ n₂ n₃ ≡-refl = - prove (n₁ ∷ n₂ ∷ n₃ ∷ []) - (con 2 :+ N₁ :+ N₂ :+ N₃) - (N₁ :+ (con 2 :+ N₂ :+ N₃)) - ≡-refl - where N₁ = var (# 0); N₂ = var (# 1); N₃ = var (# 2) +lemma₁ n₁ n₂ n₃ refl = + solve 3 (λ n₁ n₂ n₃ → + con 2 :+ n₁ :+ n₂ :+ n₃ := n₁ :+ (con 2 :+ n₂ :+ n₃)) + refl n₁ n₂ n₃ hunk ./NotStructurallyRecursive/Lemmas.agda 21 -lemma₂ n₁ n₂ ≡-refl = - prove (n₁ ∷ n₂ ∷ []) - (con 1 :+ (N₁ :+ N₂)) - (N₁ :+ (con 1 :+ N₂)) - ≡-refl - where N₁ = var (# 0); N₂ = var (# 1) +lemma₂ n₁ n₂ refl = + solve 2 (λ n₁ n₂ → con 1 :+ (n₁ :+ n₂) := n₁ :+ (con 1 :+ n₂)) + refl n₁ n₂ hunk ./Wand.agda 10 - (≡-ext : forall {a b : Set} {f g : a -> b} -> - (forall x -> f x ≡ g x) -> f ≡ g) + (ext : forall {a b : Set} {f g : a -> b} -> + (forall x -> f x ≡ g x) -> f ≡ g) hunk ./Wand.agda 17 -open MC ≡-ext -open TypeList using (_→_) +open MC ext +open TypeList using (_⟶_) hunk ./Wand.agda 90 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 95 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 97 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 99 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 102 - (proof (E'P e₂) ⟪ K ▻ V ▻ ε ⟫-cong ≡-refl) ⟩ + (proof (E'P e₂) ⟪ K ▻ V ▻ ε ⟫-cong refl) ⟩ hunk ./Wand.agda 104 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 121 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 123 - ≡⟨ proof (E'P e) ⟪ ε ⟫-cong ≡-refl ⟩ + ≡⟨ proof (E'P e) ⟪ ε ⟫-cong refl ⟩ hunk ./Wand.agda 135 - Exp' (a -> b) -> Exp' (ts → a) -> Exp' (ts → b) + Exp' (a -> b) -> Exp' (ts ⟶ a) -> Exp' (ts ⟶ b) hunk ./Wand.agda 158 - correct (id I) = ≡-refl + correct (id I) = refl hunk ./Wand.agda 160 - ≡-ext (\κ -> ≡-cong₂ _$_ - (correct e₁) - (≡-ext \v₁ -> ≡-cong (\e -> e (Step₁.add κ v₁)) - (correct e₂))) + ext (\κ -> cong₂ _$_ + (correct e₁) + (ext \v₁ -> cong (\e -> e (Step₁.add κ v₁)) + (correct e₂))) hunk ./Wand.agda 200 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 209 - ≡⟨ ≡-ext (\κ -> ≡-cong₂ _$_ + ≡⟨ ext (\κ -> cong₂ _$_ hunk ./Wand.agda 211 - (≡-ext \v₁ -> ≡-cong (\e -> e (Step₁.add κ v₁)) - (proof₁ (comp'P e₂)))) ⟩ + (ext \v₁ -> cong (\e -> e (Step₁.add κ v₁)) + (proof₁ (comp'P e₂)))) ⟩ hunk ./Wand.agda 236 - B : forall {a b} ts {f : a -> b} {g : ts → a} -> + B : forall {a b} ts {f : a -> b} {g : ts ⟶ a} -> hunk ./Wand.agda 263 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 318 - data Exp' : (n : ℕ) -> (K -> V ^ n → C) -> Set where + data Exp' : (n : ℕ) -> (K -> V ^ n ⟶ C) -> Set where hunk ./Wand.agda 351 - ≡⟨ ≡-refl ⟩ + ≡⟨ refl ⟩ hunk ./Wand.agda 362 - data Command : (n : ℕ) -> (K -> V ^ n → C) -> Set where + data Command : (n : ℕ) -> (K -> V ^ n ⟶ C) -> Set where hunk ./Wand.agda 368 - Cont : (m : ℕ) -> (K -> V ^ m → C) -> Set + Cont : (m : ℕ) -> (K -> V ^ m ⟶ C) -> Set hunk ./Wand.agda 372 - data LinearExp : (n : ℕ) -> V ^ n → C -> Set where + data LinearExp : (n : ℕ) -> V ^ n ⟶ C -> Set where hunk ./Wand.agda 384 - cast = ≡-subst (LinearExp (m + n)) (rot-lemma m n f g h) + cast = subst (LinearExp (m + n)) (rot-lemma m n f g h) hunk ./Wand.agda 407 - ⟦_⟧' : forall {a n} -> V ^ n → a -> Stack n -> a + ⟦_⟧' : forall {a n} -> V ^ n ⟶ a -> Stack n -> a hunk ./Wand.agda 411 - ⟦_⟧ : forall {a n} -> V ^ n → a -> Stack n -> a + ⟦_⟧ : forall {a n} -> V ^ n ⟶ a -> Stack n -> a hunk ./Wand.agda 469 - ≡⟨ ≡-cong (\f -> f σ) (proof (Step₁.P'P e)) ⟩ + ≡⟨ cong (\f -> f σ) (proof (Step₁.P'P e)) ⟩ hunk ./Wand2.agda 31 -infix 50 λ_ -infixr 30 _→_ +infix 50 ƛ_ +infixr 30 _⟶_ hunk ./Wand2.agda 37 - _→_ : List Ty -> Ty -> Ty + _⟶_ : List Ty -> Ty -> Ty hunk ./Wand2.agda 45 - λ_ : forall {Γ Γ⁺ τ} -> Γ ▻▻ Γ⁺ ⊢ τ -> Γ ⊢ Γ⁺ → τ - _·_ : forall {Γ Γ⁺ τ} -> Γ ⊢ Γ⁺ → τ -> Args Γ Γ⁺ -> Γ ⊢ τ + ƛ_ : forall {Γ Γ⁺ τ} -> Γ ▻▻ Γ⁺ ⊢ τ -> Γ ⊢ Γ⁺ ⟶ τ + _·_ : forall {Γ Γ⁺ τ} -> Γ ⊢ Γ⁺ ⟶ τ -> Args Γ Γ⁺ -> Γ ⊢ τ hunk ./Wand2.agda 62 - fun : ε ⊢ Types → base 0# - fun = λ var (vs vz) + fun : ε ⊢ Types ⟶ base 0# + fun = ƛ var (vs vz) hunk ./Wand2.agda 66 - args = ε ▻ ↦ x ▻ ↦ y + args = ε {NonEmpty _} ▻ ↦ x ▻ ↦ y hunk ./Wand2.agda 88 -⟦ Γ⁺ → τ ⟧⋆ = Env ⟦_⟧⋆ Γ⁺ -> Cont ⟦ τ ⟧⋆ +⟦ Γ⁺ ⟶ τ ⟧⋆ = Env ⟦_⟧⋆ Γ⁺ -> Cont ⟦ τ ⟧⋆ hunk ./Wand2.agda 90 -module Alternative where - - -- The function above is terminating, since ⟦_⟧⋆ is only applied to - -- the elements of Γ⁺. We could make this explicit by defining a new - -- type here instead of using All, but I want to use Data.Star for - -- all sequences. Note that defining a new type would imply using a - -- form of induction-recursion, by the way: - - mutual - - data SemArgs : Ctxt -> Set where - ∅ : SemArgs ε - _▷_ : forall {Γ σ} -> SemArgs Γ -> ⟦ σ ⟧⋆' -> SemArgs (Γ ▻ σ) - - ⟦_⟧⋆' : Ty -> Set - ⟦ base n ⟧⋆' = Base n - ⟦ Γ⁺ → τ ⟧⋆' = SemArgs Γ⁺ -> Cont ⟦ τ ⟧⋆' +-- The function above is terminating, since ⟦_⟧⋆ is only applied to +-- the elements of Γ⁺. hunk ./Wand2.agda 106 - ⟦ var x ⟧ ρ k = k (Env-lookup x ρ) - ⟦ λ t ⟧ ρ k = k (\vs k' -> ⟦ t ⟧ (ρ ▻▻▻ vs) k') + ⟦ var x ⟧ ρ k = k (lookup x ρ) + ⟦ ƛ t ⟧ ρ k = k (\vs k' -> ⟦ t ⟧ (ρ ▻▻▻ vs) k') hunk ./Wand2.agda 115 - Γ ⊢ Γ⁺ → τ -> Env ⟦_⟧⋆ Δ⁺ -> + Γ ⊢ Γ⁺ ⟶ τ -> Env ⟦_⟧⋆ Δ⁺ -> hunk ./Wand2.agda 138 - *fetch x = \ρ k -> k (Env-lookup x ρ) + *fetch x = \ρ k -> k (lookup x ρ) hunk ./Wand2.agda 140 - *close : forall {Γ Γ⁺ τ} -> Dom (Γ ▻▻ Γ⁺) τ -> Dom Γ (Γ⁺ → τ) + *close : forall {Γ Γ⁺ τ} -> Dom (Γ ▻▻ Γ⁺) τ -> Dom Γ (Γ⁺ ⟶ τ) hunk ./Wand2.agda 153 - *ev-fn : forall {Γ Γ⁺ τ} -> Dom Γ (Γ⁺ → τ) -> Dom' Γ⁺ Γ τ + *ev-fn : forall {Γ Γ⁺ τ} -> Dom Γ (Γ⁺ ⟶ τ) -> Dom' Γ⁺ Γ τ hunk ./Wand2.agda 159 - *ap : forall {Γ Γ⁺ τ} -> Dom' (Γ⁺ ▻ Γ⁺ → τ) Γ τ + *ap : forall {Γ Γ⁺ τ} -> Dom' (Γ⁺ ▻ Γ⁺ ⟶ τ) Γ τ hunk ./Wand2.agda 164 - prop : forall {Γ Γ⁺ τ} (f : Dom Γ (Γ⁺ → τ)) (ρ' : Env ⟦_⟧⋆ Γ⁺) -> + prop : forall {Γ Γ⁺ τ} (f : Dom Γ (Γ⁺ ⟶ τ)) (ρ' : Env ⟦_⟧⋆ Γ⁺) -> hunk ./Wand2.agda 166 - prop f ρ' = ≡-refl + prop f ρ' = refl hunk ./Wand2.agda 178 - Code (Γ ▻▻ Γ⁺) τ -> Code Γ (Γ⁺ → τ) + Code (Γ ▻▻ Γ⁺) τ -> Code Γ (Γ⁺ ⟶ τ) hunk ./Wand2.agda 184 - *ap : forall {Γ Γ⁺ τ} -> Code' (Γ⁺ ▻ Γ⁺ → τ) Γ τ + *ap : forall {Γ Γ⁺ τ} -> Code' (Γ⁺ ▻ Γ⁺ ⟶ τ) Γ τ hunk ./Wand2.agda 193 - comp (λ t) = *close (comp t) + comp (ƛ t) = *close (comp t) hunk ./Wand2.agda 197 - Γ ⊢ Γ⁺ → τ -> + Γ ⊢ Γ⁺ ⟶ τ ->