Coq의 문자열에서 nat로 변환 함수

Question

에 string -> nat 변환 함수를 작성하고 싶습니다. 여기서 문자열 내용 만 number는 nat을 반환하고 그렇지 않으면 숫자가 포함 된 알파벳이나 알파벳 또는 숫자가 포함되지 않은 모든 경우 (예 : ', -, ...) 0을 반환합니다.

예를 들어 :

"0", "1", "2", "3", ... "99",..는 반환합니다

"a", "bc", "..0d"0, 1, 2, 3, ..., 99, ...이 ... 반환합니다 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. 

Answer 1

여기 (선명도) 내 정말 비효율적 버전 : COQ에

Require Import String Ascii. 

Open Scope string_scope. 

ascii ASCII 문자의 8 비트 표현입니다, 만 0 ~ 9 번역에 당신이 패턴 일치 할 수 있도록 나머지는 "123"에서 123을 계산하기 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. 

로 전송됩니다, 나는 쉽게 역순으로 문자열을 구문 분석을 찾을 :
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.

Answer 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. 

하나의 경우는 필요가 수행되어야하고, 숫자가 깔끔하게 당신이 얻을 순서대로 하나씩 배치 (아스키 코드 있도록 설계되었다 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).