[Started using Data.Star from the standard library. Nils Anders Danielsson **20080312003502] hunk ./Exceptions.agda 27 -open import GVec -open import Vec hunk ./GVec.agda 1 ------------------------------------------------------------------------- --- Generalised vectors (the reflexive transitive closures of Norell, --- McBride and Jansson) - -module GVec where - -open import Logic -open import Relation.Binary.PropositionalEquality - -infixr 5 _∷_ - -data GVec {a : Set} (T : a -> a -> Set) : a -> a -> Set where - [] : forall {i} -> GVec T i i - _∷_ : forall {i j k} -> T i j -> GVec T j k -> GVec T i k - -private - module Dummy {a : Set} {T : a -> a -> Set} where - - infixr 5 _++_ - - _++_ : forall {i j k} -> GVec T i j -> GVec T j k -> GVec T i k - [] ++ ys = ys - (x ∷ xs) ++ ys = x ∷ (xs ++ ys) - - assoc : forall {i j k l} - (xs : GVec T i j) (ys : GVec T j k) - (zs : GVec T k l) -> - (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) - assoc [] ys zs = ≡-refl - assoc (x ∷ xs) ys zs = ≡-cong (_∷_ x) (assoc xs ys zs) - -open Dummy public rmfile ./GVec.agda hunk ./HuttonsRazor.agda 16 -open import Data.Nat -open import GVec -open import Vec +open import Data.Star +open import Data.Star.Nat +open import Data.Star.Vec hunk ./HuttonsRazor.agda 46 - push : forall {n} -> ℕ -> Op n (1 + n) - add : forall {n} -> Op (2 + n) (1 + n) + push : forall {n} -> ℕ -> Op n (1# + n) + add : forall {n} -> Op (2# + n) (1# + n) hunk ./HuttonsRazor.agda 50 - Code = GVec Op + Code = Star Op hunk ./HuttonsRazor.agda 53 - ⟪ [] ⟫ s = s - ⟪ push n ∷ ops ⟫ s = ⟪ ops ⟫ (↦ n ∷ s) - ⟪ add ∷ ops ⟫ (↦ m ∷ ↦ n ∷ s) = ⟪ ops ⟫ (↦ (n + m) ∷ s) + ⟪ ε ⟫ s = s + ⟪ push n ◅ ops ⟫ s = ⟪ ops ⟫ (↦ n ◅ s) + ⟪ add ◅ ops ⟫ (↦ m ◅ ↦ n ◅ s) = ⟪ ops ⟫ (↦ (n + m) ◅ s) hunk ./HuttonsRazor.agda 60 - comp : forall {n} -> (e : Expr) -> Code n (1 + n) - comp (val n) = push n ∷ [] - comp (e₁ ⊕ e₂) = comp e₁ ++ comp e₂ ++ add ∷ [] + comp : forall {n} -> (e : Expr) -> Code n (1# + n) + comp (val n) = push n ◅ ε + comp (e₁ ⊕ e₂) = comp e₁ ◅▻ comp e₂ ◅▻ add ◅ ε hunk ./HuttonsRazor.agda 69 - ⟪ c₁ ++ c₂ ⟫ s ≡ ⟪ c₂ ⟫ (⟪ c₁ ⟫ s) - distrib s [] c₂ = ≡-refl - distrib s (push n ∷ c₁) c₂ = distrib (↦ n ∷ s) c₁ c₂ - distrib (↦ m ∷ ↦ n ∷ s) (add ∷ c₁) c₂ = - distrib (↦ (n + m) ∷ s) c₁ c₂ + ⟪ c₁ ◅▻ c₂ ⟫ s ≡ ⟪ c₂ ⟫ (⟪ c₁ ⟫ s) + distrib s ε c₂ = ≡-refl + distrib s (push n ◅ c₁) c₂ = distrib (↦ n ◅ s) c₁ c₂ + distrib (↦ m ◅ ↦ n ◅ s) (add ◅ c₁) c₂ = + distrib (↦ (n + m) ◅ s) c₁ c₂ hunk ./HuttonsRazor.agda 75 - thm1 : forall {n} (s : Stack n) e -> ⟪ comp e ⟫ s ≡ ↦ ⟦ e ⟧ ∷ s + thm1 : forall {n} (s : Stack n) e -> ⟪ comp e ⟫ s ≡ ↦ ⟦ e ⟧ ◅ s hunk ./HuttonsRazor.agda 79 - ≡⟨ distrib s (comp e₁) (comp e₂ ++ add ∷ []) ⟩ - ⟪ comp e₂ ++ add ∷ [] ⟫ (⟪ comp e₁ ⟫ s) - ≡⟨ ≡-cong ⟪ comp e₂ ++ add ∷ [] ⟫ (thm1 s e₁) ⟩ - ⟪ comp e₂ ++ add ∷ [] ⟫ (↦ ⟦ e₁ ⟧ ∷ s) - ≡⟨ distrib (↦ ⟦ e₁ ⟧ ∷ s) (comp e₂) (add ∷ []) ⟩ - ⟪ add ∷ [] ⟫ (⟪ comp e₂ ⟫ (↦ ⟦ e₁ ⟧ ∷ s)) - ≡⟨ ≡-cong ⟪ add ∷ [] ⟫ (thm1 (↦ ⟦ e₁ ⟧ ∷ s) e₂) ⟩ - ↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s + ≡⟨ distrib s (comp e₁) (comp e₂ ◅▻ add ◅ ε) ⟩ + ⟪ comp e₂ ◅▻ add ◅ ε ⟫ (⟪ comp e₁ ⟫ s) + ≡⟨ ≡-cong ⟪ comp e₂ ◅▻ add ◅ ε ⟫ (thm1 s e₁) ⟩ + ⟪ comp e₂ ◅▻ add ◅ ε ⟫ (↦ ⟦ e₁ ⟧ ◅ s) + ≡⟨ distrib (↦ ⟦ e₁ ⟧ ◅ s) (comp e₂) (add ◅ ε) ⟩ + ⟪ add ◅ ε ⟫ (⟪ comp e₂ ⟫ (↦ ⟦ e₁ ⟧ ◅ s)) + ≡⟨ ≡-cong ⟪ add ◅ ε ⟫ (thm1 (↦ ⟦ e₁ ⟧ ◅ s) e₂) ⟩ + ↦ ⟦ e₁ ⊕ e₂ ⟧ ◅ s hunk ./HuttonsRazor.agda 90 - -- they don't mention their use of associativity of _++_. + -- they don't mention their use of associativity of _◅▻_. hunk ./HuttonsRazor.agda 92 - thm2 : forall {i j} (s : Stack i) e (ops : Code (1 + i) j) -> - ⟪ comp e ++ ops ⟫ s ≡ ⟪ ops ⟫ (↦ ⟦ e ⟧ ∷ s) + thm2 : forall {i j} (s : Stack i) e (ops : Code (1# + i) j) -> + ⟪ comp e ◅▻ ops ⟫ s ≡ ⟪ ops ⟫ (↦ ⟦ e ⟧ ◅ s) hunk ./HuttonsRazor.agda 96 - ⟪ comp (e₁ ⊕ e₂) ++ ops ⟫ s + ⟪ comp (e₁ ⊕ e₂) ◅▻ ops ⟫ s hunk ./HuttonsRazor.agda 98 - ⟪ (comp e₁ ++ comp e₂ ++ add ∷ []) ++ ops ⟫ s + ⟪ (comp e₁ ◅▻ comp e₂ ◅▻ add ◅ ε) ◅▻ ops ⟫ s hunk ./HuttonsRazor.agda 100 - (assoc (comp e₁) (comp e₂ ++ add ∷ []) ops) ⟩ - ⟪ comp e₁ ++ ((comp e₂ ++ add ∷ []) ++ ops) ⟫ s - ≡⟨ ≡-cong (\s' -> ⟪ comp e₁ ++ s' ⟫ s) - (assoc (comp e₂) (add ∷ []) ops) ⟩ - ⟪ comp e₁ ++ (comp e₂ ++ add ∷ ops) ⟫ s - ≡⟨ thm2 s e₁ (comp e₂ ++ add ∷ ops) ⟩ - ⟪ comp e₂ ++ add ∷ ops ⟫ (↦ ⟦ e₁ ⟧ ∷ s) - ≡⟨ thm2 (↦ ⟦ e₁ ⟧ ∷ s) e₂ (add ∷ ops) ⟩ - ⟪ ops ⟫ (↦ ⟦ e₁ ⊕ e₂ ⟧ ∷ s) + (◅▻-assoc (comp e₁) (comp e₂ ◅▻ add ◅ ε) ops) ⟩ + ⟪ comp e₁ ◅▻ ((comp e₂ ◅▻ add ◅ ε) ◅▻ ops) ⟫ s + ≡⟨ ≡-cong (\s' -> ⟪ comp e₁ ◅▻ s' ⟫ s) + (◅▻-assoc (comp e₂) (add ◅ ε) ops) ⟩ + ⟪ comp e₁ ◅▻ (comp e₂ ◅▻ add ◅ ops) ⟫ s + ≡⟨ thm2 s e₁ (comp e₂ ◅▻ add ◅ ops) ⟩ + ⟪ comp e₂ ◅▻ add ◅ ops ⟫ (↦ ⟦ e₁ ⟧ ◅ s) + ≡⟨ thm2 (↦ ⟦ e₁ ⟧ ◅ s) e₂ (add ◅ ops) ⟩ + ⟪ ops ⟫ (↦ ⟦ e₁ ⊕ e₂ ⟧ ◅ s) hunk ./Vec.agda 1 ------------------------------------------------------------------------- --- Ordinary vectors - -module Vec (a : Set) where - -open import GVec -open import Data.Nat - -data VecT : ℕ -> ℕ -> Set where - ↦ : forall {n} -> a -> VecT (1 + n) n - -Vec : ℕ -> Set -Vec n = GVec VecT n 0 rmfile ./Vec.agda