46 |
46 |
47 fun is_theory lthy = |
47 fun is_theory lthy = |
48 Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1; |
48 Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1; |
49 |
49 |
50 |
50 |
51 (* consts *) |
|
52 |
|
53 fun locale_const locale prmode ((b, mx), rhs) = |
|
54 Generic_Target.locale_declaration locale true (fn phi => |
|
55 let |
|
56 val b' = Morphism.binding phi b; |
|
57 val rhs' = Morphism.term phi rhs; |
|
58 val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
59 in |
|
60 Generic_Target.generic_const same_shape prmode ((b', mx), rhs') |
|
61 end) #> |
|
62 Generic_Target.const_declaration |
|
63 (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); |
|
64 |
|
65 fun class_const class prmode (b, rhs) = |
|
66 Generic_Target.locale_declaration class true (fn phi => |
|
67 let |
|
68 val b' = Morphism.binding phi b; |
|
69 val rhs' = Morphism.term phi rhs; |
|
70 val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
71 |
|
72 (* FIXME workaround based on educated guess *) |
|
73 val prefix' = Binding.prefix_of b'; |
|
74 val is_canonical_class = |
|
75 Binding.eq_name (b, b') |
|
76 andalso not (null prefix') |
|
77 andalso List.last prefix' = (Class.class_prefix class, false) |
|
78 orelse same_shape; |
|
79 in |
|
80 not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs') |
|
81 end) #> |
|
82 Generic_Target.const_declaration |
|
83 (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs); |
|
84 |
|
85 |
|
86 (* define *) |
51 (* define *) |
87 |
52 |
88 fun locale_foundation target (((b, U), mx), (b_def, rhs)) params = |
53 fun locale_foundation target (((b, U), mx), (b_def, rhs)) params = |
89 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
54 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
90 #-> (fn (lhs, def) => locale_const target Syntax.mode_default ((b, mx), lhs) |
55 #-> (fn (lhs, def) => Generic_Target.locale_const_declaration target Syntax.mode_default ((b, mx), lhs) |
91 #> pair (lhs, def)); |
56 #> pair (lhs, def)); |
92 |
57 |
93 fun class_foundation target (((b, U), mx), (b_def, rhs)) params = |
58 fun class_foundation target (((b, U), mx), (b_def, rhs)) params = |
94 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
59 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
95 #-> (fn (lhs, def) => class_const target Syntax.mode_default (b, lhs) |
60 #-> (fn (lhs, def) => Class.const target ((b, mx), lhs) params |
96 #> Class.const target ((b, mx), lhs) params |
|
97 #> pair (lhs, def)); |
61 #> pair (lhs, def)); |
98 |
62 |
99 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
63 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
100 if is_class then class_foundation target |
64 if is_class then class_foundation target |
101 else if is_locale then locale_foundation target |
65 else if is_locale then locale_foundation target |
112 (* abbrev *) |
76 (* abbrev *) |
113 |
77 |
114 fun locale_abbrev target prmode (b, mx) (t, _) xs = |
78 fun locale_abbrev target prmode (b, mx) (t, _) xs = |
115 Generic_Target.background_abbrev (b, t) |
79 Generic_Target.background_abbrev (b, t) |
116 #-> (fn (lhs, _) => |
80 #-> (fn (lhs, _) => |
117 locale_const target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
81 Generic_Target.locale_const_declaration target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
118 |
82 |
119 fun class_abbrev target prmode (b, mx) (t, t') xs = |
83 fun class_abbrev target prmode (b, mx) (t, t') xs = |
120 Generic_Target.background_abbrev (b, t) |
84 Generic_Target.background_abbrev (b, t) |
121 #-> (fn (lhs, _) => |
85 #-> (fn (lhs, _) => Class.abbrev target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)) t'); |
122 class_const target prmode (b, Term.list_comb (Logic.unvarify_global lhs, xs))) |
|
123 #> Class.abbrev target prmode ((b, mx), t'); |
|
124 |
86 |
125 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = |
87 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = |
126 if is_class then class_abbrev target |
88 if is_class then class_abbrev target |
127 else if is_locale then locale_abbrev target |
89 else if is_locale then locale_abbrev target |
128 else Generic_Target.theory_abbrev; |
90 else Generic_Target.theory_abbrev; |