src/Pure/Isar/class_target.ML
changeset 29362 f9ded2d789b9
parent 29360 a5be60c3674e
child 29439 83601bdadae8
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon Jan 05 15:55:51 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jan 06 08:50:02 2009 +0100
     1.3 @@ -69,72 +69,36 @@
     1.4  
     1.5  (*temporary adaption code to mediate between old and new locale code*)
     1.6  
     1.7 -structure Old_Locale =
     1.8 +structure Locale_Layer =
     1.9  struct
    1.10  
    1.11 -val intro_locales_tac = Old_Locale.intro_locales_tac; (*already forked!*)
    1.12 -
    1.13 -val interpretation = Old_Locale.interpretation;
    1.14 -val interpretation_in_locale = Old_Locale.interpretation_in_locale;
    1.15 +val init = Old_Locale.init;
    1.16 +val parameters_of = Old_Locale.parameters_of;
    1.17 +val intros = Old_Locale.intros;
    1.18 +val dests = Old_Locale.dests;
    1.19  val get_interpret_morph = Old_Locale.get_interpret_morph;
    1.20  val Locale = Old_Locale.Locale;
    1.21  val extern = Old_Locale.extern;
    1.22 -val intros = Old_Locale.intros;
    1.23 -val dests = Old_Locale.dests;
    1.24 -val init = Old_Locale.init;
    1.25 -val Merge = Old_Locale.Merge;
    1.26 -val parameters_of_expr = Old_Locale.parameters_of_expr;
    1.27 -val empty = Old_Locale.empty;
    1.28 -val cert_expr = Old_Locale.cert_expr;
    1.29 -val read_expr = Old_Locale.read_expr;
    1.30 -val parameters_of = Old_Locale.parameters_of;
    1.31 -val add_locale = Old_Locale.add_locale;
    1.32 -
    1.33 -end;
    1.34 -
    1.35 -(*structure New_Locale =
    1.36 -struct
    1.37 -
    1.38 -val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
    1.39 -
    1.40 -val interpretation = Locale.interpretation; (*!*)
    1.41 -val interpretation_in_locale = Locale.interpretation_in_locale; (*!*)
    1.42 -val get_interpret_morph = Locale.get_interpret_morph; (*!*)
    1.43 -fun Locale loc = ([(loc, ("", Expression.Positional []))], []);
    1.44 -val extern = NewLocale.extern;
    1.45 -val intros = Locale.intros; (*!*)
    1.46 -val dests = Locale.dests; (*!*)
    1.47 -val init = NewLocale.init;
    1.48 -fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []);
    1.49 -val parameters_of_expr = Locale.parameters_of_expr; (*!*)
    1.50 -val empty = ([], []);
    1.51 -val cert_expr = Locale.cert_expr; (*!"*)
    1.52 -val read_expr = Locale.read_expr; (*!"*)
    1.53 -val parameters_of = NewLocale.params_of; (*why typ option?*)
    1.54 -val add_locale = Expression.add_locale;
    1.55 -
    1.56 -end;*)
    1.57 -
    1.58 -structure Locale = Old_Locale;
    1.59 -
    1.60 -(*proper code again*)
    1.61 -
    1.62 -
    1.63 -(** auxiliary **)
    1.64 +val intro_locales_tac = Old_Locale.intro_locales_tac;
    1.65  
    1.66  fun prove_interpretation tac prfx_atts expr inst =
    1.67 -  Locale.interpretation I prfx_atts expr inst
    1.68 +  Old_Locale.interpretation I prfx_atts expr inst
    1.69    ##> Proof.global_terminal_proof
    1.70        (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
    1.71    ##> ProofContext.theory_of;
    1.72  
    1.73  fun prove_interpretation_in tac after_qed (name, expr) =
    1.74 -  Locale.interpretation_in_locale
    1.75 +  Old_Locale.interpretation_in_locale
    1.76        (ProofContext.theory after_qed) (name, expr)
    1.77    #> Proof.global_terminal_proof
    1.78        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.79    #> ProofContext.theory_of;
    1.80  
    1.81 +end;
    1.82 +
    1.83 +
    1.84 +(** auxiliary **)
    1.85 +
    1.86  val class_prefix = Logic.const_of_class o Sign.base_name;
    1.87  
    1.88  fun class_name_morphism class =
    1.89 @@ -143,7 +107,7 @@
    1.90  type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
    1.91  
    1.92  fun activate_class_morphism thy class inst morphism =
    1.93 -  Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
    1.94 +  Locale_Layer.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
    1.95  
    1.96  
    1.97  (** primitive axclass and instance commands **)
    1.98 @@ -308,7 +272,7 @@
    1.99        (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.100          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   1.101        if is_class thy class then (SOME o Pretty.str)
   1.102 -        ("locale: " ^ Locale.extern thy class) else NONE,
   1.103 +        ("locale: " ^ Locale_Layer.extern thy class) else NONE,
   1.104        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   1.105            (Pretty.str "parameters:" :: ps)) o map mk_param
   1.106          o these o Option.map #params o try (AxClass.get_info thy)) class,
   1.107 @@ -362,12 +326,12 @@
   1.108      val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
   1.109      fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
   1.110      fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
   1.111 -      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
   1.112 +      ORELSE' (fn n => SELECT_GOAL (Locale_Layer.intro_locales_tac false ctxt []) n));
   1.113      val prfx = class_prefix class;
   1.114    in
   1.115      thy
   1.116      |> fold2 add_constraint (map snd consts) no_constraints
   1.117 -    |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
   1.118 +    |> Locale_Layer.prove_interpretation tac (class_name_morphism class) (Locale_Layer.Locale class)
   1.119            (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
   1.120      ||> fold2 add_constraint (map snd consts) constraints
   1.121    end;
   1.122 @@ -384,8 +348,8 @@
   1.123    in
   1.124      thy
   1.125      |> AxClass.add_classrel classrel
   1.126 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
   1.127 -         I (sub, Locale.Locale sup)
   1.128 +    |> Locale_Layer.prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
   1.129 +         I (sub, Locale_Layer.Locale sup)
   1.130      |> ClassData.map (Graph.add_edge (sub, sup))
   1.131    end;
   1.132  
   1.133 @@ -401,7 +365,7 @@
   1.134    end;
   1.135  
   1.136  fun default_intro_tac ctxt [] =
   1.137 -      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] ORELSE
   1.138 +      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
   1.139        Locale.intro_locales_tac true ctxt []
   1.140    | default_intro_tac _ _ = no_tac;
   1.141  
   1.142 @@ -470,7 +434,7 @@
   1.143  
   1.144  fun init class thy =
   1.145    thy
   1.146 -  |> Locale.init class
   1.147 +  |> Locale_Layer.init class
   1.148    |> begin [class] (base_sort thy class);
   1.149  
   1.150