include "vect.idr";

vadd : Vect Int n -> Vect Int n -> Vect Int n;
vadd VNil VNil = VNil;
vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys;

vfilter : (a -> Bool) -> Vect a n -> (p | Vect a p);
vfilter f VNil = << VNil >>;
vfilter f (x :: xs) with (f x, vfilter f xs) {
   | (True, << xs' >>) = << x :: xs' >>;
   | (False, << xs' >>) = << xs' >>;
}

data Half : Nat -> # where
   even : (n:Nat) -> Half (plus n n)
 | odd : (n:Nat) -> Half (S (plus n n));

half : (n:Nat) -> Half n;
half O = even O;
half (S O) = odd O;
half (S (S k)) with half k {
  half (S (S (plus j _)))     | even _ ?= even (S j);  [halfSSe]
  half (S (S (S (plus j _)))) | odd _ ?= odd (S j);    [halfSSo]
}

data Binary : Nat -> # where
   bEnd : Binary O
 | bO : Binary n -> Binary (plus n n)
 | bI : Binary n -> Binary (S (plus n n));

-- 42: least significant first
b42 : Binary (intToNat 42);
b42 = bO (bI (bO (bI (bO (bI bEnd)))));

-- Display the index, for a sanity check.
bToInt : (Binary n) -> Int;
bToInt {n} b = natToInt n;

natToBin : (n:Nat) -> Binary n;
natToBin O = bEnd;
natToBin (S k) with half k {
   natToBin (S (plus j _)) | even _ = bI (natToBin j);
   natToBin (S (S (plus j _))) | odd _ ?= bO (natToBin (S j)); [ntbOdd]
}

-- The version that won't work:

halfF : (n:Nat) -> (Nat & Bool);
halfF O = (O, False);
halfF (S O) = (O, True);
halfF (S (S k)) with halfF k {
  | (j, parity) = (S j, parity);
}

-- We'll never get this to typecheck! But we can at least pretend we will...

natToBinF : (n:Nat) -> Binary n;
natToBinF O = bEnd;
natToBinF (S k) with halfF k {
  | (j, False) ?= bI (natToBinF j);    [fail1]
  | (j, True) ?= bO (natToBinF (S j)); [fail2]
}

--- Appendix: proofs

{-
halfSSe proof {
	%intro;
	%use value;
	%rewrite plus_nSm {n=j} {m=j};
	%refl;
	%qed;
};

halfSSo proof {
	%intro;
	%use value;
	%rewrite plus_nSm {n=j} {m=j};
	%refl;
	%qed;
};
-}

ntbOdd proof {
	%intro;
	%use value;
	%rewrite plus_nSm {n=j} {m=j};
	%refl;
	%qed;
};

{- Suspend disbelief for natToBinF above... this will make it run, but
   we'll never actually be able to prove these! 'believe' is
   implemented using a function called '__Suspend_Disbelief' which
   will give a warning when you try to compile it. 
-}

fail1 proof {
	%intro;
	%believe value;
	%qed;
};
fail2 proof {
	%intro;
	%believe value;
	%qed;
};