[Split up the code into reusable modules.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080205013235] hunk ./HuttonsRazor.agda 10
+open import Vec
+import Stack
+open Stack using (↦)
hunk ./HuttonsRazor.agda 28
-------------------------------------------------------------------------
--- Generalised vectors (the reflexive transitive closures of Norell,
--- McBride and Jansson)
-
-module Vector {a : Set} (T : a -> a -> Set) where
-
-  infixr 5 _∷_
-
-  data Vec : a -> a -> Set where
-    []  : forall {i} -> Vec i i
-    _∷_ : forall {i j k} -> T i j -> Vec j k -> Vec i k
-
-open Vector
-
-infixr 5 _++_
-
-_++_ : forall {a} {T : a -> a -> Set} {i j k} ->
-       Vec T i j -> Vec T j k -> Vec T i k
-[]       ++ ys = ys
-(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
-
-------------------------------------------------------------------------
--- Stacks (vectors containing natural numbers)
-
-data StackT (a : Set) : ℕ -> ℕ -> Set where
-  ↦ : forall {n} -> a -> StackT a (1 + n) n
-
-Stack : ℕ -> Set
-Stack n = Vec (StackT ℕ) n 0
-
hunk ./HuttonsRazor.agda 31
+Stack : ℕ -> Set
+Stack = Stack.Stack ℕ
+
hunk ./HuttonsRazor.agda 80
-assoc : forall {a} {T : a -> a -> Set} {i j k l}
-               (xs : Vec T i j) (ys : Vec T j k) (zs : Vec T k l) ->
-        (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
-assoc []       ys zs = ≡-refl
-assoc (x ∷ xs) ys zs = ≡-cong (_∷_ x) (assoc xs ys zs)
-
addfile ./Stack.agda
hunk ./Stack.agda 1
+------------------------------------------------------------------------
+-- Stacks (vectors)
+
+module Stack (a : Set) where
+
+open import Vec
+open import Data.Nat
+
+data StackT : ℕ -> ℕ -> Set where
+  ↦ : forall {n} -> a -> StackT (1 + n) n
+
+Stack : ℕ -> Set
+Stack n = Vec StackT n 0
addfile ./Vec.agda
move ./Vec.agda ./GVec.agda
move ./Stack.agda ./Vec.agda
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
hunk ./HuttonsRazor.agda 10
+open import GVec
hunk ./HuttonsRazor.agda 12
-import Stack
-open Stack using (↦)
hunk ./HuttonsRazor.agda 31
-Stack = Stack.Stack ℕ
+Stack = Vec ℕ
hunk ./HuttonsRazor.agda 38
-Code = Vec Op
+Code = GVec Op
hunk ./Vec.agda 2
--- Stacks (vectors)
+-- Ordinary vectors
hunk ./Vec.agda 4
-module Stack (a : Set) where
+module Vec (a : Set) where
hunk ./Vec.agda 6
-open import Vec
+open import GVec
hunk ./Vec.agda 9
-data StackT : ℕ -> ℕ -> Set where
-  ↦ : forall {n} -> a -> StackT (1 + n) n
+data VecT : ℕ -> ℕ -> Set where
+  ↦ : forall {n} -> a -> VecT (1 + n) n
hunk ./Vec.agda 12
-Stack : ℕ -> Set
-Stack n = Vec StackT n 0
+Vec : ℕ -> Set
+Vec n = GVec VecT n 0