29 val instance: T -> string * typ list -> typ |
29 val instance: T -> string * typ list -> typ |
30 val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T |
30 val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T |
31 val constrain: string * typ option -> T -> T |
31 val constrain: string * typ option -> T -> T |
32 val expand_abbrevs: bool -> T -> T |
32 val expand_abbrevs: bool -> T -> T |
33 val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> |
33 val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> |
34 (bstring * term) * bool -> T -> T |
34 (bstring * term) * bool -> T -> ((string * typ) * term) * T |
35 val hide: bool -> string -> T -> T |
35 val hide: bool -> string -> T -> T |
36 val empty: T |
36 val empty: T |
37 val merge: T * T -> T |
37 val merge: T * T -> T |
38 end; |
38 end; |
39 |
39 |
251 |
251 |
252 in |
252 in |
253 |
253 |
254 fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts = |
254 fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts = |
255 let |
255 let |
|
256 val full_c = NameSpace.full naming c; |
256 val rhs = raw_rhs |
257 val rhs = raw_rhs |
257 |> Term.map_types (Type.cert_typ tsig) |
258 |> Term.map_types (Type.cert_typ tsig) |
258 |> certify pp tsig (consts |> expand_abbrevs false); |
259 |> certify pp tsig (consts |> expand_abbrevs false); |
259 val rhs' = rhs |
260 val rhs' = rhs |
260 |> certify pp tsig (consts |> expand_abbrevs true); |
261 |> certify pp tsig (consts |> expand_abbrevs true); |
261 val T = Term.fastype_of rhs; |
262 val T = Term.fastype_of rhs; |
|
263 |
|
264 fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^ |
|
265 Pretty.string_of_term pp (Logic.mk_equals (Const (full_c, T), rhs))); |
|
266 val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables" |
|
267 val _ = null (Term.hidden_polymorphism rhs T) orelse err "Extra type variables"; |
262 in |
268 in |
263 consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) => |
269 consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) => |
264 let |
270 let |
265 val decls' = decls |
271 val decls' = decls |
266 |> extend_decls naming (c, (((T, Abbreviation rhs'), authentic), serial ())); |
272 |> extend_decls naming (c, (((T, Abbreviation rhs'), authentic), serial ())); |
267 val rev_abbrevs' = rev_abbrevs |
273 val rev_abbrevs' = rev_abbrevs |
268 |> fold (curry Symtab.update_list mode) (rev_abbrev (NameSpace.full naming c, T) rhs); |
274 |> fold (curry Symtab.update_list mode) (rev_abbrev (full_c, T) rhs); |
269 in (decls', constraints, rev_abbrevs', expand_abbrevs) end) |
275 in (decls', constraints, rev_abbrevs', expand_abbrevs) end) |
|
276 |> pair ((full_c, T), rhs) |
270 end; |
277 end; |
271 |
278 |
272 end; |
279 end; |
273 |
280 |
274 |
281 |