From e60c7efacf09a9c546a837bad1060fee79f3251d Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Fri, 9 Feb 2024 16:44:09 +0530
Subject: [PATCH] [coq] improve string notation example

---
 coq/string_notation.v | 41 +++++++++++++++++++++++++++++++----------
 1 file changed, 31 insertions(+), 10 deletions(-)

diff --git a/coq/string_notation.v b/coq/string_notation.v
index 18d6c47..159e90b 100644
--- a/coq/string_notation.v
+++ b/coq/string_notation.v
@@ -30,25 +30,46 @@ Fixpoint blist_parse (b: list Byte.byte): blist :=
       | _ => blist_parse bs
       end
   end.
-Fixpoint blist_print (b: blist): list Byte.byte :=
-  match b with
+(* ctr is a counter to leave a space after each 4-tuple *)
+Fixpoint blist_print_aux (bl: blist) (ctr: nat): list Byte.byte :=
+  match bl with
   | BNil => []
   | BCons b bs =>
-      match b with
-      | false => x30 :: (blist_print bs) 
-      | true => x31 :: (blist_print bs)
+      let nxt := match b with
+                 | false => x30
+                 | 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.
+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.
 Delimit Scope bl_scope with bl.
 String Notation blist blist_parse blist_print: bl_scope.
 
+Compute "0"%bl.
+Compute "00"%bl.
 Compute "000"%bl.
-(* "000"%bl : blist *)
-Compute to_list "010203"%bl.
-(* [false; true; false; false] : list bool *)
-Compute to_list "011101"%bl.
-(* [false; true; true; true; false; true] : list bool *)
+Compute "0000"%bl.
+Compute "00000"%bl.
+Compute "11101101001001001"%bl.
+(* "0001 1101 1010 0100 1001 "%bl : blist *)
+
+(* 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) *)
 
 (**********************************)