tuned;
authorwenzelm
Mon May 27 18:39:21 2013 +0200 (2013-05-27)
changeset 52186413dbb3c7251
parent 52185 1b481b490454
child 52187 1f7b3aadec69
tuned;
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon May 27 18:24:38 2013 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 18:39:21 2013 +0200
     1.3 @@ -541,45 +541,43 @@
     1.4              (mark Ts t1 $ mark Ts t2);
     1.5    in mark [] tm end;
     1.6  
     1.7 -in
     1.8 -
     1.9 -fun term_to_ast idents is_syntax_const ctxt trf tm =
    1.10 +fun prune_types ctxt tm =
    1.11    let
    1.12 -    val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
    1.13 -    val show_structs = Config.get ctxt show_structs;
    1.14      val show_free_types = Config.get ctxt show_free_types;
    1.15 -    val show_markup = Config.get ctxt show_markup;
    1.16  
    1.17 -    val {structs, fixes} = idents;
    1.18 -
    1.19 -    fun prune_typs (t_seen as (Const _, _)) = t_seen
    1.20 -      | prune_typs (t as Free (x, ty), seen) =
    1.21 +    fun prune (t_seen as (Const _, _)) = t_seen
    1.22 +      | prune (t as Free (x, ty), seen) =
    1.23            if ty = dummyT then (t, seen)
    1.24            else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
    1.25            else (t, t :: seen)
    1.26 -      | prune_typs (t as Var (xi, ty), seen) =
    1.27 +      | prune (t as Var (xi, ty), seen) =
    1.28            if ty = dummyT then (t, seen)
    1.29            else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
    1.30            else (t, t :: seen)
    1.31 -      | prune_typs (t_seen as (Bound _, _)) = t_seen
    1.32 -      | prune_typs (Abs (x, ty, t), seen) =
    1.33 -          let val (t', seen') = prune_typs (t, seen);
    1.34 +      | prune (t_seen as (Bound _, _)) = t_seen
    1.35 +      | prune (Abs (x, ty, t), seen) =
    1.36 +          let val (t', seen') = prune (t, seen);
    1.37            in (Abs (x, ty, t'), seen') end
    1.38 -      | prune_typs (t1 $ t2, seen) =
    1.39 +      | prune (t1 $ t2, seen) =
    1.40            let
    1.41 -            val (t1', seen') = prune_typs (t1, seen);
    1.42 -            val (t2', seen'') = prune_typs (t2, seen');
    1.43 +            val (t1', seen') = prune (t1, seen);
    1.44 +            val (t2', seen'') = prune (t2, seen');
    1.45            in (t1' $ t2', seen'') end;
    1.46 +  in #1 (prune (tm, [])) end;
    1.47  
    1.48 -    fun mark_atoms ((t as Const (c, _)) $ u) =
    1.49 +fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
    1.50 +  let
    1.51 +    val show_structs = Config.get ctxt show_structs;
    1.52 +
    1.53 +    fun mark ((t as Const (c, _)) $ u) =
    1.54            if member (op =) Pure_Thy.token_markers c
    1.55 -          then t $ u else mark_atoms t $ mark_atoms u
    1.56 -      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
    1.57 -      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
    1.58 -      | mark_atoms (t as Const (c, T)) =
    1.59 +          then t $ u else mark t $ mark u
    1.60 +      | mark (t $ u) = mark t $ mark u
    1.61 +      | mark (Abs (x, T, t)) = Abs (x, T, mark t)
    1.62 +      | mark (t as Const (c, T)) =
    1.63            if is_syntax_const c then t
    1.64            else Const (Lexicon.mark_const c, T)
    1.65 -      | mark_atoms (t as Free (x, T)) =
    1.66 +      | mark (t as Free (x, T)) =
    1.67            let val i = find_index (fn s => s = x) structs + 1 in
    1.68              if i = 0 andalso member (op =) fixes x then
    1.69                Const (Lexicon.mark_fixed x, T)
    1.70 @@ -587,10 +585,18 @@
    1.71                Syntax.const "_struct" $ Syntax.const "_indexdefault"
    1.72              else Syntax.const "_free" $ t
    1.73            end
    1.74 -      | mark_atoms (t as Var (xi, T)) =
    1.75 +      | mark (t as Var (xi, T)) =
    1.76            if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
    1.77            else Syntax.const "_var" $ t
    1.78 -      | mark_atoms a = a;
    1.79 +      | mark a = a;
    1.80 +  in mark tm end;
    1.81 +
    1.82 +in
    1.83 +
    1.84 +fun term_to_ast idents is_syntax_const ctxt trf tm =
    1.85 +  let
    1.86 +    val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
    1.87 +    val show_markup = Config.get ctxt show_markup;
    1.88  
    1.89      fun ast_of tm =
    1.90        (case strip_comb tm of
    1.91 @@ -621,8 +627,8 @@
    1.92    in
    1.93      tm
    1.94      |> mark_aprop
    1.95 -    |> show_types ? (#1 o prune_typs o rpair [])
    1.96 -    |> mark_atoms
    1.97 +    |> show_types ? prune_types ctxt
    1.98 +    |> mark_atoms idents is_syntax_const ctxt
    1.99      |> ast_of
   1.100    end;
   1.101