1.1 --- a/NEWS Fri Apr 08 11:39:45 2011 +0200
1.2 +++ b/NEWS Fri Apr 08 13:31:16 2011 +0200
1.3 @@ -93,9 +93,10 @@
1.4 be disabled via the configuration option Syntax.positions, which is
1.5 called "syntax_positions" in Isar attribute syntax.
1.6
1.7 -* Discontinued special treatment of structure Ast: no pervasive
1.8 -content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to
1.9 -qualified names like Ast.Constant etc.
1.10 +* Discontinued special treatment of various ML structures of inner
1.11 +syntax, such as structure Ast: no pervasive content, no inclusion in
1.12 +structure Syntax. INCOMPATIBILITY, refer to qualified names like
1.13 +Ast.Constant etc.
1.14
1.15 * Typed print translation: discontinued show_sorts argument, which is
1.16 already available via context of "advanced" translation.
2.1 --- a/src/CCL/Term.thy Fri Apr 08 11:39:45 2011 +0200
2.2 +++ b/src/CCL/Term.thy Fri Apr 08 13:31:16 2011 +0200
2.3 @@ -56,11 +56,11 @@
2.4 (** Quantifier translations: variable binding **)
2.5
2.6 (* FIXME does not handle "_idtdummy" *)
2.7 -(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
2.8 +(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
2.9
2.10 fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
2.11 fun let_tr' [a,Abs(id,T,b)] =
2.12 - let val (id',b') = variant_abs(id,T,b)
2.13 + let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
2.14 in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
2.15
2.16 fun letrec_tr [Free(f,S),Free(x,T),a,b] =
2.17 @@ -72,23 +72,23 @@
2.18 absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
2.19
2.20 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
2.21 - let val (f',b') = variant_abs(ff,SS,b)
2.22 - val (_,a'') = variant_abs(f,S,a)
2.23 - val (x',a') = variant_abs(x,T,a'')
2.24 + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
2.25 + val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
2.26 + val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
2.27 in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
2.28 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
2.29 - let val (f',b') = variant_abs(ff,SS,b)
2.30 - val ( _,a1) = variant_abs(f,S,a)
2.31 - val (y',a2) = variant_abs(y,U,a1)
2.32 - val (x',a') = variant_abs(x,T,a2)
2.33 + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
2.34 + val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
2.35 + val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
2.36 + val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
2.37 in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
2.38 end;
2.39 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
2.40 - let val (f',b') = variant_abs(ff,SS,b)
2.41 - val ( _,a1) = variant_abs(f,S,a)
2.42 - val (z',a2) = variant_abs(z,V,a1)
2.43 - val (y',a3) = variant_abs(y,U,a2)
2.44 - val (x',a') = variant_abs(x,T,a3)
2.45 + let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
2.46 + val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
2.47 + val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
2.48 + val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
2.49 + val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
2.50 in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
2.51 end;
2.52
3.1 --- a/src/CCL/Type.thy Fri Apr 08 11:39:45 2011 +0200
3.2 +++ b/src/CCL/Type.thy Fri Apr 08 13:31:16 2011 +0200
3.3 @@ -46,8 +46,10 @@
3.4 "{x: A. B}" == "CONST Subtype(A, %x. B)"
3.5
3.6 print_translation {*
3.7 - [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
3.8 - (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
3.9 + [(@{const_syntax Pi},
3.10 + Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
3.11 + (@{const_syntax Sigma},
3.12 + Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
3.13 *}
3.14
3.15 defs
4.1 --- a/src/Cube/Cube.thy Fri Apr 08 11:39:45 2011 +0200
4.2 +++ b/src/Cube/Cube.thy Fri Apr 08 13:31:16 2011 +0200
4.3 @@ -53,7 +53,8 @@
4.4 "_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10)
4.5
4.6 print_translation {*
4.7 - [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
4.8 + [(@{const_syntax Prod},
4.9 + Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
4.10 *}
4.11
4.12 axioms
5.1 --- a/src/FOLP/simp.ML Fri Apr 08 11:39:45 2011 +0200
5.2 +++ b/src/FOLP/simp.ML Fri Apr 08 13:31:16 2011 +0200
5.3 @@ -371,7 +371,7 @@
5.4 (*Replace parameters by Free variables in P*)
5.5 fun variants_abs ([],P) = P
5.6 | variants_abs ((a,T)::aTs, P) =
5.7 - variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
5.8 + variants_abs (aTs, #2 (Syntax_Trans.variant_abs(a,T,P)));
5.9
5.10 (*Select subgoal i from proof state; substitute parameters, for printing*)
5.11 fun prepare_goal i st =
6.1 --- a/src/HOL/Big_Operators.thy Fri Apr 08 11:39:45 2011 +0200
6.2 +++ b/src/HOL/Big_Operators.thy Fri Apr 08 13:31:16 2011 +0200
6.3 @@ -86,10 +86,10 @@
6.4 if x <> y then raise Match
6.5 else
6.6 let
6.7 - val x' = Syntax.mark_bound x;
6.8 + val x' = Syntax_Trans.mark_bound x;
6.9 val t' = subst_bound (x', t);
6.10 val P' = subst_bound (x', P);
6.11 - in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
6.12 + in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
6.13 | setsum_tr' _ = raise Match;
6.14 in [(@{const_syntax setsum}, setsum_tr')] end
6.15 *}
7.1 --- a/src/HOL/Complete_Lattice.thy Fri Apr 08 11:39:45 2011 +0200
7.2 +++ b/src/HOL/Complete_Lattice.thy Fri Apr 08 13:31:16 2011 +0200
7.3 @@ -159,8 +159,8 @@
7.4 "SUP x:A. B" == "CONST SUPR A (%x. B)"
7.5
7.6 print_translation {*
7.7 - [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
7.8 - Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
7.9 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
7.10 + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
7.11 *} -- {* to avoid eta-contraction of body *}
7.12
7.13 context complete_lattice
7.14 @@ -409,7 +409,7 @@
7.15 "INT x:A. B" == "CONST INTER A (%x. B)"
7.16
7.17 print_translation {*
7.18 - [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
7.19 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
7.20 *} -- {* to avoid eta-contraction of body *}
7.21
7.22 lemma INTER_eq_Inter_image:
7.23 @@ -612,7 +612,7 @@
7.24 *}
7.25
7.26 print_translation {*
7.27 - [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
7.28 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
7.29 *} -- {* to avoid eta-contraction of body *}
7.30
7.31 lemma UNION_eq_Union_image:
8.1 --- a/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 11:39:45 2011 +0200
8.2 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 13:31:16 2011 +0200
8.3 @@ -1924,12 +1924,12 @@
8.4 @{code NOT} (fm_of_term ps vs t')
8.5 | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
8.6 let
8.7 - val (xn', p') = variant_abs (xn, xT, p);
8.8 + val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
8.9 val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
8.10 in @{code E} (fm_of_term ps vs' p) end
8.11 | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
8.12 let
8.13 - val (xn', p') = variant_abs (xn, xT, p);
8.14 + val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
8.15 val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
8.16 in @{code A} (fm_of_term ps vs' p) end
8.17 | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
8.18 @@ -1988,7 +1988,7 @@
8.19 else insert (op aconv) t acc
8.20 | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a
8.21 else insert (op aconv) t acc
8.22 - | Abs p => term_bools acc (snd (variant_abs p))
8.23 + | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *)
8.24 | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
8.25 end;
8.26
9.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 08 11:39:45 2011 +0200
9.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 08 13:31:16 2011 +0200
9.3 @@ -2939,13 +2939,13 @@
9.4 | Const(@{const_name Orderings.less_eq},_)$p$q =>
9.5 @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
9.6 | Const(@{const_name Ex},_)$Abs(xn,xT,p) =>
9.7 - let val (xn', p') = variant_abs (xn,xT,p)
9.8 + let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p) (* FIXME !? *)
9.9 val x = Free(xn',xT)
9.10 fun incr i = i + 1
9.11 val m0 = (x,0):: (map (apsnd incr) m)
9.12 in @{code E} (fm_of_term m0 m' p') end
9.13 | Const(@{const_name All},_)$Abs(xn,xT,p) =>
9.14 - let val (xn', p') = variant_abs (xn,xT,p)
9.15 + let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p) (* FIXME !? *)
9.16 val x = Free(xn',xT)
9.17 fun incr i = i + 1
9.18 val m0 = (x,0):: (map (apsnd incr) m)
10.1 --- a/src/HOL/HOL.thy Fri Apr 08 11:39:45 2011 +0200
10.2 +++ b/src/HOL/HOL.thy Fri Apr 08 13:31:16 2011 +0200
10.3 @@ -130,7 +130,7 @@
10.4
10.5 print_translation {*
10.6 [(@{const_syntax The}, fn [Abs abs] =>
10.7 - let val (x, t) = atomic_abs_tr' abs
10.8 + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
10.9 in Syntax.const @{syntax_const "_The"} $ x $ t end)]
10.10 *} -- {* To avoid eta-contraction of body *}
10.11
11.1 --- a/src/HOL/HOLCF/Cfun.thy Fri Apr 08 11:39:45 2011 +0200
11.2 +++ b/src/HOL/HOLCF/Cfun.thy Fri Apr 08 13:31:16 2011 +0200
11.3 @@ -34,12 +34,12 @@
11.4
11.5 parse_translation {*
11.6 (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
11.7 - [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
11.8 + [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
11.9 *}
11.10
11.11 print_translation {*
11.12 [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
11.13 - let val (x, t) = atomic_abs_tr' abs
11.14 + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
11.15 in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
11.16 *} -- {* To avoid eta-contraction of body *}
11.17
12.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 11:39:45 2011 +0200
12.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 13:31:16 2011 +0200
12.3 @@ -132,7 +132,7 @@
12.4 (* rewrite (_pat x) => (succeed) *)
12.5 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
12.6 [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
12.7 - mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
12.8 + Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
12.9 *}
12.10
12.11 text {* Printing Case expressions *}
12.12 @@ -154,7 +154,7 @@
12.13 val abs =
12.14 case t of Abs abs => abs
12.15 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
12.16 - val (x, t') = atomic_abs_tr' abs;
12.17 + val (x, t') = Syntax_Trans.atomic_abs_tr' abs;
12.18 in (Syntax.const @{syntax_const "_variable"} $ x, t') end
12.19 | dest_LAM _ = raise Match; (* too few vars: abort translation *)
12.20
13.1 --- a/src/HOL/Hilbert_Choice.thy Fri Apr 08 11:39:45 2011 +0200
13.2 +++ b/src/HOL/Hilbert_Choice.thy Fri Apr 08 13:31:16 2011 +0200
13.3 @@ -26,7 +26,7 @@
13.4
13.5 print_translation {*
13.6 [(@{const_syntax Eps}, fn [Abs abs] =>
13.7 - let val (x, t) = atomic_abs_tr' abs
13.8 + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
13.9 in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
13.10 *} -- {* to avoid eta-contraction of body *}
13.11
14.1 --- a/src/HOL/Hoare/hoare_syntax.ML Fri Apr 08 11:39:45 2011 +0200
14.2 +++ b/src/HOL/Hoare/hoare_syntax.ML Fri Apr 08 13:31:16 2011 +0200
14.3 @@ -26,9 +26,9 @@
14.4 (SOME x, SOME y) => x = y
14.5 | _ => false);
14.6
14.7 -fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
14.8 +fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
14.9 | mk_abstuple (x :: xs) body =
14.10 - Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
14.11 + Syntax.const @{const_syntax prod_case} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
14.12
14.13 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
14.14 | mk_fbody x e (y :: xs) =
15.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 11:39:45 2011 +0200
15.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 13:31:16 2011 +0200
15.3 @@ -76,11 +76,11 @@
15.4 print_translation {*
15.5 let
15.6 fun quote_tr' f (t :: ts) =
15.7 - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
15.8 + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
15.9 | quote_tr' _ _ = raise Match;
15.10
15.11 fun annquote_tr' f (r :: t :: ts) =
15.12 - Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
15.13 + Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
15.14 | annquote_tr' _ _ = raise Match;
15.15
15.16 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
15.17 @@ -94,13 +94,13 @@
15.18 | annbexp_tr' _ _ = raise Match;
15.19
15.20 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
15.21 - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
15.22 - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
15.23 + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
15.24 + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
15.25 | assign_tr' _ = raise Match;
15.26
15.27 fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
15.28 - quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
15.29 - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
15.30 + quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
15.31 + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
15.32 | annassign_tr' _ = raise Match;
15.33
15.34 fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
16.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 11:39:45 2011 +0200
16.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 13:31:16 2011 +0200
16.3 @@ -16,7 +16,7 @@
16.4
16.5 parse_translation {*
16.6 let
16.7 - fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
16.8 + fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
16.9 | quote_tr ts = raise TERM ("quote_tr", ts);
16.10 in [(@{syntax_const "_quote"}, quote_tr)] end
16.11 *}
17.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 11:39:45 2011 +0200
17.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 13:31:16 2011 +0200
17.3 @@ -58,7 +58,7 @@
17.4 print_translation {*
17.5 let
17.6 fun quote_tr' f (t :: ts) =
17.7 - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
17.8 + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
17.9 | quote_tr' _ _ = raise Match;
17.10
17.11 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
17.12 @@ -68,8 +68,8 @@
17.13 | bexp_tr' _ _ = raise Match;
17.14
17.15 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
17.16 - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
17.17 - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
17.18 + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
17.19 + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
17.20 | assign_tr' _ = raise Match;
17.21 in
17.22 [(@{const_syntax Collect}, assert_tr'),
18.1 --- a/src/HOL/Isar_Examples/Hoare.thy Fri Apr 08 11:39:45 2011 +0200
18.2 +++ b/src/HOL/Isar_Examples/Hoare.thy Fri Apr 08 13:31:16 2011 +0200
18.3 @@ -185,8 +185,8 @@
18.4 of the concrete syntactic representation of our Hoare language, the
18.5 actual ``ML drivers'' is quite involved. Just note that the we
18.6 re-use the basic quote/antiquote translations as already defined in
18.7 - Isabelle/Pure (see \verb,Syntax.quote_tr, and
18.8 - \verb,Syntax.quote_tr',). *}
18.9 + Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
18.10 + @{ML Syntax_Trans.quote_tr'},). *}
18.11
18.12 syntax
18.13 "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000)
18.14 @@ -215,7 +215,7 @@
18.15
18.16 parse_translation {*
18.17 let
18.18 - fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
18.19 + fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
18.20 | quote_tr ts = raise TERM ("quote_tr", ts);
18.21 in [(@{syntax_const "_quote"}, quote_tr)] end
18.22 *}
18.23 @@ -228,7 +228,7 @@
18.24 print_translation {*
18.25 let
18.26 fun quote_tr' f (t :: ts) =
18.27 - Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
18.28 + Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
18.29 | quote_tr' _ _ = raise Match;
18.30
18.31 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
18.32 @@ -238,8 +238,8 @@
18.33 | bexp_tr' _ _ = raise Match;
18.34
18.35 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
18.36 - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
18.37 - (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
18.38 + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
18.39 + (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
18.40 | assign_tr' _ = raise Match;
18.41 in
18.42 [(@{const_syntax Collect}, assert_tr'),
19.1 --- a/src/HOL/Library/reflection.ML Fri Apr 08 11:39:45 2011 +0200
19.2 +++ b/src/HOL/Library/reflection.ML Fri Apr 08 13:31:16 2011 +0200
19.3 @@ -125,7 +125,7 @@
19.4 Abs(xn,xT,ta) => (
19.5 let
19.6 val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
19.7 - val (xn,ta) = variant_abs (xn,xT,ta)
19.8 + val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta) (* FIXME !? *)
19.9 val x = Free(xn,xT)
19.10 val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT)
19.11 of NONE => error "tryabsdecomp: Type not found in the Environement"
20.1 --- a/src/HOL/Orderings.thy Fri Apr 08 11:39:45 2011 +0200
20.2 +++ b/src/HOL/Orderings.thy Fri Apr 08 13:31:16 2011 +0200
20.3 @@ -660,7 +660,7 @@
20.4 Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
20.5 | _ => false);
20.6 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
20.7 - fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
20.8 + fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
20.9
20.10 fun tr' q = (q,
20.11 fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
21.1 --- a/src/HOL/Product_Type.thy Fri Apr 08 11:39:45 2011 +0200
21.2 +++ b/src/HOL/Product_Type.thy Fri Apr 08 13:31:16 2011 +0200
21.3 @@ -199,8 +199,8 @@
21.4 fun split_tr' [Abs (x, T, t as (Abs abs))] =
21.5 (* split (%x y. t) => %(x,y) t *)
21.6 let
21.7 - val (y, t') = atomic_abs_tr' abs;
21.8 - val (x', t'') = atomic_abs_tr' (x, T, t');
21.9 + val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
21.10 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
21.11 in
21.12 Syntax.const @{syntax_const "_abs"} $
21.13 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
21.14 @@ -210,7 +210,7 @@
21.15 let
21.16 val Const (@{syntax_const "_abs"}, _) $
21.17 (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
21.18 - val (x', t'') = atomic_abs_tr' (x, T, t');
21.19 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
21.20 in
21.21 Syntax.const @{syntax_const "_abs"} $
21.22 (Syntax.const @{syntax_const "_pattern"} $ x' $
21.23 @@ -221,7 +221,7 @@
21.24 split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
21.25 | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
21.26 (* split (%pttrn z. t) => %(pttrn,z). t *)
21.27 - let val (z, t) = atomic_abs_tr' abs in
21.28 + let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
21.29 Syntax.const @{syntax_const "_abs"} $
21.30 (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
21.31 end
21.32 @@ -239,8 +239,8 @@
21.33 | _ =>
21.34 let
21.35 val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
21.36 - val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
21.37 - val (x', t'') = atomic_abs_tr' (x, xT, t');
21.38 + val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
21.39 + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
21.40 in
21.41 Syntax.const @{syntax_const "_abs"} $
21.42 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
21.43 @@ -251,8 +251,9 @@
21.44 | _ =>
21.45 let
21.46 val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
21.47 - val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
21.48 - val (x', t'') = atomic_abs_tr' ("x", xT, t');
21.49 + val (y, t') =
21.50 + Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
21.51 + val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
21.52 in
21.53 Syntax.const @{syntax_const "_abs"} $
21.54 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
21.55 @@ -276,10 +277,10 @@
21.56 | _ => f ts;
21.57 fun contract2 (Q,f) = (Q, contract Q f);
21.58 val pairs =
21.59 - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
21.60 - Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
21.61 - Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
21.62 - Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
21.63 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
21.64 + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
21.65 + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
21.66 + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
21.67 in map contract2 pairs end
21.68 *}
21.69
22.1 --- a/src/HOL/Set.thy Fri Apr 08 11:39:45 2011 +0200
22.2 +++ b/src/HOL/Set.thy Fri Apr 08 13:31:16 2011 +0200
22.3 @@ -246,7 +246,7 @@
22.4
22.5 fun mk v v' c n P =
22.6 if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
22.7 - then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
22.8 + then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
22.9
22.10 fun tr' q = (q,
22.11 fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
22.12 @@ -275,7 +275,7 @@
22.13
22.14 parse_translation {*
22.15 let
22.16 - val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
22.17 + val ex_tr = snd (Syntax_Trans.mk_binder_tr ("EX ", @{const_syntax Ex}));
22.18
22.19 fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
22.20 | nvars _ = 1;
22.21 @@ -291,13 +291,13 @@
22.22 *}
22.23
22.24 print_translation {*
22.25 - [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
22.26 - Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
22.27 + [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
22.28 + Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
22.29 *} -- {* to avoid eta-contraction of body *}
22.30
22.31 print_translation {*
22.32 let
22.33 - val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
22.34 + val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
22.35
22.36 fun setcompr_tr' [Abs (abs as (_, _, P))] =
22.37 let
22.38 @@ -315,7 +315,7 @@
22.39 if check (P, 0) then tr' P
22.40 else
22.41 let
22.42 - val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
22.43 + val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
22.44 val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
22.45 in
22.46 case t of
23.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 11:39:45 2011 +0200
23.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 13:31:16 2011 +0200
23.3 @@ -454,12 +454,12 @@
23.4 let val xs = Term.add_frees pat [] in
23.5 Syntax.const @{syntax_const "_case1"} $
23.6 map_aterms
23.7 - (fn Free p => Syntax.mark_boundT p
23.8 + (fn Free p => Syntax_Trans.mark_boundT p
23.9 | Const (s, _) => Syntax.const (Syntax.mark_const s)
23.10 | t => t) pat $
23.11 map_aterms
23.12 (fn x as Free (s, T) =>
23.13 - if member (op =) xs (s, T) then Syntax.mark_bound s else x
23.14 + if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
23.15 | t => t) rhs
23.16 end;
23.17 in
24.1 --- a/src/HOL/Tools/Qelim/cooper.ML Fri Apr 08 11:39:45 2011 +0200
24.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Apr 08 13:31:16 2011 +0200
24.3 @@ -579,13 +579,13 @@
24.4 else insert (op aconv) t
24.5 | f $ a => if skip orelse is_op f then add_bools a o add_bools f
24.6 else insert (op aconv) t
24.7 - | Abs p => add_bools (snd (variant_abs p))
24.8 + | Abs p => add_bools (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *)
24.9 | _ => if skip orelse is_op t then I else insert (op aconv) t
24.10 end;
24.11
24.12 fun descend vs (abs as (_, xT, _)) =
24.13 let
24.14 - val (xn', p') = variant_abs abs;
24.15 + val (xn', p') = Syntax_Trans.variant_abs abs; (* FIXME !? *)
24.16 in ((xn', xT) :: vs, p') end;
24.17
24.18 local structure Proc = Cooper_Procedure in
25.1 --- a/src/HOL/Tools/record.ML Fri Apr 08 11:39:45 2011 +0200
25.2 +++ b/src/HOL/Tools/record.ML Fri Apr 08 13:31:16 2011 +0200
25.3 @@ -963,7 +963,7 @@
25.4 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
25.5 (case dest_update ctxt c of
25.6 SOME name =>
25.7 - (case try Syntax.const_abs_tr' k of
25.8 + (case try Syntax_Trans.const_abs_tr' k of
25.9 SOME t =>
25.10 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
25.11 (field_updates_tr' ctxt u)
26.1 --- a/src/HOL/ex/Antiquote.thy Fri Apr 08 11:39:45 2011 +0200
26.2 +++ b/src/HOL/ex/Antiquote.thy Fri Apr 08 13:31:16 2011 +0200
26.3 @@ -25,11 +25,13 @@
26.4 where "Expr exp env = exp env"
26.5
26.6 parse_translation {*
26.7 - [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
26.8 + [Syntax_Trans.quote_antiquote_tr
26.9 + @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
26.10 *}
26.11
26.12 print_translation {*
26.13 - [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
26.14 + [Syntax_Trans.quote_antiquote_tr'
26.15 + @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
26.16 *}
26.17
26.18 term "EXPR (a + b + c)"
27.1 --- a/src/Pure/IsaMakefile Fri Apr 08 11:39:45 2011 +0200
27.2 +++ b/src/Pure/IsaMakefile Fri Apr 08 13:31:16 2011 +0200
27.3 @@ -185,9 +185,9 @@
27.4 Syntax/printer.ML \
27.5 Syntax/simple_syntax.ML \
27.6 Syntax/syn_ext.ML \
27.7 - Syntax/syn_trans.ML \
27.8 Syntax/syntax.ML \
27.9 Syntax/syntax_phases.ML \
27.10 + Syntax/syntax_trans.ML \
27.11 Syntax/term_position.ML \
27.12 System/isabelle_process.ML \
27.13 System/isabelle_system.ML \
28.1 --- a/src/Pure/Isar/attrib.ML Fri Apr 08 11:39:45 2011 +0200
28.2 +++ b/src/Pure/Isar/attrib.ML Fri Apr 08 13:31:16 2011 +0200
28.3 @@ -407,7 +407,7 @@
28.4 register_config Syntax.show_structs_raw #>
28.5 register_config Syntax.show_question_marks_raw #>
28.6 register_config Syntax.ambiguity_level_raw #>
28.7 - register_config Syntax.eta_contract_raw #>
28.8 + register_config Syntax_Trans.eta_contract_raw #>
28.9 register_config ML_Context.trace_raw #>
28.10 register_config ProofContext.show_abbrevs_raw #>
28.11 register_config Goal_Display.goals_limit_raw #>
29.1 --- a/src/Pure/Isar/obtain.ML Fri Apr 08 11:39:45 2011 +0200
29.2 +++ b/src/Pure/Isar/obtain.ML Fri Apr 08 13:31:16 2011 +0200
29.3 @@ -231,7 +231,7 @@
29.4 handle Type.TUNIFY =>
29.5 err ("Failed to unify variable " ^
29.6 string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
29.7 - string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
29.8 + string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
29.9 val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
29.10 (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
29.11 val norm_type = Envir.norm_type tyenv;
30.1 --- a/src/Pure/ProofGeneral/preferences.ML Fri Apr 08 11:39:45 2011 +0200
30.2 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Apr 08 13:31:16 2011 +0200
30.3 @@ -133,7 +133,7 @@
30.4 bool_pref Goal_Display.show_main_goal_default
30.5 "show-main-goal"
30.6 "Show main goal in proof state display",
30.7 - bool_pref Syntax.eta_contract_default
30.8 + bool_pref Syntax_Trans.eta_contract_default
30.9 "eta-contract"
30.10 "Print terms eta-contracted"];
30.11
31.1 --- a/src/Pure/ROOT.ML Fri Apr 08 11:39:45 2011 +0200
31.2 +++ b/src/Pure/ROOT.ML Fri Apr 08 13:31:16 2011 +0200
31.3 @@ -124,7 +124,7 @@
31.4 use "Syntax/ast.ML";
31.5 use "Syntax/syn_ext.ML";
31.6 use "Syntax/parser.ML";
31.7 -use "Syntax/syn_trans.ML";
31.8 +use "Syntax/syntax_trans.ML";
31.9 use "Syntax/mixfix.ML";
31.10 use "Syntax/printer.ML";
31.11 use "Syntax/syntax.ML";
32.1 --- a/src/Pure/Syntax/local_syntax.ML Fri Apr 08 11:39:45 2011 +0200
32.2 +++ b/src/Pure/Syntax/local_syntax.ML Fri Apr 08 13:31:16 2011 +0200
32.3 @@ -58,7 +58,7 @@
32.4 | update_gram ((false, add, m), decls) =
32.5 Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
32.6
32.7 - val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
32.8 + val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
32.9 val local_syntax = thy_syntax
32.10 |> Syntax.update_trfuns
32.11 (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
33.1 --- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 11:39:45 2011 +0200
33.2 +++ b/src/Pure/Syntax/mixfix.ML Fri Apr 08 13:31:16 2011 +0200
33.3 @@ -154,10 +154,10 @@
33.4 val xconsts = map #1 const_decls;
33.5 val binders = map_filter binder const_decls;
33.6 val binder_trs = binders
33.7 - |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
33.8 + |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
33.9 val binder_trs' = binders
33.10 |> map (Syn_Ext.stamp_trfun binder_stamp o
33.11 - apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
33.12 + apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
33.13 in
33.14 Syn_Ext.syn_ext' true is_logtype
33.15 mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
34.1 --- a/src/Pure/Syntax/printer.ML Fri Apr 08 11:39:45 2011 +0200
34.2 +++ b/src/Pure/Syntax/printer.ML Fri Apr 08 13:31:16 2011 +0200
34.3 @@ -173,9 +173,9 @@
34.4
34.5 (*default applications: prefix / postfix*)
34.6 val appT =
34.7 - if type_mode then Syn_Trans.tappl_ast_tr'
34.8 - else if curried then Syn_Trans.applC_ast_tr'
34.9 - else Syn_Trans.appl_ast_tr';
34.10 + if type_mode then Syntax_Trans.tappl_ast_tr'
34.11 + else if curried then Syntax_Trans.applC_ast_tr'
34.12 + else Syntax_Trans.appl_ast_tr';
34.13
34.14 fun synT _ ([], args) = ([], args)
34.15 | synT m (Arg p :: symbs, t :: args) =
35.1 --- a/src/Pure/Syntax/syn_trans.ML Fri Apr 08 11:39:45 2011 +0200
35.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
35.3 @@ -1,560 +0,0 @@
35.4 -(* Title: Pure/Syntax/syn_trans.ML
35.5 - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
35.6 -
35.7 -Syntax translation functions.
35.8 -*)
35.9 -
35.10 -signature SYN_TRANS0 =
35.11 -sig
35.12 - val eta_contract_default: bool Unsynchronized.ref
35.13 - val eta_contract_raw: Config.raw
35.14 - val eta_contract: bool Config.T
35.15 - val atomic_abs_tr': string * typ * term -> term * term
35.16 - val const_abs_tr': term -> term
35.17 - val mk_binder_tr: string * string -> string * (term list -> term)
35.18 - val mk_binder_tr': string * string -> string * (term list -> term)
35.19 - val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
35.20 - val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
35.21 - val dependent_tr': string * string -> term list -> term
35.22 - val antiquote_tr: string -> term -> term
35.23 - val quote_tr: string -> term -> term
35.24 - val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
35.25 - val antiquote_tr': string -> term -> term
35.26 - val quote_tr': string -> term -> term
35.27 - val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
35.28 - val update_name_tr': term -> term
35.29 - val mark_bound: string -> term
35.30 - val mark_boundT: string * typ -> term
35.31 - val bound_vars: (string * typ) list -> term -> term
35.32 - val variant_abs: string * typ * term -> string * term
35.33 - val variant_abs': string * typ * term -> string * term
35.34 -end;
35.35 -
35.36 -signature SYN_TRANS1 =
35.37 -sig
35.38 - include SYN_TRANS0
35.39 - val no_brackets: unit -> bool
35.40 - val no_type_brackets: unit -> bool
35.41 - val non_typed_tr': (term list -> term) -> typ -> term list -> term
35.42 - val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
35.43 - val constrainAbsC: string
35.44 - val abs_tr: term list -> term
35.45 - val pure_trfuns:
35.46 - (string * (Ast.ast list -> Ast.ast)) list *
35.47 - (string * (term list -> term)) list *
35.48 - (string * (term list -> term)) list *
35.49 - (string * (Ast.ast list -> Ast.ast)) list
35.50 - val struct_trfuns: string list ->
35.51 - (string * (Ast.ast list -> Ast.ast)) list *
35.52 - (string * (term list -> term)) list *
35.53 - (string * (typ -> term list -> term)) list *
35.54 - (string * (Ast.ast list -> Ast.ast)) list
35.55 -end;
35.56 -
35.57 -signature SYN_TRANS =
35.58 -sig
35.59 - include SYN_TRANS1
35.60 - val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
35.61 - val abs_tr': Proof.context -> term -> term
35.62 - val prop_tr': term -> term
35.63 - val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
35.64 - val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
35.65 -end;
35.66 -
35.67 -structure Syn_Trans: SYN_TRANS =
35.68 -struct
35.69 -
35.70 -(* print mode *)
35.71 -
35.72 -val bracketsN = "brackets";
35.73 -val no_bracketsN = "no_brackets";
35.74 -
35.75 -fun no_brackets () =
35.76 - find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
35.77 - (print_mode_value ()) = SOME no_bracketsN;
35.78 -
35.79 -val type_bracketsN = "type_brackets";
35.80 -val no_type_bracketsN = "no_type_brackets";
35.81 -
35.82 -fun no_type_brackets () =
35.83 - find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
35.84 - (print_mode_value ()) <> SOME type_bracketsN;
35.85 -
35.86 -
35.87 -
35.88 -(** parse (ast) translations **)
35.89 -
35.90 -(* strip_positions *)
35.91 -
35.92 -fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
35.93 - | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
35.94 -
35.95 -
35.96 -(* constify *)
35.97 -
35.98 -fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
35.99 - | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
35.100 -
35.101 -
35.102 -(* type syntax *)
35.103 -
35.104 -fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
35.105 - | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
35.106 -
35.107 -fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
35.108 - | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
35.109 -
35.110 -fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
35.111 - | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
35.112 -
35.113 -
35.114 -(* application *)
35.115 -
35.116 -fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
35.117 - | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
35.118 -
35.119 -fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
35.120 - | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
35.121 -
35.122 -
35.123 -(* abstraction *)
35.124 -
35.125 -fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
35.126 - | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
35.127 -
35.128 -fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
35.129 - | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
35.130 -
35.131 -fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
35.132 - | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
35.133 -
35.134 -val constrainAbsC = "_constrainAbs";
35.135 -
35.136 -fun absfree_proper (x, T, t) =
35.137 - if can Name.dest_internal x
35.138 - then error ("Illegal internal variable in abstraction: " ^ quote x)
35.139 - else Term.absfree (x, T, t);
35.140 -
35.141 -fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
35.142 - | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
35.143 - | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT
35.144 - | abs_tr ts = raise TERM ("abs_tr", ts);
35.145 -
35.146 -
35.147 -(* binder *)
35.148 -
35.149 -fun mk_binder_tr (syn, name) =
35.150 - let
35.151 - fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
35.152 - fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
35.153 - | binder_tr [x, t] =
35.154 - let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
35.155 - in Lexicon.const name $ abs end
35.156 - | binder_tr ts = err ts;
35.157 - in (syn, binder_tr) end;
35.158 -
35.159 -
35.160 -(* type propositions *)
35.161 -
35.162 -fun mk_type ty =
35.163 - Lexicon.const "_constrain" $
35.164 - Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
35.165 -
35.166 -fun ofclass_tr [ty, cls] = cls $ mk_type ty
35.167 - | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
35.168 -
35.169 -fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
35.170 - | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
35.171 -
35.172 -
35.173 -(* meta propositions *)
35.174 -
35.175 -fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
35.176 - | aprop_tr ts = raise TERM ("aprop_tr", ts);
35.177 -
35.178 -
35.179 -(* meta implication *)
35.180 -
35.181 -fun bigimpl_ast_tr (asts as [asms, concl]) =
35.182 - let val prems =
35.183 - (case Ast.unfold_ast_p "_asms" asms of
35.184 - (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
35.185 - | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
35.186 - in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
35.187 - | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
35.188 -
35.189 -
35.190 -(* type/term reflection *)
35.191 -
35.192 -fun type_tr [ty] = mk_type ty
35.193 - | type_tr ts = raise TERM ("type_tr", ts);
35.194 -
35.195 -
35.196 -(* dddot *)
35.197 -
35.198 -fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
35.199 -
35.200 -
35.201 -(* quote / antiquote *)
35.202 -
35.203 -fun antiquote_tr name =
35.204 - let
35.205 - fun tr i ((t as Const (c, _)) $ u) =
35.206 - if c = name then tr i u $ Bound i
35.207 - else tr i t $ tr i u
35.208 - | tr i (t $ u) = tr i t $ tr i u
35.209 - | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
35.210 - | tr _ a = a;
35.211 - in tr 0 end;
35.212 -
35.213 -fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
35.214 -
35.215 -fun quote_antiquote_tr quoteN antiquoteN name =
35.216 - let
35.217 - fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
35.218 - | tr ts = raise TERM ("quote_tr", ts);
35.219 - in (quoteN, tr) end;
35.220 -
35.221 -
35.222 -(* corresponding updates *)
35.223 -
35.224 -fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
35.225 - | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
35.226 - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
35.227 - if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
35.228 - else
35.229 - list_comb (c $ update_name_tr [t] $
35.230 - (Lexicon.fun_type $
35.231 - (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
35.232 - | update_name_tr ts = raise TERM ("update_name_tr", ts);
35.233 -
35.234 -
35.235 -(* indexed syntax *)
35.236 -
35.237 -fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
35.238 - | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
35.239 -
35.240 -fun index_ast_tr ast =
35.241 - Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
35.242 -
35.243 -fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
35.244 - | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
35.245 -
35.246 -fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
35.247 - | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
35.248 -
35.249 -fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
35.250 - | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
35.251 -
35.252 -fun index_tr [t] = t
35.253 - | index_tr ts = raise TERM ("index_tr", ts);
35.254 -
35.255 -
35.256 -(* implicit structures *)
35.257 -
35.258 -fun the_struct structs i =
35.259 - if 1 <= i andalso i <= length structs then nth structs (i - 1)
35.260 - else error ("Illegal reference to implicit structure #" ^ string_of_int i);
35.261 -
35.262 -fun struct_tr structs [Const ("_indexdefault", _)] =
35.263 - Lexicon.free (the_struct structs 1)
35.264 - | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
35.265 - Lexicon.free (the_struct structs
35.266 - (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
35.267 - | struct_tr _ ts = raise TERM ("struct_tr", ts);
35.268 -
35.269 -
35.270 -
35.271 -(** print (ast) translations **)
35.272 -
35.273 -(* types *)
35.274 -
35.275 -fun non_typed_tr' f _ ts = f ts;
35.276 -fun non_typed_tr'' f x _ ts = f x ts;
35.277 -
35.278 -
35.279 -(* type syntax *)
35.280 -
35.281 -fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
35.282 - | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
35.283 - | tappl_ast_tr' (f, ty :: tys) =
35.284 - Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
35.285 -
35.286 -fun fun_ast_tr' asts =
35.287 - if no_brackets () orelse no_type_brackets () then raise Match
35.288 - else
35.289 - (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
35.290 - (dom as _ :: _ :: _, cod)
35.291 - => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
35.292 - | _ => raise Match);
35.293 -
35.294 -
35.295 -(* application *)
35.296 -
35.297 -fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
35.298 - | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
35.299 -
35.300 -fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
35.301 - | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
35.302 -
35.303 -
35.304 -(* partial eta-contraction before printing *)
35.305 -
35.306 -fun eta_abs (Abs (a, T, t)) =
35.307 - (case eta_abs t of
35.308 - t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
35.309 - | t' as f $ u =>
35.310 - (case eta_abs u of
35.311 - Bound 0 =>
35.312 - if Term.is_dependent f then Abs (a, T, t')
35.313 - else incr_boundvars ~1 f
35.314 - | _ => Abs (a, T, t'))
35.315 - | t' => Abs (a, T, t'))
35.316 - | eta_abs t = t;
35.317 -
35.318 -val eta_contract_default = Unsynchronized.ref true;
35.319 -val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
35.320 -val eta_contract = Config.bool eta_contract_raw;
35.321 -
35.322 -fun eta_contr ctxt tm =
35.323 - if Config.get ctxt eta_contract then eta_abs tm else tm;
35.324 -
35.325 -
35.326 -(* abstraction *)
35.327 -
35.328 -fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
35.329 -fun mark_bound x = mark_boundT (x, dummyT);
35.330 -
35.331 -fun bound_vars vars body =
35.332 - subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
35.333 -
35.334 -fun strip_abss vars_of body_of tm =
35.335 - let
35.336 - val vars = vars_of tm;
35.337 - val body = body_of tm;
35.338 - val rev_new_vars = Term.rename_wrt_term body vars;
35.339 - fun subst (x, T) b =
35.340 - if can Name.dest_internal x andalso not (Term.is_dependent b)
35.341 - then (Const ("_idtdummy", T), incr_boundvars ~1 b)
35.342 - else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
35.343 - val (rev_vars', body') = fold_map subst rev_new_vars body;
35.344 - in (rev rev_vars', body') end;
35.345 -
35.346 -
35.347 -fun abs_tr' ctxt tm =
35.348 - uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
35.349 - (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
35.350 -
35.351 -fun atomic_abs_tr' (x, T, t) =
35.352 - let val [xT] = Term.rename_wrt_term t [(x, T)]
35.353 - in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
35.354 -
35.355 -fun abs_ast_tr' asts =
35.356 - (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
35.357 - ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
35.358 - | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
35.359 -
35.360 -fun const_abs_tr' t =
35.361 - (case eta_abs t of
35.362 - Abs (_, _, t') =>
35.363 - if Term.is_dependent t' then raise Match
35.364 - else incr_boundvars ~1 t'
35.365 - | _ => raise Match);
35.366 -
35.367 -
35.368 -(* binders *)
35.369 -
35.370 -fun mk_binder_tr' (name, syn) =
35.371 - let
35.372 - fun mk_idts [] = raise Match (*abort translation*)
35.373 - | mk_idts [idt] = idt
35.374 - | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
35.375 -
35.376 - fun tr' t =
35.377 - let
35.378 - val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
35.379 - in Lexicon.const syn $ mk_idts xs $ bd end;
35.380 -
35.381 - fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
35.382 - | binder_tr' [] = raise Match;
35.383 - in (name, binder_tr') end;
35.384 -
35.385 -fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
35.386 - let val (x, t) = atomic_abs_tr' abs
35.387 - in list_comb (Lexicon.const syn $ x $ t, ts) end);
35.388 -
35.389 -fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
35.390 - let val (x, t) = atomic_abs_tr' abs
35.391 - in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
35.392 -
35.393 -
35.394 -(* idtyp constraints *)
35.395 -
35.396 -fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
35.397 - Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
35.398 - | idtyp_ast_tr' _ _ = raise Match;
35.399 -
35.400 -
35.401 -(* meta propositions *)
35.402 -
35.403 -fun prop_tr' tm =
35.404 - let
35.405 - fun aprop t = Lexicon.const "_aprop" $ t;
35.406 -
35.407 - fun is_prop Ts t =
35.408 - fastype_of1 (Ts, t) = propT handle TERM _ => false;
35.409 -
35.410 - fun is_term (Const ("Pure.term", _) $ _) = true
35.411 - | is_term _ = false;
35.412 -
35.413 - fun tr' _ (t as Const _) = t
35.414 - | tr' Ts (t as Const ("_bound", _) $ u) =
35.415 - if is_prop Ts u then aprop t else t
35.416 - | tr' _ (t as Free (x, T)) =
35.417 - if T = propT then aprop (Lexicon.free x) else t
35.418 - | tr' _ (t as Var (xi, T)) =
35.419 - if T = propT then aprop (Lexicon.var xi) else t
35.420 - | tr' Ts (t as Bound _) =
35.421 - if is_prop Ts t then aprop t else t
35.422 - | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
35.423 - | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
35.424 - if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
35.425 - else tr' Ts t1 $ tr' Ts t2
35.426 - | tr' Ts (t as t1 $ t2) =
35.427 - (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
35.428 - then I else aprop) (tr' Ts t1 $ tr' Ts t2);
35.429 - in tr' [] tm end;
35.430 -
35.431 -
35.432 -(* meta implication *)
35.433 -
35.434 -fun impl_ast_tr' asts =
35.435 - if no_brackets () then raise Match
35.436 - else
35.437 - (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
35.438 - (prems as _ :: _ :: _, concl) =>
35.439 - let
35.440 - val (asms, asm) = split_last prems;
35.441 - val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
35.442 - in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
35.443 - | _ => raise Match);
35.444 -
35.445 -
35.446 -(* dependent / nondependent quantifiers *)
35.447 -
35.448 -fun var_abs mark (x, T, b) =
35.449 - let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
35.450 - in (x', subst_bound (mark (x', T), b)) end;
35.451 -
35.452 -val variant_abs = var_abs Free;
35.453 -val variant_abs' = var_abs mark_boundT;
35.454 -
35.455 -fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
35.456 - if Term.is_dependent B then
35.457 - let val (x', B') = variant_abs' (x, dummyT, B);
35.458 - in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
35.459 - else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
35.460 - | dependent_tr' _ _ = raise Match;
35.461 -
35.462 -
35.463 -(* quote / antiquote *)
35.464 -
35.465 -fun antiquote_tr' name =
35.466 - let
35.467 - fun tr' i (t $ u) =
35.468 - if u aconv Bound i then Lexicon.const name $ tr' i t
35.469 - else tr' i t $ tr' i u
35.470 - | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
35.471 - | tr' i a = if a aconv Bound i then raise Match else a;
35.472 - in tr' 0 end;
35.473 -
35.474 -fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
35.475 - | quote_tr' _ _ = raise Match;
35.476 -
35.477 -fun quote_antiquote_tr' quoteN antiquoteN name =
35.478 - let
35.479 - fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
35.480 - | tr' _ = raise Match;
35.481 - in (name, tr') end;
35.482 -
35.483 -
35.484 -(* corresponding updates *)
35.485 -
35.486 -local
35.487 -
35.488 -fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
35.489 - | upd_type _ = dummyT;
35.490 -
35.491 -fun upd_tr' (x_upd, T) =
35.492 - (case try (unsuffix "_update") x_upd of
35.493 - SOME x => (x, upd_type T)
35.494 - | NONE => raise Match);
35.495 -
35.496 -in
35.497 -
35.498 -fun update_name_tr' (Free x) = Free (upd_tr' x)
35.499 - | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
35.500 - | update_name_tr' (Const x) = Const (upd_tr' x)
35.501 - | update_name_tr' _ = raise Match;
35.502 -
35.503 -end;
35.504 -
35.505 -
35.506 -(* indexed syntax *)
35.507 -
35.508 -fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
35.509 - | index_ast_tr' _ = raise Match;
35.510 -
35.511 -
35.512 -(* implicit structures *)
35.513 -
35.514 -fun the_struct' structs s =
35.515 - [(case Lexicon.read_nat s of
35.516 - SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
35.517 - | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
35.518 -
35.519 -fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
35.520 - | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
35.521 - the_struct' structs s
35.522 - | struct_ast_tr' _ _ = raise Match;
35.523 -
35.524 -
35.525 -
35.526 -(** Pure translations **)
35.527 -
35.528 -val pure_trfuns =
35.529 - ([("_strip_positions", strip_positions_ast_tr),
35.530 - ("_constify", constify_ast_tr),
35.531 - ("_tapp", tapp_ast_tr),
35.532 - ("_tappl", tappl_ast_tr),
35.533 - ("_bracket", bracket_ast_tr),
35.534 - ("_appl", appl_ast_tr),
35.535 - ("_applC", applC_ast_tr),
35.536 - ("_lambda", lambda_ast_tr),
35.537 - ("_idtyp", idtyp_ast_tr),
35.538 - ("_idtypdummy", idtypdummy_ast_tr),
35.539 - ("_bigimpl", bigimpl_ast_tr),
35.540 - ("_indexdefault", indexdefault_ast_tr),
35.541 - ("_indexnum", indexnum_ast_tr),
35.542 - ("_indexvar", indexvar_ast_tr),
35.543 - ("_struct", struct_ast_tr)],
35.544 - [("_abs", abs_tr),
35.545 - ("_aprop", aprop_tr),
35.546 - ("_ofclass", ofclass_tr),
35.547 - ("_sort_constraint", sort_constraint_tr),
35.548 - ("_TYPE", type_tr),
35.549 - ("_DDDOT", dddot_tr),
35.550 - ("_update_name", update_name_tr),
35.551 - ("_index", index_tr)],
35.552 - ([]: (string * (term list -> term)) list),
35.553 - [("\\<^type>fun", fun_ast_tr'),
35.554 - ("_abs", abs_ast_tr'),
35.555 - ("_idts", idtyp_ast_tr' "_idts"),
35.556 - ("_pttrns", idtyp_ast_tr' "_pttrns"),
35.557 - ("\\<^const>==>", impl_ast_tr'),
35.558 - ("_index", index_ast_tr')]);
35.559 -
35.560 -fun struct_trfuns structs =
35.561 - ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
35.562 -
35.563 -end;
36.1 --- a/src/Pure/Syntax/syntax.ML Fri Apr 08 11:39:45 2011 +0200
36.2 +++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 13:31:16 2011 +0200
36.3 @@ -7,7 +7,6 @@
36.4
36.5 signature BASIC_SYNTAX =
36.6 sig
36.7 - include SYN_TRANS0
36.8 include MIXFIX0
36.9 include PRINTER0
36.10 end;
36.11 @@ -16,7 +15,6 @@
36.12 sig
36.13 include LEXICON0
36.14 include SYN_EXT0
36.15 - include SYN_TRANS1
36.16 include MIXFIX1
36.17 include PRINTER0
36.18 val positions_raw: Config.raw
36.19 @@ -727,7 +725,7 @@
36.20
36.21 (*export parts of internal Syntax structures*)
36.22 val syntax_tokenize = tokenize;
36.23 -open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
36.24 +open Lexicon Syn_Ext Mixfix Printer;
36.25 val tokenize = syntax_tokenize;
36.26
36.27 end;
37.1 --- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 11:39:45 2011 +0200
37.2 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 13:31:16 2011 +0200
37.3 @@ -532,7 +532,7 @@
37.4
37.5 fun ast_of tm =
37.6 (case strip_comb tm of
37.7 - (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
37.8 + (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
37.9 | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
37.10 Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
37.11 | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
37.12 @@ -557,7 +557,7 @@
37.13 else simple_ast_of ctxt t;
37.14 in
37.15 tm
37.16 - |> Syn_Trans.prop_tr'
37.17 + |> Syntax_Trans.prop_tr'
37.18 |> show_types ? (#1 o prune_typs o rpair [])
37.19 |> mark_atoms
37.20 |> ast_of
38.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
38.2 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Apr 08 13:31:16 2011 +0200
38.3 @@ -0,0 +1,556 @@
38.4 +(* Title: Pure/Syntax/syntax_trans.ML
38.5 + Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
38.6 +
38.7 +Syntax translation functions.
38.8 +*)
38.9 +
38.10 +signature BASIC_SYNTAX_TRANS =
38.11 +sig
38.12 + val eta_contract: bool Config.T
38.13 +end
38.14 +
38.15 +signature SYNTAX_TRANS =
38.16 +sig
38.17 + include BASIC_SYNTAX_TRANS
38.18 + val no_brackets: unit -> bool
38.19 + val no_type_brackets: unit -> bool
38.20 + val abs_tr: term list -> term
38.21 + val mk_binder_tr: string * string -> string * (term list -> term)
38.22 + val antiquote_tr: string -> term -> term
38.23 + val quote_tr: string -> term -> term
38.24 + val quote_antiquote_tr: string -> string -> string -> string * (term list -> term)
38.25 + val non_typed_tr': (term list -> term) -> typ -> term list -> term
38.26 + val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term
38.27 + val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
38.28 + val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
38.29 + val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
38.30 + val eta_contract_default: bool Unsynchronized.ref
38.31 + val eta_contract_raw: Config.raw
38.32 + val mark_bound: string -> term
38.33 + val mark_boundT: string * typ -> term
38.34 + val bound_vars: (string * typ) list -> term -> term
38.35 + val abs_tr': Proof.context -> term -> term
38.36 + val atomic_abs_tr': string * typ * term -> term * term
38.37 + val const_abs_tr': term -> term
38.38 + val mk_binder_tr': string * string -> string * (term list -> term)
38.39 + val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
38.40 + val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
38.41 + val prop_tr': term -> term
38.42 + val variant_abs: string * typ * term -> string * term
38.43 + val variant_abs': string * typ * term -> string * term
38.44 + val dependent_tr': string * string -> term list -> term
38.45 + val antiquote_tr': string -> term -> term
38.46 + val quote_tr': string -> term -> term
38.47 + val quote_antiquote_tr': string -> string -> string -> string * (term list -> term)
38.48 + val update_name_tr': term -> term
38.49 + val pure_trfuns:
38.50 + (string * (Ast.ast list -> Ast.ast)) list *
38.51 + (string * (term list -> term)) list *
38.52 + (string * (term list -> term)) list *
38.53 + (string * (Ast.ast list -> Ast.ast)) list
38.54 + val struct_trfuns: string list ->
38.55 + (string * (Ast.ast list -> Ast.ast)) list *
38.56 + (string * (term list -> term)) list *
38.57 + (string * (typ -> term list -> term)) list *
38.58 + (string * (Ast.ast list -> Ast.ast)) list
38.59 +end;
38.60 +
38.61 +structure Syntax_Trans: SYNTAX_TRANS =
38.62 +struct
38.63 +
38.64 +(* print mode *)
38.65 +
38.66 +val bracketsN = "brackets";
38.67 +val no_bracketsN = "no_brackets";
38.68 +
38.69 +fun no_brackets () =
38.70 + find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
38.71 + (print_mode_value ()) = SOME no_bracketsN;
38.72 +
38.73 +val type_bracketsN = "type_brackets";
38.74 +val no_type_bracketsN = "no_type_brackets";
38.75 +
38.76 +fun no_type_brackets () =
38.77 + find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
38.78 + (print_mode_value ()) <> SOME type_bracketsN;
38.79 +
38.80 +
38.81 +
38.82 +(** parse (ast) translations **)
38.83 +
38.84 +(* strip_positions *)
38.85 +
38.86 +fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
38.87 + | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
38.88 +
38.89 +
38.90 +(* constify *)
38.91 +
38.92 +fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
38.93 + | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
38.94 +
38.95 +
38.96 +(* type syntax *)
38.97 +
38.98 +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
38.99 + | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
38.100 +
38.101 +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
38.102 + | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
38.103 +
38.104 +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
38.105 + | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
38.106 +
38.107 +
38.108 +(* application *)
38.109 +
38.110 +fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
38.111 + | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
38.112 +
38.113 +fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
38.114 + | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
38.115 +
38.116 +
38.117 +(* abstraction *)
38.118 +
38.119 +fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
38.120 + | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
38.121 +
38.122 +fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
38.123 + | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
38.124 +
38.125 +fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
38.126 + | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
38.127 +
38.128 +fun absfree_proper (x, T, t) =
38.129 + if can Name.dest_internal x
38.130 + then error ("Illegal internal variable in abstraction: " ^ quote x)
38.131 + else Term.absfree (x, T, t);
38.132 +
38.133 +fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
38.134 + | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
38.135 + | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
38.136 + Lexicon.const "_constrainAbs" $ abs_tr [x, t] $ tT
38.137 + | abs_tr ts = raise TERM ("abs_tr", ts);
38.138 +
38.139 +
38.140 +(* binder *)
38.141 +
38.142 +fun mk_binder_tr (syn, name) =
38.143 + let
38.144 + fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
38.145 + fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
38.146 + | binder_tr [x, t] =
38.147 + let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
38.148 + in Lexicon.const name $ abs end
38.149 + | binder_tr ts = err ts;
38.150 + in (syn, binder_tr) end;
38.151 +
38.152 +
38.153 +(* type propositions *)
38.154 +
38.155 +fun mk_type ty =
38.156 + Lexicon.const "_constrain" $
38.157 + Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
38.158 +
38.159 +fun ofclass_tr [ty, cls] = cls $ mk_type ty
38.160 + | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
38.161 +
38.162 +fun sort_constraint_tr [ty] = Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty
38.163 + | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
38.164 +
38.165 +
38.166 +(* meta propositions *)
38.167 +
38.168 +fun aprop_tr [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
38.169 + | aprop_tr ts = raise TERM ("aprop_tr", ts);
38.170 +
38.171 +
38.172 +(* meta implication *)
38.173 +
38.174 +fun bigimpl_ast_tr (asts as [asms, concl]) =
38.175 + let val prems =
38.176 + (case Ast.unfold_ast_p "_asms" asms of
38.177 + (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
38.178 + | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
38.179 + in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
38.180 + | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
38.181 +
38.182 +
38.183 +(* type/term reflection *)
38.184 +
38.185 +fun type_tr [ty] = mk_type ty
38.186 + | type_tr ts = raise TERM ("type_tr", ts);
38.187 +
38.188 +
38.189 +(* dddot *)
38.190 +
38.191 +fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
38.192 +
38.193 +
38.194 +(* quote / antiquote *)
38.195 +
38.196 +fun antiquote_tr name =
38.197 + let
38.198 + fun tr i ((t as Const (c, _)) $ u) =
38.199 + if c = name then tr i u $ Bound i
38.200 + else tr i t $ tr i u
38.201 + | tr i (t $ u) = tr i t $ tr i u
38.202 + | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
38.203 + | tr _ a = a;
38.204 + in tr 0 end;
38.205 +
38.206 +fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
38.207 +
38.208 +fun quote_antiquote_tr quoteN antiquoteN name =
38.209 + let
38.210 + fun tr [t] = Lexicon.const name $ quote_tr antiquoteN t
38.211 + | tr ts = raise TERM ("quote_tr", ts);
38.212 + in (quoteN, tr) end;
38.213 +
38.214 +
38.215 +(* corresponding updates *)
38.216 +
38.217 +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
38.218 + | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
38.219 + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
38.220 + if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
38.221 + else
38.222 + list_comb (c $ update_name_tr [t] $
38.223 + (Lexicon.fun_type $
38.224 + (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
38.225 + | update_name_tr ts = raise TERM ("update_name_tr", ts);
38.226 +
38.227 +
38.228 +(* indexed syntax *)
38.229 +
38.230 +fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
38.231 + | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
38.232 +
38.233 +fun index_ast_tr ast =
38.234 + Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
38.235 +
38.236 +fun indexdefault_ast_tr [] = index_ast_tr (Ast.Constant "_indexdefault")
38.237 + | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
38.238 +
38.239 +fun indexnum_ast_tr [ast] = index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
38.240 + | indexnum_ast_tr asts = raise Ast.AST ("indexnum_ast_tr", asts);
38.241 +
38.242 +fun indexvar_ast_tr [] = Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
38.243 + | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
38.244 +
38.245 +fun index_tr [t] = t
38.246 + | index_tr ts = raise TERM ("index_tr", ts);
38.247 +
38.248 +
38.249 +(* implicit structures *)
38.250 +
38.251 +fun the_struct structs i =
38.252 + if 1 <= i andalso i <= length structs then nth structs (i - 1)
38.253 + else error ("Illegal reference to implicit structure #" ^ string_of_int i);
38.254 +
38.255 +fun struct_tr structs [Const ("_indexdefault", _)] =
38.256 + Lexicon.free (the_struct structs 1)
38.257 + | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
38.258 + Lexicon.free (the_struct structs
38.259 + (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
38.260 + | struct_tr _ ts = raise TERM ("struct_tr", ts);
38.261 +
38.262 +
38.263 +
38.264 +(** print (ast) translations **)
38.265 +
38.266 +(* types *)
38.267 +
38.268 +fun non_typed_tr' f _ ts = f ts;
38.269 +fun non_typed_tr'' f x _ ts = f x ts;
38.270 +
38.271 +
38.272 +(* type syntax *)
38.273 +
38.274 +fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
38.275 + | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
38.276 + | tappl_ast_tr' (f, ty :: tys) =
38.277 + Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
38.278 +
38.279 +fun fun_ast_tr' asts =
38.280 + if no_brackets () orelse no_type_brackets () then raise Match
38.281 + else
38.282 + (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
38.283 + (dom as _ :: _ :: _, cod)
38.284 + => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
38.285 + | _ => raise Match);
38.286 +
38.287 +
38.288 +(* application *)
38.289 +
38.290 +fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
38.291 + | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
38.292 +
38.293 +fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
38.294 + | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
38.295 +
38.296 +
38.297 +(* partial eta-contraction before printing *)
38.298 +
38.299 +fun eta_abs (Abs (a, T, t)) =
38.300 + (case eta_abs t of
38.301 + t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
38.302 + | t' as f $ u =>
38.303 + (case eta_abs u of
38.304 + Bound 0 =>
38.305 + if Term.is_dependent f then Abs (a, T, t')
38.306 + else incr_boundvars ~1 f
38.307 + | _ => Abs (a, T, t'))
38.308 + | t' => Abs (a, T, t'))
38.309 + | eta_abs t = t;
38.310 +
38.311 +val eta_contract_default = Unsynchronized.ref true;
38.312 +val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
38.313 +val eta_contract = Config.bool eta_contract_raw;
38.314 +
38.315 +fun eta_contr ctxt tm =
38.316 + if Config.get ctxt eta_contract then eta_abs tm else tm;
38.317 +
38.318 +
38.319 +(* abstraction *)
38.320 +
38.321 +fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
38.322 +fun mark_bound x = mark_boundT (x, dummyT);
38.323 +
38.324 +fun bound_vars vars body =
38.325 + subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
38.326 +
38.327 +fun strip_abss vars_of body_of tm =
38.328 + let
38.329 + val vars = vars_of tm;
38.330 + val body = body_of tm;
38.331 + val rev_new_vars = Term.rename_wrt_term body vars;
38.332 + fun subst (x, T) b =
38.333 + if can Name.dest_internal x andalso not (Term.is_dependent b)
38.334 + then (Const ("_idtdummy", T), incr_boundvars ~1 b)
38.335 + else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
38.336 + val (rev_vars', body') = fold_map subst rev_new_vars body;
38.337 + in (rev rev_vars', body') end;
38.338 +
38.339 +
38.340 +fun abs_tr' ctxt tm =
38.341 + uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
38.342 + (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
38.343 +
38.344 +fun atomic_abs_tr' (x, T, t) =
38.345 + let val [xT] = Term.rename_wrt_term t [(x, T)]
38.346 + in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
38.347 +
38.348 +fun abs_ast_tr' asts =
38.349 + (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
38.350 + ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
38.351 + | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
38.352 +
38.353 +fun const_abs_tr' t =
38.354 + (case eta_abs t of
38.355 + Abs (_, _, t') =>
38.356 + if Term.is_dependent t' then raise Match
38.357 + else incr_boundvars ~1 t'
38.358 + | _ => raise Match);
38.359 +
38.360 +
38.361 +(* binders *)
38.362 +
38.363 +fun mk_binder_tr' (name, syn) =
38.364 + let
38.365 + fun mk_idts [] = raise Match (*abort translation*)
38.366 + | mk_idts [idt] = idt
38.367 + | mk_idts (idt :: idts) = Lexicon.const "_idts" $ idt $ mk_idts idts;
38.368 +
38.369 + fun tr' t =
38.370 + let
38.371 + val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
38.372 + in Lexicon.const syn $ mk_idts xs $ bd end;
38.373 +
38.374 + fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
38.375 + | binder_tr' [] = raise Match;
38.376 + in (name, binder_tr') end;
38.377 +
38.378 +fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
38.379 + let val (x, t) = atomic_abs_tr' abs
38.380 + in list_comb (Lexicon.const syn $ x $ t, ts) end);
38.381 +
38.382 +fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
38.383 + let val (x, t) = atomic_abs_tr' abs
38.384 + in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
38.385 +
38.386 +
38.387 +(* idtyp constraints *)
38.388 +
38.389 +fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
38.390 + Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
38.391 + | idtyp_ast_tr' _ _ = raise Match;
38.392 +
38.393 +
38.394 +(* meta propositions *)
38.395 +
38.396 +fun prop_tr' tm =
38.397 + let
38.398 + fun aprop t = Lexicon.const "_aprop" $ t;
38.399 +
38.400 + fun is_prop Ts t =
38.401 + fastype_of1 (Ts, t) = propT handle TERM _ => false;
38.402 +
38.403 + fun is_term (Const ("Pure.term", _) $ _) = true
38.404 + | is_term _ = false;
38.405 +
38.406 + fun tr' _ (t as Const _) = t
38.407 + | tr' Ts (t as Const ("_bound", _) $ u) =
38.408 + if is_prop Ts u then aprop t else t
38.409 + | tr' _ (t as Free (x, T)) =
38.410 + if T = propT then aprop (Lexicon.free x) else t
38.411 + | tr' _ (t as Var (xi, T)) =
38.412 + if T = propT then aprop (Lexicon.var xi) else t
38.413 + | tr' Ts (t as Bound _) =
38.414 + if is_prop Ts t then aprop t else t
38.415 + | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
38.416 + | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
38.417 + if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
38.418 + else tr' Ts t1 $ tr' Ts t2
38.419 + | tr' Ts (t as t1 $ t2) =
38.420 + (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
38.421 + then I else aprop) (tr' Ts t1 $ tr' Ts t2);
38.422 + in tr' [] tm end;
38.423 +
38.424 +
38.425 +(* meta implication *)
38.426 +
38.427 +fun impl_ast_tr' asts =
38.428 + if no_brackets () then raise Match
38.429 + else
38.430 + (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
38.431 + (prems as _ :: _ :: _, concl) =>
38.432 + let
38.433 + val (asms, asm) = split_last prems;
38.434 + val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
38.435 + in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
38.436 + | _ => raise Match);
38.437 +
38.438 +
38.439 +(* dependent / nondependent quantifiers *)
38.440 +
38.441 +fun var_abs mark (x, T, b) =
38.442 + let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
38.443 + in (x', subst_bound (mark (x', T), b)) end;
38.444 +
38.445 +val variant_abs = var_abs Free;
38.446 +val variant_abs' = var_abs mark_boundT;
38.447 +
38.448 +fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
38.449 + if Term.is_dependent B then
38.450 + let val (x', B') = variant_abs' (x, dummyT, B);
38.451 + in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
38.452 + else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
38.453 + | dependent_tr' _ _ = raise Match;
38.454 +
38.455 +
38.456 +(* quote / antiquote *)
38.457 +
38.458 +fun antiquote_tr' name =
38.459 + let
38.460 + fun tr' i (t $ u) =
38.461 + if u aconv Bound i then Lexicon.const name $ tr' i t
38.462 + else tr' i t $ tr' i u
38.463 + | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
38.464 + | tr' i a = if a aconv Bound i then raise Match else a;
38.465 + in tr' 0 end;
38.466 +
38.467 +fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
38.468 + | quote_tr' _ _ = raise Match;
38.469 +
38.470 +fun quote_antiquote_tr' quoteN antiquoteN name =
38.471 + let
38.472 + fun tr' (t :: ts) = Term.list_comb (Lexicon.const quoteN $ quote_tr' antiquoteN t, ts)
38.473 + | tr' _ = raise Match;
38.474 + in (name, tr') end;
38.475 +
38.476 +
38.477 +(* corresponding updates *)
38.478 +
38.479 +local
38.480 +
38.481 +fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
38.482 + | upd_type _ = dummyT;
38.483 +
38.484 +fun upd_tr' (x_upd, T) =
38.485 + (case try (unsuffix "_update") x_upd of
38.486 + SOME x => (x, upd_type T)
38.487 + | NONE => raise Match);
38.488 +
38.489 +in
38.490 +
38.491 +fun update_name_tr' (Free x) = Free (upd_tr' x)
38.492 + | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
38.493 + | update_name_tr' (Const x) = Const (upd_tr' x)
38.494 + | update_name_tr' _ = raise Match;
38.495 +
38.496 +end;
38.497 +
38.498 +
38.499 +(* indexed syntax *)
38.500 +
38.501 +fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
38.502 + | index_ast_tr' _ = raise Match;
38.503 +
38.504 +
38.505 +(* implicit structures *)
38.506 +
38.507 +fun the_struct' structs s =
38.508 + [(case Lexicon.read_nat s of
38.509 + SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
38.510 + | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
38.511 +
38.512 +fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] = the_struct' structs "1"
38.513 + | struct_ast_tr' structs [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
38.514 + the_struct' structs s
38.515 + | struct_ast_tr' _ _ = raise Match;
38.516 +
38.517 +
38.518 +
38.519 +(** Pure translations **)
38.520 +
38.521 +val pure_trfuns =
38.522 + ([("_strip_positions", strip_positions_ast_tr),
38.523 + ("_constify", constify_ast_tr),
38.524 + ("_tapp", tapp_ast_tr),
38.525 + ("_tappl", tappl_ast_tr),
38.526 + ("_bracket", bracket_ast_tr),
38.527 + ("_appl", appl_ast_tr),
38.528 + ("_applC", applC_ast_tr),
38.529 + ("_lambda", lambda_ast_tr),
38.530 + ("_idtyp", idtyp_ast_tr),
38.531 + ("_idtypdummy", idtypdummy_ast_tr),
38.532 + ("_bigimpl", bigimpl_ast_tr),
38.533 + ("_indexdefault", indexdefault_ast_tr),
38.534 + ("_indexnum", indexnum_ast_tr),
38.535 + ("_indexvar", indexvar_ast_tr),
38.536 + ("_struct", struct_ast_tr)],
38.537 + [("_abs", abs_tr),
38.538 + ("_aprop", aprop_tr),
38.539 + ("_ofclass", ofclass_tr),
38.540 + ("_sort_constraint", sort_constraint_tr),
38.541 + ("_TYPE", type_tr),
38.542 + ("_DDDOT", dddot_tr),
38.543 + ("_update_name", update_name_tr),
38.544 + ("_index", index_tr)],
38.545 + ([]: (string * (term list -> term)) list),
38.546 + [("\\<^type>fun", fun_ast_tr'),
38.547 + ("_abs", abs_ast_tr'),
38.548 + ("_idts", idtyp_ast_tr' "_idts"),
38.549 + ("_pttrns", idtyp_ast_tr' "_pttrns"),
38.550 + ("\\<^const>==>", impl_ast_tr'),
38.551 + ("_index", index_ast_tr')]);
38.552 +
38.553 +fun struct_trfuns structs =
38.554 + ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
38.555 +
38.556 +end;
38.557 +
38.558 +structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
38.559 +open Basic_Syntax_Trans;
39.1 --- a/src/Pure/Thy/thy_output.ML Fri Apr 08 11:39:45 2011 +0200
39.2 +++ b/src/Pure/Thy/thy_output.ML Fri Apr 08 13:31:16 2011 +0200
39.3 @@ -453,7 +453,7 @@
39.4 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
39.5 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
39.6 val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
39.7 -val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
39.8 +val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
39.9 val _ = add_option "display" (Config.put display o boolean);
39.10 val _ = add_option "break" (Config.put break o boolean);
39.11 val _ = add_option "quotes" (Config.put quotes o boolean);
40.1 --- a/src/Pure/primitive_defs.ML Fri Apr 08 11:39:45 2011 +0200
40.2 +++ b/src/Pure/primitive_defs.ML Fri Apr 08 13:31:16 2011 +0200
40.3 @@ -27,7 +27,7 @@
40.4 val eq_body = Term.strip_all_body eq;
40.5
40.6 val display_terms =
40.7 - commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars);
40.8 + commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
40.9 val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
40.10
40.11 val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
41.1 --- a/src/Pure/pure_thy.ML Fri Apr 08 11:39:45 2011 +0200
41.2 +++ b/src/Pure/pure_thy.ML Fri Apr 08 13:31:16 2011 +0200
41.3 @@ -128,7 +128,7 @@
41.4 ("_indexvar", typ "index", Delimfix "'\\<index>"),
41.5 ("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
41.6 ("_update_name", typ "idt", NoSyn),
41.7 - (Syntax.constrainAbsC, typ "'a", NoSyn),
41.8 + ("_constrainAbs", typ "'a", NoSyn),
41.9 ("_constrain_position", typ "id => id_position", Delimfix "_"),
41.10 ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
41.11 ("_type_constraint_", typ "'a", NoSyn),
41.12 @@ -169,7 +169,7 @@
41.13 #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
41.14 #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
41.15 #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
41.16 - #> Sign.add_trfuns Syntax.pure_trfuns
41.17 + #> Sign.add_trfuns Syntax_Trans.pure_trfuns
41.18 #> Sign.local_path
41.19 #> Sign.add_consts_i
41.20 [(Binding.name "term", typ "'a => prop", NoSyn),
42.1 --- a/src/Pure/raw_simplifier.ML Fri Apr 08 11:39:45 2011 +0200
42.2 +++ b/src/Pure/raw_simplifier.ML Fri Apr 08 13:31:16 2011 +0200
42.3 @@ -306,7 +306,7 @@
42.4 let
42.5 val names = Term.declare_term_names t Name.context;
42.6 val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
42.7 - fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
42.8 + fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
42.9 in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
42.10
42.11 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
43.1 --- a/src/Pure/sign.ML Fri Apr 08 11:39:45 2011 +0200
43.2 +++ b/src/Pure/sign.ML Fri Apr 08 13:31:16 2011 +0200
43.3 @@ -477,9 +477,9 @@
43.4
43.5 in
43.6
43.7 -val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax.non_typed_tr';
43.8 +val add_trfuns = gen_add_trfuns Syntax.update_trfuns Syntax_Trans.non_typed_tr';
43.9 val add_trfunsT = gen_add_trfunsT Syntax.update_trfuns;
43.10 -val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax.non_typed_tr'';
43.11 +val add_advanced_trfuns = gen_add_trfuns Syntax.update_advanced_trfuns Syntax_Trans.non_typed_tr'';
43.12 val add_advanced_trfunsT = gen_add_trfunsT Syntax.update_advanced_trfuns;
43.13
43.14 end;
44.1 --- a/src/Pure/type_infer.ML Fri Apr 08 11:39:45 2011 +0200
44.2 +++ b/src/Pure/type_infer.ML Fri Apr 08 13:31:16 2011 +0200
44.3 @@ -300,7 +300,7 @@
44.4 val (Ts', Ts'') = chop (length Ts) Ts_bTs';
44.5 fun prep t =
44.6 let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
44.7 - in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
44.8 + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
44.9 in (map prep ts', Ts') end;
44.10
44.11 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
45.1 --- a/src/Tools/Code/code_thingol.ML Fri Apr 08 11:39:45 2011 +0200
45.2 +++ b/src/Tools/Code/code_thingol.ML Fri Apr 08 13:31:16 2011 +0200
45.3 @@ -688,7 +688,7 @@
45.4 pair (IVar (SOME v))
45.5 | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
45.6 let
45.7 - val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
45.8 + val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
45.9 val v'' = if member (op =) (Term.add_free_names t' []) v'
45.10 then SOME v' else NONE
45.11 in
46.1 --- a/src/Tools/induct.ML Fri Apr 08 11:39:45 2011 +0200
46.2 +++ b/src/Tools/induct.ML Fri Apr 08 13:31:16 2011 +0200
46.3 @@ -580,7 +580,7 @@
46.4 in
46.5 if not (null params) then
46.6 (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
46.7 - commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
46.8 + commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
46.9 Seq.single rule)
46.10 else
46.11 let
47.1 --- a/src/Tools/misc_legacy.ML Fri Apr 08 11:39:45 2011 +0200
47.2 +++ b/src/Tools/misc_legacy.ML Fri Apr 08 13:31:16 2011 +0200
47.3 @@ -61,7 +61,7 @@
47.4 fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
47.5 strip_context_aux (params, H :: Hs, B)
47.6 | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
47.7 - let val (b, u) = Syntax.variant_abs (a, T, t)
47.8 + let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
47.9 in strip_context_aux ((b, T) :: params, Hs, u) end
47.10 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
47.11
48.1 --- a/src/Tools/subtyping.ML Fri Apr 08 11:39:45 2011 +0200
48.2 +++ b/src/Tools/subtyping.ML Fri Apr 08 13:31:16 2011 +0200
48.3 @@ -200,7 +200,7 @@
48.4 val (Ts', Ts'') = chop (length Ts) Ts_bTs';
48.5 fun prep t =
48.6 let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
48.7 - in Term.subst_bounds (map Syntax.mark_boundT xs, t) end;
48.8 + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
48.9 in (map prep ts', Ts') end;
48.10
48.11 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);