--- a/NEWS Fri Apr 08 11:39:45 2011 +0200
+++ b/NEWS Fri Apr 08 13:31:16 2011 +0200
@@ -93,9 +93,10 @@
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 treatment of various ML structures of inner
+syntax, such as structure Ast: no pervasive content, no inclusion in
+structure Syntax. INCOMPATIBILITY, refer to qualified names like
+Ast.Constant etc.
* Typed print translation: discontinued show_sorts argument, which is
already available via context of "advanced" translation.
--- a/src/CCL/Term.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/CCL/Term.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/CCL/Type.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/Cube/Cube.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/FOLP/simp.ML Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Big_Operators.thy Fri Apr 08 13:31:16 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/Complete_Lattice.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/HOL.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Fri Apr 08 13:31:16 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/ex/Pattern_Match.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 13:31:16 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 *)
--- a/src/HOL/Hilbert_Choice.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Fri Apr 08 13:31:16 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}, _) $
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Fri Apr 08 13:31:16 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/Isar_Examples/Hoare.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Apr 08 13:31:16 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/reflection.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Library/reflection.ML Fri Apr 08 13:31:16 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/Orderings.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Orderings.thy Fri Apr 08 13:31:16 2011 +0200
@@ -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 11:39:45 2011 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/HOL/Set.thy Fri Apr 08 13:31:16 2011 +0200
@@ -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/Tools/Datatype/datatype_case.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 13:31:16 2011 +0200
@@ -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
+ (fn Free p => Syntax_Trans.mark_boundT p
| Const (s, _) => Syntax.const (Syntax.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/Qelim/cooper.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Apr 08 13:31:16 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/record.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Tools/record.ML Fri Apr 08 13:31:16 2011 +0200
@@ -963,7 +963,7 @@
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)
--- a/src/HOL/ex/Antiquote.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/ex/Antiquote.thy Fri Apr 08 13:31:16 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/Pure/IsaMakefile Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/IsaMakefile Fri Apr 08 13:31:16 2011 +0200
@@ -185,9 +185,9 @@
Syntax/printer.ML \
Syntax/simple_syntax.ML \
Syntax/syn_ext.ML \
- Syntax/syn_trans.ML \
Syntax/syntax.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 11:39:45 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Apr 08 13:31:16 2011 +0200
@@ -407,7 +407,7 @@
register_config Syntax.show_structs_raw #>
register_config Syntax.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/obtain.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Apr 08 13:31:16 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/ProofGeneral/preferences.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Fri Apr 08 13:31:16 2011 +0200
@@ -133,7 +133,7 @@
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"];
--- a/src/Pure/ROOT.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/ROOT.ML Fri Apr 08 13:31:16 2011 +0200
@@ -124,7 +124,7 @@
use "Syntax/ast.ML";
use "Syntax/syn_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/local_syntax.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/local_syntax.ML Fri Apr 08 13:31:16 2011 +0200
@@ -58,7 +58,7 @@
| 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,
--- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML Fri Apr 08 13:31:16 2011 +0200
@@ -154,10 +154,10 @@
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 (Syn_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);
+ apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
in
Syn_Ext.syn_ext' true is_logtype
mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
--- a/src/Pure/Syntax/printer.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Apr 08 13:31:16 2011 +0200
@@ -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) =
--- a/src/Pure/Syntax/syn_trans.ML Fri Apr 08 11:39:45 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,560 +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 [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);
-
-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 [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 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 [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;
--- a/src/Pure/Syntax/syntax.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 13:31:16 2011 +0200
@@ -7,7 +7,6 @@
signature BASIC_SYNTAX =
sig
- include SYN_TRANS0
include MIXFIX0
include PRINTER0
end;
@@ -16,7 +15,6 @@
sig
include LEXICON0
include SYN_EXT0
- include SYN_TRANS1
include MIXFIX1
include PRINTER0
val positions_raw: Config.raw
@@ -727,7 +725,7 @@
(*export parts of internal Syntax structures*)
val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Mixfix Printer;
val tokenize = syntax_tokenize;
end;
--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 13:31:16 2011 +0200
@@ -532,7 +532,7 @@
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)
| ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
@@ -557,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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Apr 08 13:31:16 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 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 [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/thy_output.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Apr 08 13:31:16 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/primitive_defs.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/primitive_defs.ML Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 13:31:16 2011 +0200
@@ -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 11:39:45 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/Pure/sign.ML Fri Apr 08 13:31:16 2011 +0200
@@ -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/type_infer.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/type_infer.ML Fri Apr 08 13:31:16 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/Tools/Code/code_thingol.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Apr 08 13:31:16 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/induct.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/induct.ML Fri Apr 08 13:31:16 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/misc_legacy.ML Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Tools/misc_legacy.ML Fri Apr 08 13:31:16 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 11:39:45 2011 +0200
+++ b/src/Tools/subtyping.ML Fri Apr 08 13:31:16 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);