explicit support for type annotations within printed syntax trees;
authorwenzelm
Tue May 28 23:06:32 2013 +0200 (2013-05-28)
changeset 5221166bc827e37f8
parent 52210 0226035df99d
child 52212 afe61eefdc61
explicit support for type annotations within printed syntax trees;
eliminated obsolete show_free_types;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/type_annotation.ML
src/Pure/goal_display.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/ROOT	Tue May 28 16:29:11 2013 +0200
     1.2 +++ b/src/Pure/ROOT	Tue May 28 23:06:32 2013 +0200
     1.3 @@ -174,6 +174,7 @@
     1.4      "Syntax/syntax_phases.ML"
     1.5      "Syntax/syntax_trans.ML"
     1.6      "Syntax/term_position.ML"
     1.7 +    "Syntax/type_annotation.ML"
     1.8      "System/command_line.ML"
     1.9      "System/invoke_scala.ML"
    1.10      "System/isabelle_process.ML"
     2.1 --- a/src/Pure/ROOT.ML	Tue May 28 16:29:11 2013 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Tue May 28 23:06:32 2013 +0200
     2.3 @@ -121,6 +121,7 @@
     2.4  
     2.5  (* inner syntax *)
     2.6  
     2.7 +use "Syntax/type_annotation.ML";
     2.8  use "Syntax/term_position.ML";
     2.9  use "Syntax/lexicon.ML";
    2.10  use "Syntax/ast.ML";
     3.1 --- a/src/Pure/Syntax/printer.ML	Tue May 28 16:29:11 2013 +0200
     3.2 +++ b/src/Pure/Syntax/printer.ML	Tue May 28 23:06:32 2013 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4    val show_brackets: bool Config.T
     3.5    val show_types: bool Config.T
     3.6    val show_sorts: bool Config.T
     3.7 -  val show_free_types: bool Config.T
     3.8    val show_markup: bool Config.T
     3.9    val show_structs: bool Config.T
    3.10    val show_question_marks: bool Config.T
    3.11 @@ -58,8 +57,6 @@
    3.12  val show_sorts_raw = Config.declare_option "show_sorts";
    3.13  val show_sorts = Config.bool show_sorts_raw;
    3.14  
    3.15 -val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    3.16 -
    3.17  val show_markup_default = Unsynchronized.ref false;
    3.18  val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
    3.19  val show_markup = Config.bool show_markup_raw;
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue May 28 16:29:11 2013 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue May 28 23:06:32 2013 +0200
     4.3 @@ -533,7 +533,7 @@
     4.4      fun aprop t = Syntax.const "_aprop" $ t;
     4.5  
     4.6      fun is_prop Ts t =
     4.7 -      fastype_of1 (Ts, t) = propT handle TERM _ => false;
     4.8 +      Type_Annotation.fastype_of Ts t = propT handle TERM _ => false;
     4.9  
    4.10      fun is_term (Const ("Pure.term", _) $ _) = true
    4.11        | is_term _ = false;
    4.12 @@ -554,21 +554,18 @@
    4.13  
    4.14  fun prune_types ctxt tm =
    4.15    let
    4.16 -    val show_free_types = Config.get ctxt show_free_types;
    4.17 +    fun regard t t' seen =
    4.18 +      if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
    4.19 +      else if member (op aconv) seen t then (t', seen)
    4.20 +      else (t, t :: seen);
    4.21  
    4.22 -    fun prune (t_seen as (Const _, _)) = t_seen
    4.23 -      | prune (t as Free (x, ty), seen) =
    4.24 -          if ty = dummyT then (t, seen)
    4.25 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
    4.26 -          else (t, t :: seen)
    4.27 -      | prune (t as Var (xi, ty), seen) =
    4.28 -          if ty = dummyT then (t, seen)
    4.29 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
    4.30 -          else (t, t :: seen)
    4.31 -      | prune (t_seen as (Bound _, _)) = t_seen
    4.32 -      | prune (Abs (x, ty, t), seen) =
    4.33 +    fun prune (t as Const _, seen) = (t, seen)
    4.34 +      | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
    4.35 +      | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
    4.36 +      | prune (t as Bound _, seen) = (t, seen)
    4.37 +      | prune (Abs (x, T, t), seen) =
    4.38            let val (t', seen') = prune (t, seen);
    4.39 -          in (Abs (x, ty, t'), seen') end
    4.40 +          in (Abs (x, T, t'), seen') end
    4.41        | prune (t1 $ t2, seen) =
    4.42            let
    4.43              val (t1', seen') = prune (t1, seen);
    4.44 @@ -624,17 +621,19 @@
    4.45            in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
    4.46        | (Const ("_idtdummy", T), ts) =>
    4.47            Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
    4.48 -      | (const as Const (c, T), ts) => trans c T ts
    4.49 +      | (const as Const (c, T), ts) => trans c (Type_Annotation.clean T) ts
    4.50        | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
    4.51  
    4.52      and trans a T args = ast_of (trf a ctxt T args)
    4.53        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    4.54  
    4.55 -    and constrain t T =
    4.56 -      if (show_types orelse show_markup) andalso T <> dummyT then
    4.57 -        Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
    4.58 -          ast_of_termT ctxt trf (term_of_typ ctxt T)]
    4.59 -      else simple_ast_of ctxt t;
    4.60 +    and constrain t T0 =
    4.61 +      let val T = Type_Annotation.smash T0 in
    4.62 +        if (show_types orelse show_markup) andalso T <> dummyT then
    4.63 +          Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
    4.64 +            ast_of_termT ctxt trf (term_of_typ ctxt T)]
    4.65 +        else simple_ast_of ctxt t
    4.66 +      end;
    4.67    in
    4.68      tm
    4.69      |> mark_aprop
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Syntax/type_annotation.ML	Tue May 28 23:06:32 2013 +0200
     5.3 @@ -0,0 +1,65 @@
     5.4 +(*  Title:      Pure/Syntax/type_annotation.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Type annotations within syntax trees, notably for pretty printing.
     5.8 +*)
     5.9 +
    5.10 +signature TYPE_ANNOTATION =
    5.11 +sig
    5.12 +  val ignore_type: typ -> typ
    5.13 +  val ignore_free_types: term -> term
    5.14 +  val is_ignored: typ -> bool
    5.15 +  val is_omitted: typ -> bool
    5.16 +  val clean: typ -> typ
    5.17 +  val smash: typ -> typ
    5.18 +  val fastype_of: typ list -> term -> typ
    5.19 +end;
    5.20 +
    5.21 +structure Type_Annotation: TYPE_ANNOTATION =
    5.22 +struct
    5.23 +
    5.24 +(* annotations *)
    5.25 +
    5.26 +fun ignore_type T = Type ("_ignore_type", [T]);
    5.27 +
    5.28 +val ignore_free_types = Term.map_aterms (fn Free (x, T) => Free (x, ignore_type T) | a => a);
    5.29 +
    5.30 +fun is_ignored (Type ("_ignore_type", _)) = true
    5.31 +  | is_ignored _ = false;
    5.32 +
    5.33 +fun is_omitted T = is_ignored T orelse T = dummyT;
    5.34 +
    5.35 +fun clean (Type ("_ignore_type", [T])) = clean T
    5.36 +  | clean (Type (a, Ts)) = Type (a, map clean Ts)
    5.37 +  | clean T = T;
    5.38 +
    5.39 +fun smash (Type ("_ignore_type", [_])) = dummyT
    5.40 +  | smash (Type (a, Ts)) = Type (a, map smash Ts)
    5.41 +  | smash T = T;
    5.42 +
    5.43 +
    5.44 +(* determine type -- propagate annotations *)
    5.45 +
    5.46 +local
    5.47 +
    5.48 +fun dest_fun ignored (Type ("fun", [_, T])) = SOME ((ignored ? ignore_type) T)
    5.49 +  | dest_fun _ (Type ("_ignore_type", [T])) = dest_fun true T
    5.50 +  | dest_fun _ _ = NONE;
    5.51 +
    5.52 +in
    5.53 +
    5.54 +fun fastype_of Ts (t $ u) =
    5.55 +      (case dest_fun false (fastype_of Ts t) of
    5.56 +        SOME T => T
    5.57 +      | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
    5.58 +  | fastype_of _ (Const (_, T)) = T
    5.59 +  | fastype_of _ (Free (_, T)) = T
    5.60 +  | fastype_of _ (Var (_, T)) = T
    5.61 +  | fastype_of Ts (Bound i) =
    5.62 +      (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
    5.63 +  | fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
    5.64 +
    5.65 +end;
    5.66 +
    5.67 +end;
    5.68 +
     6.1 --- a/src/Pure/goal_display.ML	Tue May 28 16:29:11 2013 +0200
     6.2 +++ b/src/Pure/goal_display.ML	Tue May 28 23:06:32 2013 +0200
     6.3 @@ -70,7 +70,6 @@
     6.4  fun pretty_goals ctxt0 state =
     6.5    let
     6.6      val ctxt = ctxt0
     6.7 -      |> Config.put show_free_types false
     6.8        |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
     6.9        |> Config.put show_sorts false;
    6.10  
    6.11 @@ -82,7 +81,7 @@
    6.12  
    6.13      val prt_sort = Syntax.pretty_sort ctxt;
    6.14      val prt_typ = Syntax.pretty_typ ctxt;
    6.15 -    val prt_term = Syntax.pretty_term ctxt;
    6.16 +    val prt_term = Syntax.pretty_term ctxt o Type_Annotation.ignore_free_types;
    6.17  
    6.18      fun prt_atoms prt prtT (X, xs) = Pretty.block
    6.19        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
     7.1 --- a/src/Pure/pure_thy.ML	Tue May 28 16:29:11 2013 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Tue May 28 23:06:32 2013 +0200
     7.3 @@ -81,6 +81,7 @@
     7.4      ("",            typ "prop' => prop'",              Delimfix "'(_')"),
     7.5      ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
     7.6      ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
     7.7 +    ("_ignore_type", typ "'a",                         NoSyn),
     7.8      ("",            typ "tid_position => type",        Delimfix "_"),
     7.9      ("",            typ "tvar_position => type",       Delimfix "_"),
    7.10      ("",            typ "type_name => type",           Delimfix "_"),