more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
authorwenzelm
Sat Sep 29 18:23:46 2012 +0200 (2012-09-29)
changeset 49660de49d9b4d7bc
parent 49659 251342b60a82
child 49661 ac48def96b69
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
src/CCL/Term.thy
src/HOL/Big_Operators.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/Pure/Isar/obtain.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/raw_simplifier.ML
src/Pure/type_infer_context.ML
src/Tools/induct.ML
src/Tools/subtyping.ML
     1.1 --- a/src/CCL/Term.thy	Sat Sep 29 16:51:04 2012 +0200
     1.2 +++ b/src/CCL/Term.thy	Sat Sep 29 18:23:46 2012 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  (** Quantifier translations: variable binding **)
     1.5  
     1.6  (* FIXME does not handle "_idtdummy" *)
     1.7 -(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
     1.8 +(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *)
     1.9  
    1.10  fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
    1.11  fun let_tr' [a,Abs(id,T,b)] =
     2.1 --- a/src/HOL/Big_Operators.thy	Sat Sep 29 16:51:04 2012 +0200
     2.2 +++ b/src/HOL/Big_Operators.thy	Sat Sep 29 18:23:46 2012 +0200
     2.3 @@ -201,10 +201,12 @@
     2.4          if x <> y then raise Match
     2.5          else
     2.6            let
     2.7 -            val x' = Syntax_Trans.mark_bound x;
     2.8 +            val x' = Syntax_Trans.mark_bound_body (x, Tx);
     2.9              val t' = subst_bound (x', t);
    2.10              val P' = subst_bound (x', P);
    2.11 -          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
    2.12 +          in
    2.13 +            Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
    2.14 +          end
    2.15      | setsum_tr' _ = raise Match;
    2.16  in [(@{const_syntax setsum}, setsum_tr')] end
    2.17  *}
     3.1 --- a/src/HOL/Orderings.thy	Sat Sep 29 16:51:04 2012 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Sat Sep 29 18:23:46 2012 +0200
     3.3 @@ -644,16 +644,16 @@
     3.4        Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     3.5      | _ => false);
     3.6    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
     3.7 -  fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
     3.8 +  fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
     3.9  
    3.10    fun tr' q = (q,
    3.11 -    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
    3.12 +    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
    3.13          Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    3.14          (case AList.lookup (op =) trans (q, c, d) of
    3.15            NONE => raise Match
    3.16          | SOME (l, g) =>
    3.17 -            if matches_bound v t andalso not (contains_var v u) then mk v l u P
    3.18 -            else if matches_bound v u andalso not (contains_var v t) then mk v g t P
    3.19 +            if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
    3.20 +            else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
    3.21              else raise Match)
    3.22       | _ => raise Match);
    3.23  in [tr' All_binder, tr' Ex_binder] end
     4.1 --- a/src/HOL/Set.thy	Sat Sep 29 16:51:04 2012 +0200
     4.2 +++ b/src/HOL/Set.thy	Sat Sep 29 18:23:46 2012 +0200
     4.3 @@ -270,17 +270,17 @@
     4.4      ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
     4.5      ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
     4.6  
     4.7 -  fun mk v v' c n P =
     4.8 +  fun mk v (v', T) c n P =
     4.9      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
    4.10 -    then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
    4.11 +    then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P else raise Match;
    4.12  
    4.13    fun tr' q = (q,
    4.14          fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
    4.15              Const (c, _) $
    4.16 -              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
    4.17 +              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
    4.18              (case AList.lookup (op =) trans (q, c, d) of
    4.19                NONE => raise Match
    4.20 -            | SOME l => mk v v' l n P)
    4.21 +            | SOME l => mk v (v', T) l n P)
    4.22           | _ => raise Match);
    4.23  in
    4.24    [tr' All_binder, tr' Ex_binder]
     5.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Sep 29 16:51:04 2012 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Sep 29 18:23:46 2012 +0200
     5.3 @@ -451,12 +451,12 @@
     5.4          let val xs = Term.add_frees pat [] in
     5.5            Syntax.const @{syntax_const "_case1"} $
     5.6              map_aterms
     5.7 -              (fn Free p => Syntax_Trans.mark_boundT p
     5.8 +              (fn Free p => Syntax_Trans.mark_bound_abs p
     5.9                  | Const (s, _) => Syntax.const (Lexicon.mark_const s)
    5.10                  | t => t) pat $
    5.11              map_aterms
    5.12 -              (fn x as Free (s, T) =>
    5.13 -                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
    5.14 +              (fn x as Free v =>
    5.15 +                  if member (op =) xs v then Syntax_Trans.mark_bound_body v else x
    5.16                  | t => t) rhs
    5.17          end;
    5.18      in
     6.1 --- a/src/Pure/Isar/obtain.ML	Sat Sep 29 16:51:04 2012 +0200
     6.2 +++ b/src/Pure/Isar/obtain.ML	Sat Sep 29 18:23:46 2012 +0200
     6.3 @@ -232,7 +232,7 @@
     6.4        handle Type.TUNIFY =>
     6.5          err ("Failed to unify variable " ^
     6.6            string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
     6.7 -          string_of_term (Syntax_Trans.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
     6.8 +          string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule;
     6.9      val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
    6.10        (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
    6.11      val norm_type = Envir.norm_type tyenv;
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:51:04 2012 +0200
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 18:23:46 2012 +0200
     7.3 @@ -550,8 +550,12 @@
     7.4            Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
     7.5        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
     7.6            Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
     7.7 -      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
     7.8 -          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
     7.9 +      | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
    7.10 +          let
    7.11 +            val X =
    7.12 +              if show_markup andalso not show_types orelse B <> dummyT then T
    7.13 +              else dummyT;
    7.14 +          in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
    7.15        | (Const ("_idtdummy", T), ts) =>
    7.16            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    7.17        | (const as Const (c, T), ts) =>
     8.1 --- a/src/Pure/Syntax/syntax_trans.ML	Sat Sep 29 16:51:04 2012 +0200
     8.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Sat Sep 29 18:23:46 2012 +0200
     8.3 @@ -30,8 +30,8 @@
     8.4    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     8.5    val eta_contract_default: bool Unsynchronized.ref
     8.6    val eta_contract_raw: Config.raw
     8.7 -  val mark_bound: string -> term
     8.8 -  val mark_boundT: string * typ -> term
     8.9 +  val mark_bound_abs: string * typ -> term
    8.10 +  val mark_bound_body: string * typ -> term
    8.11    val bound_vars: (string * typ) list -> term -> term
    8.12    val abs_tr': Proof.context -> term -> term
    8.13    val atomic_abs_tr': string * typ * term -> term * term
    8.14 @@ -312,11 +312,11 @@
    8.15  
    8.16  (* abstraction *)
    8.17  
    8.18 -fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
    8.19 -fun mark_bound x = mark_boundT (x, dummyT);
    8.20 +fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
    8.21 +fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
    8.22  
    8.23  fun bound_vars vars body =
    8.24 -  subst_bounds (map mark_boundT (Term.rename_wrt_term body vars), body);
    8.25 +  subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
    8.26  
    8.27  fun strip_abss vars_of body_of tm =
    8.28    let
    8.29 @@ -326,7 +326,7 @@
    8.30      fun subst (x, T) b =
    8.31        if can Name.dest_internal x andalso not (Term.is_dependent b)
    8.32        then (Const ("_idtdummy", T), incr_boundvars ~1 b)
    8.33 -      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
    8.34 +      else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
    8.35      val (rev_vars', body') = fold_map subst rev_new_vars body;
    8.36    in (rev rev_vars', body') end;
    8.37  
    8.38 @@ -337,7 +337,7 @@
    8.39  
    8.40  fun atomic_abs_tr' (x, T, t) =
    8.41    let val [xT] = Term.rename_wrt_term t [(x, T)]
    8.42 -  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
    8.43 +  in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
    8.44  
    8.45  fun abs_ast_tr' asts =
    8.46    (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
    8.47 @@ -437,12 +437,12 @@
    8.48    in (x', subst_bound (mark (x', T), b)) end;
    8.49  
    8.50  val variant_abs = var_abs Free;
    8.51 -val variant_abs' = var_abs mark_boundT;
    8.52 +val variant_abs' = var_abs mark_bound_abs;
    8.53  
    8.54  fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
    8.55        if Term.is_dependent B then
    8.56          let val (x', B') = variant_abs' (x, dummyT, B);
    8.57 -        in Term.list_comb (Syntax.const q $ mark_boundT (x', T) $ A $ B', ts) end
    8.58 +        in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
    8.59        else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
    8.60    | dependent_tr' _ _ = raise Match;
    8.61  
     9.1 --- a/src/Pure/raw_simplifier.ML	Sat Sep 29 16:51:04 2012 +0200
     9.2 +++ b/src/Pure/raw_simplifier.ML	Sat Sep 29 18:23:46 2012 +0200
     9.3 @@ -302,7 +302,7 @@
     9.4    let
     9.5      val names = Term.declare_term_names t Name.context;
     9.6      val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
     9.7 -    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
     9.8 +    fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
     9.9    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
    9.10  
    9.11  fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
    10.1 --- a/src/Pure/type_infer_context.ML	Sat Sep 29 16:51:04 2012 +0200
    10.2 +++ b/src/Pure/type_infer_context.ML	Sat Sep 29 18:23:46 2012 +0200
    10.3 @@ -246,7 +246,7 @@
    10.4          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    10.5          fun prep t =
    10.6            let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
    10.7 -          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
    10.8 +          in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
    10.9        in (map prep ts', Ts') end;
   10.10  
   10.11      fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
    11.1 --- a/src/Tools/induct.ML	Sat Sep 29 16:51:04 2012 +0200
    11.2 +++ b/src/Tools/induct.ML	Sat Sep 29 18:23:46 2012 +0200
    11.3 @@ -597,7 +597,7 @@
    11.4    in
    11.5      if not (null params) then
    11.6        (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
    11.7 -        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_boundT) params));
    11.8 +        commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params));
    11.9        Seq.single rule)
   11.10      else
   11.11        let
    12.1 --- a/src/Tools/subtyping.ML	Sat Sep 29 16:51:04 2012 +0200
    12.2 +++ b/src/Tools/subtyping.ML	Sat Sep 29 18:23:46 2012 +0200
    12.3 @@ -231,7 +231,7 @@
    12.4      val (Ts', Ts'') = chop (length Ts) Ts_bTs';
    12.5      fun prep t =
    12.6        let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
    12.7 -      in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
    12.8 +      in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
    12.9    in (map prep ts', Ts') end;
   12.10  
   12.11  fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);