author | wenzelm |
Wed, 06 Apr 2011 17:00:40 +0200 | |
changeset 42254 | f427c9890c46 |
parent 42245 | 29e3967550d5 |
child 42262 | 4821a2a91548 |
permissions | -rw-r--r-- |
18 | 1 |
(* Title: Pure/Syntax/type_ext.ML |
0 | 2 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
3 |
||
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
4 |
Utilities for input and output of types. The concrete syntax of types. |
0 | 5 |
*) |
6 |
||
7 |
signature TYPE_EXT0 = |
|
2584 | 8 |
sig |
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42223
diff
changeset
|
9 |
val decode_position_term: term -> Position.T option |
42053
006095137a81
update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents:
42052
diff
changeset
|
10 |
val is_position: term -> bool |
42050
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
11 |
val strip_positions: term -> term |
42052
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
12 |
val strip_positions_ast: Ast.ast -> Ast.ast |
10572 | 13 |
val no_brackets: unit -> bool |
16614 | 14 |
val no_type_brackets: unit -> bool |
2584 | 15 |
end; |
0 | 16 |
|
17 |
signature TYPE_EXT = |
|
2584 | 18 |
sig |
0 | 19 |
include TYPE_EXT0 |
1511 | 20 |
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36502
diff
changeset
|
21 |
val type_ext: Syn_Ext.syn_ext |
2584 | 22 |
end; |
0 | 23 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36502
diff
changeset
|
24 |
structure Type_Ext: TYPE_EXT = |
0 | 25 |
struct |
2584 | 26 |
|
27 |
(** input utils **) |
|
0 | 28 |
|
42050
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
29 |
(* positions *) |
22704 | 30 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42223
diff
changeset
|
31 |
fun decode_position_term (Free (x, _)) = Lexicon.decode_position x |
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42223
diff
changeset
|
32 |
| decode_position_term _ = NONE; |
42131
1d9710ff7209
decode_term/disambig: report resolved term variables for the unique (!) result;
wenzelm
parents:
42053
diff
changeset
|
33 |
|
42242
39261908e12f
moved decode/parse operations to standard_syntax.ML;
wenzelm
parents:
42223
diff
changeset
|
34 |
val is_position = is_some o decode_position_term; |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
39288
diff
changeset
|
35 |
|
42050
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
36 |
fun strip_positions ((t as Const (c, _)) $ u $ v) = |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
37 |
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
38 |
then strip_positions u |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
39 |
else t $ strip_positions u $ strip_positions v |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
40 |
| strip_positions (t $ u) = strip_positions t $ strip_positions u |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
41 |
| strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
42 |
| strip_positions t = t; |
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
43 |
|
42052
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
44 |
fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) = |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
45 |
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x) |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
46 |
then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts) |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
47 |
else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts)) |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
48 |
| strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts) |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
49 |
| strip_positions_ast ast = ast; |
34f1d2d81284
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm
parents:
42050
diff
changeset
|
50 |
|
42050
5a505dfec04e
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
wenzelm
parents:
42048
diff
changeset
|
51 |
|
0 | 52 |
|
53 |
(** the type syntax **) |
|
54 |
||
10572 | 55 |
(* print mode *) |
56 |
||
57 |
val bracketsN = "brackets"; |
|
58 |
val no_bracketsN = "no_brackets"; |
|
59 |
||
60 |
fun no_brackets () = |
|
24613 | 61 |
find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) |
62 |
(print_mode_value ()) = SOME no_bracketsN; |
|
11312 | 63 |
|
64 |
val type_bracketsN = "type_brackets"; |
|
65 |
val no_type_bracketsN = "no_type_brackets"; |
|
66 |
||
67 |
fun no_type_brackets () = |
|
24613 | 68 |
find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) |
69 |
(print_mode_value ()) <> SOME type_bracketsN; |
|
10572 | 70 |
|
71 |
||
18 | 72 |
(* parse ast translations *) |
0 | 73 |
|
42204 | 74 |
fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] |
75 |
| tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); |
|
347
cd41a57221d0
changed translation of type applications according to new grammar;
wenzelm
parents:
330
diff
changeset
|
76 |
|
42204 | 77 |
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) |
78 |
| tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
79 |
|
42204 | 80 |
fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) |
81 |
| bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); |
|
0 | 82 |
|
83 |
||
18 | 84 |
(* print ast translations *) |
0 | 85 |
|
5690 | 86 |
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) |
87 |
| tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] |
|
347
cd41a57221d0
changed translation of type applications according to new grammar;
wenzelm
parents:
330
diff
changeset
|
88 |
| tappl_ast_tr' (f, ty :: tys) = |
5690 | 89 |
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; |
0 | 90 |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
91 |
fun fun_ast_tr' (*"\\<^type>fun"*) asts = |
16614 | 92 |
if no_brackets () orelse no_type_brackets () then raise Match |
10572 | 93 |
else |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
94 |
(case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of |
10572 | 95 |
(dom as _ :: _ :: _, cod) |
96 |
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] |
|
97 |
| _ => raise Match); |
|
0 | 98 |
|
99 |
||
100 |
(* type_ext *) |
|
101 |
||
42204 | 102 |
fun typ c = Type (c, []); |
103 |
||
104 |
val class_nameT = typ "class_name"; |
|
105 |
val type_nameT = typ "type_name"; |
|
106 |
||
107 |
val sortT = typ "sort"; |
|
108 |
val classesT = typ "classes"; |
|
109 |
val typesT = typ "types"; |
|
0 | 110 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36502
diff
changeset
|
111 |
local open Lexicon Syn_Ext in |
5690 | 112 |
|
35668 | 113 |
val type_ext = syn_ext' false (K false) |
347
cd41a57221d0
changed translation of type applications according to new grammar;
wenzelm
parents:
330
diff
changeset
|
114 |
[Mfix ("_", tidT --> typeT, "", [], max_pri), |
239 | 115 |
Mfix ("_", tvarT --> typeT, "", [], max_pri), |
42204 | 116 |
Mfix ("_", type_nameT --> typeT, "", [], max_pri), |
117 |
Mfix ("_", idT --> type_nameT, "_type_name", [], max_pri), |
|
118 |
Mfix ("_", longidT --> type_nameT, "_type_name", [], max_pri), |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
258
diff
changeset
|
119 |
Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
239 | 120 |
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
14838 | 121 |
Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri), |
42204 | 122 |
Mfix ("_", class_nameT --> sortT, "", [], max_pri), |
123 |
Mfix ("_", idT --> class_nameT, "_class_name", [], max_pri), |
|
124 |
Mfix ("_", longidT --> class_nameT, "_class_name", [], max_pri), |
|
2584 | 125 |
Mfix ("{}", sortT, "_topsort", [], max_pri), |
239 | 126 |
Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), |
42204 | 127 |
Mfix ("_", class_nameT --> classesT, "", [], max_pri), |
128 |
Mfix ("_,_", [class_nameT, classesT] ---> classesT, "_classes", [], max_pri), |
|
129 |
Mfix ("_ _", [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri), |
|
130 |
Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri), |
|
239 | 131 |
Mfix ("_", typeT --> typesT, "", [], max_pri), |
132 |
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
133 |
Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0), |
624 | 134 |
Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0), |
2678 | 135 |
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri), |
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35262
diff
changeset
|
136 |
Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)] |
35433
73cc288b4f83
"_type_prop" is syntax const -- recovered printing of OFCLASS;
wenzelm
parents:
35429
diff
changeset
|
137 |
["_type_prop"] |
42204 | 138 |
(map Syn_Ext.mk_trfun |
139 |
[("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)], |
|
140 |
[], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')]) |
|
26708
fc2e7d2f763d
moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
wenzelm
parents:
26039
diff
changeset
|
141 |
[] |
239 | 142 |
([], []); |
0 | 143 |
|
144 |
end; |
|
5690 | 145 |
|
146 |
end; |