Merge pull request #8 from gmalecha/notations

Use String Notations instead of dependent types

CHANGELOG.md

@@ -1,3 +1,9 @@
+# Next
+
+- Add notations for format strings (`Format.t`)
+- `sprintf` and `sscanf` now take a format string of type `Format.t` instead of `string`
+- No longer compatible with 8.8 and 8.9
+
 # 1.0.1
 
 - Add `sscanf`

_CoqProject

@@ -3,6 +3,8 @@
 theories/Flags.v
 theories/Digits.v
 theories/Format.v
+theories/FormatParser.v
+theories/FormatNotations.v
 theories/Justify.v
 theories/Printf.v
 theories/Scanf.v

test-suite/TestPrintf.v

@@ -2,6 +2,7 @@ Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import Coq.NArith.NArith.
 Require Import Coq.ZArith.ZArith.
+Require Import Printf.Digits.
 Require Import Printf.Printf.
 
 Local Open Scope string_scope.

theories/Digits.v

@@ -108,3 +108,18 @@ Definition string_of_digits (digit : N -> ascii) : digits -> string :=
 
 Definition string_of_N (base : N) (digit : N -> ascii) (n : N) : string :=
   string_of_digits digit (digits_of_N base n).
+
+Definition binary_string (n : N) :=
+  string_of_N 2 binary_ascii n.
+
+Definition hex_string (n : N) :=
+  string_of_N 16 hex_ascii n.
+
+Definition hex_string_upper (n : N) :=
+  string_of_N 16 hex_ascii_upper n.
+
+Definition octal_string (n : N) :=
+  string_of_N 8 octal_ascii n.
+
+Definition decimal_string (n : N) :=
+  string_of_N 10 decimal_ascii n.

theories/Format.v

@@ -4,30 +4,8 @@ Require Import Coq.NArith.NArith.
 Require Import Coq.ZArith.ZArith.
 Require Import Printf.Flags.
 
-(** ** Error handling in dependent types *)
-
-(** This tagged unit type indicates an error in the computation of a type. *)
-Variant tyerror {A : Type} (a : A) : Set := Invalid.
-
-(** Construct a dependent type from a computation which may fail. *)
-Definition for_good {E R : Type} (er : E + R) (k : R -> Type) : Type :=
-  match er with
-  | inl e => tyerror e
-  | inr r => k r
-  end.
-
-(** Apply a dependent function to the result of a computation when it is successful. *)
-Definition on_success {E R : Type} {er : E + R} {k : R -> Type} (f : forall r, k r)
-  : for_good er k :=
-  match er with
-  | inl e => Invalid e
-  | inr r => f r
-  end.
-
 (** ** String utilities *)
 
