27 val extern_syntax: Proof.context -> T -> string -> xstring |
27 val extern_syntax: Proof.context -> T -> string -> xstring |
28 val read_const: T -> string * Position.T -> term |
28 val read_const: T -> string * Position.T -> term |
29 val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) |
29 val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) |
30 val typargs: T -> string * typ -> typ list |
30 val typargs: T -> string * typ -> typ list |
31 val instance: T -> string * typ list -> typ |
31 val instance: T -> string * typ list -> typ |
32 val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T |
32 val declare: Context.generic -> binding * typ -> T -> T |
33 val constrain: string * typ option -> T -> T |
33 val constrain: string * typ option -> T -> T |
34 val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string -> |
34 val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T |
35 binding * term -> T -> (term * term) * T |
|
36 val revert_abbrev: string -> string -> T -> T |
35 val revert_abbrev: string -> string -> T -> T |
37 val hide: bool -> string -> T -> T |
36 val hide: bool -> string -> T -> T |
38 val empty: T |
37 val empty: T |
39 val merge: T * T -> T |
38 val merge: T * T -> T |
40 end; |
39 end; |
230 (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs)); |
229 (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs)); |
231 |
230 |
232 |
231 |
233 (* declarations *) |
232 (* declarations *) |
234 |
233 |
235 fun declare ctxt naming (b, declT) = |
234 fun declare context (b, declT) = |
236 map_consts (fn (decls, constraints, rev_abbrevs) => |
235 map_consts (fn (decls, constraints, rev_abbrevs) => |
237 let |
236 let |
238 val decl = {T = declT, typargs = typargs_of declT}; |
237 val decl = {T = declT, typargs = typargs_of declT}; |
239 val _ = Binding.check b; |
238 val _ = Binding.check b; |
240 val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE)); |
239 val (_, decls') = decls |> Name_Space.define context true (b, (decl, NONE)); |
241 in (decls', constraints, rev_abbrevs) end); |
240 in (decls', constraints, rev_abbrevs) end); |
242 |
241 |
243 |
242 |
244 (* constraints *) |
243 (* constraints *) |
245 |
244 |
266 val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []; |
265 val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []; |
267 in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; |
266 in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; |
268 |
267 |
269 in |
268 in |
270 |
269 |
271 fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts = |
270 fun abbreviate context tsig mode (b, raw_rhs) consts = |
272 let |
271 let |
273 val pp = Context.pretty ctxt; |
272 val pp = Context.pretty_generic context; |
274 val cert_term = certify pp tsig false consts; |
273 val cert_term = certify pp tsig false consts; |
275 val expand_term = certify pp tsig true consts; |
274 val expand_term = certify pp tsig true consts; |
276 val force_expand = mode = Print_Mode.internal; |
275 val force_expand = mode = Print_Mode.internal; |
277 |
276 |
278 val _ = Term.exists_subterm Term.is_Var raw_rhs andalso |
277 val _ = Term.exists_subterm Term.is_Var raw_rhs andalso |
282 |> Term.map_types (Type.cert_typ tsig) |
281 |> Term.map_types (Type.cert_typ tsig) |
283 |> cert_term |
282 |> cert_term |
284 |> Term.close_schematic_term; |
283 |> Term.close_schematic_term; |
285 val normal_rhs = expand_term rhs; |
284 val normal_rhs = expand_term rhs; |
286 val T = Term.fastype_of rhs; |
285 val T = Term.fastype_of rhs; |
287 val lhs = Const (Name_Space.full_name naming b, T); |
286 val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T); |
288 in |
287 in |
289 consts |> map_consts (fn (decls, constraints, rev_abbrevs) => |
288 consts |> map_consts (fn (decls, constraints, rev_abbrevs) => |
290 let |
289 let |
291 val decl = {T = T, typargs = typargs_of T}; |
290 val decl = {T = T, typargs = typargs_of T}; |
292 val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; |
291 val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; |
293 val _ = Binding.check b; |
292 val _ = Binding.check b; |
294 val (_, decls') = decls |
293 val (_, decls') = decls |
295 |> Name_Space.define ctxt true naming (b, (decl, SOME abbr)); |
294 |> Name_Space.define context true (b, (decl, SOME abbr)); |
296 val rev_abbrevs' = rev_abbrevs |
295 val rev_abbrevs' = rev_abbrevs |
297 |> update_abbrevs mode (rev_abbrev lhs rhs); |
296 |> update_abbrevs mode (rev_abbrev lhs rhs); |
298 in (decls', constraints, rev_abbrevs') end) |
297 in (decls', constraints, rev_abbrevs') end) |
299 |> pair (lhs, rhs) |
298 |> pair (lhs, rhs) |
300 end; |
299 end; |