--- 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.
--- 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 ("_\<Colon>_", [4, 0], 3)),
--- 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 "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
& @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
--- 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}}} \\
--- 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
--- 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
--- 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 (!?) *)
--- 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;
--- 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
--- 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 "\<rightarrow>" 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
--- 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 =
--- 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
*}
--- 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)
--- 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:
--- 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;
--- 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)
--- 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 *}
--- 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 *}
--- 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)
--- 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
--- 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
--- 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 *}
--- 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) =
--- 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;
*}
--- 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
*}
--- 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'),
--- 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 ("_\<Colon>_", [4, 0], 3)),
--- 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")) ();
--- 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'),
--- 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,
--- 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 ("_\<Colon>_", [4, 0], 3)),
--- 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"
--- 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
--- 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, _),
--- 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
*}
--- 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
--- 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)
--- 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
--- 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 _ = "";
--- 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
--- 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)) ::
--- 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;
--- 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
--- 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
--- 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) ^
--- 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
--- 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
--- 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;
--- 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
--- 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;
--- 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"},
--- 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 *)
--- 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)"
--- 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);
--- 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
--- 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 \
--- 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 #>
--- 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;
--- 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)
--- 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)
--- 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);
--- 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;
--- 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) [];
--- 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
--- 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;
--- 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;
--- 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 =
--- 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";
--- 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 *)
--- 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"
--- 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 *)
--- 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\\<Lambda>_./ _)", [0, 3], 3)),
- (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
- (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
|> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [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"])])]);
--- 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"];
--- 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";
--- 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;
--- 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;
--- 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)
--- 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;
+
--- 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;
--- 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;
+
--- 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 =
--- 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 =) ["(", ")", "/", "_", "\\<index>"];
-
-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)) ||
- $$ "\\<index>" >> 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 (\\<index>)";
-
-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;
--- 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;
--- 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";
-
--- /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 =) ["(", ")", "/", "_", "\\<index>"];
+
+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)) ||
+ $$ "\\<index>" >> 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 (\\<index>)";
+
+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;
--- 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};
--- /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;
--- 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
--- 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);
--- 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;
--- 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);
--- 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 (==)";
--- 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 "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [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),
--- 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" ^
--- 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;
--- 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));
--- 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);
--- 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;
--- 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
--- 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;
--- 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
--- 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"))
--- 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);
--- 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);
--- 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)
--- 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*)
--- 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)