more systematic naming of tsig operations;
authorwenzelm
Wed Apr 28 11:13:11 2010 +0200 (2010-04-28 ago)
changeset 3645062eaaffe6e47
parent 36449 78721f3adb13
child 36451 ddc965e172c4
more systematic naming of tsig operations;
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:09:19 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:13:11 2010 +0200
     1.3 @@ -181,14 +181,14 @@
     1.4     {mode: mode,                       (*inner syntax mode*)
     1.5      naming: Name_Space.naming,        (*local naming conventions*)
     1.6      syntax: Local_Syntax.T,           (*local syntax*)
     1.7 -    tsigs: Type.tsig * Type.tsig,     (*local/global type signature -- local name space only*)
     1.8 +    tsig: Type.tsig * Type.tsig,      (*local/global type signature -- local name space only*)
     1.9      consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
    1.10      facts: Facts.T,                   (*local facts*)
    1.11      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    1.12  
    1.13 -fun make_ctxt (mode, naming, syntax, tsigs, consts, facts, cases) =
    1.14 +fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
    1.15    Ctxt {mode = mode, naming = naming, syntax = syntax,
    1.16 -    tsigs = tsigs, consts = consts, facts = facts, cases = cases};
    1.17 +    tsig = tsig, consts = consts, facts = facts, cases = cases};
    1.18  
    1.19  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    1.20  
    1.21 @@ -204,39 +204,39 @@
    1.22  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
    1.23  
    1.24  fun map_context f =
    1.25 -  ContextData.map (fn Ctxt {mode, naming, syntax, tsigs, consts, facts, cases} =>
    1.26 -    make_ctxt (f (mode, naming, syntax, tsigs, consts, facts, cases)));
    1.27 +  ContextData.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
    1.28 +    make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases)));
    1.29  
    1.30 -fun set_mode mode = map_context (fn (_, naming, syntax, tsigs, consts, facts, cases) =>
    1.31 -  (mode, naming, syntax, tsigs, consts, facts, cases));
    1.32 +fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) =>
    1.33 +  (mode, naming, syntax, tsig, consts, facts, cases));
    1.34  
    1.35  fun map_mode f =
    1.36 -  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsigs, consts, facts, cases) =>
    1.37 -    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsigs, consts, facts, cases));
    1.38 +  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
    1.39 +    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
    1.40  
    1.41  fun map_naming f =
    1.42 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.43 -    (mode, f naming, syntax, tsigs, consts, facts, cases));
    1.44 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.45 +    (mode, f naming, syntax, tsig, consts, facts, cases));
    1.46  
    1.47  fun map_syntax f =
    1.48 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.49 -    (mode, naming, f syntax, tsigs, consts, facts, cases));
    1.50 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.51 +    (mode, naming, f syntax, tsig, consts, facts, cases));
    1.52  
    1.53 -fun map_tsigs f =
    1.54 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.55 -    (mode, naming, syntax, f tsigs, consts, facts, cases));
    1.56 +fun map_tsig f =
    1.57 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.58 +    (mode, naming, syntax, f tsig, consts, facts, cases));
    1.59  
    1.60  fun map_consts f =
    1.61 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.62 -    (mode, naming, syntax, tsigs, f consts, facts, cases));
    1.63 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.64 +    (mode, naming, syntax, tsig, f consts, facts, cases));
    1.65  
    1.66  fun map_facts f =
    1.67 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.68 -    (mode, naming, syntax, tsigs, consts, f facts, cases));
    1.69 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.70 +    (mode, naming, syntax, tsig, consts, f facts, cases));
    1.71  
    1.72  fun map_cases f =
    1.73 -  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    1.74 -    (mode, naming, syntax, tsigs, consts, facts, f cases));
    1.75 +  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.76 +    (mode, naming, syntax, tsig, consts, facts, f cases));
    1.77  
    1.78  val get_mode = #mode o rep_context;
    1.79  val restore_mode = set_mode o get_mode;
    1.80 @@ -254,7 +254,7 @@
    1.81  val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
    1.82  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    1.83  
    1.84 -val tsig_of = #1 o #tsigs o rep_context;
    1.85 +val tsig_of = #1 o #tsig o rep_context;
    1.86  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.87  
    1.88  val consts_of = #1 o #consts o rep_context;
    1.89 @@ -268,10 +268,10 @@
    1.90  
    1.91  fun transfer_syntax thy ctxt = ctxt |>
    1.92    map_syntax (Local_Syntax.rebuild thy) |>
    1.93 -  map_tsigs (fn tsigs as (local_tsig, global_tsig) =>
    1.94 +  map_tsig (fn tsig as (local_tsig, global_tsig) =>
    1.95      let val thy_tsig = Sign.tsig_of thy in
    1.96 -      if Type.eq_tsig (thy_tsig, global_tsig) then tsigs
    1.97 -      else (Type.merge_tsigs (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
    1.98 +      if Type.eq_tsig (thy_tsig, global_tsig) then tsig
    1.99 +      else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
   1.100      end) |>
   1.101    map_consts (fn consts as (local_consts, global_consts) =>
   1.102      let val thy_consts = Sign.consts_of thy in
   1.103 @@ -1140,8 +1140,8 @@
   1.104  
   1.105  (* aliases *)
   1.106  
   1.107 -fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
   1.108 -fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
   1.109 +fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
   1.110 +fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
   1.111  fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
   1.112  
   1.113  
     2.1 --- a/src/Pure/sign.ML	Wed Apr 28 11:09:19 2010 +0200
     2.2 +++ b/src/Pure/sign.ML	Wed Apr 28 11:13:11 2010 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4  
     2.5        val naming = Name_Space.default_naming;
     2.6        val syn = Syntax.merge_syntaxes syn1 syn2;
     2.7 -      val tsig = Type.merge_tsigs pp (tsig1, tsig2);
     2.8 +      val tsig = Type.merge_tsig pp (tsig1, tsig2);
     2.9        val consts = Consts.merge (consts1, consts2);
    2.10      in make_sign (naming, syn, tsig, consts) end;
    2.11  );
     3.1 --- a/src/Pure/type.ML	Wed Apr 28 11:09:19 2010 +0200
     3.2 +++ b/src/Pure/type.ML	Wed Apr 28 11:13:11 2010 +0200
     3.3 @@ -89,7 +89,7 @@
     3.4    val hide_type: bool -> string -> tsig -> tsig
     3.5    val add_arity: Pretty.pp -> arity -> tsig -> tsig
     3.6    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
     3.7 -  val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
     3.8 +  val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
     3.9  end;
    3.10  
    3.11  structure Type: TYPE =
    3.12 @@ -621,7 +621,7 @@
    3.13  
    3.14  (* merge type signatures *)
    3.15  
    3.16 -fun merge_tsigs pp (tsig1, tsig2) =
    3.17 +fun merge_tsig pp (tsig1, tsig2) =
    3.18    let
    3.19      val (TSig {classes = (space1, classes1), default = default1, types = types1,
    3.20        log_types = _}) = tsig1;