# HG changeset patch # User bulwahn # Date 1302275629 -7200 # Node ID c2b5dbb76b7ee6b39473142eacdb7e8ab847ee57 # Parent 12635bb655fd0c2da33e189b5f65d9b267743285# Parent b3196458428bab7b4aa71d3e840add48e1048cfd merged diff -r 12635bb655fd -r c2b5dbb76b7e NEWS --- a/NEWS Fri Apr 08 16:31:14 2011 +0200 +++ b/NEWS Fri Apr 08 17:13:49 2011 +0200 @@ -93,9 +93,11 @@ be disabled via the configuration option Syntax.positions, which is called "syntax_positions" in Isar attribute syntax. -* Discontinued special treatment of structure Ast: no pervasive -content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to -qualified names like Ast.Constant etc. +* Discontinued special status of various ML structures that contribute +to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less +pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY, +refer directly to Ast.Constant, Lexicon.is_identifier, +Syntax_Trans.mk_binder_tr etc. * Typed print translation: discontinued show_sorts argument, which is already available via context of "advanced" translation. diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Fri Apr 08 17:13:49 2011 +0200 @@ -10,8 +10,8 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax.typeT; - val spropT = Syntax.spropT; + val typeT = Syntax_Ext.typeT; + val spropT = Syntax_Ext.spropT; in Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Apr 08 17:13:49 2011 +0200 @@ -496,7 +496,6 @@ @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ - & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Apr 08 17:13:49 2011 +0200 @@ -522,7 +522,6 @@ \indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{4}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ - & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|=?=| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|==| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|&&&| \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Apr 08 17:13:49 2011 +0200 @@ -132,12 +132,12 @@ This \verb!no_vars! business can become a bit tedious. If you would rather never see question marks, simply put \begin{quote} -@{ML "show_question_marks_default := false"}\verb!;! +@{ML "Printer.show_question_marks_default := false"}\verb!;! \end{quote} at the beginning of your file \texttt{ROOT.ML}. The rest of this document is produced with this flag set to \texttt{false}. -Hint: Setting \verb!show_question_marks_default! to \texttt{false} only +Hint: Setting @{ML Printer.show_question_marks_default} to \texttt{false} only suppresses question marks; variables that end in digits, e.g. @{text"x1"}, are still printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their internal index. This can be avoided by diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Apr 08 17:13:49 2011 +0200 @@ -173,12 +173,12 @@ This \verb!no_vars! business can become a bit tedious. If you would rather never see question marks, simply put \begin{quote} -\verb|show_question_marks_default := false|\verb!;! +\verb|Printer.show_question_marks_default := false|\verb!;! \end{quote} at the beginning of your file \texttt{ROOT.ML}. The rest of this document is produced with this flag set to \texttt{false}. -Hint: Setting \verb!show_question_marks_default! to \texttt{false} only +Hint: Setting \verb|Printer.show_question_marks_default| to \texttt{false} only suppresses question marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, their internal index. This can be avoided by diff -r 12635bb655fd -r c2b5dbb76b7e doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/doc-src/antiquote_setup.ML Fri Apr 08 17:13:49 2011 +0200 @@ -71,7 +71,8 @@ if txt2 = "" then txt1 else if kind = "type" then txt1 ^ " = " ^ txt2 else if kind = "exception" then txt1 ^ " of " ^ txt2 - else if Syntax.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2 + else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1)) + then txt1 ^ ": " ^ txt2 else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) diff -r 12635bb655fd -r c2b5dbb76b7e src/CCL/Term.thy --- a/src/CCL/Term.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/CCL/Term.thy Fri Apr 08 17:13:49 2011 +0200 @@ -56,11 +56,11 @@ (** Quantifier translations: variable binding **) (* FIXME does not handle "_idtdummy" *) -(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) +(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *) fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b); fun let_tr' [a,Abs(id,T,b)] = - let val (id',b') = variant_abs(id,T,b) + let val (id',b') = Syntax_Trans.variant_abs(id,T,b) in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end; fun letrec_tr [Free(f,S),Free(x,T),a,b] = @@ -72,23 +72,23 @@ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = - let val (f',b') = variant_abs(ff,SS,b) - val (_,a'') = variant_abs(f,S,a) - val (x',a') = variant_abs(x,T,a'') + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) + val (_,a'') = Syntax_Trans.variant_abs(f,S,a) + val (x',a') = Syntax_Trans.variant_abs(x,T,a'') in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = - let val (f',b') = variant_abs(ff,SS,b) - val ( _,a1) = variant_abs(f,S,a) - val (y',a2) = variant_abs(y,U,a1) - val (x',a') = variant_abs(x,T,a2) + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) + val ( _,a1) = Syntax_Trans.variant_abs(f,S,a) + val (y',a2) = Syntax_Trans.variant_abs(y,U,a1) + val (x',a') = Syntax_Trans.variant_abs(x,T,a2) in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' end; fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = - let val (f',b') = variant_abs(ff,SS,b) - val ( _,a1) = variant_abs(f,S,a) - val (z',a2) = variant_abs(z,V,a1) - val (y',a3) = variant_abs(y,U,a2) - val (x',a') = variant_abs(x,T,a3) + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b) + val ( _,a1) = Syntax_Trans.variant_abs(f,S,a) + val (z',a2) = Syntax_Trans.variant_abs(z,V,a1) + val (y',a3) = Syntax_Trans.variant_abs(y,U,a2) + val (x',a') = Syntax_Trans.variant_abs(x,T,a3) in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' end; diff -r 12635bb655fd -r c2b5dbb76b7e src/CCL/Type.thy --- a/src/CCL/Type.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/CCL/Type.thy Fri Apr 08 17:13:49 2011 +0200 @@ -46,8 +46,10 @@ "{x: A. B}" == "CONST Subtype(A, %x. B)" print_translation {* - [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), - (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] + [(@{const_syntax Pi}, + Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), + (@{const_syntax Sigma}, + Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] *} defs diff -r 12635bb655fd -r c2b5dbb76b7e src/Cube/Cube.thy --- a/src/Cube/Cube.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Cube/Cube.thy Fri Apr 08 17:13:49 2011 +0200 @@ -53,7 +53,8 @@ "_arrow" :: "[term, term] => term" (infixr "\" 10) print_translation {* - [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] + [(@{const_syntax Prod}, + Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] *} axioms diff -r 12635bb655fd -r c2b5dbb76b7e src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/FOLP/simp.ML Fri Apr 08 17:13:49 2011 +0200 @@ -371,7 +371,7 @@ (*Replace parameters by Free variables in P*) fun variants_abs ([],P) = P | variants_abs ((a,T)::aTs, P) = - variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P))); + variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P))); (*Select subgoal i from proof state; substitute parameters, for printing*) fun prepare_goal i st = diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Big_Operators.thy Fri Apr 08 17:13:49 2011 +0200 @@ -86,10 +86,10 @@ if x <> y then raise Match else let - val x' = Syntax.mark_bound x; + val x' = Syntax_Trans.mark_bound x; val t' = subst_bound (x', t); val P' = subst_bound (x', P); - in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end + in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end | setsum_tr' _ = raise Match; in [(@{const_syntax setsum}, setsum_tr')] end *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Apr 08 17:13:49 2011 +0200 @@ -51,7 +51,7 @@ fun mk_syntax name i = let - val syn = Syntax.escape name + val syn = Syntax_Ext.escape name val args = space_implode ",/ " (replicate i "_") in if i = 0 then Mixfix (syn, [], 1000) diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Complete_Lattice.thy Fri Apr 08 17:13:49 2011 +0200 @@ -159,8 +159,8 @@ "SUP x:A. B" == "CONST SUPR A (%x. B)" print_translation {* - [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, - Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] *} -- {* to avoid eta-contraction of body *} context complete_lattice @@ -409,7 +409,7 @@ "INT x:A. B" == "CONST INTER A (%x. B)" print_translation {* - [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}] *} -- {* to avoid eta-contraction of body *} lemma INTER_eq_Inter_image: @@ -612,7 +612,7 @@ *} print_translation {* - [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}] *} -- {* to avoid eta-contraction of body *} lemma UNION_eq_Union_image: diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 17:13:49 2011 +0200 @@ -1924,12 +1924,12 @@ @{code NOT} (fm_of_term ps vs t') | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) = let - val (xn', p') = variant_abs (xn, xT, p); + val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; in @{code E} (fm_of_term ps vs' p) end | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) = let - val (xn', p') = variant_abs (xn, xT, p); + val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; in @{code A} (fm_of_term ps vs' p) end | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); @@ -1988,7 +1988,7 @@ else insert (op aconv) t acc | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a else insert (op aconv) t acc - | Abs p => term_bools acc (snd (variant_abs p)) + | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *) | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc end; diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 08 17:13:49 2011 +0200 @@ -2939,13 +2939,13 @@ | Const(@{const_name Orderings.less_eq},_)$p$q => @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q)) | Const(@{const_name Ex},_)$Abs(xn,xT,p) => - let val (xn', p') = variant_abs (xn,xT,p) + let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p) (* FIXME !? *) val x = Free(xn',xT) fun incr i = i + 1 val m0 = (x,0):: (map (apsnd incr) m) in @{code E} (fm_of_term m0 m' p') end | Const(@{const_name All},_)$Abs(xn,xT,p) => - let val (xn', p') = variant_abs (xn,xT,p) + let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p) (* FIXME !? *) val x = Free(xn',xT) fun incr i = i + 1 val m0 = (x,0):: (map (apsnd incr) m) diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/HOL.thy Fri Apr 08 17:13:49 2011 +0200 @@ -130,7 +130,7 @@ print_translation {* [(@{const_syntax The}, fn [Abs abs] => - let val (x, t) = atomic_abs_tr' abs + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_The"} $ x $ t end)] *} -- {* To avoid eta-contraction of body *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Fri Apr 08 17:13:49 2011 +0200 @@ -34,12 +34,12 @@ parse_translation {* (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *) - [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})]; + [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})]; *} print_translation {* [(@{const_syntax Abs_cfun}, fn [Abs abs] => - let val (x, t) = atomic_abs_tr' abs + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_cabs"} $ x $ t end)] *} -- {* To avoid eta-contraction of body *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Apr 08 17:13:49 2011 +0200 @@ -442,7 +442,7 @@ (* define syntax for case combinator *) (* TODO: re-implement case syntax using a parse translation *) local - fun syntax c = Syntax.mark_const (fst (dest_Const c)) + fun syntax c = Lexicon.mark_const (fst (dest_Const c)) fun xconst c = Long_Name.base_name (fst (dest_Const c)) fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con) fun showint n = string_of_int (n+1) diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Fri Apr 08 17:13:49 2011 +0200 @@ -47,10 +47,10 @@ *) fun transform thy (c, T, mx) = let - fun syntax b = Syntax.mark_const (Sign.full_bname thy b) + fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) val c1 = Binding.name_of c val c2 = c1 ^ "_cont_syntax" - val n = Syntax.mixfix_args mx + val n = Mixfix.mixfix_args mx in ((c, T, NoSyn), (Binding.name c2, change_arrow n T, mx), @@ -64,7 +64,7 @@ | is_contconst (_, _, Binder _) = false (* FIXME ? *) | is_contconst (c, T, mx) = let - val n = Syntax.mixfix_args mx handle ERROR msg => + val n = Mixfix.mixfix_args mx handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c)) in cfun_arity T >= n end diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 17:13:49 2011 +0200 @@ -132,7 +132,7 @@ (* rewrite (_pat x) => (succeed) *) (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *) [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}), - mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})]; + Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})]; *} text {* Printing Case expressions *} @@ -154,7 +154,7 @@ val abs = case t of Abs abs => abs | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); - val (x, t') = atomic_abs_tr' abs; + val (x, t') = Syntax_Trans.atomic_abs_tr' abs; in (Syntax.const @{syntax_const "_variable"} $ x, t') end | dest_LAM _ = raise Match; (* too few vars: abort translation *) @@ -497,7 +497,7 @@ (* syntax translations for pattern combinators *) local - fun syntax c = Syntax.mark_const (fst (dest_Const c)); + fun syntax c = Lexicon.mark_const (fst (dest_Const c)); fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]; val capp = app @{const_syntax Rep_cfun}; val capps = Library.foldl capp diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Apr 08 17:13:49 2011 +0200 @@ -26,7 +26,7 @@ print_translation {* [(@{const_syntax Eps}, fn [Abs abs] => - let val (x, t) = atomic_abs_tr' abs + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_Eps"} $ x $ t end)] *} -- {* to avoid eta-contraction of body *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Hoare/hoare_syntax.ML --- a/src/HOL/Hoare/hoare_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Hoare/hoare_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -26,9 +26,9 @@ (SOME x, SOME y) => x = y | _ => false); -fun mk_abstuple [x] body = Syntax.abs_tr [x, body] +fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] | mk_abstuple (x :: xs) body = - Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body]; + Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; fun mk_fbody x e [y] = if eq_idt (x, y) then e else y | mk_fbody x e (y :: xs) = diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 17:13:49 2011 +0200 @@ -76,11 +76,11 @@ print_translation {* let fun quote_tr' f (t :: ts) = - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | quote_tr' _ _ = raise Match; fun annquote_tr' f (r :: t :: ts) = - Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) + Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | annquote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); @@ -94,13 +94,13 @@ | annbexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f) - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) + quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f) + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | annassign_tr' _ = raise Match; fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $ @@ -115,13 +115,13 @@ in [(@{const_syntax Collect}, assert_tr'), (@{const_syntax Basic}, assign_tr'), - (@{const_syntax Cond}, bexp_tr' "_Cond"), - (@{const_syntax While}, bexp_tr' "_While_inv"), + (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), + (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"}), (@{const_syntax AnnBasic}, annassign_tr'), - (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"), - (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"), - (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"), - (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")] + (@{const_syntax AnnWhile}, annbexp_tr' @{syntax_const "_AnnWhile"}), + (@{const_syntax AnnAwait}, annbexp_tr' @{syntax_const "_AnnAwait"}), + (@{const_syntax AnnCond1}, annbexp_tr' @{syntax_const "_AnnCond1"}), + (@{const_syntax AnnCond2}, annbexp_tr' @{syntax_const "_AnnCond2"})] end; *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Hoare_Parallel/Quote_Antiquote.thy --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 17:13:49 2011 +0200 @@ -16,7 +16,7 @@ parse_translation {* let - fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t + fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, quote_tr)] end *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 17:13:49 2011 +0200 @@ -58,7 +58,7 @@ print_translation {* let fun quote_tr' f (t :: ts) = - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | quote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); @@ -68,8 +68,8 @@ | bexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; in [(@{const_syntax Collect}, assert_tr'), diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Apr 08 17:13:49 2011 +0200 @@ -11,8 +11,8 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax.typeT; - val spropT = Syntax.spropT; + val typeT = Syntax_Ext.typeT; + val spropT = Syntax_Ext.spropT; in Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Apr 08 17:13:49 2011 +0200 @@ -178,14 +178,14 @@ (* Compatibility. *) -val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix; +val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix; fun mk_syn thy c = - if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn - else Delimfix (Syntax.escape c) + if Lexicon.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn + else Delimfix (Syntax_Ext.escape c) fun quotename c = - if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c + if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c fun simple_smart_string_of_cterm ctxt0 ct = let @@ -454,7 +454,7 @@ val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table) val invented_isavar = Unsynchronized.ref 0 -fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s) +fun innocent_varname s = Lexicon.is_identifier s andalso not (String.isPrefix "u_" s) fun valid_boundvarname s = can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) (); diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Isar_Examples/Hoare.thy Fri Apr 08 17:13:49 2011 +0200 @@ -185,8 +185,8 @@ of the concrete syntactic representation of our Hoare language, the actual ``ML drivers'' is quite involved. Just note that the we re-use the basic quote/antiquote translations as already defined in - Isabelle/Pure (see \verb,Syntax.quote_tr, and - \verb,Syntax.quote_tr',). *} + Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and + @{ML Syntax_Trans.quote_tr'},). *} syntax "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000) @@ -215,7 +215,7 @@ parse_translation {* let - fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t + fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, quote_tr)] end *} @@ -228,7 +228,7 @@ print_translation {* let fun quote_tr' f (t :: ts) = - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | quote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); @@ -238,8 +238,8 @@ | bexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; in [(@{const_syntax Collect}, assert_tr'), diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Library/BigO.thy Fri Apr 08 17:13:49 2011 +0200 @@ -25,9 +25,6 @@ the form @{text "f < g + O(h)"}. \end{itemize} -See \verb,Complex/ex/BigO_Complex.thy, for additional lemmas that -require the \verb,HOL-Complex, logic image. - Note also since the Big O library includes rules that demonstrate set inclusion, to use the automated reasoners effectively with the library one should redeclare the theorem @{text "subsetI"} as an intro rule, diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Library/OptionalSugar.thy Fri Apr 08 17:13:49 2011 +0200 @@ -51,8 +51,8 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax.typeT; - val spropT = Syntax.spropT; + val typeT = Syntax_Ext.typeT; + val spropT = Syntax_Ext.spropT; in Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Library/reflection.ML Fri Apr 08 17:13:49 2011 +0200 @@ -125,7 +125,7 @@ Abs(xn,xT,ta) => ( let val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt - val (xn,ta) = variant_abs (xn,xT,ta) + val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta) (* FIXME !? *) val x = Free(xn,xT) val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of NONE => error "tryabsdecomp: Type not found in the Environement" diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 17:13:49 2011 +0200 @@ -32,7 +32,7 @@ let fun cart t u = Syntax.const @{type_syntax cart} $ t $ u; fun finite_cart_tr [t, u as Free (x, _)] = - if Syntax.is_tid x then + if Lexicon.is_tid x then cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) else cart t u | finite_cart_tr [t, u] = cart t u diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Orderings.thy Fri Apr 08 17:13:49 2011 +0200 @@ -638,8 +638,8 @@ print_translation {* let - val All_binder = Syntax.binder_name @{const_syntax All}; - val Ex_binder = Syntax.binder_name @{const_syntax Ex}; + val All_binder = Mixfix.binder_name @{const_syntax All}; + val Ex_binder = Mixfix.binder_name @{const_syntax Ex}; val impl = @{const_syntax HOL.implies}; val conj = @{const_syntax HOL.conj}; val less = @{const_syntax less}; @@ -660,7 +660,7 @@ Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' | _ => false); fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false); - fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P; + fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P; fun tr' q = (q, fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _), diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Product_Type.thy Fri Apr 08 17:13:49 2011 +0200 @@ -199,8 +199,8 @@ fun split_tr' [Abs (x, T, t as (Abs abs))] = (* split (%x y. t) => %(x,y) t *) let - val (y, t') = atomic_abs_tr' abs; - val (x', t'') = atomic_abs_tr' (x, T, t'); + val (y, t') = Syntax_Trans.atomic_abs_tr' abs; + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); in Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' @@ -210,7 +210,7 @@ let val Const (@{syntax_const "_abs"}, _) $ (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t]; - val (x', t'') = atomic_abs_tr' (x, T, t'); + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); in Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x' $ @@ -221,7 +221,7 @@ split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *) | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = (* split (%pttrn z. t) => %(pttrn,z). t *) - let val (z, t) = atomic_abs_tr' abs in + let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t end @@ -239,8 +239,8 @@ | _ => let val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; - val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); - val (x', t'') = atomic_abs_tr' (x, xT, t'); + val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); in Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' @@ -251,8 +251,9 @@ | _ => let val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; - val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); - val (x', t'') = atomic_abs_tr' ("x", xT, t'); + val (y, t') = + Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); in Syntax.const @{syntax_const "_abs"} $ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' @@ -276,10 +277,10 @@ | _ => f ts; fun contract2 (Q,f) = (Q, contract Q f); val pairs = - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, - Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}, - Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, - Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] in map contract2 pairs end *} diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Set.thy Fri Apr 08 17:13:49 2011 +0200 @@ -231,8 +231,8 @@ print_translation {* let val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *) - val All_binder = Syntax.binder_name @{const_syntax All}; - val Ex_binder = Syntax.binder_name @{const_syntax Ex}; + val All_binder = Mixfix.binder_name @{const_syntax All}; + val Ex_binder = Mixfix.binder_name @{const_syntax Ex}; val impl = @{const_syntax HOL.implies}; val conj = @{const_syntax HOL.conj}; val sbset = @{const_syntax subset}; @@ -246,7 +246,7 @@ fun mk v v' c n P = if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n) - then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match; + then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match; fun tr' q = (q, fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)), @@ -275,7 +275,7 @@ parse_translation {* let - val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex})); + val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex})); fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1 | nvars _ = 1; @@ -291,13 +291,13 @@ *} print_translation {* - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, - Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}] + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}] *} -- {* to avoid eta-contraction of body *} print_translation {* let - val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY")); + val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY")); fun setcompr_tr' [Abs (abs as (_, _, P))] = let @@ -315,7 +315,7 @@ if check (P, 0) then tr' P else let - val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs; + val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs; val M = Syntax.const @{syntax_const "_Coll"} $ x $ t; in case t of diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Fri Apr 08 17:13:49 2011 +0200 @@ -643,8 +643,7 @@ *) val nums = (0 upto 10000); val nums' = (0 upto 3000); -val const_decls = map (fn i => Syntax.no_syn - ("const" ^ string_of_int i,Type ("nat",[]))) nums +val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums val consts = sort Term_Ord.fast_term_ord (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums) diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Fri Apr 08 17:13:49 2011 +0200 @@ -344,8 +344,6 @@ fun K_const T = Const ("StateFun.K_statefun",T --> T --> T); -val no_syn = #3 (Syntax.no_syn ((),())); - fun add_declaration name decl thy = thy diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Apr 08 17:13:49 2011 +0200 @@ -232,7 +232,7 @@ fun name_of_typ (Type (s, Ts)) = let val s' = Long_Name.base_name s in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @ - [if Syntax.is_identifier s' then s' else "x"]) + [if Lexicon.is_identifier s' then s' else "x"]) end | name_of_typ _ = ""; diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 17:13:49 2011 +0200 @@ -418,7 +418,7 @@ | _ => NONE); val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of; -val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT); +val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT); (* destruct nested patterns *) @@ -454,12 +454,12 @@ let val xs = Term.add_frees pat [] in Syntax.const @{syntax_const "_case1"} $ map_aterms - (fn Free p => Syntax.mark_boundT p - | Const (s, _) => Syntax.const (Syntax.mark_const s) + (fn Free p => Syntax_Trans.mark_boundT p + | Const (s, _) => Syntax.const (Lexicon.mark_const s) | t => t) pat $ map_aterms (fn x as Free (s, T) => - if member (op =) xs (s, T) then Syntax.mark_bound s else x + if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x | t => t) rhs end; in diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 17:13:49 2011 +0200 @@ -224,7 +224,7 @@ fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [], map (fn case_name => - let val case_name' = Syntax.mark_const case_name + let val case_name' = Lexicon.mark_const case_name in (case_name', Datatype_Case.case_tr' info_of_case case_name') end) case_names, []) thy; @@ -244,7 +244,7 @@ val (vs, cos) = the_spec thy dtco; val ty = Type (dtco, map TFree vs); val pretty_typ_bracket = - Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt); + Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt); fun pretty_constr (co, tys) = Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Apr 08 17:13:49 2011 +0200 @@ -49,7 +49,7 @@ fun type_name (TFree (name, _)) = unprefix "'" name | type_name (Type (name, _)) = let val name' = Long_Name.base_name name - in if Syntax.is_identifier name' then name' else "x" end; + in if Lexicon.is_identifier name' then name' else "x" end; in indexify_names (map type_name Ts) end; diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Apr 08 17:13:49 2011 +0200 @@ -579,13 +579,13 @@ else insert (op aconv) t | f $ a => if skip orelse is_op f then add_bools a o add_bools f else insert (op aconv) t - | Abs p => add_bools (snd (variant_abs p)) + | Abs p => add_bools (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *) | _ => if skip orelse is_op t then I else insert (op aconv) t end; fun descend vs (abs as (_, xT, _)) = let - val (xn', p') = variant_abs abs; + val (xn', p') = Syntax_Trans.variant_abs abs; (* FIXME !? *) in ((xn', xT) :: vs, p') end; local structure Proc = Cooper_Procedure in diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 08 17:13:49 2011 +0200 @@ -47,10 +47,9 @@ val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts) in Function.add_function - (map (fn (name, T) => - Syntax.no_syn (Binding.conceal (Binding.name name), SOME T)) - (names ~~ Ts)) - (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t) + (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn)) + (names ~~ Ts)) + (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t) Function_Common.default_config pat_completeness_auto #> snd #> Local_Theory.restore diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Apr 08 17:13:49 2011 +0200 @@ -99,7 +99,7 @@ fun needs_quoting reserved s = Symtab.defined reserved s orelse - exists (not o Syntax.is_identifier) (Long_Name.explode s) + exists (not o Lexicon.is_identifier) (Long_Name.explode s) fun make_name reserved multi j name = (name |> needs_quoting reserved name ? quote) ^ diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 08 17:13:49 2011 +0200 @@ -72,7 +72,7 @@ val unyxml = XML.content_of o YXML.parse_body -val is_long_identifier = forall Syntax.is_identifier o space_explode "." +val is_long_identifier = forall Lexicon.is_identifier o space_explode "." fun maybe_quote y = let val s = unyxml y in y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/choice_specification.ML Fri Apr 08 17:13:49 2011 +0200 @@ -160,7 +160,7 @@ let val T = type_of c val cname = Long_Name.base_name (fst (dest_Const c)) - val vname = if Syntax.is_identifier cname + val vname = if Lexicon.is_identifier cname then cname else "x" in diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/float_syntax.ML --- a/src/HOL/Tools/float_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/float_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -27,7 +27,7 @@ fun mk_frac str = let - val {mant = i, exp = n} = Syntax.read_float str; + val {mant = i, exp = n} = Lexicon.read_float str; val exp = Syntax.const @{const_syntax Power.power}; val ten = mk_number 10; val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/numeral_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -22,7 +22,7 @@ fun mk 0 = Syntax.const @{const_name Int.Pls} | mk ~1 = Syntax.const @{const_name Int.Min} | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; - in mk (#value (Syntax.read_xnum num)) end; + in mk (#value (Lexicon.read_xnum num)) end; in diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/record.ML Fri Apr 08 17:13:49 2011 +0200 @@ -715,7 +715,7 @@ val more' = mk_ext rest; in list_comb - (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more']) + (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more']) end | NONE => err ("no fields defined for " ^ ext)) | NONE => err (name ^ " is no proper field")) @@ -760,7 +760,7 @@ let val (args, rest) = split_args (map fst (fst (split_last fields))) fargs; val more' = mk_ext rest; - in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end + in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end | NONE => err ("no fields defined for " ^ ext)) | NONE => err (name ^ " is no proper field")) | mk_ext [] = more; @@ -889,14 +889,14 @@ fun record_ext_type_tr' name = let - val ext_type_name = Syntax.mark_type (suffix ext_typeN name); + val ext_type_name = Lexicon.mark_type (suffix ext_typeN name); fun tr' ctxt ts = record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts)); in (ext_type_name, tr') end; fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name = let - val ext_type_name = Syntax.mark_type (suffix ext_typeN name); + val ext_type_name = Lexicon.mark_type (suffix ext_typeN name); fun tr' ctxt ts = record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt (list_comb (Syntax.const ext_type_name, ts)); @@ -919,7 +919,7 @@ fun strip_fields t = (case strip_comb t of (Const (ext, _), args as (_ :: _)) => - (case try (Syntax.unmark_const o unsuffix extN) ext of + (case try (Lexicon.unmark_const o unsuffix extN) ext of SOME ext' => (case get_extfields thy ext' of SOME fields => @@ -946,7 +946,7 @@ fun record_ext_tr' name = let - val ext_name = Syntax.mark_const (name ^ extN); + val ext_name = Lexicon.mark_const (name ^ extN); fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts)); in (ext_name, tr') end; @@ -956,14 +956,14 @@ local fun dest_update ctxt c = - (case try Syntax.unmark_const c of + (case try Lexicon.unmark_const c of SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d) | NONE => NONE); fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = (case dest_update ctxt c of SOME name => - (case try Syntax.const_abs_tr' k of + (case try Syntax_Trans.const_abs_tr' k of SOME t => apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t)) (field_updates_tr' ctxt u) @@ -982,7 +982,7 @@ fun field_update_tr' name = let - val update_name = Syntax.mark_const (name ^ updateN); + val update_name = Lexicon.mark_const (name ^ updateN); fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u) | tr' _ _ = raise Match; in (update_name, tr') end; diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/string_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -16,11 +16,11 @@ (* nibble *) val mk_nib = - Ast.Constant o Syntax.mark_const o + Ast.Constant o Lexicon.mark_const o fst o Term.dest_Const o HOLogic.mk_nibble; fun dest_nib (Ast.Constant s) = - (case try Syntax.unmark_const s of + (case try Lexicon.unmark_const s of NONE => raise Match | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match)); @@ -44,11 +44,12 @@ | dest_char _ = raise Match; fun syntax_string cs = - Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)]; + Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, + Ast.Variable (Lexicon.implode_xstr cs)]; fun char_ast_tr [Ast.Variable xstr] = - (case Syntax.explode_xstr xstr of + (case Lexicon.explode_xstr xstr of [c] => mk_char c | _ => error ("Single character expected: " ^ xstr)) | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts); @@ -65,7 +66,7 @@ Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs]; fun string_ast_tr [Ast.Variable xstr] = - (case Syntax.explode_xstr xstr of + (case Lexicon.explode_xstr xstr of [] => Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/Tools/typedef.ML Fri Apr 08 17:13:49 2011 +0200 @@ -144,7 +144,7 @@ error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT)); val goal = mk_inhabited set; - val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT)); + val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT)); (* lhs *) diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/ex/Antiquote.thy --- a/src/HOL/ex/Antiquote.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/ex/Antiquote.thy Fri Apr 08 17:13:49 2011 +0200 @@ -25,11 +25,13 @@ where "Expr exp env = exp env" parse_translation {* - [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] + [Syntax_Trans.quote_antiquote_tr + @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] *} print_translation {* - [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] + [Syntax_Trans.quote_antiquote_tr' + @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] *} term "EXPR (a + b + c)" diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/ex/Binary.thy Fri Apr 08 17:13:49 2011 +0200 @@ -191,11 +191,11 @@ parse_translation {* let val syntax_consts = - map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a); + map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a); fun binary_tr [Const (num, _)] = let - val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num; + val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num; val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num); in syntax_consts (mk_binary n) end | binary_tr ts = raise TERM ("binary_tr", ts); diff -r 12635bb655fd -r c2b5dbb76b7e src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Fri Apr 08 16:31:14 2011 +0200 +++ b/src/HOL/ex/Numeral.thy Fri Apr 08 17:13:49 2011 +0200 @@ -285,7 +285,7 @@ else raise Match; fun numeral_tr [Free (num, _)] = let - val {leading_zeros, value, ...} = Syntax.read_xnum num; + val {leading_zeros, value, ...} = Lexicon.read_xnum num; val _ = leading_zeros = 0 andalso value > 0 orelse error ("Bad numeral: " ^ num); in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/IsaMakefile Fri Apr 08 17:13:49 2011 +0200 @@ -184,10 +184,10 @@ Syntax/parser.ML \ Syntax/printer.ML \ Syntax/simple_syntax.ML \ - Syntax/syn_ext.ML \ - Syntax/syn_trans.ML \ Syntax/syntax.ML \ + Syntax/syntax_ext.ML \ Syntax/syntax_phases.ML \ + Syntax/syntax_trans.ML \ Syntax/term_position.ML \ System/isabelle_process.ML \ System/isabelle_system.ML \ diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Apr 08 17:13:49 2011 +0200 @@ -382,14 +382,14 @@ val config = coerce config_value; in (config, register_config config_value) end; -val config_bool = declare_config Config.Bool Config.bool false; -val config_int = declare_config Config.Int Config.int false; -val config_real = declare_config Config.Real Config.real false; +val config_bool = declare_config Config.Bool Config.bool false; +val config_int = declare_config Config.Int Config.int false; +val config_real = declare_config Config.Real Config.real false; val config_string = declare_config Config.String Config.string false; -val config_bool_global = declare_config Config.Bool Config.bool true; -val config_int_global = declare_config Config.Int Config.int true; -val config_real_global = declare_config Config.Real Config.real true; +val config_bool_global = declare_config Config.Bool Config.bool true; +val config_int_global = declare_config Config.Int Config.int true; +val config_real_global = declare_config Config.Real Config.real true; val config_string_global = declare_config Config.String Config.string true; end; @@ -398,16 +398,16 @@ (* theory setup *) val _ = Context.>> (Context.map_theory - (register_config Ast.ast_trace_raw #> - register_config Ast.ast_stat_raw #> + (register_config Ast.trace_raw #> + register_config Ast.stat_raw #> register_config Syntax.positions_raw #> - register_config Syntax.show_brackets_raw #> - register_config Syntax.show_sorts_raw #> - register_config Syntax.show_types_raw #> - register_config Syntax.show_structs_raw #> - register_config Syntax.show_question_marks_raw #> + register_config Printer.show_brackets_raw #> + register_config Printer.show_sorts_raw #> + register_config Printer.show_types_raw #> + register_config Printer.show_structs_raw #> + register_config Printer.show_question_marks_raw #> register_config Syntax.ambiguity_level_raw #> - register_config Syntax.eta_contract_raw #> + register_config Syntax_Trans.eta_contract_raw #> register_config ML_Context.trace_raw #> register_config ProofContext.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/auto_bind.ML --- a/src/Pure/Isar/auto_bind.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/auto_bind.ML Fri Apr 08 17:13:49 2011 +0200 @@ -45,8 +45,8 @@ fun facts _ [] = [] | facts thy props = let val prop = List.last props - in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end; + in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end; -val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)]; +val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)]; end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/element.ML Fri Apr 08 17:13:49 2011 +0200 @@ -169,7 +169,7 @@ val prt_name_atts = pretty_name_atts ctxt; fun prt_mixfix NoSyn = [] - | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; + | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx]; fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") :: Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/expression.ML Fri Apr 08 17:13:49 2011 +0200 @@ -613,7 +613,7 @@ (* achieve plain syntax for locale predicates (without "PROP") *) -fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args => +fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args => if length args = n then Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Apr 08 17:13:49 2011 +0200 @@ -42,7 +42,7 @@ ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ (if mx = NoSyn then "" - else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx))); + else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); NoSyn); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Apr 08 17:13:49 2011 +0200 @@ -231,7 +231,7 @@ handle Type.TUNIFY => err ("Failed to unify variable " ^ string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ - string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; + string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule; val (tyenv, _) = fold unify (map #1 vars ~~ take m params) (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); val norm_type = Envir.norm_type tyenv; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/parse.ML Fri Apr 08 17:13:49 2011 +0200 @@ -305,7 +305,7 @@ val fixes = and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) || - params >> map Syntax.no_syn) >> flat; + params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) []; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/parse_spec.ML Fri Apr 08 17:13:49 2011 +0200 @@ -87,7 +87,7 @@ val locale_fixes = Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix >> (single o Parse.triple1) || - Parse.params >> map Syntax.no_syn) >> flat; + Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; val locale_insts = Scan.optional diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/proof.ML Fri Apr 08 17:13:49 2011 +0200 @@ -566,7 +566,7 @@ val write_cmd = gen_write (fn ctxt => fn (c, mx) => - (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx)); + (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx)); end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Apr 08 17:13:49 2011 +0200 @@ -447,7 +447,7 @@ val tsig = tsig_of ctxt; val (c, pos) = token_content text; in - if Syntax.is_tid c then + if Lexicon.is_tid c then (Context_Position.report ctxt pos Markup.tfree; TFree (c, default_sort ctxt (c, ~1))) else @@ -915,7 +915,7 @@ (* variables *) fun declare_var (x, opt_T, mx) ctxt = - let val T = (case opt_T of SOME T => T | NONE => Syntax.mixfixT mx) + let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx) in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end; local @@ -924,7 +924,7 @@ fold_map (fn (b, raw_T, mx) => fn ctxt => let val x = Name.of_binding b; - val _ = Syntax.is_identifier (no_skolem internal x) orelse + val _ = Lexicon.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ quote (Binding.str_of b)); fun cond_tvars T = @@ -949,7 +949,7 @@ fun const_ast_tr intern ctxt [Ast.Variable c] = let val Const (c', _) = read_const_proper ctxt false c; - val d = if intern then Syntax.mark_const c' else c; + val d = if intern then Lexicon.mark_const c' else c; in Ast.Constant d end | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts); @@ -978,13 +978,13 @@ local fun type_syntax (Type (c, args), mx) = - SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx)) + SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx)) | type_syntax _ = NONE; fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of ctxt)) c of - SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx)) + SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) | NONE => NONE) | const_syntax _ _ = NONE; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Isar/token.ML Fri Apr 08 17:13:49 2011 +0200 @@ -279,7 +279,7 @@ fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true - | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s; + | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s; (* scan verbatim text *) @@ -335,13 +335,13 @@ (Scan.max token_leq (Scan.literal lex2 >> pair Command) (Scan.literal lex1 >> pair Keyword)) - (Syntax.scan_longid >> pair LongIdent || - Syntax.scan_id >> pair Ident || - Syntax.scan_var >> pair Var || - Syntax.scan_tid >> pair TypeIdent || - Syntax.scan_tvar >> pair TypeVar || - Syntax.scan_float >> pair Float || - Syntax.scan_nat >> pair Nat || + (Lexicon.scan_longid >> pair LongIdent || + Lexicon.scan_id >> pair Ident || + Lexicon.scan_var >> pair Var || + Lexicon.scan_tid >> pair TypeIdent || + Lexicon.scan_tvar >> pair TypeVar || + Lexicon.scan_float >> pair Float || + Lexicon.scan_nat >> pair Nat || scan_symid >> pair SymIdent) >> uncurry token)); fun recover msg = diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Fri Apr 08 17:13:49 2011 +0200 @@ -23,8 +23,6 @@ (** ML system and platform related **) -val forget_structure = PolyML.Compiler.forgetStructure; - val _ = PolyML.Compiler.forgetValue "isSome"; val _ = PolyML.Compiler.forgetValue "getOpt"; val _ = PolyML.Compiler.forgetValue "valOf"; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Apr 08 17:13:49 2011 +0200 @@ -103,8 +103,6 @@ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); in use_text context (1, name) verbose txt end; -fun forget_structure _ = (); - (* toplevel pretty printing *) diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Fri Apr 08 17:13:49 2011 +0200 @@ -105,7 +105,7 @@ fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => ProofContext.read_class ctxt s - |> syn ? Syntax.mark_class + |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); val _ = inline "class" (class false); @@ -131,7 +131,7 @@ val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c)); val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)); val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)); -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c)); +val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c)); (* constants *) @@ -146,7 +146,7 @@ val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c))); val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))); -val _ = inline "const_syntax" (const_name (fn (_, c) => Syntax.mark_const c)); +val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c)); val _ = inline "syntax_const" diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ML/ml_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -34,7 +34,7 @@ (* reserved words *) -val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords; +val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords; val reserved = Name.make_context reserved_names; val is_reserved = Name.is_declared reserved; @@ -42,7 +42,7 @@ (* identifiers *) fun is_identifier name = - not (is_reserved name) andalso Syntax.is_ascii_identifier name; + not (is_reserved name) andalso Lexicon.is_ascii_identifier name; (* literal output -- unformatted *) diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -66,8 +66,8 @@ ("", paramT --> paramsT, Delimfix "_")] |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\_./ _)", [0, 3], 3)), - (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule @@ -80,10 +80,10 @@ (Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam1") [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], - Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A", + Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A", (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], - Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst")) + Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst")) [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Apr 08 17:13:49 2011 +0200 @@ -115,25 +115,25 @@ val display_preferences = - [bool_pref show_types_default + [bool_pref Printer.show_types_default "show-types" "Include types in display of Isabelle terms", - bool_pref show_sorts_default + bool_pref Printer.show_sorts_default "show-sorts" "Include sorts in display of Isabelle terms", - bool_pref show_consts_default + bool_pref Goal_Display.show_consts_default "show-consts" "Show types of consts in Isabelle goal display", bool_pref long_names "long-names" "Show fully qualified names in Isabelle terms", - bool_pref show_brackets_default + bool_pref Printer.show_brackets_default "show-brackets" "Show full bracketing in Isabelle terms", bool_pref Goal_Display.show_main_goal_default "show-main-goal" "Show main goal in proof state display", - bool_pref Syntax.eta_contract_default + bool_pref Syntax_Trans.eta_contract_default "eta-contract" "Print terms eta-contracted"]; @@ -142,7 +142,7 @@ "goals-limit" "Setting for maximum number of goals printed", print_depth_pref, - bool_pref show_question_marks_default + bool_pref Printer.show_question_marks_default "show-question-marks" "Show leading question mark of variable name"]; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/ROOT.ML Fri Apr 08 17:13:49 2011 +0200 @@ -122,9 +122,9 @@ use "Syntax/lexicon.ML"; use "Syntax/simple_syntax.ML"; use "Syntax/ast.ML"; -use "Syntax/syn_ext.ML"; +use "Syntax/syntax_ext.ML"; use "Syntax/parser.ML"; -use "Syntax/syn_trans.ML"; +use "Syntax/syntax_trans.ML"; use "Syntax/mixfix.ML"; use "Syntax/printer.ML"; use "Syntax/syntax.ML"; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/ast.ML Fri Apr 08 17:13:49 2011 +0200 @@ -21,10 +21,10 @@ val fold_ast_p: string -> ast list * ast -> ast val unfold_ast: string -> ast -> ast list val unfold_ast_p: string -> ast -> ast list * ast - val ast_trace_raw: Config.raw - val ast_trace: bool Config.T - val ast_stat_raw: Config.raw - val ast_stat: bool Config.T + val trace_raw: Config.raw + val trace: bool Config.T + val stat_raw: Config.raw + val stat: bool Config.T val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast end; @@ -164,11 +164,11 @@ (* normalize *) -val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false); -val ast_trace = Config.bool ast_trace_raw; +val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false); +val trace = Config.bool trace_raw; -val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false); -val ast_stat = Config.bool ast_stat_raw; +val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false); +val stat = Config.bool stat_raw; fun message head body = Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); @@ -176,8 +176,8 @@ (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) fun normalize ctxt get_rules pre_ast = let - val trace = Config.get ctxt ast_trace; - val stat = Config.get ctxt ast_stat; + val trace = Config.get ctxt trace; + val stat = Config.get ctxt stat; val passes = Unsynchronized.ref 0; val failed_matches = Unsynchronized.ref 0; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/lexicon.ML Fri Apr 08 17:13:49 2011 +0200 @@ -4,10 +4,11 @@ Lexer for the inner Isabelle syntax (terms and types). *) -signature LEXICON0 = +signature LEXICON = sig val is_identifier: string -> bool val is_ascii_identifier: string -> bool + val is_xid: string -> bool val is_tid: string -> bool val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list @@ -19,37 +20,6 @@ val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list - val implode_xstr: string list -> string - val explode_xstr: string -> string list - val read_indexname: string -> indexname - val read_var: string -> term - val read_variable: string -> indexname option - val const: string -> term - val free: string -> term - val var: indexname -> term - val read_nat: string -> int option - val read_int: string -> int option - val read_xnum: string -> {radix: int, leading_zeros: int, value: int} - val read_float: string -> {mant: int, exp: int} - val mark_class: string -> string val unmark_class: string -> string - val mark_type: string -> string val unmark_type: string -> string - val mark_const: string -> string val unmark_const: string -> string - val mark_fixed: string -> string val unmark_fixed: string -> string - val unmark: - {case_class: string -> 'a, - case_type: string -> 'a, - case_const: string -> 'a, - case_fixed: string -> 'a, - case_default: string -> 'a} -> string -> 'a - val is_marked: string -> bool - val dummy_type: term - val fun_type: term -end; - -signature LEXICON = -sig - include LEXICON0 - val is_xid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF @@ -73,7 +43,32 @@ val matching_tokens: token * token -> bool val valued_token: token -> bool val predef_term: string -> token option + val implode_xstr: string list -> string + val explode_xstr: string -> string list val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list + val read_indexname: string -> indexname + val const: string -> term + val free: string -> term + val var: indexname -> term + val read_var: string -> term + val read_variable: string -> indexname option + val read_nat: string -> int option + val read_int: string -> int option + val read_xnum: string -> {radix: int, leading_zeros: int, value: int} + val read_float: string -> {mant: int, exp: int} + val mark_class: string -> string val unmark_class: string -> string + val mark_type: string -> string val unmark_type: string -> string + val mark_const: string -> string val unmark_const: string -> string + val mark_fixed: string -> string val unmark_fixed: string -> string + val unmark: + {case_class: string -> 'a, + case_type: string -> 'a, + case_const: string -> 'a, + case_fixed: string -> 'a, + case_default: string -> 'a} -> string -> 'a + val is_marked: string -> bool + val dummy_type: term + val fun_type: term end; structure Lexicon: LEXICON = @@ -352,37 +347,6 @@ in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end; -(* logical entities *) - -fun marker s = (prefix s, unprefix s); - -val (mark_class, unmark_class) = marker "\\<^class>"; -val (mark_type, unmark_type) = marker "\\<^type>"; -val (mark_const, unmark_const) = marker "\\<^const>"; -val (mark_fixed, unmark_fixed) = marker "\\<^fixed>"; - -fun unmark {case_class, case_type, case_const, case_fixed, case_default} s = - (case try unmark_class s of - SOME c => case_class c - | NONE => - (case try unmark_type s of - SOME c => case_type c - | NONE => - (case try unmark_const s of - SOME c => case_const c - | NONE => - (case try unmark_fixed s of - SOME c => case_fixed c - | NONE => case_default s)))); - -val is_marked = - unmark {case_class = K true, case_type = K true, case_const = K true, - case_fixed = K true, case_default = K false}; - -val dummy_type = const (mark_type "dummy"); -val fun_type = const (mark_type "fun"); - - (* read numbers *) local @@ -456,4 +420,35 @@ exp = length fracpart} end; + +(* marked logical entities *) + +fun marker s = (prefix s, unprefix s); + +val (mark_class, unmark_class) = marker "\\<^class>"; +val (mark_type, unmark_type) = marker "\\<^type>"; +val (mark_const, unmark_const) = marker "\\<^const>"; +val (mark_fixed, unmark_fixed) = marker "\\<^fixed>"; + +fun unmark {case_class, case_type, case_const, case_fixed, case_default} s = + (case try unmark_class s of + SOME c => case_class c + | NONE => + (case try unmark_type s of + SOME c => case_type c + | NONE => + (case try unmark_const s of + SOME c => case_const c + | NONE => + (case try unmark_fixed s of + SOME c => case_fixed c + | NONE => case_default s)))); + +val is_marked = + unmark {case_class = K true, case_type = K true, case_const = K true, + case_fixed = K true, case_default = K false}; + +val dummy_type = const (mark_type "dummy"); +val fun_type = const (mark_type "fun"); + end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/local_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -58,11 +58,11 @@ | update_gram ((false, add, m), decls) = Syntax.update_const_gram add (Sign.is_logtype thy) m decls; - val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; + val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs; val local_syntax = thy_syntax |> Syntax.update_trfuns - (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, - map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') + (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs, + map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs') |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; @@ -83,7 +83,7 @@ | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) | prep_mixfix add mode (Fixed, (x, T, mx)) = - SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx))); + SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); fun prep_struct (Fixed, (c, _, Structure)) = SOME c | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c) diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Apr 08 17:13:49 2011 +0200 @@ -4,7 +4,7 @@ Mixfix declarations, infixes, binders. *) -signature MIXFIX0 = +signature BASIC_MIXFIX = sig datatype mixfix = NoSyn | @@ -15,30 +15,23 @@ Infixr of string * int | Binder of string * int * int | Structure - val binder_name: string -> string end; -signature MIXFIX1 = +signature MIXFIX = sig - include MIXFIX0 - val no_syn: 'a * 'b -> 'a * 'b * mixfix + include BASIC_MIXFIX val pretty_mixfix: mixfix -> Pretty.T val mixfix_args: mixfix -> int val mixfixT: mixfix -> typ val make_type: int -> typ -end; - -signature MIXFIX = -sig - include MIXFIX1 - val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext - val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext + val binder_name: string -> string + val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext + val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext end; structure Mixfix: MIXFIX = struct - (** mixfix declarations **) datatype mixfix = @@ -51,8 +44,6 @@ Binder of string * int * int | Structure; -fun no_syn (x, y) = (x, y, NoSyn); - (* pretty_mixfix *) @@ -83,11 +74,11 @@ (* syntax specifications *) fun mixfix_args NoSyn = 0 - | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy - | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy - | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy - | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy - | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy + | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy + | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy + | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy + | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy + | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy | mixfix_args (Binder _) = 1 | mixfix_args Structure = 0; @@ -97,29 +88,29 @@ (* syn_ext_types *) -fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT; +fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT; fun syn_ext_types type_decls = let - fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3); + fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3); fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p)) - | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri)) + | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p)) + | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri)) | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p) | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p) | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); - fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) = - if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then () - else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix + fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) = + if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () + else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix | check_args _ NONE = (); val mfix = map mfix_of type_decls; val _ = map2 check_args type_decls mfix; val xconsts = map #1 type_decls; - in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end; + in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end; (* syn_ext_consts *) @@ -130,21 +121,21 @@ fun syn_ext_consts is_logtype const_decls = let fun mk_infix sy ty c p1 p2 p3 = - [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri), - Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; + [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri), + Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 | binder_typ c _ = error ("Bad type of binder: " ^ quote c); fun mfix_of (_, _, NoSyn) = [] - | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)] - | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)] + | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)] + | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)] | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p | mfix_of (c, ty, Binder (sy, p, q)) = - [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] + [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); fun binder (c, _, Binder _) = SOME (binder_name c, c) @@ -154,13 +145,17 @@ val xconsts = map #1 const_decls; val binders = map_filter binder const_decls; val binder_trs = binders - |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr); + |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr); val binder_trs' = binders - |> map (Syn_Ext.stamp_trfun binder_stamp o - apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap); + |> map (Syntax_Ext.stamp_trfun binder_stamp o + apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap); in - Syn_Ext.syn_ext' true is_logtype + Syntax_Ext.syn_ext' true is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], []) end; end; + +structure Basic_Mixfix: BASIC_MIXFIX = Mixfix; +open Basic_Mixfix; + diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/parser.ML Fri Apr 08 17:13:49 2011 +0200 @@ -8,7 +8,7 @@ sig type gram val empty_gram: gram - val extend_gram: Syn_Ext.xprod list -> gram -> gram + val extend_gram: Syntax_Ext.xprod list -> gram -> gram val merge_gram: gram * gram -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = @@ -468,10 +468,10 @@ delimiters and predefined terms are stored as terminals, nonterminals are converted to integer tags*) fun symb_of [] nt_count tags result = (nt_count, tags, rev result) - | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result = + | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = symb_of ss nt_count tags (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result) - | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result = + | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = let val (nt_count', tags', new_symb) = (case Lexicon.predef_term s of @@ -485,7 +485,7 @@ (*Convert list of productions by invoking symb_of for each of them*) fun prod_of [] nt_count prod_count tags result = (nt_count, prod_count, tags, result) - | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps) + | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps) nt_count prod_count tags result = let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; @@ -699,15 +699,16 @@ fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = - if Lexicon.valued_token c then (A, j, Tip c :: ts, sa, id, i) + if Lexicon.valued_token c orelse id <> "" + then (A, j, Tip c :: ts, sa, id, i) else (A, j, ts, sa, id, i); fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) = - (A, j, List.revAppend (tt, ts), sa, id, i); + (A, j, tt @ ts, sa, id, i); fun movedot_lambda [] _ = [] | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) = - if k <= ki then (B, j, List.revAppend (t, tss), sa, id, i) :: movedot_lambda ts state + if k <= ki then (B, j, t @ tss, sa, id, i) :: movedot_lambda ts state else movedot_lambda ts state; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/printer.ML Fri Apr 08 17:13:49 2011 +0200 @@ -4,34 +4,34 @@ Pretty printing of asts, terms, types and print (ast) translation. *) -signature PRINTER0 = +signature BASIC_PRINTER = sig - val show_brackets_default: bool Unsynchronized.ref - val show_brackets_raw: Config.raw val show_brackets: bool Config.T - val show_types_default: bool Unsynchronized.ref - val show_types_raw: Config.raw val show_types: bool Config.T - val show_sorts_default: bool Unsynchronized.ref - val show_sorts_raw: Config.raw val show_sorts: bool Config.T val show_free_types: bool Config.T val show_all_types: bool Config.T - val show_structs_raw: Config.raw val show_structs: bool Config.T - val show_question_marks_default: bool Unsynchronized.ref - val show_question_marks_raw: Config.raw val show_question_marks: bool Config.T val pretty_priority: int Config.T end; signature PRINTER = sig - include PRINTER0 + include BASIC_PRINTER + val show_brackets_default: bool Unsynchronized.ref + val show_brackets_raw: Config.raw + val show_types_default: bool Unsynchronized.ref + val show_types_raw: Config.raw + val show_sorts_default: bool Unsynchronized.ref + val show_sorts_raw: Config.raw + val show_structs_raw: Config.raw + val show_question_marks_default: bool Unsynchronized.ref + val show_question_marks_raw: Config.raw type prtabs val empty_prtabs: prtabs - val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs - val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs + val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs + val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs val merge_prtabs: prtabs -> prtabs -> prtabs val pretty_term_ast: bool -> Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> @@ -93,29 +93,29 @@ (* xprod_to_fmt *) -fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE - | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) = +fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE + | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) = let fun arg (s, p) = (if s = "type" then TypArg else Arg) - (if Lexicon.is_terminal s then Syn_Ext.max_pri else p); + (if Lexicon.is_terminal s then Syntax_Ext.max_pri else p); - fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) = + fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) = apfst (cons (String s)) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) = apfst (cons (arg s_p)) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syn_Ext.Space s :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) = apfst (cons (Space s)) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) = let val (bsyms, xsyms') = xsyms_to_syms xsyms; val (syms, xsyms'') = xsyms_to_syms xsyms'; in (Block (i, bsyms) :: syms, xsyms'') end - | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) = apfst (cons (Break i)) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms) + | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms) | xsyms_to_syms [] = ([], []); fun nargs (Arg _ :: syms) = nargs syms + 1 @@ -145,7 +145,7 @@ fun remove_prtabs mode xprods prtabs = let val tab = mode_tab prtabs mode; - val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) => + val fmts = map_filter (fn xprod as Syntax_Ext.XProd (_, _, c, _) => if null (Symtab.lookup_list tab c) then NONE else xprod_to_fmt xprod) xprods; val tab' = fold (Symtab.remove_list (op =)) fmts tab; @@ -173,9 +173,9 @@ (*default applications: prefix / postfix*) val appT = - if type_mode then Syn_Trans.tappl_ast_tr' - else if curried then Syn_Trans.applC_ast_tr' - else Syn_Trans.appl_ast_tr'; + if type_mode then Syntax_Trans.tappl_ast_tr' + else if curried then Syntax_Trans.applC_ast_tr' + else Syntax_Trans.appl_ast_tr'; fun synT _ ([], args) = ([], args) | synT m (Arg p :: symbs, t :: args) = @@ -210,10 +210,12 @@ val T = if i < 0 then Pretty.fbrk else Pretty.brk i; in (T :: Ts, args') end - and parT m (pr, args, p, p': int) = #1 (synT m - (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr)) - then [Block (1, Space "(" :: pr @ [Space ")"])] - else pr, args)) + and parT m (pr, args, p, p': int) = + #1 (synT m + (if p > p' orelse + (show_brackets andalso p' <> Syntax_Ext.max_pri andalso not (is_chain pr)) + then [Block (1, Space "(" :: pr @ [Space ")"])] + else pr, args)) and atomT a = Pretty.marks_str (markup_extern a) @@ -265,3 +267,7 @@ pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast; end; + +structure Basic_Printer: BASIC_PRINTER = Printer; +open Basic_Printer; + diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/simple_syntax.ML --- a/src/Pure/Syntax/simple_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/simple_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -17,7 +17,7 @@ (* scanning tokens *) val lexicon = Scan.make_lexicon - (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&&", "CONST"]); + (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=>", "&&&", "CONST"]); fun read scan s = (case @@ -79,7 +79,6 @@ term1 = term2 ==> ... ==> term2 | term2 term2 = term3 == term2 - | term3 =?= term2 | term3 &&& term2 | term3 term3 = ident :: typ @@ -109,7 +108,7 @@ (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies || term2 env T) x and term2 env T x = - (equal env "==" || equal env "=?=" || + (equal env "==" || term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction || term3 env T) x and equal env eq x = diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Fri Apr 08 16:31:14 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,389 +0,0 @@ -(* Title: Pure/Syntax/syn_ext.ML - Author: Markus Wenzel and Carsten Clasohm, TU Muenchen - -Syntax extension (internal interface). -*) - -signature SYN_EXT0 = -sig - val dddot_indexname: indexname - val typeT: typ - val spropT: typ - val default_root: string Config.T - val max_pri: int - val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp) - val mk_trfun: string * 'a -> string * ('a * stamp) - val eq_trfun: ('a * stamp) * ('a * stamp) -> bool - val escape: string -> string - val token_markers: string list -end; - -signature SYN_EXT = -sig - include SYN_EXT0 - val logic: string - val args: string - val cargs: string - val any: string - val sprop: string - datatype mfix = Mfix of string * typ * string * int list * int - val err_in_mfix: string -> mfix -> 'a - val typ_to_nonterm: typ -> string - datatype xsymb = - Delim of string | - Argument of string * int | - Space of string | - Bg of int | Brk of int | En - datatype xprod = XProd of string * xsymb list * string * int - val chain_pri: int - val delims_of: xprod list -> string list list - datatype syn_ext = - Syn_Ext of { - xprods: xprod list, - consts: string list, - parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, - parse_rules: (Ast.ast * Ast.ast) list, - parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, - print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, - print_rules: (Ast.ast * Ast.ast) list, - print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} - val mfix_delims: string -> string list - val mfix_args: string -> int - val syn_ext': bool -> (string -> bool) -> mfix list -> - string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * - (string * ((Proof.context -> term list -> term) * stamp)) list * - (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> - (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext: mfix list -> string list -> - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * - (string * ((Proof.context -> term list -> term) * stamp)) list * - (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> - (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_const_names: string list -> syn_ext - val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_trfuns: - (string * ((Ast.ast list -> Ast.ast) * stamp)) list * - (string * ((term list -> term) * stamp)) list * - (string * ((typ -> term list -> term) * stamp)) list * - (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext - val syn_ext_advanced_trfuns: - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * - (string * ((Proof.context -> term list -> term) * stamp)) list * - (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext - val pure_ext: syn_ext -end; - -structure Syn_Ext: SYN_EXT = -struct - - -(** misc definitions **) - -val dddot_indexname = ("dddot", 0); - - -(* syntactic categories *) - -val logic = "logic"; -val logicT = Type (logic, []); - -val args = "args"; -val cargs = "cargs"; - -val typeT = Type ("type", []); - -val sprop = "#prop"; -val spropT = Type (sprop, []); - -val any = "any"; -val anyT = Type (any, []); - -val default_root = - Config.string (Config.declare "Syntax.default_root" (K (Config.String any))); - - - -(** datatype xprod **) - -(*Delim s: delimiter s - Argument (s, p): nonterminal s requiring priority >= p, or valued token - Space s: some white space for printing - Bg, Brk, En: blocks and breaks for pretty printing*) - -datatype xsymb = - Delim of string | - Argument of string * int | - Space of string | - Bg of int | Brk of int | En; - -fun is_delim (Delim _) = true - | is_delim _ = false; - -fun is_terminal (Delim _) = true - | is_terminal (Argument (s, _)) = Lexicon.is_terminal s - | is_terminal _ = false; - -fun is_argument (Argument _) = true - | is_argument _ = false; - -fun is_index (Argument ("index", _)) = true - | is_index _ = false; - -val index = Argument ("index", 1000); - - -(*XProd (lhs, syms, c, p): - lhs: name of nonterminal on the lhs of the production - syms: list of symbols on the rhs of the production - c: head of parse tree - p: priority of this production*) - -datatype xprod = XProd of string * xsymb list * string * int; - -val max_pri = 1000; (*maximum legal priority*) -val chain_pri = ~1; (*dummy for chain productions*) - -fun delims_of xprods = - fold (fn XProd (_, xsymbs, _, _) => - fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods [] - |> map Symbol.explode; - - - -(** datatype mfix **) - -(*Mfix (sy, ty, c, ps, p): - sy: rhs of production as symbolic string - ty: type description of production - c: head of parse tree - ps: priorities of arguments in sy - p: priority of production*) - -datatype mfix = Mfix of string * typ * string * int list * int; - -fun err_in_mfix msg (Mfix (sy, _, const, _, _)) = - cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const); - - -(* typ_to_nonterm *) - -fun typ_to_nt _ (Type (c, _)) = c - | typ_to_nt default _ = default; - -(*get nonterminal for rhs*) -val typ_to_nonterm = typ_to_nt any; - -(*get nonterminal for lhs*) -val typ_to_nonterm1 = typ_to_nt logic; - - -(* read mixfix annotations *) - -local - -val is_meta = member (op =) ["(", ")", "/", "_", "\\"]; - -val scan_delim_char = - $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) || - Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular); - -fun read_int ["0", "0"] = ~1 - | read_int cs = #1 (Library.read_int cs); - -val scan_sym = - $$ "_" >> K (Argument ("", 0)) || - $$ "\\" >> K index || - $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) || - $$ ")" >> K En || - $$ "/" -- $$ "/" >> K (Brk ~1) || - $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) || - Scan.many1 Symbol.is_blank >> (Space o implode) || - Scan.repeat1 scan_delim_char >> (Delim o implode); - -val scan_symb = - scan_sym >> SOME || - $$ "'" -- Scan.one Symbol.is_blank >> K NONE; - -val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); -val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; - -fun unique_index xsymbs = - if length (filter is_index xsymbs) <= 1 then xsymbs - else error "Duplicate index arguments (\\)"; - -in - -val read_mfix = unique_index o read_symbs o Symbol.explode; - -fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; -val mfix_args = length o filter is_argument o read_mfix; - -val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; - -end; - - -(* mfix_to_xprod *) - -fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) = - let - fun check_pri p = - if p >= 0 andalso p <= max_pri then () - else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix; - - fun blocks_ok [] 0 = true - | blocks_ok [] _ = false - | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1) - | blocks_ok (En :: _) 0 = false - | blocks_ok (En :: syms) n = blocks_ok syms (n - 1) - | blocks_ok (_ :: syms) n = blocks_ok syms n; - - fun check_blocks syms = - if blocks_ok syms 0 then () - else err_in_mfix "Unbalanced block parentheses" mfix; - - - val cons_fst = apfst o cons; - - fun add_args [] ty [] = ([], typ_to_nonterm1 ty) - | add_args [] _ _ = err_in_mfix "Too many precedences" mfix - | add_args ((arg as Argument ("index", _)) :: syms) ty ps = - cons_fst arg (add_args syms ty ps) - | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] = - cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys []) - | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) = - cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps) - | add_args (Argument _ :: _) _ _ = - err_in_mfix "More arguments than in corresponding type" mfix - | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps); - - fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) - | rem_pri sym = sym; - - fun logify_types (a as (Argument (s, p))) = - if s <> "prop" andalso is_logtype s then Argument (logic, p) else a - | logify_types a = a; - - - val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix; - val args = filter (fn Argument _ => true | _ => false) raw_symbs; - val (const', typ', parse_rules) = - if not (exists is_index args) then (const, typ, []) - else - let - val indexed_const = - if const <> "" then const ^ "_indexed" - else err_in_mfix "Missing constant name for indexed syntax" mfix; - val rangeT = Term.range_type typ handle Match => - err_in_mfix "Missing structure argument for indexed syntax" mfix; - - val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1)); - val (xs1, xs2) = chop (find_index is_index args) xs; - val i = Ast.Variable "i"; - val lhs = Ast.mk_appl (Ast.Constant indexed_const) - (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); - val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs); - in (indexed_const, rangeT, [(lhs, rhs)]) end; - - val (symbs, lhs) = add_args raw_symbs typ' pris; - - val copy_prod = - (lhs = "prop" orelse lhs = "logic") - andalso const <> "" - andalso not (null symbs) - andalso not (exists is_delim symbs); - val lhs' = - if convert andalso not copy_prod then - (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs) - else lhs; - val symbs' = map logify_types symbs; - val xprod = XProd (lhs', symbs', const', pri); - - val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs'); - val xprod' = - if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix - else if const <> "" then xprod - else if length (filter is_argument symbs') <> 1 then - err_in_mfix "Copy production must have exactly one argument" mfix - else if exists is_terminal symbs' then xprod - else XProd (lhs', map rem_pri symbs', "", chain_pri); - - in (xprod', parse_rules) end; - - - -(** datatype syn_ext **) - -datatype syn_ext = - Syn_Ext of { - xprods: xprod list, - consts: string list, - parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, - parse_rules: (Ast.ast * Ast.ast) list, - parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, - print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, - print_rules: (Ast.ast * Ast.ast) list, - print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}; - - -(* syn_ext *) - -fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) = - let - val (parse_ast_translation, parse_translation, print_translation, - print_ast_translation) = trfuns; - - val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes - |> split_list |> apsnd (rev o flat); - val mfix_consts = - distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); - in - Syn_Ext { - xprods = xprods, - consts = union (op =) consts mfix_consts, - parse_ast_translation = parse_ast_translation, - parse_rules = parse_rules' @ parse_rules, - parse_translation = parse_translation, - print_translation = print_translation, - print_rules = map swap parse_rules' @ print_rules, - print_ast_translation = print_ast_translation} - end; - - -val syn_ext = syn_ext' true (K false); - -fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []); -fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; -fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []); - -fun syn_ext_trfuns (atrs, trs, tr's, atr's) = - let fun simple (name, (f, s)) = (name, (K f, s)) in - syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's) - end; - -fun stamp_trfun s (c, f) = (c, (f, s)); -fun mk_trfun tr = stamp_trfun (stamp ()) tr; -fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; - - -(* pure_ext *) - -val token_markers = - ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; - -val pure_ext = syn_ext' false (K false) - [Mfix ("_", spropT --> propT, "", [0], 0), - Mfix ("_", logicT --> anyT, "", [0], 0), - Mfix ("_", spropT --> anyT, "", [0], 0), - Mfix ("'(_')", logicT --> logicT, "", [0], max_pri), - Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), - Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), - Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] - token_markers - ([], [], [], []) - ([], []); - -end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Fri Apr 08 16:31:14 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,567 +0,0 @@ -(* Title: Pure/Syntax/syn_trans.ML - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen - -Syntax translation functions. -*) - -signature SYN_TRANS0 = -sig - val eta_contract_default: bool Unsynchronized.ref - val eta_contract_raw: Config.raw - val eta_contract: bool Config.T - val atomic_abs_tr': string * typ * term -> term * term - val const_abs_tr': term -> term - val mk_binder_tr: string * string -> string * (term list -> term) - val mk_binder_tr': string * string -> string * (term list -> term) - val preserve_binder_abs_tr': string -> string -> string * (term list -> term) - val preserve_binder_abs2_tr': string -> string -> string * (term list -> term) - val dependent_tr': string * string -> term list -> term - val antiquote_tr: string -> term -> term - val quote_tr: string -> term -> term - val quote_antiquote_tr: string -> string -> string -> string * (term list -> term) - val antiquote_tr': string -> term -> term - val quote_tr': string -> term -> term - val quote_antiquote_tr': string -> string -> string -> string * (term list -> term) - val update_name_tr': term -> term - val mark_bound: string -> term - val mark_boundT: string * typ -> term - val bound_vars: (string * typ) list -> term -> term - val variant_abs: string * typ * term -> string * term - val variant_abs': string * typ * term -> string * term -end; - -signature SYN_TRANS1 = -sig - include SYN_TRANS0 - val no_brackets: unit -> bool - val no_type_brackets: unit -> bool - val non_typed_tr': (term list -> term) -> typ -> term list -> term - val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term - val constrainAbsC: string - val abs_tr: term list -> term - val pure_trfuns: - (string * (Ast.ast list -> Ast.ast)) list * - (string * (term list -> term)) list * - (string * (term list -> term)) list * - (string * (Ast.ast list -> Ast.ast)) list - val struct_trfuns: string list -> - (string * (Ast.ast list -> Ast.ast)) list * - (string * (term list -> term)) list * - (string * (typ -> term list -> term)) list * - (string * (Ast.ast list -> Ast.ast)) list -end; - -signature SYN_TRANS = -sig - include SYN_TRANS1 - val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast - val abs_tr': Proof.context -> term -> term - val prop_tr': term -> term - val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast - val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast -end; - -structure Syn_Trans: SYN_TRANS = -struct - -(* print mode *) - -val bracketsN = "brackets"; -val no_bracketsN = "no_brackets"; - -fun no_brackets () = - find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) - (print_mode_value ()) = SOME no_bracketsN; - -val type_bracketsN = "type_brackets"; -val no_type_bracketsN = "no_type_brackets"; - -fun no_type_brackets () = - find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) - (print_mode_value ()) <> SOME type_bracketsN; - - - -(** parse (ast) translations **) - -(* strip_positions *) - -fun strip_positions_ast_tr [ast] = Ast.strip_positions ast - | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts); - - -(* constify *) - -fun constify_ast_tr [Ast.Variable c] = Ast.Constant c - | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); - - -(* type syntax *) - -fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] - | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); - -fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) - | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); - -fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) - | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); - - -(* application *) - -fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) - | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts); - -fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) - | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts); - - -(* abstraction *) - -fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty] - | idtyp_ast_tr (*"_idtyp"*) asts = raise Ast.AST ("idtyp_ast_tr", asts); - -fun idtypdummy_ast_tr (*"_idtypdummy"*) [ty] = - Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty] - | idtypdummy_ast_tr (*"_idtypdummy"*) asts = raise Ast.AST ("idtyp_ast_tr", asts); -fun lambda_ast_tr (*"_lambda"*) [pats, body] = - Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) - | lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts); - -val constrainAbsC = "_constrainAbs"; - -fun absfree_proper (x, T, t) = - if can Name.dest_internal x - then error ("Illegal internal variable in abstraction: " ^ quote x) - else Term.absfree (x, T, t); - -fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t) - | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t) - | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT - | abs_tr ts = raise TERM ("abs_tr", ts); - - -(* binder *) - -fun mk_binder_tr (syn, name) = - let - fun err ts = raise TERM ("binder_tr: " ^ syn, ts) - fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]] - | binder_tr [x, t] = - let val abs = abs_tr [x, t] handle TERM _ => err [x, t] - in Lexicon.const name $ abs end - | binder_tr ts = err ts; - in (syn, binder_tr) end; - - -(* type propositions *) - -fun mk_type ty = - Lexicon.const "_constrain" $ - Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty); - -fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty - | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts); - -fun sort_constraint_tr (*"_sort_constraint"*) [ty] = - Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty - | sort_constraint_tr (*"_sort_constraint"*) ts = raise TERM ("sort_constraint_tr", ts); - - -(* meta propositions *) - -fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop" - | aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts); - - -(* meta implication *) - -fun bigimpl_ast_tr (*"_bigimpl"*) (asts as [asms, concl]) = - let val prems = - (case Ast.unfold_ast_p "_asms" asms of - (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] - | _ => raise Ast.AST ("bigimpl_ast_tr", asts)) - in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end - | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts); - - -(* type/term reflection *) - -fun type_tr (*"_TYPE"*) [ty] = mk_type ty - | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts); - - -(* dddot *) - -fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts); - - -(* quote / antiquote *) - -fun antiquote_tr name = - let - fun tr i ((t as Const (c, _)) $ u) = - if c = name then tr i u $ Bound i - else tr i t $ tr i u - | tr i (t $ u) = tr i t $ tr i u - | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) - | tr _ a = a; - in tr 0 end; - -fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t)); - -fun quote_antiquote_tr quoteN antiquoteN name = - let - fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t - | tr ts = raise TERM ("quote_tr", ts); - in (quoteN, tr) end; - - -(* corresponding updates *) - -fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) - | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = - if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) - else - list_comb (c $ update_name_tr [t] $ - (Lexicon.fun_type $ - (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts) - | update_name_tr ts = raise TERM ("update_name_tr", ts); - - -(* indexed syntax *) - -fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast - | struct_ast_tr (*"_struct"*) asts = Ast.mk_appl (Ast.Constant "_struct") asts; - -fun index_ast_tr ast = - Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]]; - -fun indexdefault_ast_tr (*"_indexdefault"*) [] = - index_ast_tr (Ast.Constant "_indexdefault") - | indexdefault_ast_tr (*"_indexdefault"*) asts = - raise Ast.AST ("indexdefault_ast_tr", asts); - -fun indexnum_ast_tr (*"_indexnum"*) [ast] = - index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast]) - | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts); - -fun indexvar_ast_tr (*"_indexvar"*) [] = - Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"] - | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts); - -fun index_tr (*"_index"*) [t] = t - | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts); - - -(* implicit structures *) - -fun the_struct structs i = - if 1 <= i andalso i <= length structs then nth structs (i - 1) - else error ("Illegal reference to implicit structure #" ^ string_of_int i); - -fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] = - Lexicon.free (the_struct structs 1) - | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] = - Lexicon.free (the_struct structs - (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t]))) - | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts); - - - -(** print (ast) translations **) - -(* types *) - -fun non_typed_tr' f _ ts = f ts; -fun non_typed_tr'' f x _ ts = f x ts; - - -(* type syntax *) - -fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) - | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] - | tappl_ast_tr' (f, ty :: tys) = - Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; - -fun fun_ast_tr' asts = - if no_brackets () orelse no_type_brackets () then raise Match - else - (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of - (dom as _ :: _ :: _, cod) - => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] - | _ => raise Match); - - -(* application *) - -fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) - | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; - -fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) - | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args]; - - -(* partial eta-contraction before printing *) - -fun eta_abs (Abs (a, T, t)) = - (case eta_abs t of - t' as Const ("_aprop", _) $ _ => Abs (a, T, t') - | t' as f $ u => - (case eta_abs u of - Bound 0 => - if Term.is_dependent f then Abs (a, T, t') - else incr_boundvars ~1 f - | _ => Abs (a, T, t')) - | t' => Abs (a, T, t')) - | eta_abs t = t; - -val eta_contract_default = Unsynchronized.ref true; -val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); -val eta_contract = Config.bool eta_contract_raw; - -fun eta_contr ctxt tm = - if Config.get ctxt eta_contract then eta_abs tm else tm; - - -(* abstraction *) - -fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T); -fun mark_bound x = mark_boundT (x, dummyT); - -fun bound_vars vars body = - subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body); - -fun strip_abss vars_of body_of tm = - let - val vars = vars_of tm; - val body = body_of tm; - val rev_new_vars = Term.rename_wrt_term body vars; - fun subst (x, T) b = - if can Name.dest_internal x andalso not (Term.is_dependent b) - then (Const ("_idtdummy", T), incr_boundvars ~1 b) - else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b)); - val (rev_vars', body') = fold_map subst rev_new_vars body; - in (rev rev_vars', body') end; - - -fun abs_tr' ctxt tm = - uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t)) - (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); - -fun atomic_abs_tr' (x, T, t) = - let val [xT] = Term.rename_wrt_term t [(x, T)] - in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end; - -fun abs_ast_tr' asts = - (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of - ([], _) => raise Ast.AST ("abs_ast_tr'", asts) - | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); - -fun const_abs_tr' t = - (case eta_abs t of - Abs (_, _, t') => - if Term.is_dependent t' then raise Match - else incr_boundvars ~1 t' - | _ => raise Match); - - -(* binders *) - -fun mk_binder_tr' (name, syn) = - let - fun mk_idts [] = raise Match (*abort translation*) - | mk_idts [idt] = idt - | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts; - - fun tr' t = - let - val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; - in Lexicon.const syn $ mk_idts xs $ bd end; - - fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts) - | binder_tr' [] = raise Match; - in (name, binder_tr') end; - -fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts => - let val (x, t) = atomic_abs_tr' abs - in list_comb (Lexicon.const syn $ x $ t, ts) end); - -fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts => - let val (x, t) = atomic_abs_tr' abs - in list_comb (Lexicon.const syn $ x $ A $ t, ts) end); - - -(* idtyp constraints *) - -fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] = - Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs] - | idtyp_ast_tr' _ _ = raise Match; - - -(* meta propositions *) - -fun prop_tr' tm = - let - fun aprop t = Lexicon.const "_aprop" $ t; - - fun is_prop Ts t = - fastype_of1 (Ts, t) = propT handle TERM _ => false; - - fun is_term (Const ("Pure.term", _) $ _) = true - | is_term _ = false; - - fun tr' _ (t as Const _) = t - | tr' Ts (t as Const ("_bound", _) $ u) = - if is_prop Ts u then aprop t else t - | tr' _ (t as Free (x, T)) = - if T = propT then aprop (Lexicon.free x) else t - | tr' _ (t as Var (xi, T)) = - if T = propT then aprop (Lexicon.var xi) else t - | tr' Ts (t as Bound _) = - if is_prop Ts t then aprop t else t - | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t) - | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = - if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 - else tr' Ts t1 $ tr' Ts t2 - | tr' Ts (t as t1 $ t2) = - (if is_Const (Term.head_of t) orelse not (is_prop Ts t) - then I else aprop) (tr' Ts t1 $ tr' Ts t2); - in tr' [] tm end; - - -(* meta implication *) - -fun impl_ast_tr' (*"==>"*) asts = - if no_brackets () then raise Match - else - (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of - (prems as _ :: _ :: _, concl) => - let - val (asms, asm) = split_last prems; - val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]); - in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end - | _ => raise Match); - - -(* dependent / nondependent quantifiers *) - -fun var_abs mark (x, T, b) = - let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) - in (x', subst_bound (mark (x', T), b)) end; - -val variant_abs = var_abs Free; -val variant_abs' = var_abs mark_boundT; - -fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = - if Term.is_dependent B then - let val (x', B') = variant_abs' (x, dummyT, B); - in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end - else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts) - | dependent_tr' _ _ = raise Match; - - -(* quote / antiquote *) - -fun antiquote_tr' name = - let - fun tr' i (t $ u) = - if u aconv Bound i then Lexicon.const name $ tr' i t - else tr' i t $ tr' i u - | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) - | tr' i a = if a aconv Bound i then raise Match else a; - in tr' 0 end; - -fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t) - | quote_tr' _ _ = raise Match; - -fun quote_antiquote_tr' quoteN antiquoteN name = - let - fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts) - | tr' _ = raise Match; - in (name, tr') end; - - -(* corresponding updates *) - -local - -fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T - | upd_type _ = dummyT; - -fun upd_tr' (x_upd, T) = - (case try (unsuffix "_update") x_upd of - SOME x => (x, upd_type T) - | NONE => raise Match); - -in - -fun update_name_tr' (Free x) = Free (upd_tr' x) - | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x) - | update_name_tr' (Const x) = Const (upd_tr' x) - | update_name_tr' _ = raise Match; - -end; - - -(* indexed syntax *) - -fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast - | index_ast_tr' _ = raise Match; - - -(* implicit structures *) - -fun the_struct' structs s = - [(case Lexicon.read_nat s of - SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match) - | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free"); - -fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] = - the_struct' structs "1" - | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] = - the_struct' structs s - | struct_ast_tr' _ _ = raise Match; - - - -(** Pure translations **) - -val pure_trfuns = - ([("_strip_positions", strip_positions_ast_tr), - ("_constify", constify_ast_tr), - ("_tapp", tapp_ast_tr), - ("_tappl", tappl_ast_tr), - ("_bracket", bracket_ast_tr), - ("_appl", appl_ast_tr), - ("_applC", applC_ast_tr), - ("_lambda", lambda_ast_tr), - ("_idtyp", idtyp_ast_tr), - ("_idtypdummy", idtypdummy_ast_tr), - ("_bigimpl", bigimpl_ast_tr), - ("_indexdefault", indexdefault_ast_tr), - ("_indexnum", indexnum_ast_tr), - ("_indexvar", indexvar_ast_tr), - ("_struct", struct_ast_tr)], - [("_abs", abs_tr), - ("_aprop", aprop_tr), - ("_ofclass", ofclass_tr), - ("_sort_constraint", sort_constraint_tr), - ("_TYPE", type_tr), - ("_DDDOT", dddot_tr), - ("_update_name", update_name_tr), - ("_index", index_tr)], - ([]: (string * (term list -> term)) list), - [("\\<^type>fun", fun_ast_tr'), - ("_abs", abs_ast_tr'), - ("_idts", idtyp_ast_tr' "_idts"), - ("_pttrns", idtyp_ast_tr' "_pttrns"), - ("\\<^const>==>", impl_ast_tr'), - ("_index", index_ast_tr')]); - -fun struct_trfuns structs = - ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); - -end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -5,20 +5,13 @@ (specified by mixfix declarations). *) -signature BASIC_SYNTAX = -sig - include SYN_TRANS0 - include MIXFIX0 - include PRINTER0 -end; - signature SYNTAX = sig - include LEXICON0 - include SYN_EXT0 - include SYN_TRANS1 - include MIXFIX1 - include PRINTER0 + val max_pri: int + val const: string -> term + val free: string -> term + val var: indexname -> term + val root: string Config.T val positions_raw: Config.raw val positions: bool Config.T val ambiguity_enabled: bool Config.T @@ -100,9 +93,9 @@ val string_of_sort_global: theory -> sort -> string val pp: Proof.context -> Pretty.pp val pp_global: theory -> Pretty.pp - type ruletab type syntax val eq_syntax: syntax * syntax -> bool + val is_const: syntax -> string -> bool val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list @@ -130,7 +123,6 @@ Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule - val is_const: syntax -> string -> bool val update_trfuns: (string * ((Ast.ast list -> Ast.ast) * stamp)) list * (string * ((term list -> term) * stamp)) list * @@ -151,10 +143,20 @@ structure Syntax: SYNTAX = struct +val max_pri = Syntax_Ext.max_pri; + +val const = Lexicon.const; +val free = Lexicon.free; +val var = Lexicon.var; + + + (** inner syntax operations **) (* configuration options *) +val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any))); + val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true); val positions = Config.bool positions_raw; @@ -408,12 +410,12 @@ fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); -fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns; +fun remove_trtab trfuns = fold (Symtab.remove Syntax_Ext.eq_trfun) trfuns; fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab) handle Symtab.DUP c => err_dup_trfun name c; -fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2) +fun merge_trtabs name tab1 tab2 = Symtab.merge Syntax_Ext.eq_trfun (tab1, tab2) handle Symtab.DUP c => err_dup_trfun name c; @@ -433,9 +435,9 @@ | app_first (f :: fs) = f ctxt args handle Match => app_first fs; in app_first fns end; -fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns; -fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns; -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2); +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syntax_Ext.eq_trfun) trfuns; +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syntax_Ext.eq_trfun) trfuns; +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syntax_Ext.eq_trfun (tab1, tab2); @@ -455,7 +457,7 @@ datatype syntax = Syntax of { - input: Syn_Ext.xprod list, + input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, gram: Parser.gram, consts: string list, @@ -468,9 +470,9 @@ print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, prtabs: Printer.prtabs} * stamp; -fun rep_syntax (Syntax (tabs, _)) = tabs; fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; +fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram; @@ -512,7 +514,7 @@ let val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; - val Syn_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation, + val Syntax_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val new_xprods = @@ -521,7 +523,7 @@ in Syntax ({input = new_xprods @ input, - lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon, + lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, gram = Parser.extend_gram new_xprods gram, consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2), prmodes = insert (op =) mode prmodes, @@ -540,7 +542,7 @@ fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let - val Syn_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules, + val Syntax_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; @@ -550,7 +552,7 @@ in Syntax ({input = input', - lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon, + lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon, gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram, consts = consts, prmodes = prmodes, @@ -597,12 +599,12 @@ (* basic syntax *) -val basic_syntax = update_syntax mode_default Syn_Ext.pure_ext empty_syntax; +val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax; val basic_nonterms = - (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes", - Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", - "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index", + (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes", + Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", + "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index", "struct", "id_position", "longid_position", "type_name", "class_name"]); @@ -687,9 +689,6 @@ | print_rule (Parse_Print_Rule pats) = SOME (swap pats); -fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c; - - (* check_rules *) local @@ -715,8 +714,8 @@ fun ext_syntax f decls = update_syntax mode_default (f decls); -val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns; -val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns; +val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns; +val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns; fun update_type_gram add prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls); @@ -724,20 +723,8 @@ fun update_const_gram add is_logtype prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls); -val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules; -val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules; - - -(*export parts of internal Syntax structures*) -val syntax_tokenize = tokenize; -open Lexicon Syn_Ext Syn_Trans Mixfix Printer; -val tokenize = syntax_tokenize; +val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules; +val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; end; -structure Basic_Syntax: BASIC_SYNTAX = Syntax; -open Basic_Syntax; - -forget_structure "Syn_Ext"; -forget_structure "Mixfix"; - diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syntax_ext.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 17:13:49 2011 +0200 @@ -0,0 +1,380 @@ +(* Title: Pure/Syntax/syntax_ext.ML + Author: Markus Wenzel and Carsten Clasohm, TU Muenchen + +Syntax extension. +*) + +signature SYNTAX_EXT = +sig + val dddot_indexname: indexname + val logic: string + val args: string + val cargs: string + val typeT: typ + val any: string + val sprop: string + val spropT: typ + val max_pri: int + datatype mfix = Mfix of string * typ * string * int list * int + val err_in_mfix: string -> mfix -> 'a + val typ_to_nonterm: typ -> string + datatype xsymb = + Delim of string | + Argument of string * int | + Space of string | + Bg of int | Brk of int | En + datatype xprod = XProd of string * xsymb list * string * int + val chain_pri: int + val delims_of: xprod list -> string list list + datatype syn_ext = + Syn_Ext of { + xprods: xprod list, + consts: string list, + parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, + parse_rules: (Ast.ast * Ast.ast) list, + parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, + print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, + print_rules: (Ast.ast * Ast.ast) list, + print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} + val mfix_delims: string -> string list + val mfix_args: string -> int + val escape: string -> string + val syn_ext': bool -> (string -> bool) -> mfix list -> + string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * + (string * ((Proof.context -> term list -> term) * stamp)) list * + (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> + (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext: mfix list -> string list -> + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * + (string * ((Proof.context -> term list -> term) * stamp)) list * + (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> + (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext_const_names: string list -> syn_ext + val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext_trfuns: + (string * ((Ast.ast list -> Ast.ast) * stamp)) list * + (string * ((term list -> term) * stamp)) list * + (string * ((typ -> term list -> term) * stamp)) list * + (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext + val syn_ext_advanced_trfuns: + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * + (string * ((Proof.context -> term list -> term) * stamp)) list * + (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext + val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp) + val mk_trfun: string * 'a -> string * ('a * stamp) + val eq_trfun: ('a * stamp) * ('a * stamp) -> bool + val token_markers: string list + val pure_ext: syn_ext +end; + +structure Syntax_Ext: SYNTAX_EXT = +struct + + +(** misc definitions **) + +val dddot_indexname = ("dddot", 0); + + +(* syntactic categories *) + +val logic = "logic"; +val logicT = Type (logic, []); + +val args = "args"; +val cargs = "cargs"; + +val typeT = Type ("type", []); + +val sprop = "#prop"; +val spropT = Type (sprop, []); + +val any = "any"; +val anyT = Type (any, []); + + + +(** datatype xprod **) + +(*Delim s: delimiter s + Argument (s, p): nonterminal s requiring priority >= p, or valued token + Space s: some white space for printing + Bg, Brk, En: blocks and breaks for pretty printing*) + +datatype xsymb = + Delim of string | + Argument of string * int | + Space of string | + Bg of int | Brk of int | En; + +fun is_delim (Delim _) = true + | is_delim _ = false; + +fun is_terminal (Delim _) = true + | is_terminal (Argument (s, _)) = Lexicon.is_terminal s + | is_terminal _ = false; + +fun is_argument (Argument _) = true + | is_argument _ = false; + +fun is_index (Argument ("index", _)) = true + | is_index _ = false; + +val index = Argument ("index", 1000); + + +(*XProd (lhs, syms, c, p): + lhs: name of nonterminal on the lhs of the production + syms: list of symbols on the rhs of the production + c: head of parse tree + p: priority of this production*) + +datatype xprod = XProd of string * xsymb list * string * int; + +val max_pri = 1000; (*maximum legal priority*) +val chain_pri = ~1; (*dummy for chain productions*) + +fun delims_of xprods = + fold (fn XProd (_, xsymbs, _, _) => + fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods [] + |> map Symbol.explode; + + + +(** datatype mfix **) + +(*Mfix (sy, ty, c, ps, p): + sy: rhs of production as symbolic string + ty: type description of production + c: head of parse tree + ps: priorities of arguments in sy + p: priority of production*) + +datatype mfix = Mfix of string * typ * string * int list * int; + +fun err_in_mfix msg (Mfix (sy, _, const, _, _)) = + cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const); + + +(* typ_to_nonterm *) + +fun typ_to_nt _ (Type (c, _)) = c + | typ_to_nt default _ = default; + +(*get nonterminal for rhs*) +val typ_to_nonterm = typ_to_nt any; + +(*get nonterminal for lhs*) +val typ_to_nonterm1 = typ_to_nt logic; + + +(* read mixfix annotations *) + +local + +val is_meta = member (op =) ["(", ")", "/", "_", "\\"]; + +val scan_delim_char = + $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) || + Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular); + +fun read_int ["0", "0"] = ~1 + | read_int cs = #1 (Library.read_int cs); + +val scan_sym = + $$ "_" >> K (Argument ("", 0)) || + $$ "\\" >> K index || + $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) || + $$ ")" >> K En || + $$ "/" -- $$ "/" >> K (Brk ~1) || + $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) || + Scan.many1 Symbol.is_blank >> (Space o implode) || + Scan.repeat1 scan_delim_char >> (Delim o implode); + +val scan_symb = + scan_sym >> SOME || + $$ "'" -- Scan.one Symbol.is_blank >> K NONE; + +val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); +val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; + +fun unique_index xsymbs = + if length (filter is_index xsymbs) <= 1 then xsymbs + else error "Duplicate index arguments (\\)"; + +in + +val read_mfix = unique_index o read_symbs o Symbol.explode; + +fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; +val mfix_args = length o filter is_argument o read_mfix; + +val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; + +end; + + +(* mfix_to_xprod *) + +fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) = + let + fun check_pri p = + if p >= 0 andalso p <= max_pri then () + else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix; + + fun blocks_ok [] 0 = true + | blocks_ok [] _ = false + | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1) + | blocks_ok (En :: _) 0 = false + | blocks_ok (En :: syms) n = blocks_ok syms (n - 1) + | blocks_ok (_ :: syms) n = blocks_ok syms n; + + fun check_blocks syms = + if blocks_ok syms 0 then () + else err_in_mfix "Unbalanced block parentheses" mfix; + + + val cons_fst = apfst o cons; + + fun add_args [] ty [] = ([], typ_to_nonterm1 ty) + | add_args [] _ _ = err_in_mfix "Too many precedences" mfix + | add_args ((arg as Argument ("index", _)) :: syms) ty ps = + cons_fst arg (add_args syms ty ps) + | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] = + cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys []) + | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) = + cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps) + | add_args (Argument _ :: _) _ _ = + err_in_mfix "More arguments than in corresponding type" mfix + | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps); + + fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) + | rem_pri sym = sym; + + fun logify_types (a as (Argument (s, p))) = + if s <> "prop" andalso is_logtype s then Argument (logic, p) else a + | logify_types a = a; + + + val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix; + val args = filter (fn Argument _ => true | _ => false) raw_symbs; + val (const', typ', parse_rules) = + if not (exists is_index args) then (const, typ, []) + else + let + val indexed_const = + if const <> "" then const ^ "_indexed" + else err_in_mfix "Missing constant name for indexed syntax" mfix; + val rangeT = Term.range_type typ handle Match => + err_in_mfix "Missing structure argument for indexed syntax" mfix; + + val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1)); + val (xs1, xs2) = chop (find_index is_index args) xs; + val i = Ast.Variable "i"; + val lhs = Ast.mk_appl (Ast.Constant indexed_const) + (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); + val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs); + in (indexed_const, rangeT, [(lhs, rhs)]) end; + + val (symbs, lhs) = add_args raw_symbs typ' pris; + + val copy_prod = + (lhs = "prop" orelse lhs = "logic") + andalso const <> "" + andalso not (null symbs) + andalso not (exists is_delim symbs); + val lhs' = + if convert andalso not copy_prod then + (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs) + else lhs; + val symbs' = map logify_types symbs; + val xprod = XProd (lhs', symbs', const', pri); + + val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs'); + val xprod' = + if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix + else if const <> "" then xprod + else if length (filter is_argument symbs') <> 1 then + err_in_mfix "Copy production must have exactly one argument" mfix + else if exists is_terminal symbs' then xprod + else XProd (lhs', map rem_pri symbs', "", chain_pri); + + in (xprod', parse_rules) end; + + + +(** datatype syn_ext **) + +datatype syn_ext = + Syn_Ext of { + xprods: xprod list, + consts: string list, + parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, + parse_rules: (Ast.ast * Ast.ast) list, + parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, + print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, + print_rules: (Ast.ast * Ast.ast) list, + print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}; + + +(* syn_ext *) + +fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) = + let + val (parse_ast_translation, parse_translation, print_translation, + print_ast_translation) = trfuns; + + val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes + |> split_list |> apsnd (rev o flat); + val mfix_consts = + distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); + in + Syn_Ext { + xprods = xprods, + consts = union (op =) consts mfix_consts, + parse_ast_translation = parse_ast_translation, + parse_rules = parse_rules' @ parse_rules, + parse_translation = parse_translation, + print_translation = print_translation, + print_rules = map swap parse_rules' @ print_rules, + print_ast_translation = print_ast_translation} + end; + + +val syn_ext = syn_ext' true (K false); + +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []); +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; +fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []); + +fun syn_ext_trfuns (atrs, trs, tr's, atr's) = + let fun simple (name, (f, s)) = (name, (K f, s)) in + syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's) + end; + +fun stamp_trfun s (c, f) = (c, (f, s)); +fun mk_trfun tr = stamp_trfun (stamp ()) tr; +fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2; + + +(* pure_ext *) + +val token_markers = + ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; + +val pure_ext = syn_ext' false (K false) + [Mfix ("_", spropT --> propT, "", [0], 0), + Mfix ("_", logicT --> anyT, "", [0], 0), + Mfix ("_", spropT --> anyT, "", [0], 0), + Mfix ("'(_')", logicT --> logicT, "", [0], max_pri), + Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), + Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), + Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] + token_markers + ([], [], [], []) + ([], []); + +end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 17:13:49 2011 +0200 @@ -89,6 +89,14 @@ (* parsetree_to_ast *) +fun markup_const ctxt c = + [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c]; + +fun markup_free ctxt x = + [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ + (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] + else [Markup.hilite]); + fun parsetree_to_ast ctxt constrain_pos trf parsetree = let val tsig = ProofContext.tsig_of ctxt; @@ -98,6 +106,13 @@ fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c]; fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c]; + val markup_entity = Lexicon.unmark + {case_class = markup_class, + case_type = markup_type, + case_const = markup_const ctxt, + case_fixed = markup_free ctxt, + case_default = K []}; + val reports = Unsynchronized.ref ([]: Position.reports); fun report pos = Position.reports reports [pos]; @@ -106,23 +121,37 @@ NONE => Ast.mk_appl (Ast.Constant a) args | SOME f => f ctxt args); - fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) = + fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = let val c = get_class (Lexicon.str_of_token tok); val _ = report (Lexicon.pos_of_token tok) markup_class c; - in Ast.Constant (Lexicon.mark_class c) end - | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) = + in [Ast.Constant (Lexicon.mark_class c)] end + | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = let val c = get_type (Lexicon.str_of_token tok); val _ = report (Lexicon.pos_of_token tok) markup_type c; - in Ast.Constant (Lexicon.mark_type c) end - | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = + in [Ast.Constant (Lexicon.mark_type c)] end + | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = if constrain_pos then - Ast.Appl [Ast.Constant "_constrain", ast_of pt, - Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))] - else ast_of pt - | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) - | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); + [Ast.Appl [Ast.Constant "_constrain", ast_of pt, + Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]] + else [ast_of pt] + | asts_of (Parser.Node (a, pts)) = + let + val _ = pts |> List.app + (fn Parser.Node _ => () | Parser.Tip tok => + if Lexicon.valued_token tok then () + else report (Lexicon.pos_of_token tok) markup_entity a); + in [trans a (maps asts_of pts)] end + | asts_of (Parser.Tip tok) = + if Lexicon.valued_token tok + then [Ast.Variable (Lexicon.str_of_token tok)] + else [] + + and ast_of pt = + (case asts_of pt of + [ast] => ast + | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts)); val ast = Exn.interruptible_capture ast_of parsetree; in (! reports, ast) end; @@ -152,16 +181,10 @@ fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result | decode_term ctxt (reports0, Exn.Result tm) = let - val consts = ProofContext.consts_of ctxt; fun get_const a = ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a))) - handle ERROR _ => (false, Consts.intern consts a)); + handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a)); val get_free = ProofContext.intern_skolem ctxt; - fun markup_const c = [Name_Space.markup_entry (Consts.space_of consts) c]; - fun markup_free x = - [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ - (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] - else [Markup.hilite]); fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; fun markup_bound def id = [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound]; @@ -187,23 +210,23 @@ | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u | decode ps _ _ (Const (a, T)) = (case try Lexicon.unmark_fixed a of - SOME x => (report ps markup_free x; Free (x, T)) + SOME x => (report ps (markup_free ctxt) x; Free (x, T)) | NONE => let val c = (case try Lexicon.unmark_const a of SOME c => c | NONE => snd (get_const a)); - val _ = report ps markup_const c; + val _ = report ps (markup_const ctxt) c; in Const (c, T) end) | decode ps _ _ (Free (a, T)) = (case (get_free a, get_const a) of - (SOME x, _) => (report ps markup_free x; Free (x, T)) - | (_, (true, c)) => (report ps markup_const c; Const (c, T)) + (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T)) + | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T)) | (_, (false, c)) => if Long_Name.is_qualified c - then (report ps markup_const c; Const (c, T)) - else (report ps markup_free c; Free (c, T))) + then (report ps (markup_const ctxt) c; Const (c, T)) + else (report ps (markup_free ctxt) c; Free (c, T))) | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) | decode ps _ bs (t as Bound i) = (case try (nth bs) i of @@ -302,20 +325,13 @@ handle ERROR msg => parse_failed ctxt pos msg "type"; in T end; -fun parse_term T ctxt text = +fun parse_term is_prop ctxt text = let - val (T', _) = Type_Infer.paramify_dummies T 0; - val (markup, kind) = - if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); + val (markup, kind, root, constrain) = + if is_prop + then (Markup.prop, "proposition", "prop", Type.constraint propT) + else (Markup.term, "term", Config.get ctxt Syntax.root, I); val (syms, pos) = Syntax.parse_token ctxt markup text; - - val default_root = Config.get ctxt Syntax.default_root; - val root = - (case T' of - Type (c, _) => - if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c - then default_root else c - | _ => default_root); in let val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt); @@ -331,7 +347,7 @@ else ""; (*brute-force disambiguation via type-inference*) - fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) + fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t) handle exn as ERROR _ => Exn.Exn exn; val results' = @@ -345,7 +361,7 @@ val checked = map snd (proper_results results'); val len = length checked; - val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt); + val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); in if len = 0 then report_result ctxt pos @@ -418,9 +434,9 @@ fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts) | term_of (TFree (x, S)) = - if is_some (Term_Position.decode x) then Lexicon.free x - else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S - | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S; + if is_some (Term_Position.decode x) then Syntax.free x + else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S + | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S; in term_of ty end; @@ -475,7 +491,7 @@ val {structs, fixes} = idents; fun mark_atoms ((t as Const (c, _)) $ u) = - if member (op =) Syntax.token_markers c + if member (op =) Syntax_Ext.token_markers c then t $ u else mark_atoms t $ mark_atoms u | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) @@ -491,18 +507,18 @@ else Lexicon.const "_free" $ t end | mark_atoms (t as Var (xi, T)) = - if xi = Syntax.dddot_indexname then Const ("_DDDOT", T) + if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) else Lexicon.const "_var" $ t | mark_atoms a = a; fun prune_typs (t_seen as (Const _, _)) = t_seen | prune_typs (t as Free (x, ty), seen) = if ty = dummyT then (t, seen) - else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen) + else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen) else (t, t :: seen) | prune_typs (t as Var (xi, ty), seen) = if ty = dummyT then (t, seen) - else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen) + else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen) else (t, t :: seen) | prune_typs (t_seen as (Bound _, _)) = t_seen | prune_typs (Abs (x, ty, t), seen) = @@ -516,13 +532,13 @@ fun ast_of tm = (case strip_comb tm of - (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts) + (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts) | ((c as Const ("_free", _)), Free (x, T) :: ts) => - Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) + Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) | ((c as Const ("_var", _)), Var (xi, T) :: ts) => - Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts) + Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts) | ((c as Const ("_bound", _)), Free (x, T) :: ts) => - Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) + Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) | (Const ("_idtdummy", T), ts) => Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts) | (const as Const (c, T), ts) => @@ -541,7 +557,7 @@ else simple_ast_of ctxt t; in tm - |> Syn_Trans.prop_tr' + |> Syntax_Trans.prop_tr' |> show_types ? (#1 o prune_typs o rpair []) |> mark_atoms |> ast_of @@ -659,8 +675,8 @@ val _ = Syntax.install_operations {parse_sort = parse_sort, parse_typ = parse_typ, - parse_term = parse_term dummyT, - parse_prop = parse_term propT, + parse_term = parse_term false, + parse_prop = parse_term true, unparse_sort = unparse_sort, unparse_typ = unparse_typ, unparse_term = unparse_term}; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Syntax/syntax_trans.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Apr 08 17:13:49 2011 +0200 @@ -0,0 +1,556 @@ +(* Title: Pure/Syntax/syntax_trans.ML + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + +Syntax translation functions. +*) + +signature BASIC_SYNTAX_TRANS = +sig + val eta_contract: bool Config.T +end + +signature SYNTAX_TRANS = +sig + include BASIC_SYNTAX_TRANS + val no_brackets: unit -> bool + val no_type_brackets: unit -> bool + val abs_tr: term list -> term + val mk_binder_tr: string * string -> string * (term list -> term) + val antiquote_tr: string -> term -> term + val quote_tr: string -> term -> term + val quote_antiquote_tr: string -> string -> string -> string * (term list -> term) + val non_typed_tr': (term list -> term) -> typ -> term list -> term + val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term + val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast + val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast + val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast + val eta_contract_default: bool Unsynchronized.ref + val eta_contract_raw: Config.raw + val mark_bound: string -> term + val mark_boundT: string * typ -> term + val bound_vars: (string * typ) list -> term -> term + val abs_tr': Proof.context -> term -> term + val atomic_abs_tr': string * typ * term -> term * term + val const_abs_tr': term -> term + val mk_binder_tr': string * string -> string * (term list -> term) + val preserve_binder_abs_tr': string -> string -> string * (term list -> term) + val preserve_binder_abs2_tr': string -> string -> string * (term list -> term) + val prop_tr': term -> term + val variant_abs: string * typ * term -> string * term + val variant_abs': string * typ * term -> string * term + val dependent_tr': string * string -> term list -> term + val antiquote_tr': string -> term -> term + val quote_tr': string -> term -> term + val quote_antiquote_tr': string -> string -> string -> string * (term list -> term) + val update_name_tr': term -> term + val pure_trfuns: + (string * (Ast.ast list -> Ast.ast)) list * + (string * (term list -> term)) list * + (string * (term list -> term)) list * + (string * (Ast.ast list -> Ast.ast)) list + val struct_trfuns: string list -> + (string * (Ast.ast list -> Ast.ast)) list * + (string * (term list -> term)) list * + (string * (typ -> term list -> term)) list * + (string * (Ast.ast list -> Ast.ast)) list +end; + +structure Syntax_Trans: SYNTAX_TRANS = +struct + +(* print mode *) + +val bracketsN = "brackets"; +val no_bracketsN = "no_brackets"; + +fun no_brackets () = + find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) + (print_mode_value ()) = SOME no_bracketsN; + +val type_bracketsN = "type_brackets"; +val no_type_bracketsN = "no_type_brackets"; + +fun no_type_brackets () = + find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) + (print_mode_value ()) <> SOME type_bracketsN; + + + +(** parse (ast) translations **) + +(* strip_positions *) + +fun strip_positions_ast_tr [ast] = Ast.strip_positions ast + | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts); + + +(* constify *) + +fun constify_ast_tr [Ast.Variable c] = Ast.Constant c + | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); + + +(* type syntax *) + +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] + | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); + +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) + | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); + +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) + | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); + + +(* application *) + +fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) + | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts); + +fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) + | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts); + + +(* abstraction *) + +fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty] + | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); + +fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty] + | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); + +fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) + | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); + +fun absfree_proper (x, T, t) = + if can Name.dest_internal x + then error ("Illegal internal variable in abstraction: " ^ quote x) + else Term.absfree (x, T, t); + +fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t) + | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t) + | abs_tr [Const ("_constrain", _) $ x $ tT, t] = + Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT + | abs_tr ts = raise TERM ("abs_tr", ts); + + +(* binder *) + +fun mk_binder_tr (syn, name) = + let + fun err ts = raise TERM ("binder_tr: " ^ syn, ts) + fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]] + | binder_tr [x, t] = + let val abs = abs_tr [x, t] handle TERM _ => err [x, t] + in Lexicon.const name $ abs end + | binder_tr ts = err ts; + in (syn, binder_tr) end; + + +(* type propositions *) + +fun mk_type ty = + Lexicon.const "_constrain" $ + Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty); + +fun ofclass_tr [ty, cls] = cls $ mk_type ty + | ofclass_tr ts = raise TERM ("ofclass_tr", ts); + +fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty + | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts); + + +(* meta propositions *) + +fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop" + | aprop_tr ts = raise TERM ("aprop_tr", ts); + + +(* meta implication *) + +fun bigimpl_ast_tr (asts as [asms, concl]) = + let val prems = + (case Ast.unfold_ast_p "_asms" asms of + (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] + | _ => raise Ast.AST ("bigimpl_ast_tr", asts)) + in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end + | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts); + + +(* type/term reflection *) + +fun type_tr [ty] = mk_type ty + | type_tr ts = raise TERM ("type_tr", ts); + + +(* dddot *) + +fun dddot_tr ts = Term.list_comb (Lexicon.var Syntax_Ext.dddot_indexname, ts); + + +(* quote / antiquote *) + +fun antiquote_tr name = + let + fun tr i ((t as Const (c, _)) $ u) = + if c = name then tr i u $ Bound i + else tr i t $ tr i u + | tr i (t $ u) = tr i t $ tr i u + | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) + | tr _ a = a; + in tr 0 end; + +fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t)); + +fun quote_antiquote_tr quoteN antiquoteN name = + let + fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t + | tr ts = raise TERM ("quote_tr", ts); + in (quoteN, tr) end; + + +(* corresponding updates *) + +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) + | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = + if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) + else + list_comb (c $ update_name_tr [t] $ + (Lexicon.fun_type $ + (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts) + | update_name_tr ts = raise TERM ("update_name_tr", ts); + + +(* indexed syntax *) + +fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast + | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts; + +fun index_ast_tr ast = + Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]]; + +fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault") + | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts); + +fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast]) + | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts); + +fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"] + | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); + +fun index_tr [t] = t + | index_tr ts = raise TERM ("index_tr", ts); + + +(* implicit structures *) + +fun the_struct structs i = + if 1 <= i andalso i <= length structs then nth structs (i - 1) + else error ("Illegal reference to implicit structure #" ^ string_of_int i); + +fun struct_tr structs [Const ("_indexdefault", _)] = + Lexicon.free (the_struct structs 1) + | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] = + Lexicon.free (the_struct structs + (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t]))) + | struct_tr _ ts = raise TERM ("struct_tr", ts); + + + +(** print (ast) translations **) + +(* types *) + +fun non_typed_tr' f _ ts = f ts; +fun non_typed_tr'' f x _ ts = f x ts; + + +(* type syntax *) + +fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) + | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] + | tappl_ast_tr' (f, ty :: tys) = + Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; + +fun fun_ast_tr' asts = + if no_brackets () orelse no_type_brackets () then raise Match + else + (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of + (dom as _ :: _ :: _, cod) + => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] + | _ => raise Match); + + +(* application *) + +fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) + | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; + +fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) + | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args]; + + +(* partial eta-contraction before printing *) + +fun eta_abs (Abs (a, T, t)) = + (case eta_abs t of + t' as Const ("_aprop", _) $ _ => Abs (a, T, t') + | t' as f $ u => + (case eta_abs u of + Bound 0 => + if Term.is_dependent f then Abs (a, T, t') + else incr_boundvars ~1 f + | _ => Abs (a, T, t')) + | t' => Abs (a, T, t')) + | eta_abs t = t; + +val eta_contract_default = Unsynchronized.ref true; +val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); +val eta_contract = Config.bool eta_contract_raw; + +fun eta_contr ctxt tm = + if Config.get ctxt eta_contract then eta_abs tm else tm; + + +(* abstraction *) + +fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T); +fun mark_bound x = mark_boundT (x, dummyT); + +fun bound_vars vars body = + subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body); + +fun strip_abss vars_of body_of tm = + let + val vars = vars_of tm; + val body = body_of tm; + val rev_new_vars = Term.rename_wrt_term body vars; + fun subst (x, T) b = + if can Name.dest_internal x andalso not (Term.is_dependent b) + then (Const ("_idtdummy", T), incr_boundvars ~1 b) + else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b)); + val (rev_vars', body') = fold_map subst rev_new_vars body; + in (rev rev_vars', body') end; + + +fun abs_tr' ctxt tm = + uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t)) + (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); + +fun atomic_abs_tr' (x, T, t) = + let val [xT] = Term.rename_wrt_term t [(x, T)] + in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end; + +fun abs_ast_tr' asts = + (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of + ([], _) => raise Ast.AST ("abs_ast_tr'", asts) + | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); + +fun const_abs_tr' t = + (case eta_abs t of + Abs (_, _, t') => + if Term.is_dependent t' then raise Match + else incr_boundvars ~1 t' + | _ => raise Match); + + +(* binders *) + +fun mk_binder_tr' (name, syn) = + let + fun mk_idts [] = raise Match (*abort translation*) + | mk_idts [idt] = idt + | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts; + + fun tr' t = + let + val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; + in Lexicon.const syn $ mk_idts xs $ bd end; + + fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts) + | binder_tr' [] = raise Match; + in (name, binder_tr') end; + +fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts => + let val (x, t) = atomic_abs_tr' abs + in list_comb (Lexicon.const syn $ x $ t, ts) end); + +fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts => + let val (x, t) = atomic_abs_tr' abs + in list_comb (Lexicon.const syn $ x $ A $ t, ts) end); + + +(* idtyp constraints *) + +fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] = + Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs] + | idtyp_ast_tr' _ _ = raise Match; + + +(* meta propositions *) + +fun prop_tr' tm = + let + fun aprop t = Lexicon.const "_aprop" $ t; + + fun is_prop Ts t = + fastype_of1 (Ts, t) = propT handle TERM _ => false; + + fun is_term (Const ("Pure.term", _) $ _) = true + | is_term _ = false; + + fun tr' _ (t as Const _) = t + | tr' Ts (t as Const ("_bound", _) $ u) = + if is_prop Ts u then aprop t else t + | tr' _ (t as Free (x, T)) = + if T = propT then aprop (Lexicon.free x) else t + | tr' _ (t as Var (xi, T)) = + if T = propT then aprop (Lexicon.var xi) else t + | tr' Ts (t as Bound _) = + if is_prop Ts t then aprop t else t + | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t) + | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = + if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 + else tr' Ts t1 $ tr' Ts t2 + | tr' Ts (t as t1 $ t2) = + (if is_Const (Term.head_of t) orelse not (is_prop Ts t) + then I else aprop) (tr' Ts t1 $ tr' Ts t2); + in tr' [] tm end; + + +(* meta implication *) + +fun impl_ast_tr' asts = + if no_brackets () then raise Match + else + (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of + (prems as _ :: _ :: _, concl) => + let + val (asms, asm) = split_last prems; + val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]); + in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end + | _ => raise Match); + + +(* dependent / nondependent quantifiers *) + +fun var_abs mark (x, T, b) = + let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) + in (x', subst_bound (mark (x', T), b)) end; + +val variant_abs = var_abs Free; +val variant_abs' = var_abs mark_boundT; + +fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = + if Term.is_dependent B then + let val (x', B') = variant_abs' (x, dummyT, B); + in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end + else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts) + | dependent_tr' _ _ = raise Match; + + +(* quote / antiquote *) + +fun antiquote_tr' name = + let + fun tr' i (t $ u) = + if u aconv Bound i then Lexicon.const name $ tr' i t + else tr' i t $ tr' i u + | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) + | tr' i a = if a aconv Bound i then raise Match else a; + in tr' 0 end; + +fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t) + | quote_tr' _ _ = raise Match; + +fun quote_antiquote_tr' quoteN antiquoteN name = + let + fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts) + | tr' _ = raise Match; + in (name, tr') end; + + +(* corresponding updates *) + +local + +fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T + | upd_type _ = dummyT; + +fun upd_tr' (x_upd, T) = + (case try (unsuffix "_update") x_upd of + SOME x => (x, upd_type T) + | NONE => raise Match); + +in + +fun update_name_tr' (Free x) = Free (upd_tr' x) + | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x) + | update_name_tr' (Const x) = Const (upd_tr' x) + | update_name_tr' _ = raise Match; + +end; + + +(* indexed syntax *) + +fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast + | index_ast_tr' _ = raise Match; + + +(* implicit structures *) + +fun the_struct' structs s = + [(case Lexicon.read_nat s of + SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match) + | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free"); + +fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1" + | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] = + the_struct' structs s + | struct_ast_tr' _ _ = raise Match; + + + +(** Pure translations **) + +val pure_trfuns = + ([("_strip_positions", strip_positions_ast_tr), + ("_constify", constify_ast_tr), + ("_tapp", tapp_ast_tr), + ("_tappl", tappl_ast_tr), + ("_bracket", bracket_ast_tr), + ("_appl", appl_ast_tr), + ("_applC", applC_ast_tr), + ("_lambda", lambda_ast_tr), + ("_idtyp", idtyp_ast_tr), + ("_idtypdummy", idtypdummy_ast_tr), + ("_bigimpl", bigimpl_ast_tr), + ("_indexdefault", indexdefault_ast_tr), + ("_indexnum", indexnum_ast_tr), + ("_indexvar", indexvar_ast_tr), + ("_struct", struct_ast_tr)], + [("_abs", abs_tr), + ("_aprop", aprop_tr), + ("_ofclass", ofclass_tr), + ("_sort_constraint", sort_constraint_tr), + ("_TYPE", type_tr), + ("_DDDOT", dddot_tr), + ("_update_name", update_name_tr), + ("_index", index_tr)], + ([]: (string * (term list -> term)) list), + [("\\<^type>fun", fun_ast_tr'), + ("_abs", abs_ast_tr'), + ("_idts", idtyp_ast_tr' "_idts"), + ("_pttrns", idtyp_ast_tr' "_pttrns"), + ("\\<^const>==>", impl_ast_tr'), + ("_index", index_ast_tr')]); + +fun struct_trfuns structs = + ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); + +end; + +structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; +open Basic_Syntax_Trans; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Thy/latex.ML Fri Apr 08 17:13:49 2011 +0200 @@ -130,7 +130,7 @@ if invisible_token tok then "" else if Token.is_kind Token.Command tok then "\\isacommand{" ^ output_syms s ^ "}" - else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then + else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then "\\isakeyword{" ^ output_syms s ^ "}" else if Token.is_kind Token.String tok then output_syms s |> enclose diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Apr 08 17:13:49 2011 +0200 @@ -453,7 +453,7 @@ val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean); -val _ = add_option "eta_contract" (Config.put eta_contract o boolean); +val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean); val _ = add_option "display" (Config.put display o boolean); val _ = add_option "break" (Config.put break o boolean); val _ = add_option "quotes" (Config.put quotes o boolean); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -65,7 +65,7 @@ | Token.EOF => Markup.control; fun token_markup tok = - if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator + if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator else let val kind = Token.kind_of tok; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/consts.ML Fri Apr 08 17:13:49 2011 +0200 @@ -132,12 +132,12 @@ val extern = Name_Space.extern o space_of; fun intern_syntax consts s = - (case try Syntax.unmark_const s of + (case try Lexicon.unmark_const s of SOME c => c | NONE => intern consts s); fun extern_syntax consts s = - (case try Syntax.unmark_const s of + (case try Lexicon.unmark_const s of SOME c => extern consts c | NONE => s); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/primitive_defs.ML Fri Apr 08 17:13:49 2011 +0200 @@ -27,7 +27,7 @@ val eq_body = Term.strip_all_body eq; val display_terms = - commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars); + commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars); val display_types = commas_quote o map (Syntax.string_of_typ ctxt); val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)"; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/pure_thy.ML Fri Apr 08 17:13:49 2011 +0200 @@ -16,11 +16,11 @@ val typ = Simple_Syntax.read_typ; val prop = Simple_Syntax.read_prop; -val tycon = Syntax.mark_type; -val const = Syntax.mark_const; +val tycon = Lexicon.mark_type; +val const = Lexicon.mark_const; -val typeT = Syntax.typeT; -val spropT = Syntax.spropT; +val typeT = Syntax_Ext.typeT; +val spropT = Syntax_Ext.spropT; (* application syntax variants *) @@ -128,7 +128,7 @@ ("_indexvar", typ "index", Delimfix "'\\"), ("_struct", typ "index => logic", Mixfix ("\\_", [1000], 1000)), ("_update_name", typ "idt", NoSyn), - (Syntax.constrainAbsC, typ "'a", NoSyn), + ("_constrainAbs", typ "'a", NoSyn), ("_constrain_position", typ "id => id_position", Delimfix "_"), ("_constrain_position", typ "longid => longid_position", Delimfix "_"), ("_type_constraint_", typ "'a", NoSyn), @@ -169,7 +169,7 @@ #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") [] #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") [] #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] - #> Sign.add_trfuns Syntax.pure_trfuns + #> Sign.add_trfuns Syntax_Trans.pure_trfuns #> Sign.local_path #> Sign.add_consts_i [(Binding.name "term", typ "'a => prop", NoSyn), diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/raw_simplifier.ML Fri Apr 08 17:13:49 2011 +0200 @@ -306,7 +306,7 @@ let val names = Term.declare_term_names t Name.context; val xs = rev (#1 (Name.variants (rev (map #2 bs)) names)); - fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T)); + fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T)); in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^ diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/sign.ML Fri Apr 08 17:13:49 2011 +0200 @@ -334,7 +334,7 @@ fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) => let fun type_syntax (b, n, mx) = - (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx); + (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx); val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn; val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig; in (naming, syn', tsig', consts) end); @@ -373,7 +373,7 @@ fun type_notation add mode args = let fun type_syntax (Type (c, args), mx) = - SOME (Syntax.mark_type c, Syntax.make_type (length args), mx) + SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end; @@ -381,7 +381,7 @@ let fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of - SOME T => SOME (Syntax.mark_const c, T, mx) + SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end; @@ -401,7 +401,7 @@ val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b)); val T' = Logic.varifyT_global T; - in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end; + in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in thy @@ -468,7 +468,7 @@ local -fun mk trs = map Syntax.mk_trfun trs; +fun mk trs = map Syntax_Ext.mk_trfun trs; fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) = map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)); @@ -477,9 +477,9 @@ in -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr'; +val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr'; val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns; -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr''; +val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr''; val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns; end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/tactic.ML --- a/src/Pure/tactic.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/tactic.ML Fri Apr 08 17:13:49 2011 +0200 @@ -318,7 +318,7 @@ (*Renaming of parameters in a subgoal*) fun rename_tac xs i = - case Library.find_first (not o Syntax.is_identifier) xs of + case Library.find_first (not o Lexicon.is_identifier) xs of SOME x => error ("Not an identifier: " ^ x) | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i)); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/type_infer.ML Fri Apr 08 17:13:49 2011 +0200 @@ -300,7 +300,7 @@ val (Ts', Ts'') = chop (length Ts) Ts_bTs'; fun prep t = let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) - in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; in (map prep ts', Ts') end; fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); diff -r 12635bb655fd -r c2b5dbb76b7e src/Pure/unify.ML --- a/src/Pure/unify.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Pure/unify.ML Fri Apr 08 17:13:49 2011 +0200 @@ -596,7 +596,7 @@ let fun termT t = Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); - val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, termT t]; + val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]; in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end; in tracing msg; List.app pdp dpairs end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Apr 08 17:13:49 2011 +0200 @@ -688,7 +688,7 @@ pair (IVar (SOME v)) | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) = let - val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t); + val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t); val v'' = if member (op =) (Term.add_free_names t' []) v' then SOME v' else NONE in diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/WWW_Find/find_theorems.ML --- a/src/Tools/WWW_Find/find_theorems.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/WWW_Find/find_theorems.ML Fri Apr 08 17:13:49 2011 +0200 @@ -236,7 +236,7 @@ end; in -val () = show_question_marks_default := false; +val () = Printer.show_question_marks_default := false; val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems); end; diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/induct.ML Fri Apr 08 17:13:49 2011 +0200 @@ -580,7 +580,7 @@ in if not (null params) then (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ - commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params)); + commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params)); Seq.single rule) else let diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Apr 08 17:13:49 2011 +0200 @@ -112,7 +112,7 @@ val tooltip: Markup_Tree.Select[String] = { - case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + name + case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = Isabelle.Int_Property("tooltip-margin")) diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/misc_legacy.ML Fri Apr 08 17:13:49 2011 +0200 @@ -61,7 +61,7 @@ fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) = strip_context_aux (params, H :: Hs, B) | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) = - let val (b, u) = Syntax.variant_abs (a, T, t) + let val (b, u) = Syntax_Trans.variant_abs (a, T, t) in strip_context_aux ((b, T) :: params, Hs, u) end | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); diff -r 12635bb655fd -r c2b5dbb76b7e src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/Tools/subtyping.ML Fri Apr 08 17:13:49 2011 +0200 @@ -200,7 +200,7 @@ val (Ts', Ts'') = chop (length Ts) Ts_bTs'; fun prep t = let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) - in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; in (map prep ts', Ts') end; fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); diff -r 12635bb655fd -r c2b5dbb76b7e src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/ZF/Tools/datatype_package.ML Fri Apr 08 17:13:49 2011 +0200 @@ -130,7 +130,7 @@ (*The function variable for a single constructor*) fun add_case ((_, T, _), name, args, _) (opno, cases) = - if Syntax.is_identifier name then + if Lexicon.is_identifier name then (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) else (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) diff -r 12635bb655fd -r c2b5dbb76b7e src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Apr 08 17:13:49 2011 +0200 @@ -78,7 +78,7 @@ and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); val rec_base_names = map Long_Name.base_name rec_names; - val dummy = assert_all Syntax.is_identifier rec_base_names + val dummy = assert_all Lexicon.is_identifier rec_base_names (fn a => "Base name of recursive set not an identifier: " ^ a); local (*Checking the introduction rules*) diff -r 12635bb655fd -r c2b5dbb76b7e src/ZF/Tools/numeral_syntax.ML --- a/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 16:31:14 2011 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 17:13:49 2011 +0200 @@ -71,7 +71,7 @@ (* translation of integer constant tokens to and from binary *) fun int_tr [t as Free (str, _)] = - Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str)) + Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str)) | int_tr ts = raise TERM ("int_tr", ts); fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)