63 #> not pervasive ? Context.proof_map (Morphism.form decl); |
63 #> not pervasive ? Context.proof_map (Morphism.form decl); |
64 |
64 |
65 |
65 |
66 (* consts in locales *) |
66 (* consts in locales *) |
67 |
67 |
68 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi = |
68 fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = |
69 let |
69 locale_declaration target true (fn phi => |
70 val b' = Morphism.binding phi b; |
70 let |
71 val rhs' = Morphism.term phi rhs; |
71 val b' = Morphism.binding phi b; |
72 val arg = (b', Term.close_schematic_term rhs'); |
72 val rhs' = Morphism.term phi rhs; |
73 val same_shape = Term.aconv_untyped (rhs, rhs'); |
73 val arg = (b', Term.close_schematic_term rhs'); |
74 (* FIXME workaround based on educated guess *) |
74 val same_shape = Term.aconv_untyped (rhs, rhs'); |
75 val prefix' = Binding.prefix_of b'; |
75 |
76 val is_canonical_class = is_class andalso |
76 (* FIXME workaround based on educated guess *) |
77 (Binding.eq_name (b, b') |
77 val prefix' = Binding.prefix_of b'; |
78 andalso not (null prefix') |
78 val is_canonical_class = is_class andalso |
79 andalso List.last prefix' = (Class.class_prefix target, false) |
79 (Binding.eq_name (b, b') |
80 orelse same_shape); |
80 andalso not (null prefix') |
81 in |
81 andalso List.last prefix' = (Class.class_prefix target, false) |
82 not is_canonical_class ? |
82 orelse same_shape); |
83 (Context.mapping_result |
83 in |
84 (Sign.add_abbrev Print_Mode.internal arg) |
84 not is_canonical_class ? |
85 (Proof_Context.add_abbrev Print_Mode.internal arg) |
85 (Context.mapping_result |
86 #-> (fn (lhs' as Const (d, _), _) => |
86 (Sign.add_abbrev Print_Mode.internal arg) |
87 same_shape ? |
87 (Proof_Context.add_abbrev Print_Mode.internal arg) |
88 (Context.mapping |
88 #-> (fn (lhs' as Const (d, _), _) => |
89 (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #> |
89 same_shape ? |
90 Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)])))) |
90 (Context.mapping |
91 end; |
91 (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #> |
92 |
92 Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)])))) |
93 fun locale_const_declaration (ta as Target {target, ...}) prmode arg = |
93 end); |
94 locale_declaration target true (locale_const ta prmode arg); |
|
95 |
94 |
96 |
95 |
97 (* define *) |
96 (* define *) |
98 |
97 |
99 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
98 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
100 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
99 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
101 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs) |
100 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) |
102 #> pair (lhs, def)) |
101 #> pair (lhs, def)) |
103 |
102 |
104 fun class_foundation (ta as Target {target, ...}) |
103 fun class_foundation (ta as Target {target, ...}) |
105 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
104 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
106 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
105 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
107 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
106 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) |
108 #> Class.const target ((b, mx), (type_params, lhs)) |
107 #> Class.const target ((b, mx), (type_params, lhs)) |
109 #> pair (lhs, def)) |
108 #> pair (lhs, def)) |
110 |
109 |
111 fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
110 fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
112 if is_class then class_foundation ta |
111 if is_class then class_foundation ta |
135 (* abbrev *) |
134 (* abbrev *) |
136 |
135 |
137 fun locale_abbrev ta prmode ((b, mx), t) xs = |
136 fun locale_abbrev ta prmode ((b, mx), t) xs = |
138 Local_Theory.background_theory_result |
137 Local_Theory.background_theory_result |
139 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
138 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
140 (fn (lhs, _) => locale_const_declaration ta prmode |
139 (fn (lhs, _) => locale_const ta prmode |
141 ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
140 ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
142 |
141 |
143 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
142 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
144 prmode (b, mx) (global_rhs, t') xs lthy = |
143 prmode (b, mx) (global_rhs, t') xs lthy = |
145 if is_locale then |
144 if is_locale then |