<commit_before>(*  Title:      Pure/ML/ml_antiquote.ML
    ID:         $Id$
    Author:     Makarius

Common ML antiquotations.
*)

signature ML_ANTIQUOTE =
sig
  val variant: string -> Proof.context -> string * Proof.context
  val inline: string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val declaration: string -> string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val value: string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val the_thms: Proof.context -> int -> thm list
  val the_thm: Proof.context -> int -> thm
end;

structure ML_Antiquote: ML_ANTIQUOTE =
struct

(** generic tools **)

(* ML names *)

structure NamesData = ProofDataFun
(
  type T = Name.context;
  fun init _ = ML_Syntax.reserved;
);

fun variant a ctxt =
  let
    val names = NamesData.get ctxt;
    val ([b], names') = Name.variants [a] names;
    val ctxt' = NamesData.put names' ctxt;
  in (b, ctxt') end;


(* specific antiquotations *)

fun inline name scan = ML_Context.add_antiq name
  (scan >> (fn s => fn {struct_name, background} => ((K ("", s)), background)));

fun declaration kind name scan = ML_Context.add_antiq name
  (scan >> (fn s => fn {struct_name, background} =>
    let
      val (a, background') = variant name background;
      val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
      val body = struct_name ^ "." ^ a;
    in (K (env, body), background') end));

val value = declaration "val";



(** concrete antiquotations **)

(* misc *)

val _ = value "theory"
  (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
  || Scan.succeed "ML_Context.the_global_context ()");

val _ = value "theory_ref"
  (Scan.lift Args.name >> (fn name =>
    "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
  || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");

val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");

val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));

val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));

val _ = value "ctyp" (Args.typ >> (fn T =>
  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));

val _ = value "cterm" (Args.term >> (fn t =>
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));

val _ = value "cprop" (Args.prop >> (fn t =>
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));

val _ = value "cpat"
  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));


fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
    |> syn ? Sign.base_name
    |> ML_Syntax.print_string));

val _ = inline "type_name" (type_ false);
val _ = inline "type_syntax" (type_ true);


fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
  #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
  |> syn ? ProofContext.const_syntax_name ctxt
  |> ML_Syntax.print_string);

val _ = inline "const_name" (const false);
val _ = inline "const_syntax" (const true);

val _ = inline "const"
  (Args.context -- Scan.lift Args.name --
    Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
    >> (fn ((ctxt, c), Ts) =>
      let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));


(* abstract fact values *)

structure AuxFacts = ProofDataFun
(
  type T = thm list Inttab.table;
  fun init _ = Inttab.empty;
);

fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
fun the_thm ctxt name = the_single (the_thms ctxt name);

fun put_thms ths ctxt =
  let val i = serial ()
  in (i, AuxFacts.map (Inttab.update (i, ths)) ctxt) end;


fun thm_antiq kind scan = ML_Context.add_antiq kind
  (scan >> (fn ths => fn {struct_name, background} =>
    let
      val ((a, i), background') = background |> variant kind ||>> put_thms ths;
      val env = "val " ^ a ^ " = ML_Antiquote.the_" ^ kind ^
        " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
      val body = struct_name ^ "." ^ a;
    in (K (env, body), background') end));

val _ = thm_antiq "thm" (Attrib.thm >> single);
val _ = thm_antiq "thms" Attrib.thms;

end;

<commit_msg>added macro interface; added @{let}, @{note};<commit_after>(*  Title:      Pure/ML/ml_antiquote.ML
    ID:         $Id$
    Author:     Makarius

Common ML antiquotations.
*)

signature ML_ANTIQUOTE =
sig
  val macro: string ->
    (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
  val variant: string -> Proof.context -> string * Proof.context
  val inline: string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val declaration: string -> string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val value: string ->
    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
  val the_thms: Proof.context -> int -> thm list
  val the_thm: Proof.context -> int -> thm
end;

structure ML_Antiquote: ML_ANTIQUOTE =
struct

(** generic tools **)

(* ML names *)

structure NamesData = ProofDataFun
(
  type T = Name.context;
  fun init _ = ML_Syntax.reserved;
);

fun variant a ctxt =
  let
    val names = NamesData.get ctxt;
    val ([b], names') = Name.variants [a] names;
    val ctxt' = NamesData.put names' ctxt;
  in (b, ctxt') end;


(* specific antiquotations *)

fun macro name scan = ML_Context.add_antiq name
  (scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
    (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));

fun inline name scan = ML_Context.add_antiq name
  (scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));

fun declaration kind name scan = ML_Context.add_antiq name
  (scan >> (fn s => fn {struct_name, background} =>
    let
      val (a, background') = variant name background;
      val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
      val body = struct_name ^ "." ^ a;
    in (K (env, body), background') end));

val value = declaration "val";



(** concrete antiquotations **)

(* misc *)

val _ = value "theory"
  (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
  || Scan.succeed "ML_Context.the_global_context ()");

val _ = value "theory_ref"
  (Scan.lift Args.name >> (fn name =>
    "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
  || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");

val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");

val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));

val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));

val _ = macro "let" (Args.context --
  Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
    >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));

val _ = macro "note" (Args.context :|-- (fn ctxt =>
  Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
    ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
  >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));

val _ = value "ctyp" (Args.typ >> (fn T =>
  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));

val _ = value "cterm" (Args.term >> (fn t =>
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));

val _ = value "cprop" (Args.prop >> (fn t =>
  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));

val _ = value "cpat"
  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));


fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
    #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
    |> syn ? Sign.base_name
    |> ML_Syntax.print_string));

val _ = inline "type_name" (type_ false);
val _ = inline "type_syntax" (type_ true);


fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
  #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
  |> syn ? ProofContext.const_syntax_name ctxt
  |> ML_Syntax.print_string);

val _ = inline "const_name" (const false);
val _ = inline "const_syntax" (const true);

val _ = inline "const"
  (Args.context -- Scan.lift Args.name --
    Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
    >> (fn ((ctxt, c), Ts) =>
      let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));


(* abstract fact values *)

structure AuxFacts = ProofDataFun
(
  type T = thm list Inttab.table;
  fun init _ = Inttab.empty;
);

fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
fun the_thm ctxt name = the_single (the_thms ctxt name);

fun put_thms ths ctxt =
  let val i = serial ()
  in (i, AuxFacts.map (Inttab.update (i, ths)) ctxt) end;


fun thm_antiq kind scan = ML_Context.add_antiq kind
  (scan >> (fn ths => fn {struct_name, background} =>
    let
      val ((a, i), background') = background |> variant kind ||>> put_thms ths;
      val env = "val " ^ a ^ " = ML_Antiquote.the_" ^ kind ^
        " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
      val body = struct_name ^ "." ^ a;
    in (K (env, body), background') end));

val _ = thm_antiq "thm" (Attrib.thm >> single);
val _ = thm_antiq "thms" Attrib.thms;

end;


{'fraction_non_alphanumeric': 0.1628840945176053, 'fraction_numerical': 0.0010273652750537033, 'mean_word_length': 3.506734006734007, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 169, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '787085', 'n_tokens_mistral': 3950, 'n_tokens_neox': 3873, 'n_words': 1013}