Quelle term_position.ML Sprache: SML

(*  Title:      Pure/Syntax/term_position.ML
    Author:     Makarius

Reported positions within term syntax trees (non-empty list).
*)

signature TERM_POSITION =
sig
  type T = {syntax: bool, pos: Position.T}
  val syntax: Position.T -> T
  val no_syntax: Position.T -> T
  val store_reports: Position.report_text list Unsynchronized.ref ->
    T list -> ('a -> Markup.T list) -> 'a -> unit
  val pretty: Position.T list -> Pretty.T
  val encode: T list -> string
  val encode_syntax: Position.T list -> string
  val encode_no_syntax: Position.T list -> string
  val detect: string -> bool
  val decode: string -> T list
  val detect_position: term -> bool
  val decode_position: term -> (T list * typ) option
  val decode_position1: term -> T option
  val detect_positionT: typ -> bool
  val decode_positionT: typ -> T list
  val decode_positionS: sort -> T list * sort
  val markers: string list
  val strip_positions: term -> term
end;

structure Term_Position: TERM_POSITION =
struct

(* type T *)

type T = {syntax: bool, pos: Position.T};

fun syntax pos : T = {syntax = true, pos = pos};
fun no_syntax pos : T = {syntax = false, pos = pos};

fun store_reports _ [] _ _ = ()
  | store_reports (r: Position.report_text list Unsynchronized.ref) ps markup x =
      let
        val ms = markup x;
        fun store {syntax, pos} =
          fold (fn m => cons ((pos, Markup.syntax_properties syntax m), "")) ms;
      in Unsynchronized.change r (fold store ps) end;

(* markup *)

val position_dummy = "";
val position_text = XML.Text position_dummy;

fun pretty ps = Pretty.marks_str (map Position.markup ps, position_dummy);

fun encode_pos {syntax, pos} =
  XML.Elem (Position.markup pos |> Markup.syntax_properties syntax, [position_text]);

fun decode_pos (XML.Elem ((name, props), [arg])) =
      if name = Markup.positionN andalso arg = position_text
      then SOME {syntax = Markup.has_syntax props, pos = Position.of_properties props}
      else NONE
  | decode_pos _ = NONE;

(* encode *)

val encode_none = YXML.string_of (encode_pos (no_syntax Position.none));

fun encode ps =
  (case filter (Position.is_reported o #pos) ps of
    [] => encode_none
  | ps' => YXML.string_of_body (map encode_pos ps'));

val encode_syntax = encode o map syntax;
val encode_no_syntax = encode o map no_syntax;

val encode_prefix = YXML.XY ^ Markup.positionN;

(* decode *)

val detect = String.isPrefix encode_prefix;

fun decode str =
  if str = encode_none then [no_syntax Position.none]
  else if detect str then
    let
      val xml = YXML.parse_body str handle Fail msg => error msg;
      val ps = map decode_pos xml;
    in
      if not (null ps) andalso forall is_some ps then map the ps
      else if forall is_none ps then []
      else error ("Bad encoded positions: " ^ quote str)
    end
  else [];

(* positions within parse trees *)

fun detect_position (Free (x, _)) = detect x
  | detect_position _ = false;

fun decode_position (Free (x, _)) =
      (case decode x of
        [] => NONE
      | ps => SOME (ps, TFree (x, dummyS)))
  | decode_position _ = NONE;

fun decode_position1 (Free (x, _)) =
      (case decode x of
        [] => NONE
      | pos :: _ => SOME pos)
  | decode_position1 _ = NONE;

fun detect_positionT (TFree (x, _)) = detect x
  | detect_positionT _ = false;

fun decode_positionT (TFree (x, _)) = decode x
  | decode_positionT _ = [];

fun decode_positionS cs =
  let val (ps, sort) = List.partition detect cs
  in (maps decode ps, sort) end;

(* strip_positions *)

val markers = ["_constrain", "_constrainAbs", "_ofsort"];

fun strip_positions ((t as Const (c, _)) $ u $ v) =
      if member (op =) markers c andalso detect_position v
      then strip_positions u
      else t $ strip_positions u $ strip_positions v
  | strip_positions (t $ u) = strip_positions t $ strip_positions u
  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
  | strip_positions t = t;

end;

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.