CODEWITHSUNDEEP
asciicoq
Quyen
Quyen

Reputation: 1373

Convert function from string to nat in Coq

I would like to write a function convert type string -> nat in coq. Where the string contents only number will return nat otherwise it will return 0 for the alphabet or alphabet with number or any cases that is not contain number (for example: ', -, ...).

For example:

"0", "1", "2", "3", ... "99",.. will return : 0, 1, 2, 3, ..., 99, ...

"a", "bc", "..0d",... will return : 0

Am I able to write this function in Coq?

I tried by myself but I do not know how can I convert just the number and not the alphabet like my example?

Require Import Ascii String.

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

Upvotes: 1

Views: 1505

Answers (2)

Yves
Yves

Reputation: 4258

The previous answer is nice but a bit boring to write and read, and because it uses natural numbers, it is very limited. Why not move directly to integers?

First map every ascii character to an integer:

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.

Only one case needs to be done, and the digits are neatly placed one after the other in the order you obtain (the ascii code was designed that way, long before Coq was invented).

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.

Here is another attempt at handling strings with several digits, without reversing the list.

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.

In this case, the function accepts strings that have any trailing characters.

Compute num_prefix_and_length "31415926 remind me of Pi".

returns Some (31415926, 8).

Upvotes: 2

Vinz
Vinz

Reputation: 6057

Here is my really inefficient version (for clarity):

Require Import String Ascii.

Open Scope string_scope.

ascii in Coq is a 8-bit representation of ascii characters, so you can pattern match to only translate 0 to 9, the rest is sent to 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.

To compute 123 from "123", I find it easier to parse the string in reverse order:
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".

In the end, you have what you want. Be careful not to try with huge numbers, it might take a while, but you get the idea!

Best, V.

Upvotes: 2

Related Questions