# HG changeset patch # User wenzelm # Date 1369775192 -7200 # Node ID 66bc827e37f88e1b6f79654780954ea3c9e6b0d1 # Parent 0226035df99d1b9bb846f99842504d439a522c55 explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types; diff -r 0226035df99d -r 66bc827e37f8 src/Pure/ROOT --- a/src/Pure/ROOT Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/ROOT Tue May 28 23:06:32 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" diff -r 0226035df99d -r 66bc827e37f8 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/ROOT.ML Tue May 28 23:06:32 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"; diff -r 0226035df99d -r 66bc827e37f8 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/Syntax/printer.ML Tue May 28 23:06:32 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 @@ -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; diff -r 0226035df99d -r 66bc827e37f8 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Tue May 28 23:06:32 2013 +0200 @@ -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 diff -r 0226035df99d -r 66bc827e37f8 src/Pure/Syntax/type_annotation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/type_annotation.ML Tue May 28 23:06:32 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; + diff -r 0226035df99d -r 66bc827e37f8 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/goal_display.ML Tue May 28 23:06:32 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 " ::", diff -r 0226035df99d -r 66bc827e37f8 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue May 28 16:29:11 2013 +0200 +++ b/src/Pure/pure_thy.ML Tue May 28 23:06:32 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 "_"),