Type errors when using same name
Posted
by
lykimq
on Stack Overflow
See other posts from Stack Overflow
or by lykimq
Published on 2012-04-05T10:07:56Z
Indexed on
2012/04/06
5:28 UTC
Read the original article
Hit count: 222
ocaml
I have 3 files:
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
When I combine test.ml
: ocamlc -c test.ml
.
I received an error:
This expression has type Cpf0.name = char list but an expression was expected of type string
Could you please help me to correct it? Thank you very much
EDIT: Thank you for your answer. I want to explain more about these 3 files:
Because I am working with extraction in Coq to Ocaml type: cpf0.ml
is generated from
cpf.v
:
Require Import String.
Definition string := string.
Definition name := string.
Inductive symbol :=
| Symbol_name : name -> symbol.
The code extraction.v
:
Set Extraction Optimize.
Extraction Language Ocaml.
Require ExtrOcamlBasic ExtrOcamlString.
Extraction Blacklist cpf list.
where ExtrOcamlString
I opened: open Cpf0;;
in problem.ml
, and I got a new problem because in problem.ml
they have another definition for type string
This expression has type Cpf0.string = char list but an expression was expected of type Util.StrSet.elt = string
Here is a definition in util.ml
defined type string:
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;;
I was trying to change t = string
to t = char list
, but if I do that I have to change a lot of function it depend on (for example: set_add_chk
above). Could you please give me a good idea? how I would do in this case.
© Stack Overflow or respective owner