-Local Infix "::" := String : string_scope.
-
 Definition ascii_digit (c : ascii) : nat :=
   (if c =? "1" then 1
   else if c =? "2" then 2
@@ -80,118 +58,6 @@ Inductive t : Type :=
 | Hole : type -> options -> t -> t
 .
 
-Variant spec_state : Type :=
-| Flags
-| Width
-| TySpec (t : number_dectype)
-.
-
-(** Parser state machine. *)
-Variant state : Type :=
-| Ini                                  (* Initial state *)
-| Spec (j : spec_state) (o : options)  (* Parsing specifier *)
-  (* [j]: inner specifier parsing state *)
-  (* [o]: currently accumulated options *)
-.
-
-(** Parser error: dump the remaining string, that serves to locate the error. *)
-Variant error : Type :=
-| ErrorAt (i : state) (s : string)
-.
-
-Definition digit1to9 (c : ascii) : bool :=
-  (c =? "1")%char ||
-  (c =? "2")%char ||
-  (c =? "3")%char ||
-  (c =? "4")%char ||
-  (c =? "5")%char ||
-  (c =? "6")%char ||
-  (c =? "7")%char ||
-  (c =? "8")%char ||
-  (c =? "9")%char.
-
-Definition isFlagsOrWidth (j : _) : bool :=
-  match j with
-  | Flags | Width => true
-  | TySpec _ => false
-  end.
-
-Definition isWidth (j : _) : bool :=
-  match j with
-  | Width => true
-  | Flags | TySpec _ => false
-  end.
-
-Definition isFlags (j : _) : bool :=
-  match j with
-  | Flags => true
-  | Width | TySpec _ => false
-  end.
-
-(** Parse string [s] in state [i] into a format which is passed to the final
-  continuation [k], or return an error. *)
-Local Fixpoint parse_ {r : Type} (i : state) (k : t -> r) (s0 : string)
-  : error + r :=
-  match i, s0 with
-    (* The initial state looks for ["%"], indicating a specifier,
-       and keeps the rest as literal. *)
-  | Ini, ""%string => inr (k Empty)
-  | Ini, c :: s =>
-    if (c =? "%")%char then
-      let continue (_ : unit) := parse_ (Spec Flags default_options) k s in
-      match s with
-      | c' :: s =>
-        if (c' =? "%")%char then parse_ Ini (fun fmt => k (Literal "%" fmt)) s
-        else continue tt
-      | _ => continue tt
-      end
-    else
-      parse_ Ini (fun fmt => k (Literal c fmt)) s
-
-  | Spec _ _, ""%string => inl (ErrorAt i s0)
-  | Spec j o, a :: s =>
-    (* When parsing a specifier, the next character is either:
-       - a specifier character, then update the format and go back to the initial state;
-       - or a flag (or width) character, then update the options accordingly. *)
-    let specifier (t : type) := parse_ Ini (fun fmt => k (Hole t o fmt)) s in
-    let flag (j : spec_state) (o : options) := parse_ (Spec j o) k s in
-    let typ (t : number_dectype) := parse_ (Spec (TySpec t) o) k s in
-    let number b := Number b
-      match j with
-      | TySpec t => t
-      | _ => T_Nat
-      end in
-    if a =? "s" then specifier String
-    else if a =? "c" then specifier Char
-    else if a =? "b" then specifier (number Binary)
-    else if a =? "o" then specifier (number Octal)
-    else if a =? "d" then specifier (number Decimal)
-    else if a =? "x" then specifier (number HexLower)
-    else if a =? "X" then specifier (number HexUpper)
-    else if a =? "N" then typ T_N
-    else if a =? "Z" then
-      match j, s with
-      | (Flags | Width), c :: s => if c =? "d"%char then parse_ Ini (fun fmt => k (Hole SDecimal o fmt)) s
-        else inl (ErrorAt i s0)
-      | _, _ => inl (ErrorAt i s0)
-      end
-    else if ((digit1to9 a && isFlagsOrWidth j) || ((a =? "0")%char && isWidth j))%bool then
-      flag Width (update_option_width o (ascii_digit a))
-    else
-    match j with
-    | Flags =>
-      if a =? "-" then flag Flags (update_option_justify o LeftJustify)
-      else if a =? "+" then flag Flags (update_option_sign o true)
-      else if a =? " " then flag Flags (update_option_space o true)
-      else if a =? "#" then flag Flags (update_option_prefix o true)
-      else if a =? "0" then flag Flags (update_option_zero_pad o true)
-      else inl (ErrorAt i s0)
-    | _ => inl (ErrorAt i s0)
-    end
-  end%char%string.
-
-Definition parse : string -> error + t := parse_ Ini id.
-
 Definition dectype_type (t : number_dectype) : Type :=
   match t with
   | T_Nat => nat

theories/FormatNotations.v

@@ -0,0 +1,12 @@
+(** * Notations for [Format.t] *)
+
+(** Reexport only the notations. *)
+
+Require Import Printf.Format.
+Require Import Printf.FormatParser.
+
+Declare Scope fmt_scope.
+Delimit Scope fmt_scope with fmt.
+Bind Scope fmt_scope with Format.t.
+
+String Notation Format.t parse_opt print : fmt_scope.