src/Pure/Isar/generic_target.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 60924 610794dff23c
child 61701 e89cfc004f18
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
     1 (*  Title:      Pure/Isar/generic_target.ML
     2     Author:     Makarius
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Common target infrastructure.
     6 *)
     7 
     8 signature GENERIC_TARGET =
     9 sig
    10   (*auxiliary*)
    11   val export_abbrev: Proof.context ->
    12       (term -> term) -> term -> term * ((string * sort) list * (term list * term list))
    13   val check_mixfix_global: binding * bool -> mixfix -> mixfix
    14 
    15   (*background primitives*)
    16   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    17     term list * term list -> local_theory -> (term * thm) * local_theory
    18   val background_declaration: declaration -> local_theory -> local_theory
    19   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
    20 
    21   (*nested local theories primitives*)
    22   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
    23     local_theory -> local_theory
    24 
    25   (*lifting target primitives to local theory operations*)
    26   val define: (((binding * typ) * mixfix) * (binding * term) ->
    27       term list * term list -> local_theory -> (term * thm) * local_theory) ->
    28     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    29     (term * (string * thm)) * local_theory
    30   val notes:
    31     (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
    32       (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
    33     string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
    34     (string * thm list) list * local_theory
    35   val abbrev: (Syntax.mode -> binding * mixfix -> term ->
    36       term list * term list -> local_theory -> local_theory) ->
    37     Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
    38 
    39   (*theory target primitives*)
    40   val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    41      term list * term list -> local_theory -> (term * thm) * local_theory
    42   val theory_target_notes: string ->
    43     (Attrib.binding * (thm list * Token.src list) list) list ->
    44     (Attrib.binding * (thm list * Token.src list) list) list ->
    45     local_theory -> local_theory
    46   val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
    47     local_theory -> local_theory
    48 
    49   (*theory target operations*)
    50   val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
    51     local_theory -> (term * term) * local_theory
    52   val theory_declaration: declaration -> local_theory -> local_theory
    53   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    54     local_theory -> local_theory
    55 
    56   (*locale target primitives*)
    57   val locale_target_notes: string -> string ->
    58     (Attrib.binding * (thm list * Token.src list) list) list ->
    59     (Attrib.binding * (thm list * Token.src list) list) list ->
    60     local_theory -> local_theory
    61   val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
    62     local_theory -> local_theory
    63   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
    64   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
    65     (binding * mixfix) * term -> local_theory -> local_theory
    66 
    67   (*locale operations*)
    68   val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
    69     local_theory -> (term * term) * local_theory
    70   val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
    71     local_theory -> local_theory
    72   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
    73     local_theory -> local_theory
    74   val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
    75     local_theory -> local_theory
    76 end
    77 
    78 structure Generic_Target: GENERIC_TARGET =
    79 struct
    80 
    81 (** consts **)
    82 
    83 fun export_abbrev lthy preprocess rhs =
    84   let
    85     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
    86 
    87     val rhs' = rhs
    88       |> Assumption.export_term lthy (Local_Theory.target_of lthy)
    89       |> preprocess;
    90     val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
    91     val u = fold_rev lambda term_params rhs';
    92     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
    93 
    94     val extra_tfrees =
    95       subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
    96     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
    97   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
    98 
    99 fun check_mixfix ctxt (b, extra_tfrees) mx =
   100   if null extra_tfrees then mx
   101   else
   102    (if Context_Position.is_visible ctxt then
   103       warning
   104         ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
   105           commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
   106           (if mx = NoSyn then ""
   107            else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
   108     else (); NoSyn);
   109 
   110 fun check_mixfix_global (b, no_params) mx =
   111   if no_params orelse mx = NoSyn then mx
   112   else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
   113     Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
   114 
   115 fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
   116   if phi_pred phi then
   117     let
   118       val b' = Morphism.binding phi b;
   119       val rhs' = Morphism.term phi rhs;
   120       val same_shape = Term.aconv_untyped (rhs, rhs');
   121       val const_alias =
   122         if same_shape then
   123           (case rhs' of
   124             Const (c, T) =>
   125               let
   126                 val thy = Context.theory_of context;
   127                 val ctxt = Context.proof_of context;
   128               in
   129                 (case Type_Infer_Context.const_type ctxt c of
   130                   SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
   131                 | NONE => NONE)
   132               end
   133           | _ => NONE)
   134         else NONE;
   135     in
   136       (case const_alias of
   137         SOME c =>
   138           context
   139           |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
   140           |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
   141       | NONE =>
   142           context
   143           |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
   144           |-> (fn (const as Const (c, _), _) => same_shape ?
   145                 (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
   146                  Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
   147     end
   148   else context;
   149 
   150 
   151 
   152 (** background primitives **)
   153 
   154 fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   155   let
   156     val params = type_params @ term_params;
   157     val mx' = check_mixfix_global (b, null params) mx;
   158 
   159     val (const, lthy2) = lthy
   160       |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
   161     val lhs = Term.list_comb (const, params);
   162 
   163     val ((_, def), lthy3) = lthy2
   164       |> Local_Theory.background_theory_result
   165         (Thm.add_def (Proof_Context.defs_context lthy2) false false
   166           (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
   167   in ((lhs, def), lthy3) end;
   168 
   169 fun background_declaration decl lthy =
   170   let
   171     val theory_decl =
   172       Local_Theory.standard_form lthy
   173         (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
   174   in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
   175 
   176 fun background_abbrev (b, global_rhs) params =
   177   Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
   178   #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
   179 
   180 
   181 
   182 (** nested local theories primitives **)
   183 
   184 fun standard_facts lthy ctxt =
   185   Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
   186 
   187 fun standard_notes pred kind facts lthy =
   188   Local_Theory.map_contexts (fn level => fn ctxt =>
   189     if pred (Local_Theory.level lthy, level)
   190     then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
   191     else ctxt) lthy;
   192 
   193 fun standard_declaration pred decl lthy =
   194   Local_Theory.map_contexts (fn level => fn ctxt =>
   195     if pred (Local_Theory.level lthy, level)
   196     then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
   197     else ctxt) lthy;
   198 
   199 fun standard_const pred prmode ((b, mx), rhs) =
   200   standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
   201 
   202 
   203 (** lifting target primitives to local theory operations **)
   204 
   205 (* define *)
   206 
   207 fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
   208   let
   209     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
   210 
   211     (*term and type parameters*)
   212     val ((defs, _), rhs') = Thm.cterm_of lthy rhs
   213       |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
   214 
   215     val xs = Variable.add_fixed lthy rhs' [];
   216     val T = Term.fastype_of rhs;
   217     val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
   218     val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
   219     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
   220 
   221     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   222     val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs);
   223     val params = type_params @ term_params;
   224 
   225     val U = map Term.fastype_of params ---> T;
   226 
   227     (*foundation*)
   228     val ((lhs', global_def), lthy2) = lthy
   229       |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
   230 
   231     (*local definition*)
   232     val ((lhs, local_def), lthy3) = lthy2
   233       |> Local_Defs.add_def ((b, NoSyn), lhs');
   234 
   235     (*result*)
   236     val def =
   237       Thm.transitive local_def global_def
   238       |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
   239     val ([(res_name, [res])], lthy4) = lthy3
   240       |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   241   in ((lhs, (res_name, res)), lthy4) end;
   242 
   243 
   244 (* notes *)
   245 
   246 local
   247 
   248 fun import_export_proof ctxt (name, raw_th) =
   249   let
   250     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
   251 
   252     (*export assumes/defines*)
   253     val th = Goal.norm_result ctxt raw_th;
   254     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
   255     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
   256 
   257     (*export fixes*)
   258     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
   259     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
   260     val (th'' :: vs) =
   261       (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
   262       |> Variable.export ctxt thy_ctxt
   263       |> Drule.zero_var_indexes_list;
   264 
   265     (*thm definition*)
   266     val result = Global_Theory.name_thm true true name th'';
   267 
   268     (*import fixes*)
   269     val (tvars, vars) =
   270       chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
   271       |>> map Logic.dest_type;
   272 
   273     val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
   274     val inst =
   275       map_filter
   276         (fn (Var (xi, T), t) =>
   277           SOME ((xi, Term_Subst.instantiateT instT T),
   278             Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
   279         | _ => NONE) (vars ~~ frees);
   280     val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
   281 
   282     (*import assumes/defines*)
   283     val result'' =
   284       (fold (curry op COMP) asms' result'
   285         handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
   286       |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
   287       |> Goal.norm_result ctxt
   288       |> Global_Theory.name_thm false false name;
   289 
   290   in (result'', result) end;
   291 
   292 in
   293 
   294 fun notes target_notes kind facts lthy =
   295   let
   296     val facts' = facts
   297       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
   298           (Local_Theory.full_name lthy (fst a))) bs))
   299       |> Global_Theory.map_facts (import_export_proof lthy);
   300     val local_facts = Global_Theory.map_facts #1 facts';
   301     val global_facts = Global_Theory.map_facts #2 facts';
   302   in
   303     lthy
   304     |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
   305     |> Attrib.local_notes kind local_facts
   306   end;
   307 
   308 end;
   309 
   310 
   311 (* abbrev *)
   312 
   313 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   314   let
   315     val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs;
   316     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
   317   in
   318     lthy
   319     |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
   320     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
   321     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
   322   end;
   323 
   324 
   325 
   326 (** theory target primitives **)
   327 
   328 fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   329   background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
   330   #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
   331     #> pair (lhs, def));
   332 
   333 fun theory_target_notes kind global_facts local_facts =
   334   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
   335   #> standard_notes (op <>) kind local_facts;
   336 
   337 fun theory_target_abbrev prmode (b, mx) global_rhs params =
   338   Local_Theory.background_theory_result
   339     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
   340       (fn (lhs, _) =>  (* FIXME type_params!? *)
   341         Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
   342   #-> (fn lhs => standard_const (op <>) prmode
   343           ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
   344 
   345 
   346 (** theory operations **)
   347 
   348 val theory_abbrev = abbrev theory_target_abbrev;
   349 
   350 fun theory_declaration decl =
   351   background_declaration decl #> standard_declaration (K true) decl;
   352 
   353 val theory_registration =
   354   Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
   355 
   356 
   357 
   358 (** locale target primitives **)
   359 
   360 fun locale_target_notes locale kind global_facts local_facts =
   361   Local_Theory.background_theory
   362     (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
   363   (fn lthy => lthy |>
   364     Local_Theory.target (fn ctxt => ctxt |>
   365       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
   366   standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
   367 
   368 fun locale_target_declaration locale syntax decl lthy = lthy
   369   |> Local_Theory.target (fn ctxt => ctxt |>
   370     Locale.add_declaration locale syntax
   371       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
   372 
   373 fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
   374   locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
   375 
   376 
   377 (** locale operations **)
   378 
   379 fun locale_declaration locale {syntax, pervasive} decl =
   380   pervasive ? background_declaration decl
   381   #> locale_target_declaration locale syntax decl
   382   #> standard_declaration (fn (_, other) => other <> 0) decl;
   383 
   384 fun locale_const locale prmode ((b, mx), rhs) =
   385   locale_target_const locale (K true) prmode ((b, mx), rhs)
   386   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
   387 
   388 fun locale_dependency locale dep_morph mixin export =
   389   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
   390   #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
   391 
   392 
   393 (** locale abbreviations **)
   394 
   395 fun locale_target_abbrev locale prmode (b, mx) global_rhs params =
   396   background_abbrev (b, global_rhs) (snd params)
   397   #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs));
   398 
   399 fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
   400 
   401 end;