merged
authorwenzelm
Tue May 28 23:11:07 2013 +0200 (2013-05-28)
changeset 52212afe61eefdc61
parent 52209 8b2c3e548a20
parent 52211 66bc827e37f8
child 52213 f4c5c6320cce
merged
     1.1 --- a/src/HOL/Groups.thy	Tue May 28 23:01:28 2013 +0200
     1.2 +++ b/src/HOL/Groups.thy	Tue May 28 23:11:07 2013 +0200
     1.3 @@ -124,12 +124,10 @@
     1.4  typed_print_translation {*
     1.5    let
     1.6      fun tr' c = (c, fn ctxt => fn T => fn ts =>
     1.7 -      if not (null ts) orelse T = dummyT orelse
     1.8 -        not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
     1.9 -      then raise Match
    1.10 -      else
    1.11 +      if null ts andalso Printer.type_emphasis ctxt T then
    1.12          Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
    1.13 -          Syntax_Phases.term_of_typ ctxt T);
    1.14 +          Syntax_Phases.term_of_typ ctxt T
    1.15 +      else raise Match);
    1.16    in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    1.17  *} -- {* show types that are presumably too general *}
    1.18  
     2.1 --- a/src/HOL/Num.thy	Tue May 28 23:01:28 2013 +0200
     2.2 +++ b/src/HOL/Num.thy	Tue May 28 23:11:07 2013 +0200
     2.3 @@ -332,8 +332,10 @@
     2.4        in
     2.5          (case T of
     2.6            Type (@{type_name fun}, [_, T']) =>
     2.7 -            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
     2.8 -            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
     2.9 +            if Printer.type_emphasis ctxt T' then
    2.10 +              Syntax.const @{syntax_const "_constrain"} $ t' $
    2.11 +                Syntax_Phases.term_of_typ ctxt T'
    2.12 +            else t'
    2.13          | _ => if T = dummyT then t' else raise Match)
    2.14        end;
    2.15    in
     3.1 --- a/src/HOL/ex/Numeral_Representation.thy	Tue May 28 23:01:28 2013 +0200
     3.2 +++ b/src/HOL/ex/Numeral_Representation.thy	Tue May 28 23:11:07 2013 +0200
     3.3 @@ -306,11 +306,13 @@
     3.4          val k = int_of_num' n;
     3.5          val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
     3.6        in
     3.7 -        case T of
     3.8 +        (case T of
     3.9            Type (@{type_name fun}, [_, T']) =>
    3.10 -            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    3.11 -            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    3.12 -        | T' => if T' = dummyT then t' else raise Match
    3.13 +            if Printer.type_emphasis ctxt T' then
    3.14 +              Syntax.const @{syntax_const "_constrain"} $ t' $
    3.15 +                Syntax_Phases.term_of_typ ctxt T'
    3.16 +            else t'
    3.17 +        | T' => if T' = dummyT then t' else raise Match)
    3.18        end;
    3.19    in [(@{const_syntax of_num}, num_tr')] end
    3.20  *}
     4.1 --- a/src/Pure/ROOT	Tue May 28 23:01:28 2013 +0200
     4.2 +++ b/src/Pure/ROOT	Tue May 28 23:11:07 2013 +0200
     4.3 @@ -174,6 +174,7 @@
     4.4      "Syntax/syntax_phases.ML"
     4.5      "Syntax/syntax_trans.ML"
     4.6      "Syntax/term_position.ML"
     4.7 +    "Syntax/type_annotation.ML"
     4.8      "System/command_line.ML"
     4.9      "System/invoke_scala.ML"
    4.10      "System/isabelle_process.ML"
     5.1 --- a/src/Pure/ROOT.ML	Tue May 28 23:01:28 2013 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Tue May 28 23:11:07 2013 +0200
     5.3 @@ -121,6 +121,7 @@
     5.4  
     5.5  (* inner syntax *)
     5.6  
     5.7 +use "Syntax/type_annotation.ML";
     5.8  use "Syntax/term_position.ML";
     5.9  use "Syntax/lexicon.ML";
    5.10  use "Syntax/ast.ML";
     6.1 --- a/src/Pure/Syntax/printer.ML	Tue May 28 23:01:28 2013 +0200
     6.2 +++ b/src/Pure/Syntax/printer.ML	Tue May 28 23:11:07 2013 +0200
     6.3 @@ -9,7 +9,6 @@
     6.4    val show_brackets: bool Config.T
     6.5    val show_types: bool Config.T
     6.6    val show_sorts: bool Config.T
     6.7 -  val show_free_types: bool Config.T
     6.8    val show_markup: bool Config.T
     6.9    val show_structs: bool Config.T
    6.10    val show_question_marks: bool Config.T
    6.11 @@ -26,8 +25,8 @@
    6.12    val show_markup_raw: Config.raw
    6.13    val show_structs_raw: Config.raw
    6.14    val show_question_marks_raw: Config.raw
    6.15 -  val show_type_constraint: Proof.context -> bool
    6.16 -  val show_sort_constraint: Proof.context -> bool
    6.17 +  val show_type_emphasis: bool Config.T
    6.18 +  val type_emphasis: Proof.context -> typ -> bool
    6.19    type prtabs
    6.20    val empty_prtabs: prtabs
    6.21    val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
    6.22 @@ -58,8 +57,6 @@
    6.23  val show_sorts_raw = Config.declare_option "show_sorts";
    6.24  val show_sorts = Config.bool show_sorts_raw;
    6.25  
    6.26 -val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    6.27 -
    6.28  val show_markup_default = Unsynchronized.ref false;
    6.29  val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
    6.30  val show_markup = Config.bool show_markup_raw;
    6.31 @@ -70,8 +67,13 @@
    6.32  val show_question_marks_raw = Config.declare_option "show_question_marks";
    6.33  val show_question_marks = Config.bool show_question_marks_raw;
    6.34  
    6.35 -fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
    6.36 -fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
    6.37 +val show_type_emphasis =
    6.38 +  Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
    6.39 +
    6.40 +fun type_emphasis ctxt T =
    6.41 +  T <> dummyT andalso
    6.42 +    (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
    6.43 +      Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
    6.44  
    6.45  
    6.46  
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue May 28 23:01:28 2013 +0200
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue May 28 23:11:07 2013 +0200
     7.3 @@ -470,10 +470,10 @@
     7.4  
     7.5  fun term_of_typ ctxt ty =
     7.6    let
     7.7 -    val show_sort_constraint = Printer.show_sort_constraint ctxt;
     7.8 +    val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
     7.9  
    7.10      fun ofsort t raw_S =
    7.11 -      if show_sort_constraint then
    7.12 +      if show_sorts then
    7.13          let val S = #2 (Term_Position.decode_positionS raw_S)
    7.14          in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
    7.15        else t;
    7.16 @@ -533,7 +533,7 @@
    7.17      fun aprop t = Syntax.const "_aprop" $ t;
    7.18  
    7.19      fun is_prop Ts t =
    7.20 -      fastype_of1 (Ts, t) = propT handle TERM _ => false;
    7.21 +      Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
    7.22  
    7.23      fun is_term (Const ("Pure.term", _) $ _) = true
    7.24        | is_term _ = false;
    7.25 @@ -554,21 +554,18 @@
    7.26  
    7.27  fun prune_types ctxt tm =
    7.28    let
    7.29 -    val show_free_types = Config.get ctxt show_free_types;
    7.30 +    fun regard t t' seen =
    7.31 +      if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
    7.32 +      else if member (op aconv) seen t then (t', seen)
    7.33 +      else (t, t :: seen);
    7.34  
    7.35 -    fun prune (t_seen as (Const _, _)) = t_seen
    7.36 -      | prune (t as Free (x, ty), seen) =
    7.37 -          if ty = dummyT then (t, seen)
    7.38 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
    7.39 -          else (t, t :: seen)
    7.40 -      | prune (t as Var (xi, ty), seen) =
    7.41 -          if ty = dummyT then (t, seen)
    7.42 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
    7.43 -          else (t, t :: seen)
    7.44 -      | prune (t_seen as (Bound _, _)) = t_seen
    7.45 -      | prune (Abs (x, ty, t), seen) =
    7.46 +    fun prune (t as Const _, seen) = (t, seen)
    7.47 +      | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
    7.48 +      | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
    7.49 +      | prune (t as Bound _, seen) = (t, seen)
    7.50 +      | prune (Abs (x, T, t), seen) =
    7.51            let val (t', seen') = prune (t, seen);
    7.52 -          in (Abs (x, ty, t'), seen') end
    7.53 +          in (Abs (x, T, t'), seen') end
    7.54        | prune (t1 $ t2, seen) =
    7.55            let
    7.56              val (t1', seen') = prune (t1, seen);
    7.57 @@ -624,17 +621,19 @@
    7.58            in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
    7.59        | (Const ("_idtdummy", T), ts) =>
    7.60            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    7.61 -      | (const as Const (c, T), ts) => trans c T ts
    7.62 +      | (const as Const (c, T), ts) => trans c (Type_Annotation.clean T) ts
    7.63        | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
    7.64  
    7.65      and trans a T args = ast_of (trf a ctxt T args)
    7.66        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    7.67  
    7.68 -    and constrain t T =
    7.69 -      if (show_types orelse show_markup) andalso T <> dummyT then
    7.70 -        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
    7.71 -          ast_of_termT ctxt trf (term_of_typ ctxt T)]
    7.72 -      else simple_ast_of ctxt t;
    7.73 +    and constrain t T0 =
    7.74 +      let val T = Type_Annotation.smash T0 in
    7.75 +        if (show_types orelse show_markup) andalso T <> dummyT then
    7.76 +          Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
    7.77 +            ast_of_termT ctxt trf (term_of_typ ctxt T)]
    7.78 +        else simple_ast_of ctxt t
    7.79 +      end;
    7.80    in
    7.81      tm
    7.82      |> mark_aprop
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/Syntax/type_annotation.ML	Tue May 28 23:11:07 2013 +0200
     8.3 @@ -0,0 +1,65 @@
     8.4 +(*  Title:      Pure/Syntax/type_annotation.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Type annotations within syntax trees, notably for pretty printing.
     8.8 +*)
     8.9 +
    8.10 +signature TYPE_ANNOTATION =
    8.11 +sig
    8.12 +  val ignore_type: typ -> typ
    8.13 +  val ignore_free_types: term -> term
    8.14 +  val is_ignored: typ -> bool
    8.15 +  val is_omitted: typ -> bool
    8.16 +  val clean: typ -> typ
    8.17 +  val smash: typ -> typ
    8.18 +  val fastype_of: typ list -> term -> typ
    8.19 +end;
    8.20 +
    8.21 +structure Type_Annotation: TYPE_ANNOTATION =
    8.22 +struct
    8.23 +
    8.24 +(* annotations *)
    8.25 +
    8.26 +fun ignore_type T = Type ("_ignore_type", [T]);
    8.27 +
    8.28 +val ignore_free_types = Term.map_aterms (fn Free (x, T) => Free (x, ignore_type T) | a => a);
    8.29 +
    8.30 +fun is_ignored (Type ("_ignore_type", _)) = true
    8.31 +  | is_ignored _ = false;
    8.32 +
    8.33 +fun is_omitted T = is_ignored T orelse T = dummyT;
    8.34 +
    8.35 +fun clean (Type ("_ignore_type", [T])) = clean T
    8.36 +  | clean (Type (a, Ts)) = Type (a, map clean Ts)
    8.37 +  | clean T = T;
    8.38 +
    8.39 +fun smash (Type ("_ignore_type", [_])) = dummyT
    8.40 +  | smash (Type (a, Ts)) = Type (a, map smash Ts)
    8.41 +  | smash T = T;
    8.42 +
    8.43 +
    8.44 +(* determine type -- propagate annotations *)
    8.45 +
    8.46 +local
    8.47 +
    8.48 +fun dest_fun ignored (Type ("fun", [_, T])) = SOME ((ignored ? ignore_type) T)
    8.49 +  | dest_fun _ (Type ("_ignore_type", [T])) = dest_fun true T
    8.50 +  | dest_fun _ _ = NONE;
    8.51 +
    8.52 +in
    8.53 +
    8.54 +fun fastype_of Ts (t $ u) =
    8.55 +      (case dest_fun false (fastype_of Ts t) of
    8.56 +        SOME T => T
    8.57 +      | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
    8.58 +  | fastype_of _ (Const (_, T)) = T
    8.59 +  | fastype_of _ (Free (_, T)) = T
    8.60 +  | fastype_of _ (Var (_, T)) = T
    8.61 +  | fastype_of Ts (Bound i) =
    8.62 +      (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
    8.63 +  | fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
    8.64 +
    8.65 +end;
    8.66 +
    8.67 +end;
    8.68 +
     9.1 --- a/src/Pure/goal_display.ML	Tue May 28 23:01:28 2013 +0200
     9.2 +++ b/src/Pure/goal_display.ML	Tue May 28 23:11:07 2013 +0200
     9.3 @@ -70,7 +70,6 @@
     9.4  fun pretty_goals ctxt0 state =
     9.5    let
     9.6      val ctxt = ctxt0
     9.7 -      |> Config.put show_free_types false
     9.8        |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
     9.9        |> Config.put show_sorts false;
    9.10  
    9.11 @@ -82,7 +81,7 @@
    9.12  
    9.13      val prt_sort = Syntax.pretty_sort ctxt;
    9.14      val prt_typ = Syntax.pretty_typ ctxt;
    9.15 -    val prt_term = Syntax.pretty_term ctxt;
    9.16 +    val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
    9.17  
    9.18      fun prt_atoms prt prtT (X, xs) = Pretty.block
    9.19        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    10.1 --- a/src/Pure/pure_thy.ML	Tue May 28 23:01:28 2013 +0200
    10.2 +++ b/src/Pure/pure_thy.ML	Tue May 28 23:11:07 2013 +0200
    10.3 @@ -81,6 +81,7 @@
    10.4      ("",            typ "prop' => prop'",              Delimfix "'(_')"),
    10.5      ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
    10.6      ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
    10.7 +    ("_ignore_type", typ "'a",                         NoSyn),
    10.8      ("",            typ "tid_position => type",        Delimfix "_"),
    10.9      ("",            typ "tvar_position => type",       Delimfix "_"),
   10.10      ("",            typ "type_name => type",           Delimfix "_"),