Re: [isabelle] 2014-RC1 issues



On Wed, 30 Jul 2014, Lars Noschinski wrote:

BTW: I always use(d) "error """ the way one uses "undefined" in Haskell.
The following construct (which Makarius showed me at ITP) is a bit nicer
(you get a trace and can jump to the location of the error), but
requires a few lines of initial setup:

signature UTIL = sig
 exception Undefined
 val setup : theory -> theory
end

structure Util : UTIL = struct

exception Undefined

val setup =
 ML_Antiquotation.inline @{binding undef} (Scan.succeed "raise
Util.Undefined")
 #> ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ =>
raise Util.Undefined")

end

After that ITP session, I recalled the more basic "raise Match" idiom, but could not tell you about it. That is sufficiently short to be used literally.


I assume there is no easy way to make Isabelle/ML accept ⊥ instead of @{undef}?

That is the old questions how much of actual Standard ML we have in Isabelle/ML. There is still the claim that there is no fundamental difference, apart from antiquotations, although many delicate details have accumulated over the years.

In the past, people have occasionally proposed actual syntactic variations, like an actual arrow for fun/fn/case => like in Isabelle/HOL notation, but I always tried to keep the divergence from actual SML in check.

Technically, the token language could be "embraced and extended" further, but I think fringe languages like ML should stay as faithful to their own standards as possible. BTW, with symbols inside ML, the question of language context will show up again: You would probably expect completion for \<bottom>, but not for =>.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.