1

私は3つのファイルを持っています：

1）cpf0.ml

type string = char list
type url = string
type var = string
type name = string
type symbol =
| Symbol_name of name

2）problem.ml:

type symbol =
  | Ident of string

3）test.ml

open Problem;;
open Cpf0;;

let symbol b = function
  | Symbol_name n -> Ident n

組み合わせるとtest.ml：ocamlc -c test.ml。エラーが発生しました：

この式のタイプはCpf0.name=char listですが、タイプstringの式が必要でした

それを修正するのを手伝ってくれませんか。どうもありがとうございます

編集：あなたの答えをありがとう。これらの3つのファイルについて詳しく説明したいと思います。CoqからOcamlへの抽出を使用しているため、次のようにcpf0.ml生成され cpf.vます。

 Require Import String.
 Definition string := string.
 Definition name := string.
 Inductive symbol := 
  | Symbol_name : name -> symbol.

コードextraction.v：

Set Extraction Optimize.
Extraction Language Ocaml.
Require ExtrOcamlBasic ExtrOcamlString.
Extraction Blacklist cpf list.

ここでExtrOcamlString

を開きました：open Cpf0;;で、タイプの別の定義がproblem.mlあるため、新しい問題が発生しましたproblem.mlstring

この式のタイプはCpf0.string=char listですが、タイプUtil.StrSet.elt=stringの式が必要です。

util.ml定義された型文字列の定義は次のとおりです。

module Str = struct type t = string end;;
module StrOrd = Ord.Make (Str);;
module StrSet = Set.Make (StrOrd);;
module StrMap = Map.Make (StrOrd);;

let set_add_chk x s =
  if StrSet.mem x s then failwith (x ^ " already declared")
  else StrSet.add x s;;

に変更しようとしていましたが、変更t = stringするt = char list場合は、依存する多くの機能を変更する必要があります（例：set_add_chk上記）。いいアイデアを教えていただけませんか。この場合どうするか。

編集2：この質問を何度も編集して申し訳ありません。答えに従った後、私はファイルproblem.mlを修正しました

type symbol =
  | Ident of Cpf0.string

彼らにはこのproblem.mlような別の定義があります。そして、タイプ1は再び受け入れられません。

module SymbSet = Set.Make (SymbOrd);;
let rec ident_of_symbol = function
  | Ident s -> s

let idents_of_symbols s =
  SymbSet.fold (fun f s -> StrSet.add (ident_of_symbol f) s) s StrSet.empty;;

この式のタイプはCpf0.string=char listですが、タイプUtil.StrSet.elt=stringの式が必要です。

4

1 に答える 1

4

モジュールCfp0とProblemのタイプ文字列は同じではないため、problem.mlでモジュールCpf0を開く必要があります。

problem.ml：

open Cpf0
type symbol =
  | Ident of string

以上の場合、モジュールを開かず、次のように型文字列のプレフィックスを付けないでください。

type symbol =
  | Ident of Cpf0.string
于 2012-04-05T10:21:54.467 に答える