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