# HG changeset patch # User wenzelm # Date 1082623770 -7200 # Node ID 2bfe5de2d1fae5c5e87dd81cd3fca9130c7d97fa # Parent 79b7bd93626465b671ef1ed8d17ee669dcc5a54c improved constdefs and translation functions; diff -r 79b7bd936264 -r 2bfe5de2d1fa doc-src/IsarRef/logics.tex --- 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} diff -r 79b7bd936264 -r 2bfe5de2d1fa doc-src/IsarRef/pure.tex --- 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,\, (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} diff -r 79b7bd936264 -r 2bfe5de2d1fa src/Pure/Isar/isar_syn.ML --- 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", "|", "\\", + "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", + "binder", "concl", "defines", "files", "fixes", "in", "includes", + "infix", "infixl", "infixr", "is", "notes", "open", "output", + "overloaded", "shows", "structure", "where", "|", "\\", "\\", "\\", "\\", "\\"];