src/Pure/Thy/thy_syntax.ML
author wenzelm
Mon Nov 02 20:50:48 2009 +0100 (2009-11-02)
changeset 33388 d64545e6cba5
parent 30573 49899f26fbd1
child 36950 75b8f26f2f07
permissions -rw-r--r--
modernized structure Proof_Syntax;
     1 (*  Title:      Pure/Thy/thy_syntax.ML
     2     Author:     Makarius
     3 
     4 Superficial theory syntax: tokens and spans.
     5 *)
     6 
     7 signature THY_SYNTAX =
     8 sig
     9   val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
    10     (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
    11       Source.source) Source.source) Source.source) Source.source
    12   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
    13   val present_token: OuterLex.token -> output
    14   val report_token: OuterLex.token -> unit
    15   datatype span_kind = Command of string | Ignored | Malformed
    16   type span
    17   val span_kind: span -> span_kind
    18   val span_content: span -> OuterLex.token list
    19   val span_range: span -> Position.range
    20   val span_source: (OuterLex.token, 'a) Source.source ->
    21     (span, (OuterLex.token, 'a) Source.source) Source.source
    22   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
    23   val present_span: span -> output
    24   val report_span: span -> unit
    25   val unit_source: (span, 'a) Source.source ->
    26     (span * span list * bool, (span, 'a) Source.source) Source.source
    27 end;
    28 
    29 structure ThySyntax: THY_SYNTAX =
    30 struct
    31 
    32 structure K = OuterKeyword;
    33 structure T = OuterLex;
    34 structure P = OuterParse;
    35 
    36 
    37 (** tokens **)
    38 
    39 (* parse *)
    40 
    41 fun token_source lexs pos src =
    42   Symbol.source {do_recover = true} src
    43   |> T.source {do_recover = SOME false} (K lexs) pos;
    44 
    45 fun parse_tokens lexs pos str =
    46   Source.of_string str
    47   |> token_source lexs pos
    48   |> Source.exhaust;
    49 
    50 
    51 (* present *)
    52 
    53 local
    54 
    55 val token_kind_markup =
    56  fn T.Command       => (Markup.commandN, [])
    57   | T.Keyword       => (Markup.keywordN, [])
    58   | T.Ident         => Markup.ident
    59   | T.LongIdent     => Markup.ident
    60   | T.SymIdent      => Markup.ident
    61   | T.Var           => Markup.var
    62   | T.TypeIdent     => Markup.tfree
    63   | T.TypeVar       => Markup.tvar
    64   | T.Nat           => Markup.ident
    65   | T.String        => Markup.string
    66   | T.AltString     => Markup.altstring
    67   | T.Verbatim      => Markup.verbatim
    68   | T.Space         => Markup.none
    69   | T.Comment       => Markup.comment
    70   | T.InternalValue => Markup.none
    71   | T.Malformed     => Markup.malformed
    72   | T.Error _       => Markup.malformed
    73   | T.Sync          => Markup.control
    74   | T.EOF           => Markup.control;
    75 
    76 in
    77 
    78 fun present_token tok =
    79   Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
    80 
    81 fun report_token tok =
    82   Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
    83 
    84 end;
    85 
    86 
    87 
    88 (** spans **)
    89 
    90 (* type span *)
    91 
    92 datatype span_kind = Command of string | Ignored | Malformed;
    93 datatype span = Span of span_kind * OuterLex.token list;
    94 
    95 fun span_kind (Span (k, _)) = k;
    96 fun span_content (Span (_, toks)) = toks;
    97 
    98 fun span_range span =
    99   (case span_content span of
   100     [] => (Position.none, Position.none)
   101   | toks =>
   102       let
   103         val start_pos = T.position_of (hd toks);
   104         val end_pos = T.end_position_of (List.last toks);
   105       in (start_pos, end_pos) end);
   106 
   107 
   108 (* parse *)
   109 
   110 local
   111 
   112 val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
   113 
   114 val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
   115 
   116 val span =
   117   Scan.ahead P.command -- P.not_eof -- Scan.repeat body
   118     >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
   119   Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
   120   Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
   121 
   122 in
   123 
   124 fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
   125 
   126 end;
   127 
   128 fun parse_spans lexs pos str =
   129   Source.of_string str
   130   |> token_source lexs pos
   131   |> span_source
   132   |> Source.exhaust;
   133 
   134 
   135 (* present *)
   136 
   137 local
   138 
   139 fun kind_markup (Command name) = Markup.command_span name
   140   | kind_markup Ignored = Markup.ignored_span
   141   | kind_markup Malformed = Markup.malformed_span;
   142 
   143 in
   144 
   145 fun present_span span =
   146   Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
   147 
   148 fun report_span span =
   149   Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
   150 
   151 end;
   152 
   153 
   154 
   155 (** units: commands with proof **)
   156 
   157 (* scanning spans *)
   158 
   159 val eof = Span (Command "", []);
   160 
   161 fun is_eof (Span (Command "", _)) = true
   162   | is_eof _ = false;
   163 
   164 val not_eof = not o is_eof;
   165 
   166 val stopper = Scan.stopper (K eof) is_eof;
   167 
   168 
   169 (* unit_source *)
   170 
   171 local
   172 
   173 fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
   174 
   175 val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
   176   if d <= 0 then Scan.fail
   177   else
   178     command_with K.is_qed_global >> pair ~1 ||
   179     command_with K.is_proof_goal >> pair (d + 1) ||
   180     (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
   181     Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
   182 
   183 val unit =
   184   command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
   185   Scan.one not_eof >> (fn a => (a, [], true));
   186 
   187 in
   188 
   189 fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
   190 
   191 end;
   192 
   193 end;