73 val syn_of: theory -> Syntax.syntax |
73 val syn_of: theory -> Syntax.syntax |
74 val tsig_of: theory -> Type.tsig |
74 val tsig_of: theory -> Type.tsig |
75 val classes_of: theory -> Sorts.algebra |
75 val classes_of: theory -> Sorts.algebra |
76 val all_classes: theory -> class list |
76 val all_classes: theory -> class list |
77 val super_classes: theory -> class -> class list |
77 val super_classes: theory -> class -> class list |
|
78 val minimize_sort: theory -> sort -> sort |
|
79 val complete_sort: theory -> sort -> sort |
78 val defaultS: theory -> sort |
80 val defaultS: theory -> sort |
79 val subsort: theory -> sort * sort -> bool |
81 val subsort: theory -> sort * sort -> bool |
80 val of_sort: theory -> typ * sort -> bool |
82 val of_sort: theory -> typ * sort -> bool |
81 val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list |
83 val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list |
82 val universal_witness: theory -> (typ * sort) option |
84 val universal_witness: theory -> (typ * sort) option |
83 val all_sorts_nonempty: theory -> bool |
85 val all_sorts_nonempty: theory -> bool |
|
86 val is_logtype: theory -> string -> bool |
84 val typ_instance: theory -> typ * typ -> bool |
87 val typ_instance: theory -> typ * typ -> bool |
85 val typ_equiv: theory -> typ * typ -> bool |
88 val typ_equiv: theory -> typ * typ -> bool |
86 val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv |
89 val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv |
87 val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int |
90 val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int |
88 val is_logtype: theory -> string -> bool |
|
89 val consts_of: theory -> Consts.T |
91 val consts_of: theory -> Consts.T |
90 val const_constraint: theory -> string -> typ option |
92 val const_constraint: theory -> string -> typ option |
91 val the_const_constraint: theory -> string -> typ |
93 val the_const_constraint: theory -> string -> typ |
92 val const_type: theory -> string -> typ option |
94 val const_type: theory -> string -> typ option |
93 val the_const_type: theory -> string -> typ |
95 val the_const_type: theory -> string -> typ |
241 |
243 |
242 |
244 |
243 (* type signature *) |
245 (* type signature *) |
244 |
246 |
245 val tsig_of = #tsig o rep_sg; |
247 val tsig_of = #tsig o rep_sg; |
|
248 |
246 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; |
249 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; |
247 val all_classes = Sorts.all_classes o classes_of; |
250 val all_classes = Sorts.all_classes o classes_of; |
248 val minimal_classes = Sorts.minimal_classes o classes_of; |
251 val minimal_classes = Sorts.minimal_classes o classes_of; |
249 val super_classes = Sorts.super_classes o classes_of; |
252 val super_classes = Sorts.super_classes o classes_of; |
|
253 val minimize_sort = Sorts.minimize_sort o classes_of; |
|
254 val complete_sort = Sorts.complete_sort o classes_of; |
|
255 |
250 val defaultS = Type.defaultS o tsig_of; |
256 val defaultS = Type.defaultS o tsig_of; |
251 val subsort = Type.subsort o tsig_of; |
257 val subsort = Type.subsort o tsig_of; |
252 val of_sort = Type.of_sort o tsig_of; |
258 val of_sort = Type.of_sort o tsig_of; |
253 val witness_sorts = Type.witness_sorts o tsig_of; |
259 val witness_sorts = Type.witness_sorts o tsig_of; |
254 val universal_witness = Type.universal_witness o tsig_of; |
260 val universal_witness = Type.universal_witness o tsig_of; |
255 val all_sorts_nonempty = is_some o universal_witness; |
261 val all_sorts_nonempty = is_some o universal_witness; |
|
262 val is_logtype = member (op =) o Type.logical_types o tsig_of; |
|
263 |
256 val typ_instance = Type.typ_instance o tsig_of; |
264 val typ_instance = Type.typ_instance o tsig_of; |
257 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); |
265 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); |
258 val typ_match = Type.typ_match o tsig_of; |
266 val typ_match = Type.typ_match o tsig_of; |
259 val typ_unify = Type.unify o tsig_of; |
267 val typ_unify = Type.unify o tsig_of; |
260 val is_logtype = member (op =) o Type.logical_types o tsig_of; |
|
261 |
268 |
262 |
269 |
263 (* polymorphic constants *) |
270 (* polymorphic constants *) |
264 |
271 |
265 val consts_of = #consts o rep_sg; |
272 val consts_of = #consts o rep_sg; |