1 (* Title: Pure/Syntax/type_ext.ML |
1 (* Title: Pure/Syntax/type_ext.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
4 |
5 The concrete syntax of types (used to bootstrap Pure). |
5 Utilities for input and output of types. Also the concrete syntax of |
|
6 types, which is used to bootstrap Pure. |
6 *) |
7 *) |
7 |
8 |
8 signature TYPE_EXT0 = |
9 signature TYPE_EXT0 = |
9 sig |
10 sig |
10 val raw_term_sorts: term -> (indexname * sort) list |
11 val raw_term_sorts: (sort * sort -> bool) -> term -> (indexname * sort) list |
11 val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ |
12 val typ_of_term: (indexname -> sort) -> term -> typ |
12 end; |
13 end; |
13 |
14 |
14 signature TYPE_EXT = |
15 signature TYPE_EXT = |
15 sig |
16 sig |
16 include TYPE_EXT0 |
17 include TYPE_EXT0 |
|
18 val term_of_sort: sort -> term |
17 val term_of_typ: bool -> typ -> term |
19 val term_of_typ: bool -> typ -> term |
18 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
20 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
19 val type_ext: SynExt.syn_ext |
21 val type_ext: SynExt.syn_ext |
20 end; |
22 end; |
21 |
23 |
22 structure TypeExt : TYPE_EXT = |
24 structure TypeExt : TYPE_EXT = |
23 struct |
25 struct |
|
26 |
24 open Lexicon SynExt Ast; |
27 open Lexicon SynExt Ast; |
25 |
28 |
26 (** raw_term_sorts **) |
|
27 |
29 |
28 fun raw_term_sorts tm = |
30 (** input utils **) |
|
31 |
|
32 (* raw_term_sorts *) |
|
33 |
|
34 fun raw_term_sorts eq_sort tm = |
29 let |
35 let |
30 fun show_var (xi as (x, i)) = if i < 0 then x else string_of_vname xi; |
|
31 |
|
32 fun classes (Const (c, _)) = [c] |
36 fun classes (Const (c, _)) = [c] |
33 | classes (Free (c, _)) = [c] |
37 | classes (Free (c, _)) = [c] |
34 | classes (Const ("_classes", _) $ Const (c, _) $ cls) = c :: classes cls |
38 | classes (Const ("_classes", _) $ Const (c, _) $ cls) = c :: classes cls |
35 | classes (Const ("_classes", _) $ Free (c, _) $ cls) = c :: classes cls |
39 | classes (Const ("_classes", _) $ Free (c, _) $ cls) = c :: classes cls |
36 | classes tm = raise_term "raw_term_sorts: bad encoding of classes" [tm]; |
40 | classes tm = raise_term "raw_term_sorts: bad encoding of classes" [tm]; |
37 |
41 |
38 fun sort (Const ("_emptysort", _)) = [] |
42 fun sort (Const ("_topsort", _)) = [] |
39 | sort (Const (s, _)) = [s] |
43 | sort (Const (c, _)) = [c] |
40 | sort (Free (s, _)) = [s] |
44 | sort (Free (c, _)) = [c] |
41 | sort (Const ("_sort", _) $ cls) = classes cls |
45 | sort (Const ("_sort", _) $ cls) = classes cls |
42 | sort tm = raise_term "raw_term_sorts: bad encoding of sort" [tm]; |
46 | sort tm = raise_term "raw_term_sorts: bad encoding of sort" [tm]; |
43 |
47 |
44 fun env_of (Const ("_ofsort", _) $ Free (x, _) $ srt) = [((x, ~1), sort srt)] |
48 fun eq ((xi, S), (xi', S')) = |
45 | env_of (Const ("_ofsort", _) $ Var (xi, _) $ srt) = [(xi, sort srt)] |
49 xi = xi' andalso eq_sort (S, S'); |
|
50 |
|
51 fun env_of (Const ("_ofsort", _) $ Free (x, _) $ cls) = [((x, ~1), sort cls)] |
|
52 | env_of (Const ("_ofsort", _) $ Var (xi, _) $ cls) = [(xi, sort cls)] |
46 | env_of (Abs (_, _, t)) = env_of t |
53 | env_of (Abs (_, _, t)) = env_of t |
47 | env_of (t1 $ t2) = env_of t1 @ env_of t2 |
54 | env_of (t1 $ t2) = gen_union eq (env_of t1, env_of t2) |
48 | env_of t = []; |
55 | env_of t = []; |
49 |
56 |
50 val env = distinct (env_of tm); |
57 val env = env_of tm; |
51 in |
58 in |
52 (case gen_duplicates |
59 (case gen_duplicates eq_fst env of |
53 (fn ((n,s),(m,t)) => n=m andalso not(eq_set_string(s,t))) env of |
|
54 [] => env |
60 [] => env |
55 | dups => error ("Inconsistent sort constraints for type variable(s) " ^ |
61 | dups => error ("Inconsistent sort constraints for type variable(s) " ^ |
56 commas (map (quote o show_var o #1) dups))) |
62 commas (map (quote o string_of_vname' o #1) dups))) |
57 end; |
63 end; |
58 |
64 |
59 |
65 |
|
66 (* typ_of_term *) |
60 |
67 |
61 (** typ_of_term **) |
68 fun typ_of_term get_sort t = |
62 |
|
63 fun typ_of_term sort_env def_sort t = |
|
64 let |
69 let |
65 fun get_sort xi = |
|
66 (case assoc (sort_env, xi) of |
|
67 None => def_sort xi |
|
68 | Some s => s); |
|
69 |
|
70 fun typ_of (Free (x, _)) = |
70 fun typ_of (Free (x, _)) = |
71 if is_tid x then TFree (x, get_sort (x, ~1)) |
71 if is_tid x then TFree (x, get_sort (x, ~1)) |
72 else Type (x, []) |
72 else Type (x, []) |
73 | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) |
73 | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) |
74 | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = |
74 | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = |
90 typ_of t |
90 typ_of t |
91 end; |
91 end; |
92 |
92 |
93 |
93 |
94 |
94 |
95 (** term_of_typ **) |
95 (** output utils **) |
|
96 |
|
97 (* term_of_sort *) (* FIXME mark whole sort vs. ind. classes !? *) |
|
98 |
|
99 fun term_of_sort S = |
|
100 let |
|
101 fun class c = free c; (* FIXME mark *) |
|
102 |
|
103 fun classes [] = sys_error "term_of_sort" |
|
104 | classes [c] = class c |
|
105 | classes (c :: cs) = const "_classes" $ class c $ classes cs; |
|
106 in |
|
107 (case S of |
|
108 [] => const "_topsort" |
|
109 | [c] => class c |
|
110 | cs => const "_sort" $ classes cs) |
|
111 end; |
|
112 |
|
113 |
|
114 (* term_of_typ *) |
96 |
115 |
97 fun term_of_typ show_sorts ty = |
116 fun term_of_typ show_sorts ty = |
98 let |
117 let |
99 fun classes [] = raise Match |
118 fun of_sort t S = |
100 | classes [c] = free c |
119 if show_sorts then const "_ofsort" $ t $ term_of_sort S |
101 | classes (c :: cs) = const "_classes" $ free c $ classes cs; |
120 else t; |
102 |
|
103 fun sort [] = const "_emptysort" |
|
104 | sort [s] = free s |
|
105 | sort ss = const "_sort" $ classes ss; |
|
106 |
|
107 fun of_sort t ss = |
|
108 if show_sorts then const "_ofsort" $ t $ sort ss else t; |
|
109 |
121 |
110 fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys) |
122 fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys) |
111 | term_of (TFree (x, ss)) = of_sort (free x) ss |
123 | term_of (TFree (x, S)) = of_sort (free x) S (* FIXME mark? *) |
112 | term_of (TVar (xi, ss)) = of_sort (var xi) ss; |
124 | term_of (TVar (xi, S)) = of_sort (var xi) S; (* FIXME mark? *) |
113 in |
125 in |
114 term_of ty |
126 term_of ty |
115 end; |
127 end; |
116 |
128 |
117 |
129 |
157 Mfix ("_", tvarT --> typeT, "", [], max_pri), |
169 Mfix ("_", tvarT --> typeT, "", [], max_pri), |
158 Mfix ("_", idT --> typeT, "", [], max_pri), |
170 Mfix ("_", idT --> typeT, "", [], max_pri), |
159 Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
171 Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
160 Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
172 Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
161 Mfix ("_", idT --> sortT, "", [], max_pri), |
173 Mfix ("_", idT --> sortT, "", [], max_pri), |
162 Mfix ("{}", sortT, "_emptysort", [], max_pri), |
174 Mfix ("{}", sortT, "_topsort", [], max_pri), |
163 Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), |
175 Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), |
164 Mfix ("_", idT --> classesT, "", [], max_pri), |
176 Mfix ("_", idT --> classesT, "", [], max_pri), |
165 Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri), |
177 Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri), |
166 Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), |
178 Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), |
167 Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri), |
179 Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri), |