[Caml-list] Missleading type error

[Caml-list] Missleading type error

[薄井 千春]

Dear all.

I encountered a puzzling error message in the enclosed file:
"$ ocamlc -c boolerror.ml
File "boolerror.ml", line 33, characters 27-710:
Error: Signature mismatch:
       ...
       Values do not match:
         val insert : atom -> bool -> t -> t option
       is not included in
         val insert : atom -> bool -> t -> t option
       File "boolerror.ml", line 25, characters 2-43: Expected declaration
       File "boolerror.ml", line 40, characters 6-12: Actual declaration"

One might think that atom is defined twice in the code, but this is
not the case. The code does have a problematic part: redefinition of
bool type constructor and True and False data constructors. One might
hope that error message will complain about them rather than atom.
Removing the decolaration of bool fixed the problem. The original
error message was very puzzling and misleading. Perhaps it should be
fixed.


type atom = string;;                      (* propositional letters *)

type formula =
  | Atom of atom
  | Or of formula * formula
  | And of formula * formula
  | If of formula * formula
  | Not of formula
;;
type swff =
  | True of formula
  | False of formula
;;

(* Interpretation function of a model: assignment of truth values
   to propositional letters (atoms)
*)
module type Interpretation = sig
  type t
  val empty : t
      (* return None if adding a new atom leads to a contradiction,
         that is, inconsistent model
       *)
  val mem_pos : atom -> t -> bool
  val insert : atom -> bool-> t -> t option
end

type bool =
  | True
  | False
;;

module I : Interpretation= struct
  module S = Set.Make(struct type t = atom let compare = compare end)
  type t = {pos: S.t; neg: S.t} (*; cng: S.t} *)

  let empty = {pos = S.empty; neg = S.empty}(* ; cng = S.empty} *)


  let insert (atom:atom) sign t = match sign with
  | True ->                     (* adding a positive atom *)
      if (S.mem atom t.neg) (* || (S.mem atom t.cng) *) then None
(* inconsistency *)
         else Some {t with pos = S.add atom t.pos}
  | False ->                     (* adding a negative atom *)
      if S.mem atom t.pos then None     (* inconsistency *)
         else Some {t with neg = S.add atom t.neg}

  let mem_pos (x:atom) t = S.mem x t.pos
end
;;