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 Utilities for input and output of types. Also the concrete syntax of |
5 Utilities for input and output of types. Also the concrete syntax of |
6 types, which is used to bootstrap Pure. |
6 types, which is required to bootstrap Pure. |
7 *) |
7 *) |
8 |
8 |
9 signature TYPE_EXT0 = |
9 signature TYPE_EXT0 = |
10 sig |
10 sig |
|
11 val sort_of_term: term -> sort |
11 val raw_term_sorts: term -> (indexname * sort) list |
12 val raw_term_sorts: term -> (indexname * sort) list |
12 val typ_of_term: (indexname -> sort) -> term -> typ |
13 val typ_of_term: (indexname -> sort) -> term -> typ |
13 val term_of_typ: bool -> typ -> term |
14 val term_of_typ: bool -> typ -> term |
14 end; |
15 end; |
15 |
16 |
16 signature TYPE_EXT = |
17 signature TYPE_EXT = |
17 sig |
18 sig |
18 include TYPE_EXT0 |
19 include TYPE_EXT0 |
19 val term_of_sort: sort -> term |
20 val term_of_sort: sort -> term |
20 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
21 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast |
|
22 val sortT: typ |
21 val type_ext: SynExt.syn_ext |
23 val type_ext: SynExt.syn_ext |
22 end; |
24 end; |
23 |
25 |
24 structure TypeExt : TYPE_EXT = |
26 structure TypeExt : TYPE_EXT = |
25 struct |
27 struct |
26 |
28 |
27 |
29 |
28 (** input utils **) |
30 (** input utils **) |
29 |
31 |
30 (* raw_term_sorts *) |
32 (* sort_of_term *) |
31 |
33 |
32 fun raw_term_sorts tm = |
34 fun sort_of_term tm = |
33 let |
35 let |
34 fun classes (Const (c, _)) = [c] |
36 fun classes (Const (c, _)) = [c] |
35 | classes (Free (c, _)) = [c] |
37 | classes (Free (c, _)) = [c] |
36 | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs |
38 | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs |
37 | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs |
39 | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs |
38 | classes tm = raise TERM ("raw_term_sorts: bad encoding of classes", [tm]); |
40 | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]); |
39 |
41 |
40 fun sort (Const ("_topsort", _)) = [] |
42 fun sort (Const ("_topsort", _)) = [] |
41 | sort (Const (c, _)) = [c] |
43 | sort (Const (c, _)) = [c] |
42 | sort (Free (c, _)) = [c] |
44 | sort (Free (c, _)) = [c] |
43 | sort (Const ("_sort", _) $ cs) = classes cs |
45 | sort (Const ("_sort", _) $ cs) = classes cs |
44 | sort tm = raise TERM ("raw_term_sorts: bad encoding of sort", [tm]); |
46 | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]); |
|
47 in sort tm end; |
45 |
48 |
46 fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort cs) ins env |
49 |
47 | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort cs) ins env |
50 (* raw_term_sorts *) |
|
51 |
|
52 fun raw_term_sorts tm = |
|
53 let |
|
54 fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env |
|
55 | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env |
48 | add_env (Abs (_, _, t)) env = add_env t env |
56 | add_env (Abs (_, _, t)) env = add_env t env |
49 | add_env (t1 $ t2) env = add_env t1 (add_env t2 env) |
57 | add_env (t1 $ t2) env = add_env t1 (add_env t2 env) |
50 | add_env t env = env; |
58 | add_env t env = env; |
51 in |
59 in add_env tm [] end; |
52 add_env tm [] |
|
53 end; |
|
54 |
60 |
55 |
61 |
56 (* typ_of_term *) |
62 (* typ_of_term *) |
57 |
63 |
58 fun typ_of_term get_sort t = |
64 fun typ_of_term get_sort t = |