Строка OCaml и строка Coq (извлечение из Coq в OCaml)

Question

Я использовал извлечение из Coq в OCaml, где у меня есть тип Z, N, positive

Я не использую, чтобы извлечь его в int OCaml.

Тогда тип, который я имею после извлечения:

type positive =
| Coq_xI of positive
| Coq_xO of positive
| Coq_xH

type coq_N =
| N0
| Npos of positive

type coq_Z =
| Z0
| Zpos of positive
| Zneg of positive

У меня есть программа в OCaml, где некоторые функции, используя тип OCaml string,

В моей программе на OCaml мне нужно написать несколько функций, преобразующих тип: string -> coq_N, string -> coq_Z, string -> positive

Я пытался написать функции в Coq, а затем использовал извлечение, чтобы получить тип OCaml, но Coq string отличается от OCaml string,

Например:

open Ascii
open BinNums
open Datatypes

type string =
| EmptyString
| String of ascii * string

let string_of_coqN (s: string): coq_N =
  match s with
    | EmptyString -> N0
    | String (a, _) -> (coq_N_of_ascii a);;

где coq_N_of_ascii это извлечение из coq функция N_of_ascii,

Когда я применил функцию string_of_coqN, например:

let test (x: string) = string_of_N x;;

Я получил жалобу, что

Error: This expression has type string but an expression was expected of type
         String0.string

Не могли бы вы помочь мне найти способ написать функции преобразования: string -> coq_N, string -> coq_Z а также string -> positive?

Answer 1

Для строк проще всего, вероятно, импортировать стандартный модуль библиотеки ExtrOcamlString в вашем файле извлечения, что заставит Coq извлечь их как char list в OCaml. Затем вы можете конвертировать между char list и родной stringс пользовательским кодом. Посмотрите, например, на файл lib/Camlcoq.v в распределении CompCert, функции camlstring_of_coqstring а также coqstring_of_camlstring,