src/Pure/Syntax/type_ext.ML
changeset 42204 b3277168c1e7
parent 42170 a37a47aa985b
child 42223 098c86e53153
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -13,14 +13,10 @@
     1.4    val strip_positions: term -> term
     1.5    val strip_positions_ast: Ast.ast -> Ast.ast
     1.6    type term_context
     1.7 -  val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
     1.8 +  val decode_term: term_context -> Position.reports * term -> Position.reports * term
     1.9    val term_of_typ: bool -> typ -> term
    1.10    val no_brackets: unit -> bool
    1.11    val no_type_brackets: unit -> bool
    1.12 -  val type_ast_trs:
    1.13 -   {read_class: Proof.context -> string -> string,
    1.14 -    read_type: Proof.context -> string -> string} ->
    1.15 -    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    1.16  end;
    1.17  
    1.18  signature TYPE_EXT =
    1.19 @@ -140,16 +136,13 @@
    1.20    markup_free: string -> Markup.T list,
    1.21    markup_var: indexname -> Markup.T list};
    1.22  
    1.23 -fun decode_term (term_context: term_context) tm =
    1.24 +fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
    1.25    let
    1.26      val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
    1.27      val decodeT = typ_of_term (get_sort (term_sorts tm));
    1.28  
    1.29 -    val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
    1.30 -    fun report [] _ _ = ()
    1.31 -      | report ps markup x =
    1.32 -          let val ms = markup x
    1.33 -          in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
    1.34 +    val reports = Unsynchronized.ref reports0;
    1.35 +    fun report ps = Position.reports reports ps;
    1.36  
    1.37      fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
    1.38            (case decode_position typ of
    1.39 @@ -252,30 +245,14 @@
    1.40  
    1.41  (* parse ast translations *)
    1.42  
    1.43 -val class_ast = Ast.Constant o Lexicon.mark_class;
    1.44 -val type_ast = Ast.Constant o Lexicon.mark_type;
    1.45 -
    1.46 -fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
    1.47 -  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
    1.48 -
    1.49 -fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
    1.50 -      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
    1.51 -  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
    1.52 +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
    1.53 +  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
    1.54  
    1.55 -fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
    1.56 -  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
    1.57 -
    1.58 -fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
    1.59 -      Ast.Appl [type_ast (read_type c), ty]
    1.60 -  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
    1.61 +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
    1.62 +  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
    1.63  
    1.64 -fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
    1.65 -      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
    1.66 -  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
    1.67 -
    1.68 -fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
    1.69 -      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
    1.70 -  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
    1.71 +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
    1.72 +  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
    1.73  
    1.74  
    1.75  (* print ast translations *)
    1.76 @@ -296,32 +273,35 @@
    1.77  
    1.78  (* type_ext *)
    1.79  
    1.80 -val sortT = Type ("sort", []);
    1.81 -val classesT = Type ("classes", []);
    1.82 -val typesT = Type ("types", []);
    1.83 +fun typ c = Type (c, []);
    1.84 +
    1.85 +val class_nameT = typ "class_name";
    1.86 +val type_nameT = typ "type_name";
    1.87 +
    1.88 +val sortT = typ "sort";
    1.89 +val classesT = typ "classes";
    1.90 +val typesT = typ "types";
    1.91  
    1.92  local open Lexicon Syn_Ext in
    1.93  
    1.94  val type_ext = syn_ext' false (K false)
    1.95    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    1.96     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    1.97 -   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
    1.98 -   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
    1.99 +   Mfix ("_",           type_nameT --> typeT,          "", [], max_pri),
   1.100 +   Mfix ("_",           idT --> type_nameT,            "_type_name", [], max_pri),
   1.101 +   Mfix ("_",           longidT --> type_nameT,        "_type_name", [], max_pri),
   1.102     Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   1.103     Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   1.104     Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
   1.105 -   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
   1.106 -   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
   1.107 +   Mfix ("_",           class_nameT --> sortT,         "", [], max_pri),
   1.108 +   Mfix ("_",           idT --> class_nameT,           "_class_name", [], max_pri),
   1.109 +   Mfix ("_",           longidT --> class_nameT,       "_class_name", [], max_pri),
   1.110     Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   1.111     Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   1.112 -   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
   1.113 -   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
   1.114 -   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   1.115 -   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   1.116 -   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   1.117 -   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   1.118 -   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   1.119 -   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   1.120 +   Mfix ("_",           class_nameT --> classesT,      "", [], max_pri),
   1.121 +   Mfix ("_,_",         [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
   1.122 +   Mfix ("_ _",         [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
   1.123 +   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
   1.124     Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   1.125     Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   1.126     Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
   1.127 @@ -329,18 +309,12 @@
   1.128     Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   1.129     Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   1.130    ["_type_prop"]
   1.131 -  ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   1.132 +  (map Syn_Ext.mk_trfun
   1.133 +    [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
   1.134 +   [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   1.135    []
   1.136    ([], []);
   1.137  
   1.138 -fun type_ast_trs {read_class, read_type} =
   1.139 - [("_class_name", class_name_tr o read_class),
   1.140 -  ("_classes", classes_tr o read_class),
   1.141 -  ("_type_name", type_name_tr o read_type),
   1.142 -  ("_tapp", tapp_ast_tr o read_type),
   1.143 -  ("_tappl", tappl_ast_tr o read_type),
   1.144 -  ("_bracket", K bracket_ast_tr)];
   1.145 -
   1.146  end;
   1.147  
   1.148  end;