Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] difficulties with "value"

view this post on Zulip Email Gateway (May 13 2026 at 09:41):

From: Jonas Lochmannn <jonas.lochmann@informatik.uni-halle.de>

Hello,

I am a beginner with Isabelle. I want to work with a certain data
structure in Isabelle and there is an entry in the AFP for it.

My very simple test theory is this one:

theory Scratch
imports ROBDD.BDD_Code
begin
value "(1::int) + (2::int)"
value emptyci
end

Adding two numbers works. Printing an (internal) representation of the
data structure does not work:

structure Uint32:
sig
val shiftl: Word32.word -> int -> Word32.word
val shiftr: Word32.word -> int -> Word32.word
val shiftr_signed: Word32.word -> int -> Word32.word
val test_bit: Word32.word -> int -> bool
end
structure Bit_Shifts:
sig val drop: int -> int -> int eqtype int val push: int -> int -> int end
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: ) expected but raise was found
At (line 217 of "generated code")
Error: = expected but raise was found
At (line 217 of "generated code")
Error: end expected but ) was found
At (line 217 of "generated code")
Error: ; expected but ) was found
At (line 217 of "generated code")
Exception- Fail "Static Errors" raised

I have no clue what the messages want to tell me. Are limitations of the
"value" statement expected/normal? Any experiences regarding this and
where to start resolving it?

Best regards

Jonas

view this post on Zulip Email Gateway (May 13 2026 at 10:50):

From: Tobias Nipkow <nipkow@in.tum.de>

The value command is only meant to work for executable types and functions.
Whether emptyci is meant to be executable, the authors of the package can tell
you. Normally things should not go that drastically wrong.

Tobias

On 13/05/2026 11:10, Jonas Lochmannn wrote:

Hello,

I am a beginner with Isabelle. I want to work with a certain data
structure in Isabelle and there is an entry in the AFP for it.

My very simple test theory is this one:

theory Scratch
imports ROBDD.BDD_Code
begin
value "(1::int) + (2::int)"
value emptyci
end

Adding two numbers works. Printing an (internal) representation of the
data structure does not work:

structure Uint32:
sig
val shiftl: Word32.word -> int -> Word32.word
val shiftr: Word32.word -> int -> Word32.word
val shiftr_signed: Word32.word -> int -> Word32.word
val test_bit: Word32.word -> int -> bool
end
structure Bit_Shifts:
sig val drop: int -> int -> int eqtype int val push: int -> int -> int end
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: ) expected but raise was found
At (line 217 of "generated code")
Error: = expected but raise was found
At (line 217 of "generated code")
Error: end expected but ) was found
At (line 217 of "generated code")
Error: ; expected but ) was found
At (line 217 of "generated code")
Exception- Fail "Static Errors" raised

I have no clue what the messages want to tell me. Are limitations of the
"value" statement expected/normal? Any experiences regarding this and
where to start resolving it?

Best regards

Jonas

smime.p7s

view this post on Zulip Email Gateway (May 13 2026 at 10:53):

From: Manuel Eberl <manuel@pruvisto.org>

My guess would be that this has something to do with the code printing
for the "word" type. I vaguely recall running into similar issues when I
did some experiments with the word type. When using "export_code"
everything works fine, but the "value" command does not like it.

Someone who is familiar with the code generator would probably be the
right person to look into this.

Manuel

On 13/05/2026 12:50, Tobias Nipkow wrote:

The value command is only meant to work for executable types and
functions. Whether emptyci is meant to be executable, the authors of
the package can tell you. Normally things should not go that
drastically wrong.

Tobias

On 13/05/2026 11:10, Jonas Lochmannn wrote:

Hello,

I am a beginner with Isabelle. I want to work with a certain data
structure in Isabelle and there is an entry in the AFP for it.

My very simple test theory is this one:

theory Scratch
   imports ROBDD.BDD_Code
begin
   value "(1::int) + (2::int)"
   value emptyci
end

Adding two numbers works. Printing an (internal) representation of the
data structure does not work:

structure Uint32:
   sig
     val shiftl: Word32.word -> int -> Word32.word
     val shiftr: Word32.word -> int -> Word32.word
     val shiftr_signed: Word32.word -> int -> Word32.word
     val test_bit: Word32.word -> int -> bool
   end
structure Bit_Shifts:
   sig val drop: int -> int -> int eqtype int val push: int -> int ->
int end
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: Pattern expected but raise was found
At (line 217 of "generated code")
Error: ) expected but raise was found
At (line 217 of "generated code")
Error: = expected but raise was found
At (line 217 of "generated code")
Error: end expected but ) was found
At (line 217 of "generated code")
Error: ; expected but ) was found
At (line 217 of "generated code")
Exception- Fail "Static Errors" raised

I have no clue what the messages want to tell me. Are limitations of the
"value" statement expected/normal? Any experiences regarding this and
where to start resolving it?

Best regards

Jonas

view this post on Zulip Email Gateway (May 13 2026 at 11:04):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>

I second Manuel's suspicion. Note that the following correctly displays
the representation of the empty BDD:

ML_val ‹
    @{code emptyci} ()

›

Also note that emptyci is imperative HOL code. No idea how value copes
with Imperative HOL.

--

Peter

On 13/05/2026 12:53, Manuel Eberl wrote:

theory Scratch
   imports ROBDD.BDD_Code
begin
   value "(1::int) + (2::int)"
   value emptyci
end

view this post on Zulip Email Gateway (May 14 2026 at 09:37):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

Hi Jonas,

I am a beginner with Isabelle. I want to work with a certain data
structure in Isabelle and there is an entry in the AFP for it.

note that when reporting specific behavior it is important to mention
the Isabelle release you are using – presumably, Isabelle2025-2.

(The issue I discovered during analysis seems to be long-standing, though).

The problem is in session HOL.Imperative_HOL where a code setup is fragile.

You can amend that in an ad-hoc manner using

declare [[code drop: "Code_Evaluation.term_of :: 'a::typerep Heap ⇒ Code_Evaluation.term"]]

Then you get a more proper error message.

The underlying issue is that there is no straightforward way to
reconstruct a logical »Heap« value from an ML term.

Hope this helps,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: May 23 2026 at 03:31 UTC