Work on examples

Ignore-this: f512bef8ea852f51270895f97b134dfd

darcs-hash:20111020101859-e29d1-306ea1e6844f82160cbcca1697f796fd61586947.gz

Induction.hs

@@ -25,4 +25,38 @@ elimMulPos :: forall a (m n :: Num) . MulPos m n -> (0 <= m * n => a) -> a
 elimMulPos MulPos x = x
 
 lemmaMulPos :: forall a. pi (m n :: Nat) . (0 <= m * n => a) -> a
-lemmaMulPos {m} {n} = elimMulPos (mulPos {m} {n})
+lemmaMulPos {m} {n} = elimMulPos (mulPos {m} {n})
+
+
+
+data Prf :: * -> * where
+  Prf :: forall a. Prf a
+
+prf :: forall a . a -> Prf a
+prf _ = Prf
+
+ind :: forall (f :: Num -> *)(m :: Nat) . Prf (f 0) ->
+           (forall (n :: Nat) . Prf (f n) -> Prf (f (n+1))) ->
+               Prf (f m)
+ind _ _ = Prf
+
+
+data Proxy :: Num -> * where
+  Proxy :: forall (n :: Num) . Proxy n
+
+data ProxyNN :: (Num -> Num) -> * where
+  ProxyNN :: forall (f :: Num -> Num) . ProxyNN f
+
+indy :: forall (f :: Nat -> Nat)(m :: Nat) b . 0 <= f 0 => ProxyNN f ->
+          (forall (x :: Num) a . Proxy x -> (0 <= x => a) -> a) ->
+            (forall (n :: Nat) a . 0 <= f n => (0 <= f (n+1) => a) -> a) ->
+              (0 <= f m => b) -> b
+indy _ lie s e = lie (Proxy :: Proxy (f m)) e
+
+possy :: forall a (m n :: Nat) .
+                     (forall (x :: Num) a . Proxy x -> (0 <= x => a) -> a) ->
+                         (0 <= m * n => a) -> a
+possy lie =
+    let foo :: forall (n :: Nat) a . 0 <= m * n => (0 <= m * (n + 1) => a) -> a
+        foo x = x
+    in indy (ProxyNN :: ProxyNN ((*) m)) lie foo

Process.hs

@@ -11,6 +11,12 @@ data Vec :: Num -> * -> * where
 vhead :: forall a (m :: Num) . 0 < m => Vec m a -> a
 vhead (VCons x xs) = x
 
+rev :: forall a (m :: Nat) . Vec m a -> Vec m a
+rev = let revapp :: forall (n k :: Nat) . Vec n a -> Vec k a -> Vec (n+k) a
+          revapp xs VNil = xs
+          revapp xs (VCons y ys) = revapp (VCons y xs) ys
+      in revapp VNil
+
 data Pro :: Num -> Num -> * -> * where
   Stop  :: forall a . Pro 0 0 a
   Say   :: forall (m n :: Num) a . 0 <= m, 0 <= n =>
@@ -40,13 +46,16 @@ pipe (Ask f)    (Ask g)    = Ask (\ x -> pipe (f x) (Ask g))
 
 always p = Ask (\ zzz -> p)
 
-askB t f = let fi t f True  = t
-               fi t f False = f
-           in Ask (fi t f)
+bool t f True   = t
+bool t f False  = f
+
+askB t f = Ask (bool t f)
 
 wire     = Ask (\ a -> Say a Stop)
-notGate  = askB (Say False Stop) (Say True Stop)
+notGate  = Ask (\ b -> Say (not b) Stop)
 andGate  = askB wire (always (Say False Stop))
+split    = Ask (\ a -> Say a (Say a Stop))
+cross    = Ask (\ a -> Ask (\ b -> Say b (Say a Stop)))
 
 mkGate tt tf ft ff = askB (askB (Say tt Stop) (Say tf Stop))
                           (askB (Say ft Stop) (Say ff Stop))
@@ -70,7 +79,52 @@ bind (Ask f)   g = Ask (\ x -> bind (f x) g)
 
 
 
-v2i :: forall a (n :: Num) . a -> (a -> a) -> (a -> a) -> Vec n Bool -> a
-v2i o s d VNil = o
-v2i o s d (VCons True xs) = s (d (v2i o s d xs))
-v2i o s d (VCons False xs) = d (v2i o s d xs)
+v2i :: forall (n :: Num) . Vec n Bool -> Integer
+v2i VNil = 0
+v2i (VCons True xs) = 1 + (2 * (v2i xs))
+v2i (VCons False xs) = 2 * (v2i xs)
+
+
+odd' :: pi (n :: Nat) . Bool
+odd' {0}    = False
+odd' {n+1}  = not (odd' {n})
+
+half :: forall a. pi (n :: Nat) . (pi (m r :: Nat) . n ~ 2 * m + r, r <= 1 => a) -> a
+half {0}    f = f {0} {0} 
+half {n+1}  f = let
+                  g :: pi (m r :: Nat) . n ~ 2 * m + r, r <= 1 => a
+                  g {m} {0} = f {m} {1}
+                  g {m} {1} = f {m+1} {0}
+                in half {n} g
+
+-- This needs 2^(x + y)  ~>  2^x * 2^y
+
+toBin :: pi (m n :: Nat) . n < 2^m => Vec m Bool
+toBin {0}   {n} = VNil
+toBin {m+1} {n} = half {n} (\ {k} {r} -> VCons (odd' {r}) (toBin {m} {k}))
+
+-- A real implementation of div/mod might be nice
+
+divvy :: forall a. pi (n d :: Nat) . d >= 1 => (pi (m r :: Nat) . n ~ d * m + r, r < d => a) -> a
+divvy {n}    {d} f | {n < d} = f {0} {n}
+divvy {n}    {d} f | {n >= d} =
+                     let g :: pi (m r :: Nat) . n - d ~ d * m + r, r < d => a
+                         g {m} {r} = f {m+1} {r}
+                     in divvy {n-d} {d} g
+
+
+test :: forall (n :: Nat) . pi (m :: Nat) . Pro m n Bool ->
+            (pi (k :: Nat) . k < 2 ^ m => Integer)
+test {m} p {k} = v2i (rev (run p (rev (toBin {m} {k}))))
+
+
+hadd :: Pro 2 2 Bool
+hadd = pipe (sequ split split)
+      (pipe (sequ wire (sequ cross wire))
+            (sequ andGate xorGate))
+
+fadd :: Pro 3 2 Bool
+fadd = pipe (sequ hadd wire)
+      (pipe (sequ wire hadd)
+            (sequ wire orGate))
+