author | wenzelm |
Sun, 25 Nov 2012 19:49:24 +0100 | |
changeset 50201 | c26369c9eda6 |
parent 49685 | 4341e4d86872 |
child 52175 | 626a757d3c2d |
permissions | -rw-r--r-- |
42264 | 1 |
(* Title: Pure/Syntax/term_position.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Encoded position within term syntax trees. |
|
5 |
*) |
|
6 |
||
7 |
signature TERM_POSITION = |
|
8 |
sig |
|
9 |
val pretty: Position.T -> Pretty.T |
|
10 |
val encode: Position.T -> string |
|
11 |
val decode: string -> Position.T option |
|
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
12 |
val decode_position: term -> (Position.T * typ) option |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
13 |
val decode_positionT: typ -> Position.T option |
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
14 |
val decode_positionS: sort -> Position.T list * sort |
42264 | 15 |
val is_position: term -> bool |
45448
018f8959c7a6
more efficient prepare_sorts -- bypass encoded positions;
wenzelm
parents:
45445
diff
changeset
|
16 |
val is_positionT: typ -> bool |
42264 | 17 |
val strip_positions: term -> term |
18 |
end; |
|
19 |
||
20 |
structure Term_Position: TERM_POSITION = |
|
21 |
struct |
|
22 |
||
23 |
(* markup *) |
|
24 |
||
25 |
val position_dummy = "<position>"; |
|
26 |
val position_text = XML.Text position_dummy; |
|
27 |
||
28 |
fun pretty pos = |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49685
diff
changeset
|
29 |
Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; |
42264 | 30 |
|
31 |
fun encode pos = |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49685
diff
changeset
|
32 |
YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); |
42264 | 33 |
|
34 |
fun decode str = |
|
35 |
(case YXML.parse_body str handle Fail msg => error msg of |
|
36 |
[XML.Elem ((name, props), [arg])] => |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49685
diff
changeset
|
37 |
if name = Markup.positionN andalso arg = position_text |
42264 | 38 |
then SOME (Position.of_properties props) |
39 |
else NONE |
|
40 |
| _ => NONE); |
|
41 |
||
42 |
||
43 |
(* positions within parse trees *) |
|
44 |
||
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
45 |
fun decode_position (Free (x, _)) = |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
46 |
(case decode x of |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
47 |
SOME pos => SOME (pos, TFree (x, dummyS)) |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
48 |
| NONE => NONE) |
42264 | 49 |
| decode_position _ = NONE; |
50 |
||
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
51 |
fun decode_positionT (TFree (x, _)) = decode x |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
52 |
| decode_positionT _ = NONE; |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
42264
diff
changeset
|
53 |
|
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
54 |
fun decode_positionS cs = |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
55 |
let val (ps, sort) = List.partition (is_some o decode) cs |
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset
|
56 |
in (map (the o decode) ps, sort) end; |
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
45666
diff
changeset
|
57 |
|
42264 | 58 |
val is_position = is_some o decode_position; |
45448
018f8959c7a6
more efficient prepare_sorts -- bypass encoded positions;
wenzelm
parents:
45445
diff
changeset
|
59 |
val is_positionT = is_some o decode_positionT; |
42264 | 60 |
|
61 |
fun strip_positions ((t as Const (c, _)) $ u $ v) = |
|
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
45666
diff
changeset
|
62 |
if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v |
42264 | 63 |
then strip_positions u |
64 |
else t $ strip_positions u $ strip_positions v |
|
65 |
| strip_positions (t $ u) = strip_positions t $ strip_positions u |
|
66 |
| strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) |
|
67 |
| strip_positions t = t; |
|
68 |
||
69 |
end; |