FinMatrix.CoqExt.StrExt
Require Export Nat List.
Export ListNotations.
Require Export Ascii String.
Open Scope string.
Open Scope nat.
nat to ascii：只有0~9能正确转换，其余的都会转换为'A'
Definition nat2ascii (n:nat) : ascii :=
match n with
| 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
| 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | 9 => "9"
| _ => "A"
end.
match n with
| 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
| 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | 9 => "9"
| _ => "A"
end.
nat to string 的辅助函数。
cnt 用于循环计数，初始值至少是位数那么大，比如125的位数是3
n 输入的自然数
suffix 后缀字符串，初始值为 ""，随着循环会逐步构成 "5", "25", "125"
Fixpoint nat2str_aux (cnt:nat) (n:nat) (suffix:string) : string :=
let suffix' := String (nat2ascii (n mod 10)) suffix in
match cnt with
| O => suffix'
| S cnt' => match (n/10) with
| O => suffix'
| n' => nat2str_aux cnt' n' suffix'
end
end.
let suffix' := String (nat2ascii (n mod 10)) suffix in
match cnt with
| O => suffix'
| S cnt' => match (n/10) with
| O => suffix'
| n' => nat2str_aux cnt' n' suffix'
end
end.
nat to string
生成 n 个字符串：a1,a2,...,an
Definition create_nstrs (n:nat) (prefix:string) : list string :=
map (fun i => prefix ++ nat2str i) (seq 1 n).
map (fun i => prefix ++ nat2str i) (seq 1 n).
用指定字符构成的字符串
Definition str_repeat (c : ascii) (len : nat) : string :=
let fix f (aux:string) (n:nat) :=
match n with
| O => aux
| S n => String c (f aux n)
end in
f "" len.
let fix f (aux:string) (n:nat) :=
match n with
| O => aux
| S n => String c (f aux n)
end in
f "" len.
左填充的定长字符串。不足右侧用空格填充，多余时剪掉右侧
Definition str_alignl (s : string) (len : nat) : string :=
let len_s := length s in
if len_s =? len
then s
else if len_s <? len
then s ++ (str_repeat " " (len - len_s))
else
substring 0 len s.
let len_s := length s in
if len_s =? len
then s
else if len_s <? len
then s ++ (str_repeat " " (len - len_s))
else
substring 0 len s.
右对齐的定长字符串。不足时左侧填充空格，多余时剪掉左侧
Definition str_alignr (s : string) (len : nat) : string :=
let len_s := length s in
if len_s =? len
then s
else if len_s <? len
then (str_repeat " " (len - len_s)) ++ s
else
substring (len_s - len) len s.
let len_s := length s in
if len_s =? len
then s
else if len_s <? len
then (str_repeat " " (len - len_s)) ++ s
else
substring (len_s - len) len s.
Section LF_CR.
Definition CharLF : ascii := ascii_of_nat 10.
Definition CharCR : ascii := ascii_of_nat 13.
Definition strNewlineUnix : string := String CharLF "".
Definition strNewlineWin : string := String CharCR (String CharLF "").
Definition strNewlineMac : string := String CharCR "".
Definition strNewline : string := strNewlineUnix.
End LF_CR.
Definition CharLF : ascii := ascii_of_nat 10.
Definition CharCR : ascii := ascii_of_nat 13.
Definition strNewlineUnix : string := String CharLF "".
Definition strNewlineWin : string := String CharCR (String CharLF "").
Definition strNewlineMac : string := String CharCR "".
Definition strNewline : string := strNewlineUnix.
End LF_CR.