From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <199902221816.TAA25711@pauillac.inria.fr>
Subject: Re: Warnings in ocaml
To: dsyme@microsoft.com (Don Syme)
Date: Mon, 22 Feb 1999 19:16:51 +0100 (MET)
In-Reply-To: <39ADCF833E74D111A2D700805F1951EF0F00B9E4@RED-MSG-06> from "Don Syme" at Feb 22, 99 09:25:27 am
> Here's another problem: I wrote about 20,000 lines where I used the built in
> equality for
> a particular type (that represented terms in a theorem prover). Now I want
> to implement
> my own equality function on the type, and never user built-in equality. I
[...]
> Don
[...]
> email: dsyme@microsoft.com
> ------------------------------------------------------------------------
A quick hack that may helps could be to use the compiler to detect
those applications by redefining the (=) predicate with a type that is
not compatible with the type term. For instance, you may redefine (=)
for integers only (or strings only), and this way you may statically
find applications of generic equality to your term values since they
become ill-typed. Admittedly, this is not perfect, but can be of some
help in a very symbolic code as a theorem prover, where application of
= to values that are not of type term may be sparse.
Pierre Weis
INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:20 MET