From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id E63787EC6E for ; Fri, 13 Jun 2014 13:02:22 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of sybukstein@gmail.com) identity=pra; client-ip=209.85.219.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sybukstein@gmail.com"; x-sender="sybukstein@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of sybukstein@gmail.com designates 209.85.219.54 as permitted sender) identity=mailfrom; client-ip=209.85.219.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sybukstein@gmail.com"; x-sender="sybukstein@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-oa0-f54.google.com) identity=helo; client-ip=209.85.219.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sybukstein@gmail.com"; x-sender="postmaster@mail-oa0-f54.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjABAD/ZmlPRVds2lGdsb2JhbABag19ZgmypV5c/CBYPAQEBAQcLCwkSKoQcEQQZATkDDQUQDwImAiQSAQUBV4gMAxGjQ4MSaosnhQGTfycNV4VAAQUMgR6NT4JfgUwEijmPfYFDkCAYKYFpgxIu X-IPAS-Result: AjABAD/ZmlPRVds2lGdsb2JhbABag19ZgmypV5c/CBYPAQEBAQcLCwkSKoQcEQQZATkDDQUQDwImAiQSAQUBV4gMAxGjQ4MSaosnhQGTfycNV4VAAQUMgR6NT4JfgUwEijmPfYFDkCAYKYFpgxIu X-IronPort-AV: E=Sophos;i="5.01,471,1400018400"; d="scan'208";a="79881383" Received: from mail-oa0-f54.google.com ([209.85.219.54]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 13:02:22 +0200 Received: by mail-oa0-f54.google.com with SMTP id eb12so2606270oac.13 for ; Fri, 13 Jun 2014 04:02:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:date:message-id:subject:from:to:content-type; bh=WV0xbsqBa3gZhprWZ6w8awegwhm7qgj4IcSA2Ok8bV8=; b=ARl5Lsu7kx3GeICxdOEZWeYIsy63k+UU8YmCrTOe+sItdL3J5BZyArDV9T1c2EJtdR Qlym08XzOtGnLLqO+uV60V7I5fXFFtrOz+igriQh/wIDIsk7aNdpRb3iBgSRs7sgPrLv RkW7FCLaASSP9JrRVW5LErKc+sXXJgzqn0tDLEVzSQYe50yMRJjXnZAhyVznxvYZECf7 epk+TA7Gy53rN+Ux0tw5H+3O4EubBxRYCnHXe013lrBn+6MV8A9aCHWFbCtuRgWASs2O m/390len6+hPUHyVfqJNBBq1ZrZ49ZuxT27r/EJ/+DiYZVOdm/80AQDnHSaoG96U6I4Q YifA== MIME-Version: 1.0 X-Received: by 10.182.209.10 with SMTP id mi10mr1839927obc.37.1402657341005; Fri, 13 Jun 2014 04:02:21 -0700 (PDT) Sender: sybukstein@gmail.com Received: by 10.76.100.76 with HTTP; Fri, 13 Jun 2014 04:02:20 -0700 (PDT) Date: Fri, 13 Jun 2014 20:02:20 +0900 X-Google-Sender-Auth: hQuZBWT8W8PSrcBm5w8ZeLun1qA Message-ID: From: =?UTF-8?B?6JaE5LqV44CA5Y2D5pil?= To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Subject: [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 ;;