56 SOME target => target |
56 SOME target => target |
57 | _ => error "Not in a named target") |
57 | _ => error "Not in a named target") |
58 end; |
58 end; |
59 |
59 |
60 |
60 |
61 (* consts in locale *) |
61 (* consts *) |
62 |
62 |
63 fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = |
63 fun locale_const locale prmode ((b, mx), rhs) = |
64 Generic_Target.locale_declaration target true (fn phi => |
64 Generic_Target.locale_declaration locale true (fn phi => |
65 let |
65 let |
66 val b' = Morphism.binding phi b; |
66 val b' = Morphism.binding phi b; |
67 val rhs' = Morphism.term phi rhs; |
67 val rhs' = Morphism.term phi rhs; |
68 val same_shape = Term.aconv_untyped (rhs, rhs'); |
68 val same_shape = Term.aconv_untyped (rhs, rhs'); |
69 |
|
70 (* FIXME workaround based on educated guess *) |
|
71 val prefix' = Binding.prefix_of b'; |
|
72 val is_canonical_class = is_class andalso |
|
73 (Binding.eq_name (b, b') |
|
74 andalso not (null prefix') |
|
75 andalso List.last prefix' = (Class.class_prefix target, false) |
|
76 orelse same_shape); |
|
77 in |
69 in |
78 not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs') |
70 Generic_Target.generic_const same_shape prmode ((b', mx), rhs') |
79 end) #> |
71 end) #> |
80 Generic_Target.const_declaration |
72 Generic_Target.const_declaration |
81 (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); |
73 (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); |
82 |
74 |
|
75 fun class_const class prmode (b, rhs) = |
|
76 Generic_Target.locale_declaration class true (fn phi => |
|
77 let |
|
78 val b' = Morphism.binding phi b; |
|
79 val rhs' = Morphism.term phi rhs; |
|
80 val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
81 |
|
82 (* FIXME workaround based on educated guess *) |
|
83 val prefix' = Binding.prefix_of b'; |
|
84 val is_canonical_class = |
|
85 Binding.eq_name (b, b') |
|
86 andalso not (null prefix') |
|
87 andalso List.last prefix' = (Class.class_prefix class, false) |
|
88 orelse same_shape; |
|
89 in |
|
90 not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs') |
|
91 end) #> |
|
92 Generic_Target.const_declaration |
|
93 (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs); |
|
94 |
83 |
95 |
84 (* define *) |
96 (* define *) |
85 |
97 |
86 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = |
98 fun locale_foundation target (((b, U), mx), (b_def, rhs)) params = |
87 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
99 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
88 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) |
100 #-> (fn (lhs, def) => locale_const target Syntax.mode_default ((b, mx), lhs) |
89 #> pair (lhs, def)); |
101 #> pair (lhs, def)); |
90 |
102 |
91 fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = |
103 fun class_foundation target (((b, U), mx), (b_def, rhs)) params = |
92 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
104 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
93 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) |
105 #-> (fn (lhs, def) => class_const target Syntax.mode_default (b, lhs) |
94 #> Class.const target ((b, mx), (#1 params, #2 params, lhs)) |
106 #> Class.const target ((b, mx), (#1 params, #2 params, lhs)) |
95 #> pair (lhs, def)); |
107 #> pair (lhs, def)); |
96 |
108 |
97 fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
109 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
98 if is_class then class_foundation ta |
110 if is_class then class_foundation target |
99 else if is_locale then locale_foundation ta |
111 else if is_locale then locale_foundation target |
100 else Generic_Target.theory_foundation; |
112 else Generic_Target.theory_foundation; |
101 |
113 |
102 |
114 |
103 (* notes *) |
115 (* notes *) |
104 |
116 |
107 else Generic_Target.theory_notes; |
119 else Generic_Target.theory_notes; |
108 |
120 |
109 |
121 |
110 (* abbrev *) |
122 (* abbrev *) |
111 |
123 |
112 fun locale_abbrev ta prmode ((b, mx), t) xs = |
124 fun locale_abbrev target prmode (b, mx) (t, _) xs = |
113 Local_Theory.background_theory_result |
125 Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) |
114 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
126 #-> (fn (lhs, _) => |
115 (fn (lhs, _) => |
127 locale_const target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
116 locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
128 |
117 |
129 fun class_abbrev target prmode (b, mx) (t, t') xs = |
118 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = |
130 Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) |
119 if is_locale then |
131 #-> (fn (lhs, _) => |
120 lthy |
132 class_const target prmode (b, Term.list_comb (Logic.unvarify_global lhs, xs))) |
121 |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs |
133 #> Class.abbrev target prmode ((b, mx), t'); |
122 |> is_class ? Class.abbrev target prmode ((b, mx), t') |
134 |
123 else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; |
135 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = |
|
136 if is_class then class_abbrev target |
|
137 else if is_locale then locale_abbrev target |
|
138 else Generic_Target.theory_abbrev; |
124 |
139 |
125 |
140 |
126 (* declaration *) |
141 (* declaration *) |
127 |
142 |
128 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |
143 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |