src/Pure/Isar/local_syntax.ML

importing of polymorphic introduction rules with different schematic variable names

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

Local syntax depending on theory syntax.
*)

val show_structs = Unsynchronized.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 -> (bool * (string * typ * mixfix)) list -> T -> T
  val set_mode: Syntax.mode -> T -> T
  val restore_mode: T -> T -> T
  val update_modesyntax: theory -> bool -> Syntax.mode ->
    (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) *                                    (*name, fixed?*)
  ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)

datatype T = Syntax of
 {thy_syntax: Syntax.syntax,
  local_syntax: Syntax.syntax,
  mode: Syntax.mode,
  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;
    fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
      | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    val local_syntax = thy_syntax
      |> Syntax.update_trfuns
          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
      |> fold const_gram (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.mode_default [] ([], []);

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


(* mixfix declarations *)

local

fun prep_mixfix _ (_, (_, _, Structure)) = NONE
  | prep_mixfix mode (fixed, (x, T, mx)) =
      let val c = if fixed then Syntax.fixedN ^ x else x
      in SOME ((x, fixed), (mode, (c, T, mx))) end;

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

in

fun update_syntax add thy raw_decls
    (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
  (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
    [] => syntax
  | decls =>
      let
        val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
        val new_structs = map_filter prep_struct decls;
        val mixfixes' = rev new_mixfixes @ mixfixes;
        val structs' =
          if add then structs @ new_structs
          else subtract (op =) new_structs structs;
        val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
      in build_syntax thy mode mixfixes' (structs', fixes') end);

val add_syntax = update_syntax true;

end;


(* 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;

fun update_modesyntax thy add mode args syntax =
  syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;


(* extern_term *)

fun extern_term syntax =
  let
    val (structs, fixes) = idents_of syntax;
    fun map_free (t as Free (x, T)) =
          let val i = find_index (fn s => s = x) structs + 1 in
            if i = 0 andalso member (op =) fixes x then
              Const (Syntax.fixedN ^ x, T)
            else if i = 1 andalso not (! show_structs) then
              Syntax.const "_struct" $ Syntax.const "_indexdefault"
            else t
          end
      | map_free t = t;
  in Term.map_aterms map_free end;

end;