[coq] add example with String Notation

coq/string_notation.v

@@ -0,0 +1,74 @@
+Require Import List.
+Import ListNotations.
+Require Import Strings.Byte.
+
+Inductive blist: Type :=
+| BNil
+| BCons: bool -> blist -> blist.
+
+Fixpoint to_list (bl: blist): list bool :=
+  match bl with
+  | BNil => nil
+  | BCons b bs => b :: to_list bs
+  end.
+
+Fixpoint of_list (l: list bool): blist :=
+  match l with
+  | nil => BNil
+  | cons b bs => BCons b (of_list bs)
+  end.
+
+Definition length (bl: blist): nat := List.length (to_list bl).
+
+Fixpoint blist_parse (b: list Byte.byte): blist :=
+  match b with
+  | nil => BNil
+  | cons b bs =>
+      match b with
+      | x30 => BCons false (blist_parse bs)
+      | x31 => BCons true (blist_parse bs)
+      | _ => blist_parse bs
+      end
+  end.
+Fixpoint blist_print (b: blist): list Byte.byte :=
+  match b with
+  | BNil => []
+  | BCons b bs =>
+      match b with
+      | false => x30 :: (blist_print bs) 
+      | true => x31 :: (blist_print bs)
+      end
+  end.
+Declare Scope bl_scope.
+Delimit Scope bl_scope with bl.
+String Notation blist blist_parse blist_print: bl_scope.
+
+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 *)
+
+(**********************************)
+
+Declare Scope bv_scope.
+Delimit Scope bv_scope with bv.
+
+Definition byte_parse (b: Byte.byte): bool :=
+  match b with
+  | x31 => true
+  | _ => false
+  end.
+Definition byte_print (b: bool): Byte.byte :=
+  match b with
+  | false => x30
+  | true => x31
+  end.
+String Notation bool byte_parse byte_print: bv_scope.
+
+Compute [false; true].
+(* ["0"%bv; "1"%bv] : list bool *)
+Compute ["0"; "1"]%bv.
+(* ["0"%bv; "1"%bv] : list bool *)
+