ParsonsChallenge.v

Require Import Unicode.Utf8.
Require Import Arith.Compare_dec.
Require Vectors.Vector.

Set Implicit Arguments.

Fixpoint pow (n : nat) (e : nat) : nat :=
  match e with
  | 0 => 1
  | S e' => n * pow n e'
  end.

Fixpoint natBits (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => if gt_dec (pow 2 (natBits n')) n then natBits n' else S (natBits n')
  end.

Fixpoint bitIncHelper {n} (v : Vector.t bool n) : Vector.t bool n * bool :=
  match v in (Vector.t _ x) with
  | Vector.nil _ => (Vector.nil _, false)
  | Vector.cons _ false 0 _ => (Vector.cons _ true _ (Vector.nil _), false)
  | Vector.cons _ true 0 _ => (Vector.cons _ false _ (Vector.nil _), true)
  | Vector.cons _ false (S n) v => match bitIncHelper v with
                                   | (v', false) => (Vector.cons _ false _ v', false)
                                   | (v', true) => (Vector.cons _ true _ v', false)
                                   end
  | Vector.cons _ true (S n) v => match bitIncHelper v with
                                   | (v', false) => (Vector.cons _ true _ v', false)
                                   | (v', true) => (Vector.cons _ false _ v', true)
                                   end
  end.

Definition bitInc {n} (v : Vector.t bool n) : Vector.t bool n :=
  fst (bitIncHelper v).

Fixpoint zeros (n : nat) : Vector.t bool n :=
  match n with
  | 0 => Vector.nil _
  | S n' => Vector.cons _ false _ (zeros n')
  end.

Definition msbOne (n : nat) : Vector.t bool n :=
  match n with
  | 0 => Vector.nil _
  | S n' => Vector.cons _ true _ (zeros n')
  end.

Fixpoint natToVec (n : nat) : Vector.t bool (natBits n) :=
  match n with
  | 0 => Vector.cons _ false _ (Vector.nil _)
  | S n' => match gt_dec (pow 2 (natBits n')) (S n') as r return Vector.t bool (if r
                                                                           then (natBits n')
                                                                           else (S (natBits n')))
            with
            | left _ => bitInc (natToVec n')
            | right _ => msbOne (S (natBits n'))
            end
  end.

Eval compute in natToVec 4.