author | wenzelm |
Mon, 02 Nov 2015 16:03:03 +0100 | |
changeset 61544 | 19d84de5f534 |
parent 52689 | 6419ada0664a |
permissions | -rw-r--r-- |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Syntax/type_annotation.ML |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
3 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
4 |
Type annotations within syntax trees, notably for pretty printing. |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
5 |
*) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
6 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
7 |
signature TYPE_ANNOTATION = |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
8 |
sig |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
9 |
val ignore_type: typ -> typ |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
10 |
val ignore_free_types: term -> term |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
11 |
val is_ignored: typ -> bool |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
12 |
val is_omitted: typ -> bool |
52464
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
13 |
val clean: typ -> typ |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
14 |
val smash: typ -> typ |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
15 |
val fastype_of: typ list -> term -> typ |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
16 |
end; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
17 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
18 |
structure Type_Annotation: TYPE_ANNOTATION = |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
19 |
struct |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
20 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
21 |
(* annotations *) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
22 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
23 |
fun ignore_type T = Type ("_ignore_type", [T]); |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
24 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
25 |
val ignore_free_types = Term.map_aterms (fn Free (x, T) => Free (x, ignore_type T) | a => a); |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
26 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
27 |
fun is_ignored (Type ("_ignore_type", _)) = true |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
28 |
| is_ignored _ = false; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
29 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
30 |
fun is_omitted T = is_ignored T orelse T = dummyT; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
31 |
|
52464
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
32 |
fun clean (Type ("_ignore_type", [T])) = clean T |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
33 |
| clean (Type (a, Ts)) = Type (a, map clean Ts) |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
34 |
| clean T = T; |
36497ee02ed8
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
wenzelm
parents:
52219
diff
changeset
|
35 |
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
36 |
fun smash (Type ("_ignore_type", [_])) = dummyT |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
37 |
| smash (Type (a, Ts)) = Type (a, map smash Ts) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
38 |
| smash T = T; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
39 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
40 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
41 |
(* determine type -- propagate annotations *) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
42 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
43 |
local |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
44 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
45 |
fun dest_fun ignored (Type ("fun", [_, T])) = SOME ((ignored ? ignore_type) T) |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
46 |
| dest_fun _ (Type ("_ignore_type", [T])) = dest_fun true T |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
47 |
| dest_fun _ _ = NONE; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
48 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
49 |
in |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
50 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
51 |
fun fastype_of Ts (t $ u) = |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
52 |
(case dest_fun false (fastype_of Ts t) of |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
53 |
SOME T => T |
52689 | 54 |
| NONE => raise TERM ("fastype_of: expected function type", [t $ u])) |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
55 |
| fastype_of _ (Const (_, T)) = T |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
56 |
| fastype_of _ (Free (_, T)) = T |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
57 |
| fastype_of _ (Var (_, T)) = T |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
58 |
| fastype_of Ts (Bound i) = |
52689 | 59 |
(nth Ts i handle General.Subscript => raise TERM ("fastype_of: Bound", [Bound i])) |
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
60 |
| fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
61 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
62 |
end; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
63 |
|
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
64 |
end; |
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
diff
changeset
|
65 |