Merge pull request #1 from majorseitan/master

added new specifiers

Makefile

@@ -6,3 +6,6 @@ test: all
 
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq clean

README.md

@@ -0,0 +1,51 @@
+# cop-printf
+
+Implementation of sprintf for Coq
+
+## format specifiers
+
+Regexp
+
+%(-|+| |#|0)^* (\d+) (s|b|o|d|x|X|c)
+
+Structure
+
+%[flags]       [width]  specifier
+
+## flags
+
+| flags | description                                                                 |
+|-------|-----------------------------------------------------------------------------|
+| '-'   | left justify                                                                |
+| '+'   | precede with a plus sign (only applys to nat)                               |
+| ' '   | space if no sign precedes                                                   |
+| '#'   | with specfier o x X precede with 0 0x 0X for for values different than zero |
+
+
+'0' pad with 0's instead of space
+
+## specifier
+
+| specifier | description            |
+|-----------|------------------------|
+| 's'       | string                 |
+| 'b'       | binary                 |
+| 'o'       | octal                  |
+| 'd'       | decimal                |
+| 'x'       | hexidecimal lower case |
+| 'X'       | hexidecimal upper case |
+| 'c'       | character              |
+
+
+## example
+
+```Coq
+Require Import Coq.Strings.String.
+Require Import Printf.Printf.
+
+Eval compute in (sprintf "%b" 1234).
+```
+
+## resources
+
+reference : http://www.cplusplus.com/reference/cstdio/printf

_CoqProject

@@ -1,3 +1,5 @@
 -Q theories Printf
 
+theories/Flags.v
+theories/Justify.v
 theories/Printf.v

test-suite/TestPrintf.v

@@ -0,0 +1,120 @@
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+Require Import Printf.Printf.
+
+Local Open Scope string_scope.
+
+Example test_hex_1234: (hex_string 1234) = "4d2"%string.
+Proof.
+  unfold hex_string.
+  reflexivity.
+Qed.
+
+Example test_4: (hex_string 4) = "4"%string.
+Proof.
+  unfold hex_string.
+  reflexivity.
+Qed.
+
+Example test_1234_hex_upper: (hex_string_upper 1234) = "4D2"%string.
+Proof.
+  unfold hex_string.
+  reflexivity.
+Qed.
+
+Example test_1234_octal: (octal_string 1234) = "2322"%string.
+Proof.
+  unfold hex_string.
+  reflexivity.
+Qed.
+
+Goal sprintf "Hello, %s!" "world" = "Hello, world!".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%d, %d, %d, ..." 1 2 3 = "1, 2, 3, ...".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%d%%" 100 = "100%".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%c" "x"%char = "x".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%o" 1234 = "2322".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%x" 1234 = "4d2".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%X" 1234 = "4D2".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%b" 1234 = "10011010010".
+Proof.
+  reflexivity.
+Qed.
+
+Goal (sprintf "%o, %x, %X, %b, ..." 1234 1234 1234 1234) = "2322, 4d2, 4D2, 10011010010, ...".
+Proof.
+  reflexivity.
+Qed.
+
+Goal (sprintf "%4X" 1234) = " 4D2".
+Proof.
+  reflexivity.
+Qed.
+
+Goal (sprintf "%05X" 1234) = "004D2".
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%-4X" 1234 = "4D2 "%string.
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%-05X" 1234 = "4D200"%string.
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "% d" 1234 = " 1234"%string.
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%+d" 1234 = "+1234"%string.
+Proof.
+  reflexivity.
+Qed.
+
+
+Goal sprintf "%-#05X" 1234 = "0X4D2"%string.
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%-#05X" 0 = "00000"%string.
+Proof.
+  reflexivity.
+Qed.
+
+Goal sprintf "%-#05x" 1234 = "0x4d2"%string.
+Proof.
+  reflexivity.
+Qed.

test-suite/demo.v

@@ -14,4 +14,4 @@ Goal sprintf "%d%%" 100 = "100%".
 Proof. reflexivity. Qed.
 
 Goal sprintf "%c" "x"%char = "x".
-Proof. reflexivity. Qed.
+Proof. reflexivity. Qed.

theories/Flags.v

@@ -0,0 +1,117 @@
+Set Primitive Projections.
+
+Variant justify : Set := LeftJustify | RightJustify.
+
+(* Reference : http://www.cplusplus.com/reference/cstdio/printf/            *)
+(* %[flags]     [width]  specifier                                          *)
+(* %(-|+| |#|0)^* (\d+)    specifier                                        *)
+Record options : Set :=
+  { option_justify : justify ;  (* '-'   : left justify                     *)
+    option_sign : bool ;        (* '+'   : precede with plus sign           *)
+    option_space : bool ;       (* ' '   : space if no sign displayed       *)
+    option_prefix : bool ;      (* '#'   : precede with o x X , 0 0x 0X     *)
+                                (*         for values different than zero   *)
+    option_zero_pad : bool ;    (* '0'   : pad with 0's instead of space    *)
+    option_width : option nat ; (* (\d+) : width of field                   *)
+  }.
+
+
+
+(* default options *)
+Definition default_options : options :=
+  {| option_justify :=  RightJustify ;
+     option_sign := false;
+     option_space := false;
+     option_prefix := false;
+     option_zero_pad := false;
+     option_width := None;
+  |}.
+
+Definition update_option_justify o v :=
+  {| option_justify := v ;
+     option_sign := o.(option_sign) ;
+     option_space := o.(option_space) ;
+     option_prefix := o.(option_prefix) ;
+     option_zero_pad := o.(option_zero_pad) ;
+     option_width := o.(option_width) ;
+  |}.
+
+Definition update_option_sign o v :=
+  {| option_justify := o.(option_justify) ;
+     option_sign := v ;
+     option_space := o.(option_space) ;
+     option_prefix := o.(option_prefix) ;
+     option_zero_pad := o.(option_zero_pad) ;
+     option_width := o.(option_width) ;
+  |}.
+
+Definition update_option_space o v :=
+  {| option_justify := o.(option_justify) ;
+     option_sign := o.(option_sign) ;
+     option_space := v ;
+     option_prefix := o.(option_prefix) ;
+     option_zero_pad := o.(option_zero_pad) ;
+     option_width := o.(option_width) ;
+  |}.
+
+Definition update_option_prefix o v :=
+  {| option_justify := o.(option_justify) ;
+     option_sign := o.(option_sign) ;
+     option_space := o.(option_space) ;
+     option_prefix := v ;
+     option_zero_pad := o.(option_zero_pad) ;
+     option_width := o.(option_width) ;
+  |}.
+
+Definition update_option_zero_pad o v :=
+  {| option_justify := o.(option_justify) ;
+     option_sign := o.(option_sign) ;
+     option_space := o.(option_space) ;
+     option_prefix := o.(option_prefix) ;
+     option_zero_pad := v;
+    option_width := option_width o;
+  |}.
+
+Definition update_option_width' o width' :=
+  {| option_justify := o.(option_justify) ;
+     option_sign := o.(option_sign) ;
+     option_space := o.(option_space) ;
+     option_prefix := o.(option_prefix) ;
+     option_zero_pad := o.(option_zero_pad) ;
+     option_width := width'
+  |}.
+
+Definition update_option_width o width :=
+  update_option_width'
+    o
+    (match option_width o with
+     | None => Some width
+     | Some width' => Some ((10 * width') + width)
+     end).
+
+
+Theorem option_identity :
+  forall o justify sign space prefix zero_pad width ,
+         (update_option_width'
+         (update_option_zero_pad
+         (update_option_prefix
+         (update_option_space
+         (update_option_sign
+         (update_option_justify o justify)
+         sign)
+         space)
+         prefix)
+         zero_pad)
+         width) =
+         {| option_justify := justify ;
+            option_sign := sign ;
+            option_space := space ;
+            option_prefix := prefix ;
+            option_zero_pad := zero_pad ;
+            option_width := width
+         |}.
+Proof.
+  intros.
+  unfold update_option_width'.
+  reflexivity.
+Qed.