(* Title: Pure/Isar/proof_context.ML
Author: Markus Wenzel, TU Muenchen
The key concept of Isar proof contexts: elevates primitive local
reasoning Gamma |- phi to a structured concept, with generic context
elements. See also structure Variable and Assumption.
*)
signature PROOF_CONTEXT =
sig
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
val get_global: theory -> string -> Proof.context
type mode
val mode_default: mode
val mode_pattern: mode
val mode_schematic: mode
val mode_abbrev: mode
val set_mode: mode -> Proof.context -> Proof.context
val get_mode: Proof.context -> mode
val restore_mode: Proof.context -> Proof.context -> Proof.context
val abbrev_mode: Proof.context -> bool
val syn_of: Proof.context -> Syntax.syntax
val tsig_of: Proof.context -> Type.tsig
val set_defsort: sort -> Proof.context -> Proof.context
val default_sort: Proof.context -> indexname -> sort
val arity_sorts: Proof.context -> string -> sort -> sort list
val consts_of: Proof.context -> Consts.T
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
val full_name: Proof.context -> binding -> string
val get_scope: Proof.context -> Binding.scope option
val new_scope: Proof.context -> Binding.scope * Proof.context
val private_scope: Binding.scope -> Proof.context -> Proof.context
val private: Position.T -> Proof.context -> Proof.context
val qualified_scope: Binding.scope -> Proof.context -> Proof.context
val qualified: Position.T -> Proof.context -> Proof.context
val concealed: Proof.context -> Proof.context
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
val const_space: Proof.context -> Name_Space.T
val defs_context: Proof.context -> Defs.context
val intern_class: Proof.context -> xstring -> string
val intern_type: Proof.context -> xstring -> string
val intern_const: Proof.context -> xstring -> string
val extern_class: Proof.context -> string -> xstring
val markup_class: Proof.context -> string -> string
val pretty_class: Proof.context -> string -> Pretty.T
val extern_type: Proof.context -> string -> xstring
val markup_type: Proof.context -> string -> string
val pretty_type: Proof.context -> string -> Pretty.T
val extern_const: Proof.context -> string -> xstring
val markup_const: Proof.context -> string -> string
val pretty_const: Proof.context -> string -> Pretty.T
val transfer: theory -> Proof.context -> Proof.context
val transfer_facts: theory -> Proof.context -> Proof.context
val background_theory: (theory -> theory) -> Proof.context -> Proof.context
val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val facts_of: Proof.context -> Facts.T
val facts_of_fact: Proof.context -> string -> Facts.T
val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
val read_class: Proof.context -> string -> class
val read_typ: Proof.context -> string -> typ
val read_typ_syntax: Proof.context -> string -> typ
val read_typ_abbrev: Proof.context -> string -> typ
val cert_typ: Proof.context -> typ -> typ
val cert_typ_syntax: Proof.context -> typ -> typ
val cert_typ_abbrev: Proof.context -> typ -> typ
val infer_type: Proof.context -> string * typ -> typ
val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
xstring * Position.T -> typ * Position.report list
val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
val consts_completion_message: Proof.context -> xstring * Position.T list -> string
val check_const: {proper: bool, strict: bool} -> Proof.context ->
xstring * Position.T list -> term * Position.report list
val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
val read_arity: Proof.context -> xstring * string list * string -> arity
val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
val prepare_sortsT: Proof.context -> typ list -> string list * typ list
val prepare_sorts: Proof.context -> term list -> string list * term list
val check_tfree: Proof.context -> string * sort -> string * sort
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
val show_abbrevs_raw: Config.raw
val show_abbrevs: bool Config.T
val expand_abbrevs: Proof.context -> term -> term
val cert_term: Proof.context -> term -> term
val cert_prop: Proof.context -> term -> term
val def_type: Proof.context -> indexname -> typ option
val standard_typ_check: Proof.context -> typ list -> typ list
val standard_term_check_finish: Proof.context -> term list -> term list
val standard_term_uncheck: Proof.context -> term list -> term list
val goal_export: Proof.context -> Proof.context -> thm list -> thm list
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val norm_export_morphism: Proof.context -> Proof.context -> morphism
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
val match_bind: bool -> (term list * term) list -> Proof.context ->
term list * Proof.context
val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->
term list * Proof.context
val cert_propp: Proof.context -> (term * term list) list list ->
(term list list * (indexname * term) list)
val read_propp: Proof.context -> (string * string list) list list ->
(term list list * (indexname * term) list)
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option
val dynamic_facts_dummy: bool Config.T
val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
val get_fact: Proof.context -> Facts.ref -> thm list
val get_fact_single: Proof.context -> Facts.ref -> thm
val get_thms: Proof.context -> xstring -> thm list
val get_thm: Proof.context -> xstring -> thm
val set_stmt: bool -> Proof.context -> Proof.context
val restore_stmt: Proof.context -> Proof.context -> Proof.context
val add_thms_dynamic: binding * (Context.generic -> thm list) ->
Proof.context -> string * Proof.context
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
val read_var: binding * string option * mixfix -> Proof.context ->
(binding * typ option * mixfix) * Proof.context
val cert_var: binding * typ option * mixfix -> Proof.context ->
(binding * typ option * mixfix) * Proof.context
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
string list * Proof.context
val add_assms: Assumption.export ->
(Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_assms_cmd: Assumption.export ->
(Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val check_case: Proof.context -> bool ->
string * Position.T -> binding option list -> Rule_Cases.T
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
Context.generic -> Context.generic
val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
val class_alias: binding -> class -> Proof.context -> Proof.context
val type_alias: binding -> string -> Proof.context -> Proof.context
val const_alias: binding -> string -> Proof.context -> Proof.context
val fact_alias: binding -> string -> Proof.context -> Proof.context
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
val generic_add_abbrev: string -> binding * term -> Context.generic ->
(term * term) * Context.generic
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
val cert_stmt:
(binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
(((binding * typ option * mixfix) * (string * term)) list * term list list *
(indexname * term) list * (indexname * term) list) * Proof.context
val read_stmt:
(binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
(((binding * typ option * mixfix) * (string * term)) list * term list list *
(indexname * term) list * (indexname * term) list) * Proof.context
val cert_statement: (binding * typ option * mixfix) list ->
(term * term list) list list -> (term * term list) list list -> Proof.context ->
((string * term) list * term list list * term list list * (indexname * term option) list) *
Proof.context
val read_statement: (binding * string option * mixfix) list ->
(string * string list) list list -> (string * string list) list list -> Proof.context ->
((string * term) list * term list list * term list list * (indexname * term option) list) *
Proof.context
val print_syntax: Proof.context -> unit
val print_abbrevs: bool -> Proof.context -> unit
val pretty_term_bindings: Proof.context -> Pretty.T list
val pretty_local_facts: bool -> Proof.context -> Pretty.T list
val print_local_facts: bool -> Proof.context -> unit
val pretty_cases: Proof.context -> Pretty.T list
val print_cases_proof: Proof.context -> Proof.context -> string
val debug: bool Config.T
val verbose: bool Config.T
val pretty_ctxt: Proof.context -> Pretty.T list
val pretty_context: Proof.context -> Pretty.T list
end;
structure Proof_Context: PROOF_CONTEXT =
struct
val theory_of = Proof_Context.theory_of;
val init_global = Proof_Context.init_global;
val get_global = Proof_Context.get_global;
(** inner syntax mode **)
datatype mode =
Mode of
{pattern: bool, (*pattern binding schematic variables*)
schematic: bool, (*term referencing loose schematic variables*)
abbrev: bool}; (*abbrev mode -- no normalization*)
fun make_mode (pattern, schematic, abbrev) =
Mode {pattern = pattern, schematic = schematic, abbrev = abbrev};
val mode_default = make_mode (false, false, false);
val mode_pattern = make_mode (true, false, false);
val mode_schematic = make_mode (false, true, false);
val mode_abbrev = make_mode (false, false, true);
(** Isar proof context information **)
type cases = (Rule_Cases.T * {legacy: bool}) Name_Space.table;
val empty_cases: cases = Name_Space.empty_table Markup.caseN;
datatype data =
Data of
{mode: mode, (*inner syntax mode*)
syntax: Local_Syntax.T, (*local syntax*)
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
facts: Facts.T, (*local facts, based on initial global facts*)
cases: cases}; (*named case contexts: case, legacy, running index*)
fun make_data (mode, syntax, tsig, consts, facts, cases) =
Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
structure Data = Proof_Data
(
type T = data;
fun init thy =
make_data (mode_default,
Local_Syntax.init thy,
(Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
(Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
Global_Theory.facts_of thy,
empty_cases);
);
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
fun map_data_result f ctxt =
let
val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt;
val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data;
in (res, Data.put data' ctxt) end;
fun map_data f = snd o map_data_result (pair () o f);
fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
(mode, syntax, tsig, consts, facts, cases));
fun map_syntax f =
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, f syntax, tsig, consts, facts, cases));
fun map_syntax_idents f ctxt =
let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in
ctxt
|> map_syntax (K syntax')
|> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')
end;
fun map_tsig f =
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, syntax, f tsig, consts, facts, cases));
fun map_consts f =
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, syntax, tsig, f consts, facts, cases));
fun map_facts_result f =
map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
let val (res, facts') = f facts
in (res, (mode, syntax, tsig, consts, facts', cases)) end);
fun map_facts f = snd o map_facts_result (pair () o f);
fun map_cases f =
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, syntax, tsig, consts, facts, f cases));
val get_mode = #mode o rep_data;
val restore_mode = set_mode o get_mode;
val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
val syntax_of = #syntax o rep_data;
val syn_of = Local_Syntax.syn_of o syntax_of;
val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
val tsig_of = #1 o #tsig o rep_data;
val set_defsort = map_tsig o apfst o Type.set_defsort;
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
val consts_of = #1 o #consts o rep_data;
val cases_of = #cases o rep_data;
(* naming *)
val naming_of = Name_Space.naming_of o Context.Proof;
val map_naming = Context.proof_map o Name_Space.map_naming;
val restore_naming = map_naming o K o naming_of;
val full_name = Name_Space.full_name o naming_of;
val get_scope = Name_Space.get_scope o naming_of;
fun new_scope ctxt =
let
val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
val ctxt' = map_naming (K naming') ctxt;
in (scope, ctxt') end;
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
val qualified_scope = map_naming o Name_Space.qualified_scope;
val qualified = map_naming o Name_Space.qualified;
val concealed = map_naming Name_Space.concealed;
(* name spaces *)
val class_space = Type.class_space o tsig_of;
val type_space = Type.type_space o tsig_of;
val const_space = Consts.space_of o consts_of;
fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
val intern_class = Name_Space.intern o class_space;
val intern_type = Name_Space.intern o type_space;
val intern_const = Name_Space.intern o const_space;
fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup;
fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str;
fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str;
fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str;
(* theory transfer *)
fun transfer_syntax thy ctxt = ctxt |>
map_syntax (Local_Syntax.rebuild thy) |>
map_tsig (fn tsig as (local_tsig, global_tsig) =>
let val thy_tsig = Sign.tsig_of thy in
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*)
end) |>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
if Consts.eq_consts (thy_consts, global_consts) then consts
else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*)
end);
fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
fun transfer_facts thy =
map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
fun background_theory_result f ctxt =
let val (res, thy') = f (theory_of ctxt)
in (res, ctxt |> transfer thy') end;
(* hybrid facts *)
val facts_of = #facts o rep_data;
fun facts_of_fact ctxt name =
let
val local_facts = facts_of ctxt;
val global_facts = Global_Theory.facts_of (theory_of ctxt);
in
if Facts.defined local_facts name
then local_facts else global_facts
end;
fun markup_extern_fact ctxt name =
let
val facts = facts_of_fact ctxt name;
val (markup, xname) = Facts.markup_extern ctxt facts name;
val markups =
if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name]
else [markup];
in (markups, xname) end;
(** pretty printing **)
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
fun pretty_fact_name ctxt a =
Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"];
fun pretty_fact ctxt =
let
val pretty_thm = Thm.pretty_thm ctxt;
val pretty_thms = map (Thm.pretty_thm_item ctxt);
in
fn ("", [th]) => pretty_thm th
| ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
| (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th]
| (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths))
end;
(** prepare types **)
(* classes *)
fun check_class ctxt (xname, pos) =
let
val tsig = tsig_of ctxt;
val class_space = Type.class_space tsig;
val name = Type.cert_class tsig (Name_Space.intern class_space xname)
handle TYPE (msg, _, _) =>
error (msg ^ Position.here pos ^
Markup.markup_report (Completion.reported_text
(Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
val reports =
if Context_Position.is_reported ctxt pos
then [(pos, Name_Space.markup class_space name)] else [];
in (name, reports) end;
fun read_class ctxt text =
let
val source = Syntax.read_input text;
val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
val _ = Position.reports reports;
in c end;
(* types *)
fun read_typ_mode mode ctxt s =
Syntax.read_typ (Type.set_mode mode ctxt) s;
val read_typ = read_typ_mode Type.mode_default;
val read_typ_syntax = read_typ_mode Type.mode_syntax;
val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
fun cert_typ_mode mode ctxt T =
Type.cert_typ_mode mode (tsig_of ctxt) T
handle TYPE (msg, _, _) => error msg;
val cert_typ = cert_typ_mode Type.mode_default;
val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
(** prepare terms and propositions **)
(* inferred types of parameters *)
fun infer_type ctxt x =
Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
fun inferred_param x ctxt =
let val p = (x, infer_type ctxt (x, dummyT))
in (p, ctxt |> Variable.declare_term (Free p)) end;
fun inferred_fixes ctxt =
fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
(* type names *)
fun check_type_name {proper, strict} ctxt (c, pos) =
if Lexicon.is_tid c then
if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos)
else
let
val reports =
if Context_Position.is_reported ctxt pos
then [(pos, Markup.tfree)] else [];
in (TFree (c, default_sort ctxt (c, ~1)), reports) end
else
let
val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
val args =
(case decl of
Type.LogicalType n => n
| Type.Abbreviation (vs, _, _) => if strict then err () else length vs
| Type.Nonterminal => if strict then err () else 0);
in (Type (d, replicate args dummyT), reports) end;
fun read_type_name ctxt flags text =
let
val source = Syntax.read_input text;
val (T, reports) =
check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
val _ = Position.reports reports;
in T end;
(* constant names *)
fun consts_completion_message ctxt (c, ps) =
ps |> map (fn pos =>
Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
|> Completion.reported_text)
|> implode
|> Markup.markup_report;
fun check_const {proper, strict} ctxt (c, ps) =
let
val _ =
Name.reject_internal (c, ps) handle ERROR msg =>
error (msg ^ consts_completion_message ctxt (c, ps));
fun err msg = error (msg ^ Position.here_list ps);
val consts = consts_of ctxt;
val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
val (t, reports) =
(case (fixed, Variable.lookup_const ctxt c) of
(SOME x, NONE) =>
let
val reports = ps
|> filter (Context_Position.is_reported ctxt)
|> map (fn pos =>
(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
in (Free (x, infer_type ctxt (x, dummyT)), reports) end
| (_, SOME d) =>
let
val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
val reports = ps
|> filter (Context_Position.is_reported ctxt)
|> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
in (Const (d, T), reports) end
| _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
val _ =
(case (strict, t) of
(true, Const (d, _)) =>
(ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
| _ => ());
in (t, reports) end;
fun read_const ctxt flags text =
let
val source = Syntax.read_input text;
val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
val _ = Position.reports reports;
in t end;
(* type arities *)
local
fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
in
val read_arity =
prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
end;
(* read_term *)
fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
val read_term_pattern = read_term_mode mode_pattern;
val read_term_schematic = read_term_mode mode_schematic;
val read_term_abbrev = read_term_mode mode_abbrev;
(* local abbreviations *)
local
fun certify_consts ctxt =
Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
(not (abbrev_mode ctxt)) (consts_of ctxt);
fun expand_binds ctxt =
let
val Mode {pattern, schematic, ...} = get_mode ctxt;
fun reject_schematic (t as Var _) =
error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
| reject_schematic (Abs (_, _, t)) = reject_schematic t
| reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
| reject_schematic _ = ();
in
if pattern then I
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
end;
in
fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt;
end;
val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true);
val show_abbrevs = Config.bool show_abbrevs_raw;
fun contract_abbrevs ctxt t =
let
val thy = theory_of ctxt;
val consts = consts_of ctxt;
val Mode {abbrev, ...} = get_mode ctxt;
val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
in
if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
else Pattern.rewrite_term_top thy [] [match_abbrev] t
end;
(* patterns *)
fun prepare_patternT ctxt T =
let
val Mode {pattern, schematic, ...} = get_mode ctxt;
val _ =
pattern orelse schematic orelse
T |> Term.exists_subtype
(fn T as TVar (xi, _) =>
not (Type_Infer.is_param xi) andalso
error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
| _ => false)
in T end;
local
val dummies =
Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false)));
fun check_dummies ctxt t =
if Config.get ctxt dummies then t
else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
in
val allow_dummies = Config.put dummies true;
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
Type_Infer.fixate ctxt pattern #>
pattern ? Variable.polymorphic ctxt #>
(map o Term.map_types) (prepare_patternT ctxt) #>
(if pattern then prepare_dummies else map (check_dummies ctxt))
end;
end;
(* sort constraints *)
local
fun prepare_sorts_env ctxt tys =
let
val tsig = tsig_of ctxt;
val defaultS = Type.defaultS tsig;
val dummy_var = ("'_dummy_", ~1);
fun constraint (xi, raw_S) env =
let val (ps, S) = Term_Position.decode_positionS raw_S in
if xi = dummy_var orelse S = dummyS then env
else
Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
handle Vartab.DUP _ =>
error ("Inconsistent sort constraints for type variable " ^
quote (Term.string_of_vname' xi) ^ Position.here_list ps)
end;
val env =
(fold o fold_atyps)
(fn TFree (x, S) => constraint ((x, ~1), S)
| TVar v => constraint v
| _ => I) tys Vartab.empty;
fun get_sort xi raw_S =
if xi = dummy_var then
Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S))
else
(case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
(NONE, NONE) => defaultS
| (NONE, SOME S) => S
| (SOME S, NONE) => S
| (SOME S, SOME S') =>
if Type.eq_sort tsig (S, S') then S'
else
error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^