src/Pure/Syntax/term_position.ML
author wenzelm
Mon Oct 01 16:37:22 2012 +0200 (2012-10-01)
changeset 49674 dbadb4d03cbc
parent 45666 d83797ef0d2d
child 49685 4341e4d86872
permissions -rw-r--r--
report sort assignment of visible type variables;
wenzelm@42264
     1
(*  Title:      Pure/Syntax/term_position.ML
wenzelm@42264
     2
    Author:     Makarius
wenzelm@42264
     3
wenzelm@42264
     4
Encoded position within term syntax trees.
wenzelm@42264
     5
*)
wenzelm@42264
     6
wenzelm@42264
     7
signature TERM_POSITION =
wenzelm@42264
     8
sig
wenzelm@42264
     9
  val pretty: Position.T -> Pretty.T
wenzelm@42264
    10
  val encode: Position.T -> string
wenzelm@42264
    11
  val decode: string -> Position.T option
wenzelm@45445
    12
  val decode_position: term -> (Position.T * typ) option
wenzelm@45445
    13
  val decode_positionT: typ -> Position.T option
wenzelm@49674
    14
  val decode_positionS: sort -> Position.T option
wenzelm@42264
    15
  val is_position: term -> bool
wenzelm@45448
    16
  val is_positionT: typ -> bool
wenzelm@49674
    17
  val is_positionS: sort -> bool
wenzelm@42264
    18
  val strip_positions: term -> term
wenzelm@42264
    19
end;
wenzelm@42264
    20
wenzelm@42264
    21
structure Term_Position: TERM_POSITION =
wenzelm@42264
    22
struct
wenzelm@42264
    23
wenzelm@42264
    24
(* markup *)
wenzelm@42264
    25
wenzelm@42264
    26
val position_dummy = "<position>";
wenzelm@42264
    27
val position_text = XML.Text position_dummy;
wenzelm@42264
    28
wenzelm@42264
    29
fun pretty pos =
wenzelm@45666
    30
  Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy];
wenzelm@42264
    31
wenzelm@42264
    32
fun encode pos =
wenzelm@45666
    33
  YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text]));
wenzelm@42264
    34
wenzelm@42264
    35
fun decode str =
wenzelm@42264
    36
  (case YXML.parse_body str handle Fail msg => error msg of
wenzelm@42264
    37
    [XML.Elem ((name, props), [arg])] =>
wenzelm@45666
    38
      if name = Isabelle_Markup.positionN andalso arg = position_text
wenzelm@42264
    39
      then SOME (Position.of_properties props)
wenzelm@42264
    40
      else NONE
wenzelm@42264
    41
  | _ => NONE);
wenzelm@42264
    42
wenzelm@42264
    43
wenzelm@42264
    44
(* positions within parse trees *)
wenzelm@42264
    45
wenzelm@45445
    46
fun decode_position (Free (x, _)) =
wenzelm@45445
    47
      (case decode x of
wenzelm@45445
    48
        SOME pos => SOME (pos, TFree (x, dummyS))
wenzelm@45445
    49
      | NONE => NONE)
wenzelm@42264
    50
  | decode_position _ = NONE;
wenzelm@42264
    51
wenzelm@45445
    52
fun decode_positionT (TFree (x, _)) = decode x
wenzelm@45445
    53
  | decode_positionT _ = NONE;
wenzelm@45445
    54
wenzelm@49674
    55
fun decode_positionS [x] = decode x
wenzelm@49674
    56
  | decode_positionS _ = NONE;
wenzelm@49674
    57
wenzelm@42264
    58
val is_position = is_some o decode_position;
wenzelm@45448
    59
val is_positionT = is_some o decode_positionT;
wenzelm@49674
    60
val is_positionS = is_some o decode_positionS;
wenzelm@42264
    61
wenzelm@42264
    62
fun strip_positions ((t as Const (c, _)) $ u $ v) =
wenzelm@49674
    63
      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
wenzelm@42264
    64
      then strip_positions u
wenzelm@42264
    65
      else t $ strip_positions u $ strip_positions v
wenzelm@42264
    66
  | strip_positions (t $ u) = strip_positions t $ strip_positions u
wenzelm@42264
    67
  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
wenzelm@42264
    68
  | strip_positions t = t;
wenzelm@42264
    69
wenzelm@42264
    70
end;