[coq] improve string notation example
This commit is contained in:
parent
5e796ce27d
commit
e60c7efacf
|
@ -30,25 +30,46 @@ Fixpoint blist_parse (b: list Byte.byte): blist :=
|
||||||
| _ => blist_parse bs
|
| _ => blist_parse bs
|
||||||
end
|
end
|
||||||
end.
|
end.
|
||||||
Fixpoint blist_print (b: blist): list Byte.byte :=
|
(* ctr is a counter to leave a space after each 4-tuple *)
|
||||||
match b with
|
Fixpoint blist_print_aux (bl: blist) (ctr: nat): list Byte.byte :=
|
||||||
|
match bl with
|
||||||
| BNil => []
|
| BNil => []
|
||||||
| BCons b bs =>
|
| BCons b bs =>
|
||||||
match b with
|
let nxt := match b with
|
||||||
| false => x30 :: (blist_print bs)
|
| false => x30
|
||||||
| true => x31 :: (blist_print bs)
|
| true => x31
|
||||||
|
end in
|
||||||
|
nxt ::
|
||||||
|
match Nat.eqb ctr 3 with
|
||||||
|
| true => x20 :: (blist_print_aux bs 0)
|
||||||
|
| false => (blist_print_aux bs (S ctr))
|
||||||
end
|
end
|
||||||
end.
|
end.
|
||||||
|
Fixpoint blist_print (bl: blist): list Byte.byte :=
|
||||||
|
let rem := 4 - (Nat.modulo (length bl) 4) in
|
||||||
|
let prefix := List.repeat false rem in
|
||||||
|
let lst := to_list bl in
|
||||||
|
let newbl := of_list (prefix ++ lst) in
|
||||||
|
blist_print_aux newbl 0.
|
||||||
Declare Scope bl_scope.
|
Declare Scope bl_scope.
|
||||||
Delimit Scope bl_scope with bl.
|
Delimit Scope bl_scope with bl.
|
||||||
String Notation blist blist_parse blist_print: bl_scope.
|
String Notation blist blist_parse blist_print: bl_scope.
|
||||||
|
|
||||||
|
Compute "0"%bl.
|
||||||
|
Compute "00"%bl.
|
||||||
Compute "000"%bl.
|
Compute "000"%bl.
|
||||||
(* "000"%bl : blist *)
|
Compute "0000"%bl.
|
||||||
Compute to_list "010203"%bl.
|
Compute "00000"%bl.
|
||||||
(* [false; true; false; false] : list bool *)
|
Compute "11101101001001001"%bl.
|
||||||
Compute to_list "011101"%bl.
|
(* "0001 1101 1010 0100 1001 "%bl : blist *)
|
||||||
(* [false; true; true; true; false; true] : list bool *)
|
|
||||||
|
(* Before adding 4-tuple padding and space *)
|
||||||
|
(* Compute "000"%bl. *)
|
||||||
|
(* (1* "000"%bl : blist *1) *)
|
||||||
|
(* Compute to_list "010203"%bl. *)
|
||||||
|
(* (1* [false; true; false; false] : list bool *1) *)
|
||||||
|
(* Compute to_list "011101"%bl. *)
|
||||||
|
(* (1* [false; true; true; true; false; true] : list bool *1) *)
|
||||||
|
|
||||||
(**********************************)
|
(**********************************)
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue