src/Pure/Isar/keyword.ML
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago)
changeset 69913 ca515cf61651
parent 67139 8fe0aba577af
permissions -rw-r--r--
more specific keyword kinds;
wenzelm@36949
     1
(*  Title:      Pure/Isar/keyword.ML
wenzelm@17059
     2
    Author:     Makarius
wenzelm@17059
     3
wenzelm@58900
     4
Isar keyword classification.
wenzelm@17059
     5
*)
wenzelm@17059
     6
wenzelm@36949
     7
signature KEYWORD =
wenzelm@17059
     8
sig
wenzelm@58928
     9
  val diag: string
wenzelm@58999
    10
  val document_heading: string
wenzelm@58999
    11
  val document_body: string
wenzelm@58999
    12
  val document_raw: string
wenzelm@58928
    13
  val thy_begin: string
wenzelm@58928
    14
  val thy_end: string
wenzelm@58928
    15
  val thy_decl: string
wenzelm@58928
    16
  val thy_decl_block: string
wenzelm@69913
    17
  val thy_defn: string
wenzelm@69913
    18
  val thy_stmt: string
wenzelm@58928
    19
  val thy_load: string
wenzelm@58928
    20
  val thy_goal: string
wenzelm@69913
    21
  val thy_goal_defn: string
wenzelm@69913
    22
  val thy_goal_stmt: string
wenzelm@58928
    23
  val qed: string
wenzelm@58928
    24
  val qed_script: string
wenzelm@58928
    25
  val qed_block: string
wenzelm@58928
    26
  val qed_global: string
wenzelm@58928
    27
  val prf_goal: string
wenzelm@58928
    28
  val prf_block: string
wenzelm@60694
    29
  val next_block: string
wenzelm@58928
    30
  val prf_open: string
wenzelm@58928
    31
  val prf_close: string
wenzelm@58928
    32
  val prf_chain: string
wenzelm@58928
    33
  val prf_decl: string
wenzelm@58928
    34
  val prf_asm: string
wenzelm@58928
    35
  val prf_asm_goal: string
wenzelm@58928
    36
  val prf_script: string
wenzelm@60624
    37
  val prf_script_goal: string
wenzelm@60624
    38
  val prf_script_asm_goal: string
wenzelm@63441
    39
  val before_command: string
wenzelm@63430
    40
  val quasi_command: string
wenzelm@48864
    41
  type spec = (string * string list) * string list
wenzelm@63429
    42
  val no_spec: spec
wenzelm@63441
    43
  val before_command_spec: spec
wenzelm@63430
    44
  val quasi_command_spec: spec
wenzelm@67139
    45
  val document_heading_spec: spec
wenzelm@67139
    46
  val document_body_spec: spec
wenzelm@58903
    47
  type keywords
wenzelm@58903
    48
  val minor_keywords: keywords -> Scan.lexicon
wenzelm@58903
    49
  val major_keywords: keywords -> Scan.lexicon
wenzelm@58920
    50
  val no_command_keywords: keywords -> keywords
wenzelm@58903
    51
  val empty_keywords: keywords
wenzelm@58903
    52
  val merge_keywords: keywords * keywords -> keywords
wenzelm@63429
    53
  val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
wenzelm@58931
    54
  val is_keyword: keywords -> string -> bool
wenzelm@58931
    55
  val is_command: keywords -> string -> bool
wenzelm@58928
    56
  val is_literal: keywords -> string -> bool
wenzelm@61618
    57
  val dest_commands: keywords -> string list
wenzelm@59934
    58
  val command_markup: keywords -> string -> Markup.T option
wenzelm@59123
    59
  val command_kind: keywords -> string -> string option
wenzelm@58923
    60
  val command_files: keywords -> string -> Path.T -> Path.T list
wenzelm@58923
    61
  val command_tags: keywords -> string -> string list
wenzelm@58999
    62
  val is_vacuous: keywords -> string -> bool
wenzelm@58923
    63
  val is_diag: keywords -> string -> bool
wenzelm@58999
    64
  val is_document_heading: keywords -> string -> bool
wenzelm@58999
    65
  val is_document_body: keywords -> string -> bool
wenzelm@58999
    66
  val is_document_raw: keywords -> string -> bool
wenzelm@59033
    67
  val is_document: keywords -> string -> bool
wenzelm@59125
    68
  val is_theory_end: keywords -> string -> bool
