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

Local syntax depending on theory syntax.
*)

val show_structs = ref false;

signature LOCAL_SYNTAX =
sig
  type T
  val syn_of: T -> Syntax.syntax
  val structs_of: T -> string list
  val init: theory -> T
  val rebuild: theory -> T -> T
  val add_syntax: theory -> string * bool -> (bool * (string * typ * mixfix)) list -> T -> T
  val extern_term: T -> term -> term
end;

structure LocalSyntax: LOCAL_SYNTAX =
struct


(* datatype T *)

type local_mixfix =
  ((string * bool) * string list list) *          (*name, fixed?, mixfix content*)
  ((string * bool) * (string * typ * mixfix));    (*mode, inout?, mixfix syntax*)

datatype T = Syntax of
 {thy_syntax: Syntax.syntax,
  local_syntax: Syntax.syntax,
  mixfixes: local_mixfix list,
  idents: string list * string list};

fun make_syntax (thy_syntax, local_syntax, mixfixes, idents) =
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
    mixfixes = mixfixes, idents = idents};

fun map_syntax f (Syntax {thy_syntax, local_syntax, mixfixes, idents}) =
  make_syntax (f (thy_syntax, local_syntax, mixfixes, idents));

fun is_consistent thy (Syntax {thy_syntax, ...}) =
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);

fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
fun idents_of (Syntax {idents, ...}) = idents;
val structs_of = #1 o idents_of;


(* build syntax *)

fun build_syntax thy (mixfixes, idents as (structs, _)) =
  let
    val thy_syntax = Sign.syn_of thy;
    val is_logtype = Sign.is_logtype thy;
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    val local_syntax = thy_syntax
      |> Syntax.extend_trfuns
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
      |> fold (uncurry (Syntax.extend_const_gram is_logtype))
          (AList.coalesce (op =) (rev (map snd mixfixes)));
  in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end;

fun init thy = build_syntax thy ([], ([], []));

fun rebuild thy (syntax as Syntax {mixfixes, idents, ...}) =
  if is_consistent thy syntax then syntax
  else build_syntax thy (mixfixes, idents);


(* mixfix declarations *)

local

fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;

fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) =
  inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1;

fun add_mixfix (mode, inout) (fixed, (x, T, mx)) =
  let
    val content = Syntax.mixfix_content mx;
    val c = if fixed then Syntax.fixedN ^ x else x;
  in
    remove mixfix_conflict (content, inout) #>
    cons (((x, fixed), content), ((mode, inout), (c, T, mx)))
  end;

fun prep_struct (fixed, (c, _, Structure)) =
      if fixed then SOME c
      else error ("Bad mixfix declaration for const: " ^ quote c)
  | prep_struct _ = NONE;

in

fun add_syntax thy prmode raw_decls (syntax as (Syntax {mixfixes, idents = (structs, _), ...})) =
  (case filter_out mixfix_nosyn raw_decls of
    [] => syntax
  | decls =>
      let
        val mixfixes' = mixfixes |> fold (add_mixfix prmode) (filter_out mixfix_struct decls);
        val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
        val structs' = structs @ map_filter prep_struct decls;
      in build_syntax thy (mixfixes', (structs', fixes')) end);
<commit_msg>maintain implicit syntax mode; tuned;<commit_after>(*  Title:      Pure/Isar/local_syntax.ML
    ID:         $Id$
    Author:     Makarius

Local syntax depending on theory syntax.
*)

val show_structs = ref false;

signature LOCAL_SYNTAX =
sig
  type T
  val syn_of: T -> Syntax.syntax
  val structs_of: T -> string list
  val init: theory -> T
  val rebuild: theory -> T -> T
  val set_mode: string * bool -> T -> T
  val restore_mode: T -> T -> T
  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
  val extern_term: T -> term -> term
end;

structure LocalSyntax: LOCAL_SYNTAX =
struct

(* datatype T *)

type local_mixfix =
  ((string * bool) * string list list) *          (*name, fixed?, mixfix content*)
  ((string * bool) * (string * typ * mixfix));    (*mode, mixfix syntax*)

datatype T = Syntax of
 {thy_syntax: Syntax.syntax,
  local_syntax: Syntax.syntax,
  mode: string * bool,
  mixfixes: local_mixfix list,
  idents: string list * string list};

fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
    mode = mode, mixfixes = mixfixes, idents = idents};

fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));

fun is_consistent thy (Syntax {thy_syntax, ...}) =
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);

fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
fun idents_of (Syntax {idents, ...}) = idents;
val structs_of = #1 o idents_of;


(* build syntax *)

fun build_syntax thy mode mixfixes (idents as (structs, _)) =
  let
    val thy_syntax = Sign.syn_of thy;
    val is_logtype = Sign.is_logtype thy;
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    val local_syntax = thy_syntax
      |> Syntax.extend_trfuns
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
      |> fold (uncurry (Syntax.extend_const_gram is_logtype))
          (AList.coalesce (op =) (rev (map snd mixfixes)));
  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;

fun init thy = build_syntax thy Syntax.default_mode [] ([], []);

fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
  if is_consistent thy syntax then syntax
  else build_syntax thy mode mixfixes idents;


(* syntax mode *)

fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
  (thy_syntax, local_syntax, mode, mixfixes, idents));

fun restore_mode (Syntax {mode, ...}) = set_mode mode;


(* mixfix declarations *)

local

fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
fun mixfix_struct (_, (_, _, mx)) = mx = Structure;

fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) =
  inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1;

fun add_mixfix (mode, inout) (fixed, (x, T, mx)) =
  let
    val content = Syntax.mixfix_content mx;
    val c = if fixed then Syntax.fixedN ^ x else x;
  in
    remove mixfix_conflict (content, inout) #>
    cons (((x, fixed), content), ((mode, inout), (c, T, mx)))
  end;

fun prep_struct (fixed, (c, _, Structure)) =
      if fixed then SOME c
      else error ("Bad mixfix declaration for const: " ^ quote c)
  | prep_struct _ = NONE;

in

fun add_syntax thy raw_decls (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
  (case filter_out mixfix_nosyn raw_decls of
    [] => syntax
  | decls =>
      let
        val mixfixes' = mixfixes |> fold (add_mixfix mode) (filter_out mixfix_struct decls);
        val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
        val structs' = structs @ map_filter prep_struct decls;
      in build_syntax thy mode mixfixes' (structs', fixes') end);

{'fraction_non_alphanumeric': 0.1297048470078527, 'fraction_numerical': 0.002437043054427295, 'mean_word_length': 3.4634441087613292, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 49, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '750859', 'n_tokens_mistral': 2702, 'n_tokens_neox': 2591, 'n_words': 810}