--- a/src/Pure/Isar/generic_target.ML Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML Mon Jun 01 18:59:20 2015 +0200
@@ -31,29 +31,33 @@
term list * term list -> local_theory -> local_theory) ->
Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
- (*theory operations*)
- val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
- term list * term list -> local_theory -> (term * thm) * local_theory
- val theory_notes: string ->
+ (*theory target primitives*)
+ val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+ term list * term list -> local_theory -> (term * thm) * local_theory
+ val theory_target_notes: string ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
+ val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+ local_theory -> local_theory
+
+ (*theory target operations*)
val theory_declaration: declaration -> local_theory -> local_theory
- val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
- local_theory -> local_theory
val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
- (*locale operations*)
- val locale_notes: string -> string ->
+ (*locale target primitives*)
+ val locale_target_notes: string -> string ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+ val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
+ (binding * mixfix) * term -> local_theory -> local_theory
+
+ (*locale operations*)
val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
local_theory -> local_theory
- val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
- (binding * mixfix) * term -> local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
@@ -259,7 +263,7 @@
in
-fun notes notes' kind facts lthy =
+fun notes target_notes kind facts lthy =
let
val facts' = facts
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
@@ -269,7 +273,7 @@
val global_facts = Global_Theory.map_facts #2 facts';
in
lthy
- |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
+ |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
|> Attrib.local_notes kind local_facts
end;
@@ -278,7 +282,7 @@
(* abbrev *)
-fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
let
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
@@ -293,28 +297,25 @@
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
in
lthy
- |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
+ |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
|> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
|> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
end;
-(** theory operations **)
+(** theory target primitives **)
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
#-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
#> pair (lhs, def));
-fun theory_notes kind global_facts local_facts =
+fun theory_target_notes kind global_facts local_facts =
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
#> standard_notes (op <>) kind local_facts;
-fun theory_declaration decl =
- background_declaration decl #> standard_declaration (K true) decl;
-
-fun theory_abbrev prmode (b, mx) global_rhs params =
+fun theory_target_abbrev prmode (b, mx) global_rhs params =
Local_Theory.background_theory_result
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
(fn (lhs, _) => (* FIXME type_params!? *)
@@ -322,14 +323,20 @@
#-> (fn lhs => standard_const (op <>) prmode
((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
+
+(** theory operations **)
+
+fun theory_declaration decl =
+ background_declaration decl #> standard_declaration (K true) decl;
+
val theory_registration =
Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-(** locale operations **)
+(** locale target primitives **)
-fun locale_notes locale kind global_facts local_facts =
+fun locale_target_notes locale kind global_facts local_facts =
Local_Theory.background_theory
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
(fn lthy => lthy |>
@@ -342,14 +349,17 @@
Locale.add_declaration locale syntax
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
+ locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+
+
+(** locale operations **)
+
fun locale_declaration locale {syntax, pervasive} decl =
pervasive ? background_declaration decl
#> locale_target_declaration locale syntax decl
#> standard_declaration (fn (_, other) => other <> 0) decl;
-fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
- locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
-
fun locale_const locale prmode ((b, mx), rhs) =
locale_target_const locale (K true) prmode ((b, mx), rhs)
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);