--- a/doc-src/IsarRef/logics.tex Thu Apr 22 10:45:56 2004 +0200
+++ b/doc-src/IsarRef/logics.tex Thu Apr 22 10:49:30 2004 +0200
@@ -544,7 +544,7 @@
\begin{rail}
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
;
-decl: ((name ':')? term '(overloaded)'?)
+decl: ((name ':')? term '(' 'overloaded' ')'?)
\end{rail}
\begin{descr}
@@ -742,19 +742,23 @@
\isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
\end{matharray}
+\begin{rail}
+ 'constdefs' (name '::' type mixfix? prop +)
+ ;
+\end{rail}
+
HOLCF provides a separate type for continuous functions $\alpha \to
\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
syntax normally refers directly to the pure meta-level function type $\alpha
\To \beta$, with application $f\,x$.
-The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
-the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations
-involving continuous function types are treated specifically, transforming the
-syntax template accordingly and generating syntax translation rules for the
-abstract and concrete representation of application.
-
-The behavior for plain meta-level function types is unchanged. Mixed
-continuous and meta-level application is \emph{not} supported.
+The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ resemble those of Pure
+Isabelle (cf.\ \S\ref{sec:consts}), although automated type-inference is not
+supported here. Internally, declarations involving continuous function types
+are treated specifically, transforming the syntax template accordingly and
+generating syntax translation rules for the abstract and concrete
+representation of application. Note that mixing continuous and meta-level
+application is \emph{not} supported!
\subsection{Recursive domains}
--- a/doc-src/IsarRef/pure.tex Thu Apr 22 10:45:56 2004 +0200
+++ b/doc-src/IsarRef/pure.tex Thu Apr 22 10:49:30 2004 +0200
@@ -241,14 +241,21 @@
\end{matharray}
\begin{rail}
- 'consts' (constdecl +)
+ 'consts' ((name '::' type mixfix?) +)
+ ;
+ 'defs' ('(' 'overloaded' ')')? (axmdecl prop +)
;
- 'defs' ('(overloaded)')? (axmdecl prop +)
- ;
- 'constdefs' (constdecl prop +)
+\end{rail}
+
+\begin{rail}
+ 'constdefs' structs? (constdecl? constdef +)
;
- constdecl: name '::' type mixfix?
+ structs: '(' 'structure' (vars + 'and') ')'
+ ;
+ constdecl: (name '::' type) mixfix | (name '::' type) | name 'where' | mixfix
+ ;
+ constdef: thmdecl? prop
;
\end{rail}
@@ -261,13 +268,28 @@
existing constant. See \cite[\S6]{isabelle-ref} for more details on the
form of equations admitted as constant definitions.
- The $overloaded$ option declares definitions to be potentially overloaded.
+ The $(overloaded)$ option declares definitions to be potentially overloaded.
Unless this option is given, a warning message would be issued for any
definitional equation with a more special type than that of the
corresponding constant declaration.
-\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of
- constants, using the canonical name $c_def$ for the definitional axiom.
+\item [$\CONSTDEFS$] provides a streamlined combination of constants
+ declarations and definitions: type-inference takes care of the most general
+ typing of the given specification (the optional type constraint may refer to
+ type-inference dummies ``$_$'' as usual). The resulting type declaration
+ needs to agree with that of the specification; overloading is \emph{not}
+ supported here!
+
+ The constant name may be omitted altogether, if neither type nor syntax
+ declarations are given. The canonical name of the definitional axiom for
+ constant $c$ will be $c_def$, unless specified otherwise. Also note that
+ the given list of specifications is processed in a strictly sequential
+ manner, with type-checking being performed independently.
+
+ An optional initial context of $(structure)$ declarations admits use of
+ indexed syntax, using the special symbol \verb,\<index>, (printed as
+ ``\i''). The latter concept is particularly useful with locales (see also
+ \S\ref{sec:locale}).
\end{descr}
@@ -503,13 +525,15 @@
\begin{rail}
( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
- printasttranslation | tokentranslation ) text
+ printasttranslation ) ('(' 'advanced' ')')? text;
+
+ tokentranslation text
\end{rail}
Syntax translation functions written in ML admit almost arbitrary
manipulations of Isabelle's inner syntax. Any of the above commands have a
single \railqtok{text} argument that refers to an ML expression of appropriate
-type.
+type, which are as follows by default:
\begin{ttbox}
val parse_ast_translation : (string * (ast list -> ast)) list
@@ -521,7 +545,27 @@
val token_translation :
(string * string * (string -> string * real)) list
\end{ttbox}
-See \cite[\S8]{isabelle-ref} for more information on syntax transformations.
+
+In case that the $(advanced)$ option is given, the corresponding translation
+functions may depend on the signature of the current theory context. This
+allows to implement advanced syntax mechanisms, as translations functions may
+refer to specific theory declarations and auxiliary data.
+
+See also \cite[\S8]{isabelle-ref} for more information on the general concept
+of syntax transformations in Isabelle.
+
+\begin{ttbox}
+val parse_ast_translation:
+ (string * (Sign.sg -> ast list -> ast)) list
+val parse_translation:
+ (string * (Sign.sg -> term list -> term)) list
+val print_translation:
+ (string * (Sign.sg -> term list -> term)) list
+val typed_print_translation:
+ (string * (Sign.sg -> bool -> typ -> term list -> term)) list
+val print_ast_translation:
+ (string * (Sign.sg -> ast list -> ast)) list
+\end{ttbox}
\subsection{Oracles}
--- a/src/Pure/Isar/isar_syn.ML Thu Apr 22 10:45:56 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Apr 22 10:49:30 2004 +0200
@@ -131,8 +131,7 @@
OuterSyntax.command "consts" "declare constants" K.thy_decl
(Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
-val opt_overloaded =
- Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
+val opt_overloaded = P.opt_keyword "overloaded";
val finalconstsP =
OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
@@ -177,9 +176,24 @@
OuterSyntax.command "defs" "define constants" K.thy_decl
(opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
+
+(* constant definitions *)
+
+val vars = P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ));
+
+val structs =
+ Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (vars --| P.$$$ ")")) [];
+
+val constdecl =
+ (P.name --| P.$$$ "where") >> (fn x => (x, None, Syntax.NoSyn)) ||
+ P.name -- (P.$$$ "::" |-- P.!!! P.typ >> Some) -- P.opt_mixfix' >> P.triple1 ||
+ P.name -- (P.mixfix' >> pair None) >> P.triple2;
+
+val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
+
val constdefsP =
- OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
- (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs));
+ OuterSyntax.command "constdefs" "standard constant definitions" K.thy_decl
+ (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
(* theorems *)
@@ -248,25 +262,27 @@
(* translation functions *)
+val trfun = P.opt_keyword "advanced" -- P.text;
+
val parse_ast_translationP =
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
- (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
+ (trfun >> (Toplevel.theory o IsarThy.parse_ast_translation));
val parse_translationP =
OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
- (P.text >> (Toplevel.theory o IsarThy.parse_translation));
+ (trfun >> (Toplevel.theory o IsarThy.parse_translation));
val print_translationP =
OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
- (P.text >> (Toplevel.theory o IsarThy.print_translation));
+ (trfun >> (Toplevel.theory o IsarThy.print_translation));
val typed_print_translationP =
OuterSyntax.command "typed_print_translation" "install typed print translation functions"
- K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
+ K.thy_decl (trfun >> (Toplevel.theory o IsarThy.typed_print_translation));
val print_ast_translationP =
OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
- (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
+ (trfun >> (Toplevel.theory o IsarThy.print_ast_translation));
val token_translationP =
OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
@@ -287,12 +303,10 @@
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] ||
Scan.repeat1 P.locale_element >> pair Locale.empty);
-val locale_pred =
- Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "open" >> K false) --| P.$$$ ")")) true;
-
val localeP =
OuterSyntax.command "locale" "define named proof context" K.thy_decl
- (locale_pred -- P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
+ ((P.opt_keyword "open" >> not) -- P.name
+ -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
>> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
@@ -366,9 +380,8 @@
(* proof context *)
val fixP =
- OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
- (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
- >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
+ OuterSyntax.command "fix" "fix local variables (Skolem constants)" K.prf_asm
+ (vars >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
val assumeP =
OuterSyntax.command "assume" "assume propositions" K.prf_asm
@@ -733,10 +746,10 @@
val keywords =
["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
- "<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
- "concl", "defines", "files", "fixes", "in", "includes", "infix",
- "infixl", "infixr", "is", "notes", "open", "output", "overloaded",
- "shows", "structure", "where", "|", "\\<equiv>",
+ "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
+ "binder", "concl", "defines", "files", "fixes", "in", "includes",
+ "infix", "infixl", "infixr", "is", "notes", "open", "output",
+ "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
"\\<leftharpoondown>", "\\<rightharpoonup>",
"\\<rightleftharpoons>", "\\<subseteq>"];