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

Fixed type/term variables and polymorphic term abbreviations.
*)

signature VARIABLE =
sig
  val is_body: Proof.context -> bool
  val set_body: bool -> Proof.context -> Proof.context
  val restore_body: Proof.context -> Proof.context -> Proof.context
  val names_of: Proof.context -> Name.context
  val fixes_of: Proof.context -> (string * string) list
  val binds_of: Proof.context -> (typ * term) Vartab.table
  val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
  val is_declared: Proof.context -> string -> bool
  val is_fixed: Proof.context -> string -> bool
  val newly_fixed: Proof.context -> Proof.context -> string -> bool
  val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
  val default_type: Proof.context -> string -> typ option
  val def_type: Proof.context -> bool -> indexname -> typ option
  val def_sort: Proof.context -> indexname -> sort option
  val declare_constraints: term -> Proof.context -> Proof.context
  val declare_internal: term -> Proof.context -> Proof.context
  val declare_term: term -> Proof.context -> Proof.context
  val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
  val declare_thm: thm -> Proof.context -> Proof.context
  val thm_context: thm -> Proof.context
  val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
  val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
  val expand_binds: Proof.context -> term -> term
  val add_fixes: string list -> Proof.context -> string list * Proof.context
  val add_fixes_direct: string list -> Proof.context -> Proof.context
  val auto_fixes: term -> Proof.context -> Proof.context
  val variant_fixes: string list -> Proof.context -> string list * Proof.context
  val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
  val export_terms: Proof.context -> Proof.context -> term list -> term list
  val exportT_terms: Proof.context -> Proof.context -> term list -> term list
  val exportT: Proof.context -> Proof.context -> thm list -> thm list
  val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
  val export: Proof.context -> Proof.context -> thm list -> thm list
  val export_morphism: Proof.context -> Proof.context -> morphism
  val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
  val import_inst: bool -> term list -> Proof.context ->
    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
  val importT_terms: term list -> Proof.context -> term list * Proof.context
  val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
  val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
  val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
  val import_thms: bool -> thm list -> Proof.context ->
    ((ctyp list * cterm list) * thm list) * Proof.context
  val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
  val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
  val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
  val warn_extra_tfrees: Proof.context -> Proof.context -> unit
  val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
  val polymorphic: Proof.context -> term list -> term list
end;

structure Variable: VARIABLE =
struct

(** local context data **)

datatype data = Data of
 {is_body: bool,                        (*inner body mode*)
  names: Name.context,                  (*type/term variable names*)
  fixes: (string * string) list,        (*term fixes -- extern/intern*)
  binds: (typ * term) Vartab.table,     (*term bindings*)
  type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
  constraints:
    typ Vartab.table *                  (*type constraints*)
    sort Vartab.table};                 (*default sorts*)

fun make_data (is_body, names, fixes, binds, type_occs, constraints) =
  Data {is_body = is_body, names = names, fixes = fixes, binds = binds,
    type_occs = type_occs, constraints = constraints};

structure Data = ProofDataFun
(
  type T = data;
  fun init thy =
    make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
);

fun map_data f =
  Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
    make_data (f (is_body, names, fixes, binds, type_occs, constraints)));

fun map_names f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, f names, fixes, binds, type_occs, constraints));

fun map_fixes f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, f fixes, binds, type_occs, constraints));

fun map_binds f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, f binds, type_occs, constraints));

fun map_type_occs f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, binds, f type_occs, constraints));

fun map_constraints f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, binds, type_occs, f constraints));

fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);

val is_body = #is_body o rep_data;
fun set_body b = map_data (fn (_, names, fixes, binds, type_occs, constraints) =>
  (b, names, fixes, binds, type_occs, constraints));
fun restore_body ctxt = set_body (is_body ctxt);

val names_of = #names o rep_data;
val fixes_of = #fixes o rep_data;
val binds_of = #binds o rep_data;
val type_occs_of = #type_occs o rep_data;
val constraints_of = #constraints o rep_data;

