src/Pure/Isar/keyword.ML

simplified keyword kinds;
more explicit bootstrap syntax;

(*  Title:      Pure/Isar/keyword.ML
    Author:     Makarius

Isar keyword classification.
*)

signature KEYWORD =
sig
  type T
  val kind_of: T -> string
  val kind_files_of: T -> string * string list
  val diag: T
  val heading: T
  val thy_begin: T
  val thy_end: T
  val thy_decl: T
  val thy_decl_block: T
  val thy_load: T
  val thy_goal: T
  val qed: T
  val qed_script: T
  val qed_block: T
  val qed_global: T
  val prf_goal: T
  val prf_block: T
  val prf_open: T
  val prf_close: T
  val prf_chain: T
  val prf_decl: T
  val prf_asm: T
  val prf_asm_goal: T
  val prf_asm_goal_script: T
  val prf_script: T
  type spec = (string * string list) * string list
  val spec: spec -> T
  val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
  type keywords
  val minor_keywords: keywords -> Scan.lexicon
  val major_keywords: keywords -> Scan.lexicon
  val empty_keywords: keywords
  val merge_keywords: keywords * keywords -> keywords
  val no_command_keywords: keywords -> keywords
  val add: string * T option -> keywords -> keywords
  val define: string * T option -> unit
  val get_keywords: unit -> keywords
  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
  val is_keyword: string -> bool
  val command_keyword: string -> T option
  val command_files: string -> Path.T -> Path.T list
  val command_tags: string -> string list
  val is_diag: string -> bool
  val is_heading: string -> bool
  val is_theory_begin: string -> bool
  val is_theory_load: string -> bool
  val is_theory: string -> bool
  val is_theory_body: string -> bool
  val is_proof: string -> bool
  val is_proof_body: string -> bool
  val is_theory_goal: string -> bool
  val is_proof_goal: string -> bool
  val is_qed: string -> bool
  val is_qed_global: string -> bool
  val is_printed: string -> bool
end;

structure Keyword: KEYWORD =
struct

(** keyword classification **)

(* kinds *)

datatype T = Keyword of
 {kind: string,
  files: string list,  (*extensions of embedded files*)
  tags: string list};

fun kind s = Keyword {kind = s, files = [], tags = []};
fun kind_of (Keyword {kind, ...}) = kind;
fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);

val diag = kind "diag";
val heading = kind "heading";
val thy_begin = kind "thy_begin";
val thy_end = kind "thy_end";
val thy_decl = kind "thy_decl";
val thy_decl_block = kind "thy_decl_block";
val thy_load = kind "thy_load";
val thy_goal = kind "thy_goal";
val qed = kind "qed";
val qed_script = kind "qed_script";
val qed_block = kind "qed_block";
val qed_global = kind "qed_global";
val prf_goal = kind "prf_goal";
val prf_block = kind "prf_block";
val prf_open = kind "prf_open";
val prf_close = kind "prf_close";
val prf_chain = kind "prf_chain";
val prf_decl = kind "prf_decl";
val prf_asm = kind "prf_asm";
val prf_asm_goal = kind "prf_asm_goal";
val prf_asm_goal_script = kind "prf_asm_goal_script";
val prf_script = kind "prf_script";

val kinds =
  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]
  |> map kind_of;


(* specifications *)

type spec = (string * string list) * string list;

fun spec ((kind, files), tags) =
  if not (member (op =) kinds kind) then
    error ("Unknown outer syntax keyword kind " ^ quote kind)
  else if not (null files) andalso kind <> kind_of thy_load then
    error ("Illegal specification of files for " ^ quote kind)
  else Keyword {kind = kind, files = files, tags = tags};

fun command_spec ((name, s), pos) = ((name, spec s), pos);



(** keyword tables **)

(* type keywords *)

datatype keywords = Keywords of
 {minor: Scan.lexicon,
  major: Scan.lexicon,
  commands: T Symtab.table};

fun minor_keywords (Keywords {minor, ...}) = minor;
fun major_keywords (Keywords {major, ...}) = major;
fun commands (Keywords {commands, ...}) = commands;

fun make_keywords (minor, major, commands) =
  Keywords {minor = minor, major = major, commands = commands};

fun map_keywords f (Keywords {minor, major, commands}) =
  make_keywords (f (minor, major, commands));

val empty_keywords =
  make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);

fun merge_keywords
  (Keywords {minor = minor1, major = major1, commands = commands1},
    Keywords {minor = minor2, major = major2, commands = commands2}) =
  make_keywords
   (Scan.merge_lexicons (minor1, minor2),
    Scan.merge_lexicons (major1, major2),
    Symtab.merge (K true) (commands1, commands2));

val no_command_keywords =
  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));


(* add keywords *)

fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
  (case opt_kind of
    NONE =>
      let
        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
      in (minor', major, commands) end
  | SOME kind =>
      let
        val major' = Scan.extend_lexicon (Symbol.explode name) major;
        val commands' = Symtab.update (name, kind) commands;
      in (minor, major', commands') end));


(* global state *)

local val global_keywords = Unsynchronized.ref empty_keywords in

fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl));
fun get_keywords () = ! global_keywords;

end;

fun get_lexicons () =
  let val keywords = get_keywords ()
  in (minor_keywords keywords, major_keywords keywords) end;

fun get_commands () = commands (get_keywords ());


(* lookup *)

fun is_keyword s =
  let
    val (minor, major) = get_lexicons ();
    val syms = Symbol.explode s;
  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;

fun command_keyword name = Symtab.lookup (get_commands ()) name;

fun command_files name path =
  (case command_keyword name of
    NONE => []
  | SOME (Keyword {kind, files, ...}) =>
      if kind <> kind_of thy_load then []
      else if null files then [path]
      else map (fn ext => Path.ext ext path) files);

fun command_tags name =
  (case command_keyword name of
    SOME (Keyword {tags, ...}) => tags
  | NONE => []);


(* command categories *)

fun command_category ks =
  let val tab = Symtab.make_set (map kind_of ks) in
    fn name =>
      (case command_keyword name of
        NONE => false
      | SOME k => Symtab.defined tab (kind_of k))
  end;

val is_diag = command_category [diag];

val is_heading = command_category [heading];

val is_theory_begin = command_category [thy_begin];

val is_theory_load = command_category [thy_load];

val is_theory = command_category
  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];

val is_theory_body = command_category
  [thy_load, thy_decl, thy_decl_block, thy_goal];

val is_proof = command_category
  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];

val is_proof_body = command_category
  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
    prf_asm_goal, prf_asm_goal_script, prf_script];

val is_theory_goal = command_category [thy_goal];
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
val is_qed = command_category [qed, qed_script, qed_block];
val is_qed_global = command_category [qed_global];

val is_printed = is_theory_goal orf is_proof;

end;