--- a/src/HOL/Groups.thy Tue May 28 23:01:28 2013 +0200
+++ b/src/HOL/Groups.thy Tue May 28 23:11:07 2013 +0200
@@ -124,12 +124,10 @@
typed_print_translation {*
let
fun tr' c = (c, fn ctxt => fn T => fn ts =>
- if not (null ts) orelse T = dummyT orelse
- not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
- then raise Match
- else
+ if null ts andalso Printer.type_emphasis ctxt T then
Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
- Syntax_Phases.term_of_typ ctxt T);
+ Syntax_Phases.term_of_typ ctxt T
+ else raise Match);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
*} -- {* show types that are presumably too general *}
--- a/src/HOL/Num.thy Tue May 28 23:01:28 2013 +0200
+++ b/src/HOL/Num.thy Tue May 28 23:11:07 2013 +0200
@@ -332,8 +332,10 @@
in
(case T of
Type (@{type_name fun}, [_, T']) =>
- if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
- else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
+ if Printer.type_emphasis ctxt T' then
+ Syntax.const @{syntax_const "_constrain"} $ t' $
+ Syntax_Phases.term_of_typ ctxt T'
+ else t'
| _ => if T = dummyT then t' else raise Match)
end;
in
--- a/src/HOL/ex/Numeral_Representation.thy Tue May 28 23:01:28 2013 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy Tue May 28 23:11:07 2013 +0200
@@ -306,11 +306,13 @@
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in
- case T of
+ (case T of
Type (@{type_name fun}, [_, T']) =>
- if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
- else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
- | T' => if T' = dummyT then t' else raise Match
+ if Printer.type_emphasis ctxt T' then
+ Syntax.const @{syntax_const "_constrain"} $ t' $
+ Syntax_Phases.term_of_typ ctxt T'
+ else t'
+ | T' => if T' = dummyT then t' else raise Match)
end;
in [(@{const_syntax of_num}, num_tr')] end
*}
--- a/src/Pure/ROOT Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/ROOT Tue May 28 23:11:07 2013 +0200
@@ -174,6 +174,7 @@
"Syntax/syntax_phases.ML"
"Syntax/syntax_trans.ML"
"Syntax/term_position.ML"
+ "Syntax/type_annotation.ML"
"System/command_line.ML"
"System/invoke_scala.ML"
"System/isabelle_process.ML"
--- a/src/Pure/ROOT.ML Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/ROOT.ML Tue May 28 23:11:07 2013 +0200
@@ -121,6 +121,7 @@
(* inner syntax *)
+use "Syntax/type_annotation.ML";
use "Syntax/term_position.ML";
use "Syntax/lexicon.ML";
use "Syntax/ast.ML";
--- a/src/Pure/Syntax/printer.ML Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/Syntax/printer.ML Tue May 28 23:11:07 2013 +0200
@@ -9,7 +9,6 @@
val show_brackets: bool Config.T
val show_types: bool Config.T
val show_sorts: bool Config.T
- val show_free_types: bool Config.T
val show_markup: bool Config.T
val show_structs: bool Config.T
val show_question_marks: bool Config.T
@@ -26,8 +25,8 @@
val show_markup_raw: Config.raw
val show_structs_raw: Config.raw
val show_question_marks_raw: Config.raw
- val show_type_constraint: Proof.context -> bool
- val show_sort_constraint: Proof.context -> bool
+ val show_type_emphasis: bool Config.T
+ val type_emphasis: Proof.context -> typ -> bool
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -58,8 +57,6 @@
val show_sorts_raw = Config.declare_option "show_sorts";
val show_sorts = Config.bool show_sorts_raw;
-val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
-
val show_markup_default = Unsynchronized.ref false;
val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
val show_markup = Config.bool show_markup_raw;
@@ -70,8 +67,13 @@
val show_question_marks_raw = Config.declare_option "show_question_marks";
val show_question_marks = Config.bool show_question_marks_raw;
-fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
-fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
+val show_type_emphasis =
+ Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
+
+fun type_emphasis ctxt T =
+ T <> dummyT andalso
+ (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
+ Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
--- a/src/Pure/Syntax/syntax_phases.ML Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Tue May 28 23:11:07 2013 +0200
@@ -470,10 +470,10 @@
fun term_of_typ ctxt ty =
let
- val show_sort_constraint = Printer.show_sort_constraint ctxt;
+ val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
fun ofsort t raw_S =
- if show_sort_constraint then
+ if show_sorts then
let val S = #2 (Term_Position.decode_positionS raw_S)
in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
else t;
@@ -533,7 +533,7 @@
fun aprop t = Syntax.const "_aprop" $ t;
fun is_prop Ts t =
- fastype_of1 (Ts, t) = propT handle TERM _ => false;
+ Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
fun is_term (Const ("Pure.term", _) $ _) = true
| is_term _ = false;
@@ -554,21 +554,18 @@
fun prune_types ctxt tm =
let
- val show_free_types = Config.get ctxt show_free_types;
+ fun regard t t' seen =
+ if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
+ else if member (op aconv) seen t then (t', seen)
+ else (t, t :: seen);
- fun prune (t_seen as (Const _, _)) = t_seen
- | prune (t as Free (x, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
- else (t, t :: seen)
- | prune (t as Var (xi, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
- else (t, t :: seen)
- | prune (t_seen as (Bound _, _)) = t_seen
- | prune (Abs (x, ty, t), seen) =
+ fun prune (t as Const _, seen) = (t, seen)
+ | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
+ | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
+ | prune (t as Bound _, seen) = (t, seen)
+ | prune (Abs (x, T, t), seen) =
let val (t', seen') = prune (t, seen);
- in (Abs (x, ty, t'), seen') end
+ in (Abs (x, T, t'), seen') end
| prune (t1 $ t2, seen) =
let
val (t1', seen') = prune (t1, seen);
@@ -624,17 +621,19 @@
in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
- | (const as Const (c, T), ts) => trans c T ts
+ | (const as Const (c, T), ts) => trans c (Type_Annotation.clean T) ts
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args = ast_of (trf a ctxt T args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
- and constrain t T =
- if (show_types orelse show_markup) andalso T <> dummyT then
- Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
- ast_of_termT ctxt trf (term_of_typ ctxt T)]
- else simple_ast_of ctxt t;
+ and constrain t T0 =
+ let val T = Type_Annotation.smash T0 in
+ if (show_types orelse show_markup) andalso T <> dummyT then
+ Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
+ ast_of_termT ctxt trf (term_of_typ ctxt T)]
+ else simple_ast_of ctxt t
+ end;
in
tm
|> mark_aprop
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/type_annotation.ML Tue May 28 23:11:07 2013 +0200
@@ -0,0 +1,65 @@
+(* Title: Pure/Syntax/type_annotation.ML
+ Author: Makarius
+
+Type annotations within syntax trees, notably for pretty printing.
+*)
+
+signature TYPE_ANNOTATION =
+sig
+ val ignore_type: typ -> typ
+ val ignore_free_types: term -> term
+ val is_ignored: typ -> bool
+ val is_omitted: typ -> bool
+ val clean: typ -> typ
+ val smash: typ -> typ
+ val fastype_of: typ list -> term -> typ
+end;
+
+structure Type_Annotation: TYPE_ANNOTATION =
+struct
+
+(* annotations *)
+
+fun ignore_type T = Type ("_ignore_type", [T]);
+
+val ignore_free_types = Term.map_aterms (fn Free (x, T) => Free (x, ignore_type T) | a => a);
+
+fun is_ignored (Type ("_ignore_type", _)) = true
+ | is_ignored _ = false;
+
+fun is_omitted T = is_ignored T orelse T = dummyT;
+
+fun clean (Type ("_ignore_type", [T])) = clean T
+ | clean (Type (a, Ts)) = Type (a, map clean Ts)
+ | clean T = T;
+
+fun smash (Type ("_ignore_type", [_])) = dummyT
+ | smash (Type (a, Ts)) = Type (a, map smash Ts)
+ | smash T = T;
+
+
+(* determine type -- propagate annotations *)
+
+local
+
+fun dest_fun ignored (Type ("fun", [_, T])) = SOME ((ignored ? ignore_type) T)
+ | dest_fun _ (Type ("_ignore_type", [T])) = dest_fun true T
+ | dest_fun _ _ = NONE;
+
+in
+
+fun fastype_of Ts (t $ u) =
+ (case dest_fun false (fastype_of Ts t) of
+ SOME T => T
+ | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
+ | fastype_of _ (Const (_, T)) = T
+ | fastype_of _ (Free (_, T)) = T
+ | fastype_of _ (Var (_, T)) = T
+ | fastype_of Ts (Bound i) =
+ (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
+ | fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
+
+end;
+
+end;
+
--- a/src/Pure/goal_display.ML Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/goal_display.ML Tue May 28 23:11:07 2013 +0200
@@ -70,7 +70,6 @@
fun pretty_goals ctxt0 state =
let
val ctxt = ctxt0
- |> Config.put show_free_types false
|> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
|> Config.put show_sorts false;
@@ -82,7 +81,7 @@
val prt_sort = Syntax.pretty_sort ctxt;
val prt_typ = Syntax.pretty_typ ctxt;
- val prt_term = Syntax.pretty_term ctxt;
+ val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
fun prt_atoms prt prtT (X, xs) = Pretty.block
[Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
--- a/src/Pure/pure_thy.ML Tue May 28 23:01:28 2013 +0200
+++ b/src/Pure/pure_thy.ML Tue May 28 23:11:07 2013 +0200
@@ -81,6 +81,7 @@
("", typ "prop' => prop'", Delimfix "'(_')"),
("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
+ ("_ignore_type", typ "'a", NoSyn),
("", typ "tid_position => type", Delimfix "_"),
("", typ "tvar_position => type", Delimfix "_"),
("", typ "type_name => type", Delimfix "_"),