Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Pure/Syntax/type_ext.ML
changeset 37216 3165bc303f66
parent 36518 586af36cf3cc
child 39541 f1ae2493d93f
equal deleted inserted replaced
37215:91dfe7dccfdf 37216:3165bc303f66 
    25 sig
 
    25 sig
 
    26   include TYPE_EXT0
 
    26   include TYPE_EXT0
 
    27   val term_of_sort: sort -> term
 
    27   val term_of_sort: sort -> term
 
    28   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
 
    28   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
 
    29   val sortT: typ
 
    29   val sortT: typ
 
    30   val type_ext: SynExt.syn_ext
 
    30   val type_ext: Syn_Ext.syn_ext
 
    31 end;
 
    31 end;
 
    32 
    32 
    33 structure TypeExt: TYPE_EXT =
 
    33 structure Type_Ext: TYPE_EXT =
 
    34 struct
 
    34 struct
 
    35 
    35 
    36 (** input utils **)
 
    36 (** input utils **)
 
    37 
    37 
    38 (* sort_of_term *)
 
    38 (* sort_of_term *)
 
   240 
   240 
   241 val sortT = Type ("sort", []);
 
   241 val sortT = Type ("sort", []);
 
   242 val classesT = Type ("classes", []);
 
   242 val classesT = Type ("classes", []);
 
   243 val typesT = Type ("types", []);
 
   243 val typesT = Type ("types", []);
 
   244 
   244 
   245 local open Lexicon SynExt in
 
   245 local open Lexicon Syn_Ext in
 
   246 
   246 
   247 val type_ext = syn_ext' false (K false)
 
   247 val type_ext = syn_ext' false (K false)
 
   248   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
 
   248   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
 
   249    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
 
   249    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
 
   250    Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
 
   250    Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
 
   269    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
 
   269    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
 
   270    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
 
   270    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
 
   271    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
 
   271    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
 
   272    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
 
   272    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
 
   273   ["_type_prop"]
 
   273   ["_type_prop"]
 
   274   ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
 
   274   ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
 
   275   []
 
   275   []
 
   276   ([], []);
 
   276   ([], []);
 
   277 
   277 
   278 fun type_ast_trs {read_class, read_type} =
 
   278 fun type_ast_trs {read_class, read_type} =
 
   279  [("_class_name", class_name_tr o read_class),
 
   279  [("_class_name", class_name_tr o read_class),
wneuper/isa