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，但表达式应为字符串类型

你能帮我纠正一下吗？非常感谢

编辑：谢谢你的回答。我想解释更多关于这 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;;in problem.ml，我遇到了一个新问题，因为 inproblem.ml他们对类型有另一个定义string

此表达式的类型为 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：很抱歉多次编辑这个问题。按照答案后，我修复了文件问题.ml

type symbol =
  | Ident of Cpf0.string

problem.ml他们有另一个这样的定义。并且类型一再次不接受。

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

您需要在problem.ml 中打开模块Cpf0，因为模块Cfp0 和Problem 中的类型字符串不一样。

问题.ml：

open Cpf0
type symbol =
  | Ident of string

或者更好，不要打开模块并像这样为类型字符串添加前缀：

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