91 lines
2.6 KiB
Coq
91 lines
2.6 KiB
Coq
Require Import Vector String Ascii.
|
|
Import VectorNotations.
|
|
|
|
(*
|
|
Fixpoint bv (n:nat): Type :=
|
|
match n with
|
|
| O => unit
|
|
| S n' => (bv n') * bool
|
|
end.
|
|
Check (false, false, false, false, tt).
|
|
Compute bv 2.
|
|
Compute (tt, true, true) : bv 2.
|
|
|
|
Definition charToNibble (c:Ascii.ascii): bv 4 :=
|
|
(match c with
|
|
| "0" => (tt, false, false, false, false)
|
|
| "1" => (tt, true, false, false, false)
|
|
| "2" => (tt, false, true, false, false)
|
|
| "3" => (tt, true, true, false, false)
|
|
| "4" => (tt, false, false, true, false)
|
|
| "5" => (tt, true, false, true, false)
|
|
| "6" => (tt, false, true, true, false)
|
|
| "7" => (tt, true, true, true, false)
|
|
| "8" => (tt, false, false, false, true)
|
|
| "9" => (tt, true, false, false, true)
|
|
| "a" | "A" => (tt, false, true, false, true)
|
|
| "b" | "B" => (tt, true, true, false, true)
|
|
| "c" | "C" => (tt, false, false, true, true)
|
|
| "d" | "D" => (tt, true, false, true, true)
|
|
| "e" | "E" => (tt, false, true, true, true)
|
|
| "f" | "F" => (tt, true, true, true, true)
|
|
| _ => (tt, false, false, false, false)
|
|
end)%char.
|
|
|
|
Fixpoint fromHex (s:string): bv ((String.length s)*4) :=
|
|
match s with
|
|
| String x xs => (fromHex xs) (charToNibble x)
|
|
| EmptyString => tt
|
|
end.
|
|
Compute fromHex "ae".
|
|
*)
|
|
|
|
|
|
|
|
(*****************************************************)
|
|
|
|
Definition bv (n:nat):= Vector.t bool n.
|
|
|
|
Print string.
|
|
Check "c"%char.
|
|
|
|
Definition charToNibble (c:Ascii.ascii): bv 4 :=
|
|
(match c with
|
|
| "0" => [false; false; false; false]
|
|
| "1" => [true; false; false; false]
|
|
| "2" => [false; true; false; false]
|
|
| "3" => [true; true; false; false]
|
|
| "4" => [false; false; true; false]
|
|
| "5" => [true; false; true; false]
|
|
| "6" => [false; true; true; false]
|
|
| "7" => [true; true; true; false]
|
|
| "8" => [false; false; false; true]
|
|
| "9" => [true; false; false; true]
|
|
| "a" | "A" => [false; true; false; true]
|
|
| "b" | "B" => [true; true; false; true]
|
|
| "c" | "C" => [false; false; true; true]
|
|
| "d" | "D" => [true; false; true; true]
|
|
| "e" | "E" => [false; true; true; true]
|
|
| "f" | "F" => [true; true; true; true]
|
|
| _ => [false; false; false; false]
|
|
end)%char.
|
|
|
|
Fixpoint fromHex (s:string): bv ((String.length s)*4) :=
|
|
match s with
|
|
| String x xs => Vector.append (charToNibble x) (fromHex xs)
|
|
| EmptyString => Vector.nil bool
|
|
end.
|
|
Compute fromHex "ae".
|
|
|
|
Fixpoint bvToNat {n:nat} (bv: bv n) (pw: nat): nat :=
|
|
match bv with
|
|
| Vector.nil _ => 0
|
|
| Vector.cons _ x _ xs =>
|
|
match x with
|
|
| true => (Nat.pow 2 pw) + (bvToNat xs) (S pw)
|
|
| _ => bvToNat xs (S pw)
|
|
end
|
|
end.
|
|
Compute fromHex "0ea".
|
|
Compute bvToNat (fromHex "0ea") 0.
|