wenzelm@58923
    69
  val is_theory_load: keywords -> string -> bool
wenzelm@58923
    70
  val is_theory: keywords -> string -> bool
wenzelm@58923
    71
  val is_theory_body: keywords -> string -> bool
wenzelm@58923
    72
  val is_proof: keywords -> string -> bool
wenzelm@58923
    73
  val is_proof_body: keywords -> string -> bool
wenzelm@58923
    74
  val is_theory_goal: keywords -> string -> bool
wenzelm@58923
    75
  val is_proof_goal: keywords -> string -> bool
wenzelm@58923
    76
  val is_qed: keywords -> string -> bool
wenzelm@58923
    77
  val is_qed_global: keywords -> string -> bool
wenzelm@60693
    78
  val is_proof_open: keywords -> string -> bool
wenzelm@60693
    79
  val is_proof_close: keywords -> string -> bool
wenzelm@59125
    80
  val is_proof_asm: keywords -> string -> bool
wenzelm@59125
    81
  val is_improper: keywords -> string -> bool
wenzelm@58923
    82
  val is_printed: keywords -> string -> bool
wenzelm@17059
    83
end;
wenzelm@17059
    84
wenzelm@36949
    85
structure Keyword: KEYWORD =
wenzelm@17059
    86
struct
wenzelm@17059
    87
wenzelm@27357
    88
(** keyword classification **)
wenzelm@17059
    89
wenzelm@58918
    90
(* kinds *)
wenzelm@58918
    91
wenzelm@58928
    92
val diag = "diag";
wenzelm@58999
    93
val document_heading = "document_heading";
wenzelm@58999
    94
val document_body = "document_body";
wenzelm@58999
    95
val document_raw = "document_raw";
wenzelm@58928
    96
val thy_begin = "thy_begin";
wenzelm@58928
    97
val thy_end = "thy_end";
wenzelm@58928
    98
val thy_decl = "thy_decl";
wenzelm@58928
    99
val thy_decl_block = "thy_decl_block";
wenzelm@69913
   100
val thy_defn = "thy_defn";
wenzelm@69913
   101
val thy_stmt = "thy_stmt";
wenzelm@58928
   102
val thy_load = "thy_load";
wenzelm@58928
   103
val thy_goal = "thy_goal";
wenzelm@69913
   104
val thy_goal_defn = "thy_goal_defn";
wenzelm@69913
   105
val thy_goal_stmt = "thy_goal_stmt";
wenzelm@58928
   106
val qed = "qed";
wenzelm@58928
   107
val qed_script = "qed_script";
wenzelm@58928
   108
val qed_block = "qed_block";
wenzelm@58928
   109
val qed_global = "qed_global";
wenzelm@58928
   110
val prf_goal = "prf_goal";
wenzelm@58928
   111
val prf_block = "prf_block";
wenzelm@60694
   112
val next_block = "next_block";
wenzelm@58928
   113
val prf_open = "prf_open";
wenzelm@58928
   114
val prf_close = "prf_close";
wenzelm@58928
   115
val prf_chain = "prf_chain";
wenzelm@58928
   116
val prf_decl = "prf_decl";
wenzelm@58928
   117
val prf_asm = "prf_asm";
wenzelm@58928
   118
val prf_asm_goal = "prf_asm_goal";
wenzelm@58928
   119
val prf_script = "prf_script";
wenzelm@60624
   120
val prf_script_goal = "prf_script_goal";
wenzelm@60624
   121
val prf_script_asm_goal = "prf_script_asm_goal";
wenzelm@63441
   122
wenzelm@63441
   123
val before_command = "before_command";
wenzelm@63430
   124
val quasi_command = "quasi_command";
wenzelm@58928
   125
wenzelm@63430
   126
val command_kinds =
wenzelm@58999
   127
  [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
wenzelm@69913
   128
    thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script,
wenzelm@69913
   129
    qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain,
wenzelm@69913
   130
    prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal];
wenzelm@58928
   131
wenzelm@58928
   132
wenzelm@58928
   133
(* specifications *)
wenzelm@58928
   134
wenzelm@59934
   135
type spec = (string * string list) * string list;
wenzelm@59934
   136
wenzelm@63429
   137
val no_spec: spec = (("", []), []);
wenzelm@63441
   138
val before_command_spec: spec = ((before_command, []), []);
wenzelm@63430
   139
val quasi_command_spec: spec = ((quasi_command, []), []);
wenzelm@67139
   140
val document_heading_spec: spec = (("document_heading", []), ["document"]);
wenzelm@67139
   141
val document_body_spec: spec = (("document_body", []), ["document"]);
wenzelm@63429
   142
wenzelm@59934
   143
type entry =
wenzelm@59934
   144
 {pos: Position.T,
wenzelm@59934
   145
  id: serial,
wenzelm@59934
   146
  kind: string,
wenzelm@48864
   147
  files: string list,  (*extensions of embedded files*)
wenzelm@58918
   148
  tags: string list};
wenzelm@17059
   149
wenzelm@59934
   150
fun check_spec pos ((kind, files), tags) : entry =
wenzelm@63430
   151
  if not (member (op =) command_kinds kind) then
wenzelm@58918
   152
    error ("Unknown outer syntax keyword kind " ^ quote kind)
wenzelm@58928
   153
  else if not (null files) andalso kind <> thy_load then
wenzelm@58918
   154
    error ("Illegal specification of files for " ^ quote kind)
wenzelm@59934
   155
  else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
wenzelm@46961
   156
wenzelm@46938
   157
wenzelm@58903
   158
(** keyword tables **)
wenzelm@58903
   159
wenzelm@58903
   160
(* type keywords *)
wenzelm@27357
   161
wenzelm@48874
   162
datatype keywords = Keywords of
wenzelm@58903
   163
 {minor: Scan.lexicon,
wenzelm@58903
   164
  major: Scan.lexicon,
wenzelm@59934
   165
  commands: entry Symtab.table};
wenzelm@58903
   166
wenzelm@58903
   167
fun minor_keywords (Keywords {minor, ...}) = minor;
wenzelm@58903
   168
fun major_keywords (Keywords {major, ...}) = major;
wenzelm@58903
   169
wenzelm@58906
   170
fun make_keywords (minor, major, commands) =
wenzelm@58906
   171
  Keywords {minor = minor, major = major, commands = commands};
wenzelm@46957
   172
wenzelm@58906
   173
fun map_keywords f (Keywords {minor, major, commands}) =
wenzelm@58906
   174
  make_keywords (f (minor, major, commands));
wenzelm@58903
   175
wenzelm@58920
   176
val no_command_keywords =
wenzelm@58920
   177
  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
wenzelm@58920
   178
wenzelm@58920
   179
wenzelm@58920
   180
(* build keywords *)
wenzelm@58920
   181
wenzelm@58903
   182
val empty_keywords =
wenzelm@58903
   183
  make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
wenzelm@48874
   184
wenzelm@58903
   185
fun merge_keywords
wenzelm@58906
   186
  (Keywords {minor = minor1, major = major1, commands = commands1},
wenzelm@58906
   187
    Keywords {minor = minor2, major = major2, commands = commands2}) =
wenzelm@58903
   188
  make_keywords
wenzelm@58903
   189
   (Scan.merge_lexicons (minor1, minor2),
wenzelm@58903
   190
    Scan.merge_lexicons (major1, major2),
wenzelm@58906
   191
    Symtab.merge (K true) (commands1, commands2));
wenzelm@27357
   192
wenzelm@58928
   193
val add_keywords =
wenzelm@63429
   194
  fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
wenzelm@63441
   195
    if kind = "" orelse kind = before_command orelse kind = quasi_command then
wenzelm@63429
   196
      let
wenzelm@63429
   197
        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
wenzelm@63429
   198
      in (minor', major, commands) end
wenzelm@63429
   199
    else
wenzelm@63429
   200
      let
wenzelm@63429
   201
        val entry = check_spec pos spec;
wenzelm@63429
   202
        val major' = Scan.extend_lexicon (Symbol.explode name) major;
wenzelm@63429
   203
        val commands' = Symtab.update (name, entry) commands;
wenzelm@63429
   204
      in (minor, major', commands') end));
wenzelm@27357
   205
wenzelm@58903
   206
wenzelm@58931
   207
(* keyword status *)
wenzelm@27357
   208
wenzelm@58931
   209
fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
wenzelm@58931
   210
fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
wenzelm@58931
   211
fun is_literal keywords = is_keyword keywords orf is_command keywords;
wenzelm@27357
   212
wenzelm@61618
   213
fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
wenzelm@61618
   214
wenzelm@58928
   215
wenzelm@59934
   216
(* command keywords *)
wenzelm@58931
   217
wenzelm@59123
   218
fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
wenzelm@59123
   219
wenzelm@59934
   220
fun command_markup keywords name =
wenzelm@59934
   221
  lookup_command keywords name
wenzelm@59934
   222
  |> Option.map (fn {pos, id, ...} =>
wenzelm@59934
   223
      Markup.properties (Position.entity_properties_of false id pos)
wenzelm@59935
   224
        (Markup.entity Markup.command_keywordN name));
wenzelm@59934
   225
wenzelm@59123
   226
fun command_kind keywords = Option.map #kind o lookup_command keywords;
wenzelm@54523
   227
wenzelm@58923
   228
fun command_files keywords name path =
wenzelm@59123
   229
  (case lookup_command keywords name of
wenzelm@54523
   230
    NONE => []
wenzelm@58928
   231
  | SOME {kind, files, ...} =>
wenzelm@58928
   232
      if kind <> thy_load then []
wenzelm@54523
   233
      else if null files then [path]
wenzelm@54523
   234
      else map (fn ext => Path.ext ext path) files);
wenzelm@54523
   235
wenzelm@58923
   236
fun command_tags keywords name =
wenzelm@59123
   237
  (case lookup_command keywords name of
wenzelm@58928
   238
    SOME {tags, ...} => tags
wenzelm@58918
   239
  | NONE => []);
wenzelm@27357
   240
wenzelm@27433
   241
wenzelm@28431
   242
(* command categories *)
wenzelm@27433
   243
wenzelm@51225
   244
fun command_category ks =
wenzelm@58923
   245
  let
wenzelm@58928
   246
    val tab = Symtab.make_set ks;
wenzelm@58923
   247
    fun pred keywords name =
wenzelm@59123
   248
      (case lookup_command keywords name of
wenzelm@51225
   249
        NONE => false
wenzelm@58928
   250
      | SOME {kind, ...} => Symtab.defined tab kind);
wenzelm@58923
   251
  in pred end;
wenzelm@27440
   252
wenzelm@58999
   253
val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
wenzelm@58999
   254
wenzelm@29347
   255
val is_diag = command_category [diag];
wenzelm@40397
   256
wenzelm@58999
   257
val is_document_heading = command_category [document_heading];
wenzelm@58999
   258
val is_document_body = command_category [document_body];
wenzelm@58999
   259
val is_document_raw = command_category [document_raw];
wenzelm@58999
   260
val is_document = command_category [document_heading, document_body, document_raw];
wenzelm@29347
   261
wenzelm@59125
   262
val is_theory_end = command_category [thy_end];
wenzelm@29347
   263
wenzelm@48867
   264
val is_theory_load = command_category [thy_load];
wenzelm@48867
   265
wenzelm@27440
   266
val is_theory = command_category
wenzelm@69913
   267
  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal,
wenzelm@69913
   268
    thy_goal_defn, thy_goal_stmt];
wenzelm@27440
   269
wenzelm@56944
   270
val is_theory_body = command_category
wenzelm@69913
   271
  [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt];
wenzelm@56944
   272
wenzelm@27440
   273
val is_proof = command_category
wenzelm@60694
   274
  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
wenzelm@60694
   275
    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
wenzelm@60624
   276
    prf_script_asm_goal];
wenzelm@28431
   277
wenzelm@51225
   278
val is_proof_body = command_category
wenzelm@60694
   279
  [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open,
wenzelm@60694
   280
    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
wenzelm@60624
   281
    prf_script_asm_goal];
wenzelm@51225
   282
wenzelm@69913
   283
val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt];
wenzelm@60624
   284
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
wenzelm@53571
   285
val is_qed = command_category [qed, qed_script, qed_block];
wenzelm@28431
   286
val is_qed_global = command_category [qed_global];
wenzelm@27520
   287
wenzelm@60693
   288
val is_proof_open =
wenzelm@60693
   289
  command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open];
wenzelm@60693
   290
val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
wenzelm@60693
   291
wenzelm@59125
   292
val is_proof_asm = command_category [prf_asm, prf_asm_goal];
wenzelm@60624
   293
val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
wenzelm@59125
   294
wenzelm@58923
   295
fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
wenzelm@58923
   296
wenzelm@27357
   297
end;