CoqでHello, world!（改）

Coqで "Hello, world!" を標準出力させるのはちょっと難しい。
なぜならCoqはプログラミング言語ではなく、システム開発の支援をするツールであり、扱う言語は純粋関数型言語だからだ。

純粋でない部分（外部に標準出力する部分）のために、今回は16行ほどのOCamlの力を借りて実装した。
具体的には次の２つのファイルを作った。

• helloworld.v
• main.ml　(16行のOCamlコード)

ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。

 (* Coqのスタンダードライブラリより *)
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

まずCoqで書いたソース helloworld.v を見てみよう。

 (* Coqのコード helloworld.v *)
Require Import String.
Open Scope string_scope.

Definition msg := "Hello world!".

Extraction "coq_helloworld.ml" Ascii.nat_of_ascii msg.

以上のコードをコンパイルした結果、自動生成されるOCamlのコードがこれである。

 (* これはCoqのコードから自動的に生成されたOCamlのコードである。 *)
type bool =
  | True
  | False

type nat =
  | O
  | S of nat

(** val plus : nat -> nat -> nat **)

let rec plus n m =
  match n with
    | O -> m
    | S p -> S (plus p m)

(** val mult : nat -> nat -> nat **)

let rec mult n m =
  match n with
    | O -> O
    | S p -> plus m (mult p m)

type ascii =
  | Ascii of bool * bool * bool * bool * bool * bool * bool * bool

(** val nat_of_ascii : ascii -> nat **)

let nat_of_ascii = function
  | Ascii (a1, a2, a3, a4, a5, a6, a7, a8) ->
      plus
        (mult (S (S O))
          (plus
            (mult (S (S O))
              (plus
                (mult (S (S O))
                  (plus
                    (mult (S (S O))
                      (plus
                        (mult (S (S O))
                          (plus
                            (mult (S (S O))
                              (plus
                                (mult (S (S O))
                                  (match a8 with
                                     | True -> S O
                                     | False -> O))
                                (match a7 with
                                   | True -> S O
                                   | False -> O)))
                            (match a6 with
                               | True -> S O
                               | False -> O)))
                        (match a5 with
                           | True -> S O
                           | False -> O)))
                    (match a4 with
                       | True -> S O
                       | False -> O)))
                (match a3 with
                   | True -> S O
                   | False -> O)))
            (match a2 with
               | True -> S O
               | False -> O))) (match a1 with
                                  | True -> S O
                                  | False -> O)

type string =
  | EmptyString
  | String of ascii * string

(** val msg : string **)

let msg =
  String *1,
    (String *2,
    (String *3,
    (String *4,
    (String *5,
    (String *6,
    (String *7,
    (String *8,
    (String *9,
    (String *10,
    (String *11,
    (String *12,
    EmptyString)))))))))))))))))))))))

最後に以上をまとめて結果を出すOCamlのコードmain.ml。
この部分だけは証明することができない。

 (* OCamlのコード *)
module Coq = Coq_helloworld

let rec int_of_nat = function
  | Coq.O -> 0
  | Coq.S p -> 1 + (int_of_nat p)

let char_of_ascii a =
  char_of_int (int_of_nat (Coq.nat_of_ascii a))

let rec print_coqstring = function
  | Coq.EmptyString -> print_newline()
  | Coq.String (hd, tl) ->
      print_char (char_of_ascii hd);
      print_coqstring tl;;

print_coqstring Coq.msg;;

実行結果

Hello, world!

やった！できた！

*1:Ascii (False, False, False, True, False, False, True, False

*2:Ascii (True, False, True, False, False, True, True, False

*3:Ascii (False, False, True, True, False, True, True, False

*4:Ascii (False, False, True, True, False, True, True, False

*5:Ascii (True, True, True, True, False, True, True, False

*6:Ascii (False, False, False, False, False, True, False, False

*7:Ascii (True, True, True, False, True, True, True, False

*8:Ascii (True, True, True, True, False, True, True, False

*9:Ascii (False, True, False, False, True, True, True, False

*10:Ascii (False, False, True, True, False, True, True, False

*11:Ascii (False, False, True, False, False, True, True, False

*12:Ascii (True, False, False, False, False, True, False, False