Email Gateway (Aug 18 2022 at 11:44): Email Gateway (Aug 18 2022 at 11:44):From: Paolo Giarrusso <p.giarrusso@gmail.com>
Hi all, I'm a software developer and a new Isabelle user, practicing with the
tutorial. I'm using Isabelle 2007.
Note these two lines in the below theory (derived from § 2.5.6 of the
tutorial,
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf):
normal_form "val (Const True)"
gives:
"True"
:: "bool"
While
value "val (Const True)" (* this fails *)
fails (and there are no variables, so there's no reason for this).
Here's the theory:
theory ExBoolexBugReport imports Main begin
datatype boolex = Const bool | Neg boolex | And boolex boolex
consts
"val" :: "boolex \<Rightarrow> bool"
primrec
"val (Const b) = b"
"val (Neg boolex) = (\<not> (val boolex))"
"val (And b c) = ((val b) \<and> (val c))"
value "True"
normal_form "val (Const True)"
value "val (Const True)" (* this fails *)
value "val (Const (True::bool))"
end
Here's the error I get in the responses Emacs buffer.
*** Error: in 'ML', line 11.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
*** $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
*** Error: in 'ML', line 11.
*** Can't unify Term.term with EvalTerm.Generated.boolex
*** (Different type constructors) Found near
*** $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
*** Error: in 'ML', line 14.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
*** $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
*** Error: in 'ML', line 14.
*** Can't unify Term.term with EvalTerm.Generated.boolex
*** (Different type constructors) Found near
*** $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
*** Error: in 'ML', line 19.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
*** $( $( Const( ...), ...(...)), term_of_boolex(x2))
*** Error: in 'ML', line 19.
*** Can't unify Term.term with EvalTerm.Generated.boolex
*** (Different type constructors) Found near
*** $( $( Const( ...), ...(...)), term_of_boolex(x2))
*** At command "value".
If needed: I'm using ProofGeneral-3.7pre071112 and Emacs 22.1 as provided by
Ubuntu 7.04, in case it makes any difference.
Thanks in advance
signature.asc
Email Gateway (Aug 18 2022 at 11:44):From: Amine Chaieb <chaieb@in.tum.de>
Hi,
The problem appears to be with the constructor "Const" which is the same
name as the constructor "Const" for internal represaentation of Lambda
terms in Isabelle.
Your theory works if you change Const into Cst. Maybe the Code generator
should rename such constants before emitting ML Code for evaluation?
Hope it helps,
Amine.
Paolo Giarrusso wrote:
Email Gateway (Aug 18 2022 at 11:51):From: Paolo Giarrusso <p.giarrusso@gmail.com>
On Thu, Apr 17, 2008 at 11:22 AM, Amine Chaieb <chaieb@in.tum.de> wrote:
Hi,
The problem appears to be with the constructor "Const" which is the same
name as the constructor "Const" for internal represaentation of Lambda terms
in Isabelle.
Your theory works if you change Const into Cst.
Yes, indeed.
Maybe the Code generator
should rename such constants before emitting ML Code for evaluation?
Sorry for the late answer, but I thought that having a separate
namespace altogether for all user-defined symbols could be nicer. Or
not?
Anyway, is anybody working on a fix for this in the code?
Hope it helps,
Amine.
Last updated: May 03 2024 at 12:27 UTC