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.

asciiCoqでは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.

実行する必要があるのは 1 つのケースだけであり、取得した順序で数字が次々ときれいに配置されます (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".

Some (31415926, 8) を返します。

于 2013-03-21T01:00:10.457 に答える