Email Gateway (May 20 2022 at 19:59): Email Gateway (May 20 2022 at 19:59):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I just encountered a problem in the code-generator with the name “nil”
which seems to be treated specially in Eval. Can the line "code_reserved Eval nil”
or similar be added for the next Isabelle release?
Here is a minimal example
definition nil :: nat where
"nil = 42"
value (code) nil
(*
Error: Type mismatch in type constraint.
Value: nil : 'a list
Constraint: nat
Reason:
Can't unify 'a list (In Basis) with nat
(Different type constructors)
nil : nat
At (line 35 of "generated code")
Error: Type error in function application.
Function: term_of_nat : nat -> term
Argument: nil : 'a list
Reason:
Can't unify nat with 'a list (In Basis)
(Different type constructors)
term_of_nat nil
At (line 37 of "generated code")
Exception- Fail "Static Errors" raised
*)
code_reserved Eval nil
value (code) nil
(* 42 *)
Best,
René
Email Gateway (May 20 2022 at 21:00):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
that »nil« seems to enter the game by a subtle detail of the build-in
list type:
ML ‹
structure List_Copy =
struct
datatype list_copy = datatype list
end
›
ML ‹open List_Copy›
I don't know whether this has entered by recent renovations in PolyML (I
just don't remember to have seen those informative »constructor«
pseudo-statements), but anyway it is easy to accommodate that.
I will take care of this.
Cheers,
Florian
OpenPGP_signature
Email Gateway (May 22 2022 at 05:35):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Done in rev. 60c9c18a707.
Florian
OpenPGP_signature
Last updated: Jan 04 2025 at 20:18 UTC