val is_declared = Name.is_declared o names_of;
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);

fun add_fixed ctxt = Term.fold_aterms
  (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);



(** declarations **)

(* default sorts and types *)

fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1);

fun def_type ctxt pattern xi =
  let val {binds, constraints = (types, _), ...} = rep_data ctxt in
    (case Vartab.lookup types xi of
      NONE =>
        if pattern then NONE
        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
    | some => some)
  end;

val def_sort = Vartab.lookup o #2 o constraints_of;


(* names *)

val declare_type_names = map_names o
  fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I));

fun declare_names t =
  declare_type_names t #>
  map_names (fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t);


(* type occurrences *)

val decl_type_occs = fold_term_types
  (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
    | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));

val declare_type_occs = map_type_occs o decl_type_occs;


(* constraints *)

fun constrain_tvar (xi, S) =
  if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);

fun declare_constraints t = map_constraints (fn (types, sorts) =>
  let
    val types' = fold_aterms
      (fn Free (x, T) => Vartab.update ((x, ~1), T)
        | Var v => Vartab.update v
        | _ => I) t types;
    val sorts' = fold_types (fold_atyps
      (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
        | TVar v => constrain_tvar v
        | _ => I)) t sorts;
  in (types', sorts') end)
  #> declare_type_names t;


(* common declarations *)

fun declare_internal t =
  declare_names t #>
  declare_type_occs t;

fun declare_term t =
  declare_internal t #>
  declare_constraints t;

val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);

val declare_thm = Thm.fold_terms declare_internal;<commit_msg>declare_constraints: declare (fix) type variables within constraints, but not terms themselves;<commit_after>(*  Title:      Pure/variable.ML
    ID:         $Id$
    Author:     Makarius

Fixed type/term variables and polymorphic term abbreviations.
*)

signature VARIABLE =
sig
  val is_body: Proof.context -> bool
  val set_body: bool -> Proof.context -> Proof.context
  val restore_body: Proof.context -> Proof.context -> Proof.context
  val names_of: Proof.context -> Name.context
  val fixes_of: Proof.context -> (string * string) list
  val binds_of: Proof.context -> (typ * term) Vartab.table
  val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
  val is_declared: Proof.context -> string -> bool
  val is_fixed: Proof.context -> string -> bool
  val newly_fixed: Proof.context -> Proof.context -> string -> bool
  val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
  val default_type: Proof.context -> string -> typ option
  val def_type: Proof.context -> bool -> indexname -> typ option
  val def_sort: Proof.context -> indexname -> sort option
  val declare_constraints: term -> Proof.context -> Proof.context
  val declare_internal: term -> Proof.context -> Proof.context
  val declare_term: term -> Proof.context -> Proof.context
  val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
  val declare_thm: thm -> Proof.context -> Proof.context
  val thm_context: thm -> Proof.context
  val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
  val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
  val expand_binds: Proof.context -> term -> term
  val add_fixes: string list -> Proof.context -> string list * Proof.context
  val add_fixes_direct: string list -> Proof.context -> Proof.context
  val auto_fixes: term -> Proof.context -> Proof.context
  val variant_fixes: string list -> Proof.context -> string list * Proof.context
  val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
  val export_terms: Proof.context -> Proof.context -> term list -> term list
  val exportT_terms: Proof.context -> Proof.context -> term list -> term list
  val exportT: Proof.context -> Proof.context -> thm list -> thm list
  val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
  val export: Proof.context -> Proof.context -> thm list -> thm list
  val export_morphism: Proof.context -> Proof.context -> morphism
  val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
  val import_inst: bool -> term list -> Proof.context ->
    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
  val importT_terms: term list -> Proof.context -> term list * Proof.context
  val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
  val importT_thms: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
  val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
  val import_thms: bool -> thm list -> Proof.context ->
    ((ctyp list * cterm list) * thm list) * Proof.context
  val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
  val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
  val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
  val warn_extra_tfrees: Proof.context -> Proof.context -> unit
  val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
  val polymorphic: Proof.context -> term list -> term list
