src/Pure/Isar/named_target.ML
author wenzelm
Fri Sep 07 15:28:48 2012 +0200 (2012-09-07)
changeset 49198 38af9102ee75
parent 48102 9ed089bcad93
child 52103 fb577a13abbd
permissions -rw-r--r--
merged
     1 (*  Title:      Pure/Isar/named_target.ML
     2     Author:     Makarius
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Targets for theory, locale, class -- at the bottom the nested structure.
     6 *)
     7 
     8 signature NAMED_TARGET =
     9 sig
    10   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
    11   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
    12   val theory_init: theory -> local_theory
    13   val reinit: local_theory -> local_theory -> local_theory
    14   val context_cmd: xstring * Position.T -> theory -> local_theory
    15 end;
    16 
    17 structure Named_Target: NAMED_TARGET =
    18 struct
    19 
    20 (* context data *)
    21 
    22 datatype target =
    23   Target of {target: string, is_locale: bool, is_class: bool,
    24     before_exit: local_theory -> local_theory};
    25 
    26 fun make_target target is_locale is_class before_exit =
    27   Target {target = target, is_locale = is_locale, is_class = is_class,
    28     before_exit = before_exit};
    29 
    30 fun named_target _ "" before_exit = make_target "" false false before_exit
    31   | named_target thy locale before_exit =
    32       if Locale.defined thy locale
    33       then make_target locale true (Class.is_class thy locale) before_exit
    34       else error ("No such locale: " ^ quote locale);
    35 
    36 structure Data = Proof_Data
    37 (
    38   type T = target option;
    39   fun init _ = NONE;
    40 );
    41 
    42 val peek =
    43   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
    44     {target = target, is_locale = is_locale, is_class = is_class});
    45 
    46 
    47 (* consts in locale *)
    48 
    49 fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) =
    50   Generic_Target.locale_declaration target true (fn phi =>
    51     let
    52       val b' = Morphism.binding phi b;
    53       val rhs' = Morphism.term phi rhs;
    54       val same_shape = Term.aconv_untyped (rhs, rhs');
    55 
    56       (* FIXME workaround based on educated guess *)
    57       val prefix' = Binding.prefix_of b';
    58       val is_canonical_class = is_class andalso
    59         (Binding.eq_name (b, b')
    60           andalso not (null prefix')
    61           andalso List.last prefix' = (Class.class_prefix target, false)
    62         orelse same_shape);
    63     in
    64       not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
    65     end) #>
    66   (fn lthy => lthy |> Generic_Target.const_declaration
    67     (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));
    68 
    69 
    70 (* define *)
    71 
    72 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params =
    73   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
    74   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
    75     #> pair (lhs, def));
    76 
    77 fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params =
    78   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
    79   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
    80     #> Class.const target ((b, mx), (#1 params, #2 params, lhs))
    81     #> pair (lhs, def));
    82 
    83 fun target_foundation (ta as Target {is_locale, is_class, ...}) =
    84   if is_class then class_foundation ta
    85   else if is_locale then locale_foundation ta
    86   else Generic_Target.theory_foundation;
    87 
    88 
    89 (* notes *)
    90 
    91 fun target_notes (Target {target, is_locale, ...}) =
    92   if is_locale then Generic_Target.locale_notes target
    93   else Generic_Target.theory_notes;
    94 
    95 
    96 (* abbrev *)
    97 
    98 fun locale_abbrev ta prmode ((b, mx), t) xs =
    99   Local_Theory.background_theory_result
   100     (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   101       (fn (lhs, _) =>
   102         locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
   103 
   104 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy =
   105   if is_locale then
   106     lthy
   107     |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs
   108     |> is_class ? Class.abbrev target prmode ((b, mx), t')
   109   else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs;
   110 
   111 
   112 (* declaration *)
   113 
   114 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
   115   if target = "" then Generic_Target.theory_declaration decl lthy
   116   else
   117     lthy
   118     |> pervasive ? Generic_Target.background_declaration decl
   119     |> Generic_Target.locale_declaration target syntax decl
   120     |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
   121 
   122 
   123 (* pretty *)
   124 
   125 fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
   126   let
   127     val thy = Proof_Context.theory_of ctxt;
   128     val target_name =
   129       [Pretty.command (if is_class then "class" else "locale"),
   130         Pretty.str (" " ^ Locale.extern thy target)];
   131     val fixes =
   132       map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
   133         (#1 (Proof_Context.inferred_fixes ctxt));
   134     val assumes =
   135       map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
   136         (Assumption.all_assms_of ctxt);
   137     val elems =
   138       (if null fixes then [] else [Element.Fixes fixes]) @
   139       (if null assumes then [] else [Element.Assumes assumes]);
   140     val body_elems =
   141       if not is_locale then []
   142       else if null elems then [Pretty.block target_name]
   143       else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
   144         map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
   145   in
   146     Pretty.block [Pretty.command "theory", Pretty.brk 1,
   147       Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
   148   end;
   149 
   150 
   151 (* init *)
   152 
   153 fun init_context (Target {target, is_locale, is_class, ...}) =
   154   if not is_locale then Proof_Context.init_global
   155   else if not is_class then Locale.init target
   156   else Class.init target;
   157 
   158 fun init before_exit target thy =
   159   let
   160     val ta = named_target thy target before_exit;
   161     val naming = Sign.naming_of thy
   162       |> Name_Space.mandatory_path (Long_Name.base_name target);
   163   in
   164     thy
   165     |> init_context ta
   166     |> Data.put (SOME ta)
   167     |> Local_Theory.init naming
   168        {define = Generic_Target.define (target_foundation ta),
   169         notes = Generic_Target.notes (target_notes ta),
   170         abbrev = Generic_Target.abbrev (target_abbrev ta),
   171         declaration = target_declaration ta,
   172         pretty = pretty ta,
   173         exit = Local_Theory.target_of o before_exit}
   174   end;
   175 
   176 val theory_init = init I "";
   177 
   178 val reinit =
   179   Local_Theory.assert_bottom true #> Data.get #> the #>
   180   (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
   181 
   182 fun context_cmd ("-", _) thy = theory_init thy
   183   | context_cmd target thy = init I (Locale.check thy target) thy;
   184 
   185 end;