1

我想写一个函数转换类型string -> nat。coq如果字符串内容只有数字将返回nat，否则它将返回0字母或带数字的字母或任何不包含数字的情况（例如：'、-、...）。

例如：

"0", "1", "2", "3", ... "99",..将返回 ：0, 1, 2, 3, ..., 99, ...

"a", "bc", "..0d"，... 将返回 ：0

我可以写这个函数Coq吗？

我自己试过，但我不知道如何只转换数字而不像我的例子那样转换字母？

Require Import Ascii String.

  Definition nat_of_string (s : string) : nat :=
    match s with
      | EmptyString  => 0
      | String (s) _ => nat_of_ascii s
    end.
4

2 回答 2

2

这是我非常低效的版本（为了清楚起见）：

Require Import String Ascii.

Open Scope string_scope.

ascii在 Coq 中是 ascii 字符的 8 位表示，因此您可以进行模式匹配以仅将 0 转换为 9，其余发送到None

Definition num_of_ascii (c: ascii) : option nat :=
 match c with
(* Zero is 0011 0000 *)
   | Ascii false false false false true true false false => Some 0
(* One is 0011 0001 *)
   | Ascii true false false false true true false false => Some 1
(* Two is 0011 0010 *)
   | Ascii false true false false true true false false => Some 2
   | Ascii true true false false true true false false => Some 3
   | Ascii false false true false true true false false => Some 4
   | Ascii true false true false true true false false => Some 5
   | Ascii false true true false true true false false => Some 6
   | Ascii true true true false true true false false => Some 7
   | Ascii false false false true true true false false => Some 8
   | Ascii true false false true true true false false => Some 9
   | _ => None
end.

要从“123”计算 123，我发现以相反的顺序解析字符串更容易：
12345 = 5 + 10 * (4 + 10 * (3 + 10 * (2 + 10 * 1)))

(* Inefficient string reversal *)
Fixpoint string_rev (s : string) : string :=
 match s with
 | EmptyString => EmptyString
 | String c rest => append (string_rev rest) (String c EmptyString)
end.

Fixpoint num_of_string_rec (s : string) : option nat :=
  match s with
    | EmptyString => Some 0
    | String c rest => 
       match (num_of_ascii c), (num_of_string_rec rest) with
          | Some n, Some m => Some (n + 10 * m)
          | _ , _ => None
       end
   end.

Definition num_of_string (s : string) := 
  match num_of_string_rec (string_rev s) with
    | Some n => n
    | None => 0
  end.

Eval vm_compute in num_of_string "789".

最后，你有你想要的。小心不要尝试大量数字，这可能需要一段时间，但你明白了！

最好的，V.

于 2013-03-11T10:55:14.200 回答
2

前面的答案很好，但写和读有点无聊，而且因为它使用自然数，所以非常有限。为什么不直接转向整数？

首先将每个 ascii 字符映射到一个整数：

Require Import ZArith String Ascii.
Open Scope Z_scope. 

Definition Z_of_bool (b : bool) := if b then 1 else 0.

(* This coercion is used to make the next function shorter to write and read *)

Coercion Z_of_bool : bool >-> Z.

Definition Z_of_ascii a :=
  match a with
   Ascii b1 b2 b3 b4 b5 b6 b7 b8 =>
     b1 + 2 * (b2 + 2 * (b3 + 2 * (b4 + 2 *
      (b5 + 2 * (b6 + 2 * (b7 + 2 * b8))))))
  end.

只需要完成一种情况，并且数字按照您获得的顺序一个接一个地整齐地放置（ascii 代码就是这样设计的，早在 Coq 发明之前）。

Definition Z_of_0 := Eval compute in Z_of_ascii "0".

Definition Z_of_digit a := 
   let v := Z_of_ascii a - Z_of_0 in
   match v ?= 0 with
     Lt => None | Eq => Some v | 
     Gt => match v ?= 10 with Lt => Some v | _ => None end
   end.

这是在不反转列表的情况下处理具有多个数字的字符串的另一种尝试。

Fixpoint num_prefix_and_length (s : string) : option (Z * Z) :=
  match s with
    EmptyString => None
  | String a s' => 
    match Z_of_digit a with
      None => None
    | Some va =>
      match num_prefix_and_length s' with
        None => Some (va, 1)
      | Some (vs, n) => Some (va * 10 ^ n + vs, n+1)
      end
    end
  end.

在这种情况下，该函数接受具有任何尾随字符的字符串。

Compute num_prefix_and_length "31415926 remind me of Pi".

返回一些 (31415926, 8)。

于 2013-03-21T01:00:10.457 回答