end;

structure Variable: VARIABLE =
struct

(** local context data **)

datatype data = Data of
 {is_body: bool,                        (*inner body mode*)
  names: Name.context,                  (*type/term variable names*)
  fixes: (string * string) list,        (*term fixes -- extern/intern*)
  binds: (typ * term) Vartab.table,     (*term bindings*)
  type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
  constraints:
    typ Vartab.table *                  (*type constraints*)
    sort Vartab.table};                 (*default sorts*)

fun make_data (is_body, names, fixes, binds, type_occs, constraints) =
  Data {is_body = is_body, names = names, fixes = fixes, binds = binds,
    type_occs = type_occs, constraints = constraints};

structure Data = ProofDataFun
(
  type T = data;
  fun init thy =
    make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
);

fun map_data f =
  Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
    make_data (f (is_body, names, fixes, binds, type_occs, constraints)));

fun map_names f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, f names, fixes, binds, type_occs, constraints));

fun map_fixes f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, f fixes, binds, type_occs, constraints));

fun map_binds f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, f binds, type_occs, constraints));

fun map_type_occs f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, binds, f type_occs, constraints));

fun map_constraints f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
  (is_body, names, fixes, binds, type_occs, f constraints));

fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);

val is_body = #is_body o rep_data;
fun set_body b = map_data (fn (_, names, fixes, binds, type_occs, constraints) =>
  (b, names, fixes, binds, type_occs, constraints));
fun restore_body ctxt = set_body (is_body ctxt);

val names_of = #names o rep_data;
val fixes_of = #fixes o rep_data;
val binds_of = #binds o rep_data;
val type_occs_of = #type_occs o rep_data;
val constraints_of = #constraints o rep_data;

val is_declared = Name.is_declared o names_of;
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);

fun add_fixed ctxt = Term.fold_aterms
  (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);



(** declarations **)

(* default sorts and types *)

fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1);

fun def_type ctxt pattern xi =
  let val {binds, constraints = (types, _), ...} = rep_data ctxt in
    (case Vartab.lookup types xi of
      NONE =>
        if pattern then NONE
        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
    | some => some)
  end;

val def_sort = Vartab.lookup o #2 o constraints_of;


(* names *)

val declare_type_names = map_names o
  fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I));

fun declare_names t =
  declare_type_names t #>
  map_names (fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t);


(* type occurrences *)

fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T;

val decl_type_occs = fold_term_types
  (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
    | _ => decl_type_occsT);

val declare_type_occsT = map_type_occs o fold_types decl_type_occsT;
val declare_type_occs = map_type_occs o decl_type_occs;


(* constraints *)

fun constrain_tvar (xi, S) =
  if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);

fun declare_constraints t = map_constraints (fn (types, sorts) =>
  let
    val types' = fold_aterms
      (fn Free (x, T) => Vartab.update ((x, ~1), T)
        | Var v => Vartab.update v
        | _ => I) t types;
    val sorts' = fold_types (fold_atyps
      (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
        | TVar v => constrain_tvar v
        | _ => I)) t sorts;
  in (types', sorts') end)
  #> declare_type_occsT t
  #> declare_type_names t;


(* common declarations *)

fun declare_internal t =
  declare_names t #>
  declare_type_occs t;

fun declare_term t =
  declare_internal t #>
  declare_constraints t;

val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);

val declare_thm = Thm.fold_terms declare_internal;
{'fraction_non_alphanumeric': 0.12409544883679206, 'fraction_numerical': 0.000717660427007954, 'mean_word_length': 3.5170178282009723, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 296, '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': '728359', 'n_tokens_mistral': 5820, 'n_tokens_neox': 5492, 'n_words': 1786}