tuned extern_term, pretty_term';
authorwenzelm
Fri Feb 10 02:22:32 2006 +0100 (2006-02-10)
changeset 18994ce724d5bada2
parent 18993 f055b4fe381e
child 18995 ff4e4773cc7c
tuned extern_term, pretty_term';
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Feb 10 02:22:29 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 10 02:22:32 2006 +0100
     1.3 @@ -133,8 +133,9 @@
     1.4    val intern_typ: theory -> typ -> typ
     1.5    val extern_typ: theory -> typ -> typ
     1.6    val intern_term: theory -> term -> term
     1.7 +  val extern_term: (string -> xstring) -> theory -> term -> term
     1.8    val intern_tycons: theory -> typ -> typ
     1.9 -  val pretty_term': Syntax.syntax -> Consts.T -> Context.generic -> term -> Pretty.T
    1.10 +  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
    1.11    val pretty_term: theory -> term -> Pretty.T
    1.12    val pretty_typ: theory -> typ -> Pretty.T
    1.13    val pretty_sort: theory -> sort -> Pretty.T
    1.14 @@ -323,30 +324,40 @@
    1.15    | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.16    | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.17  
    1.18 +val add_classesT = Term.fold_atyps
    1.19 +  (fn TFree (_, S) => fold (insert (op =)) S
    1.20 +    | TVar (_, S) => fold (insert (op =)) S
    1.21 +    | _ => I);
    1.22 +
    1.23 +fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
    1.24 +  | add_tyconsT _ = I;
    1.25 +
    1.26 +val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
    1.27 +
    1.28  fun mapping add_names f t =
    1.29    let
    1.30      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
    1.31 -    val tab = List.mapPartial f' (add_names (t, []));
    1.32 +    val tab = List.mapPartial f' (add_names t []);
    1.33      fun get x = the_default x (AList.lookup (op =) tab x);
    1.34    in get end;
    1.35  
    1.36  fun typ_mapping f g thy T =
    1.37    T |> map_typ
    1.38 -    (mapping add_typ_classes (f thy) T)
    1.39 -    (mapping add_typ_tycons (g thy) T);
    1.40 +    (mapping add_classesT (f thy) T)
    1.41 +    (mapping add_tyconsT (g thy) T);
    1.42  
    1.43  fun term_mapping f g h thy t =
    1.44    t |> map_term
    1.45 -    (mapping add_term_classes (f thy) t)
    1.46 -    (mapping add_term_tycons (g thy) t)
    1.47 -    (mapping add_term_consts (h thy) t);
    1.48 +    (mapping (Term.fold_types add_classesT) (f thy) t)
    1.49 +    (mapping (Term.fold_types add_tyconsT) (g thy) t)
    1.50 +    (mapping add_consts (h thy) t);
    1.51  
    1.52  in
    1.53  
    1.54  val intern_typ = typ_mapping intern_class intern_type;
    1.55  val extern_typ = typ_mapping extern_class extern_type;
    1.56  val intern_term = term_mapping intern_class intern_type intern_const;
    1.57 -val extern_term = term_mapping extern_class extern_type;
    1.58 +fun extern_term h = term_mapping extern_class extern_type (K h);
    1.59  val intern_tycons = typ_mapping (K I) intern_type;
    1.60  
    1.61  end;
    1.62 @@ -355,14 +366,13 @@
    1.63  
    1.64  (** pretty printing of terms, types etc. **)
    1.65  
    1.66 -fun pretty_term' syn consts context t =
    1.67 -  let
    1.68 -    val thy = Context.theory_of context;
    1.69 -    val curried = Context.exists_name Context.CPureN thy;
    1.70 -    val extern = NameSpace.extern (Consts.space_of consts);
    1.71 -  in Syntax.pretty_term context syn curried (extern_term (K extern) thy t) end;
    1.72 +fun pretty_term' syn context t =
    1.73 +  let val curried = Context.exists_name Context.CPureN (Context.theory_of context)
    1.74 +  in Syntax.pretty_term context syn curried t end;
    1.75  
    1.76 -fun pretty_term thy t = pretty_term' (syn_of thy) (consts_of thy) (Context.Theory thy) t;
    1.77 +fun pretty_term thy t =
    1.78 +  pretty_term' (syn_of thy) (Context.Theory thy)
    1.79 +    (extern_term (NameSpace.extern (Consts.space_of (consts_of thy))) thy t);
    1.80  
    1.81  fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
    1.82  fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);