I am working with the Isabell/HOL system which is hosted by default on the PolyML system. I have found a strange syntax construct in some of the source code files consisting of @{ ...some verbage ... } , examples below. I have searched the ML library pages and the PolyML docs looking for this syntactical construct and have been unable to find it. Does anyone know what this signifies?
let metaSubst = @{lemma "PROP P t <Longrightarrow> PROP prop (x <equiv> t <Longrightarrow> PROP P x)" by (unfold propDef)}
[@{thm propDef}] Thanks David Thayer
On Jun 29, 2009, at 10:10 PM, Dave Thayer wrote:
Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing about them. Isabelle preprocesses the ML files it read and replaces the antiquotations before passing on the code to the PolyML compiler.
Steven
I am working with the Isabell/HOL system which is hosted by default on the PolyML system. I have found a strange syntax construct in some of the source code files consisting of @{ ...some verbage ... } , examples below. I have searched the ML library pages and the PolyML docs looking for this syntactical construct and have been unable to find it. Does anyone know what this signifies?
let metaSubst = @{lemma "PROP P t <Longrightarrow> PROP prop (x <equiv> t <Longrightarrow> PROP P x)" by (unfold propDef)}
[@{thm propDef}] Thanks David Thayer _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Mon, 29 Jun 2009, Steven Obua wrote:
Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing about them. Isabelle preprocesses the ML files it read and replaces the antiquotations before passing on the code to the PolyML compiler.
BTW, since people have asked this before: in Isabelle2009 the preprocesser now coexists with regular ML token syntax. This means that antiquotations within literal strings and comments are now longer expanded.
Moreover, since "@" can be part of a symbolic ML identifier, the "greatest munch rule" of lexing might confuse people who don't like spaces. E.g. in
foo::@{thms bar}
the "::@" part is taken as a single ML name. Infixes are better surrounded by spaces anyway, e.g.
foo :: @{thms bar}
(This discussion is better continued on the Isabelle mailing list.)
Makarius
Maybe the following paper is of some interest to Poly/ML users:
Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar. In G. Dos Reis and L. Th?ry, editors. The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems. Munich, August 2009. To appear in ACM Digital library. http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
The full system sources are available here (large): http://isabelle.in.tum.de/repos/isabelle/rev/Isabelle2009
The actual parallel programming library is here: http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/src/Pure/Concurre...
Makarius
-
dathayer＠microsoft.com -
makarius＠sketis.net -
obua＠in.tum.de