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