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