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
|
|
12 |
val decode_position: term -> Position.T option
|
|
13 |
val is_position: term -> bool
|
|
14 |
val strip_positions: term -> term
|
|
15 |
end;
|
|
16 |
|
|
17 |
structure Term_Position: TERM_POSITION =
|
|
18 |
struct
|
|
19 |
|
|
20 |
(* markup *)
|
|
21 |
|
|
22 |
val position_dummy = "<position>";
|
|
23 |
val position_text = XML.Text position_dummy;
|
|
24 |
|
|
25 |
fun pretty pos =
|
|
26 |
Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
|
|
27 |
|
|
28 |
fun encode pos =
|
|
29 |
YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
|
|
30 |
|
|
31 |
fun decode str =
|
|
32 |
(case YXML.parse_body str handle Fail msg => error msg of
|
|
33 |
[XML.Elem ((name, props), [arg])] =>
|
|
34 |
if name = Markup.positionN andalso arg = position_text
|
|
35 |
then SOME (Position.of_properties props)
|
|
36 |
else NONE
|
|
37 |
| _ => NONE);
|
|
38 |
|
|
39 |
|
|
40 |
(* positions within parse trees *)
|
|
41 |
|
|
42 |
fun decode_position (Free (x, _)) = decode x
|
|
43 |
| decode_position _ = NONE;
|
|
44 |
|
|
45 |
val is_position = is_some o decode_position;
|
|
46 |
|
|
47 |
fun strip_positions ((t as Const (c, _)) $ u $ v) =
|
|
48 |
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
|
|
49 |
then strip_positions u
|
|
50 |
else t $ strip_positions u $ strip_positions v
|
|
51 |
| strip_positions (t $ u) = strip_positions t $ strip_positions u
|
|
52 |
| strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
|
|
53 |
| strip_positions t = t;
|
|
54 |
|
|
55 |
end;
|