46 lines
1022 B
Coq
46 lines
1022 B
Coq
Require Import String.
|
||
|
||
(* https://docs.python.org/3/library/string.html#formatspec *)
|
||
|
||
(* bcdeEfFgGnosxX% *)
|
||
Inductive type: Set := | TypHex | TypInt | TypStr | TypFloat.
|
||
|
||
Inductive align: Set := AlignLeft | AlignRight | AlignJust | AlignCenter.
|
||
Inductive sign: Set := SignPos | SignNeg | SignSpc.
|
||
|
||
Definition digit := nat.
|
||
Definition width := digit.
|
||
Definition precision := digit.
|
||
|
||
Inductive prec :=
|
||
| Prec: width -> option type -> prec.
|
||
|
||
Notation "'․' width '_d'" := (Prec width (Some TypInt))
|
||
(at level 9, width constr).
|
||
Notation "'․' width" := (Prec width None) (at level 10).
|
||
|
||
|
||
Print Grammar constr.
|
||
Compute ․2.
|
||
Compute ․2 _d.
|
||
|
||
|
||
Inductive spec: Set :=
|
||
| Spec: option width -> precision -> type -> spec.
|
||
|
||
(* .2f *)
|
||
Check Spec None 2 TypFloat.
|
||
|
||
Notation "F '.' precision typ " := (Spec None precision typ) (at level 50).
|
||
Check F.2
|
||
|
||
|
||
(*
|
||
Inductive digit: Set := | D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9.
|
||
|
||
Inductive align: Type := option Ascii.ascii ->
|
||
|
||
Inductive spec: Type :=
|
||
| Spec: align ->
|
||
*)
|