(* Title: Pure/soft_type_system.ML
Author: Alexander Krauss
Author: Makarius
Support for a soft-type system within the Isabelle logical framework.
*)
signature SOFT_TYPE_SYSTEM =
sig
type operations =
{augment: term -> Proof.context -> Proof.context,
implicit_vars: Proof.context -> term -> (string * typ) list,
purge: theory -> term -> term}
val setup: operations -> theory -> theory
val augment: term -> Proof.context -> Proof.context
val implicit_vars: Proof.context -> term -> (string * typ) list
val global_purge: theory -> term -> term
val purge: Proof.context -> term -> term
end;
structure Soft_Type_System: SOFT_TYPE_SYSTEM =
struct
(* operations *)
type operations =
{
(*extend the proof context by additional information present in the
given term, e.g. assumptions about variables*)
augment: term -> Proof.context -> Proof.context,
(*variables from the term that are implicitly introduced into the
context via this statement*)
implicit_vars: Proof.context -> term -> (string * typ) list,
(*purge soft type annotations encoded in a term*)
purge: theory -> term -> term
};
val no_operations: operations =
{augment = K I,
implicit_vars = K (K []),
purge = K I};
(* theory data *)
structure Data = Theory_Data
(
type T = (operations * stamp) option;
val empty = NONE;
fun merge (data as SOME (_, s), SOME (_, s')) =
if s = s' then data
else error "Cannot merge theories with different soft-type systems"
| merge data = merge_options data;
);
fun setup operations =
Data.map (fn data =>
(case data of
NONE => SOME (operations, stamp ())
| SOME _ => error "Duplicate setup of soft-type system"));
(* get operations *)
fun global_operations thy =
(case Data.get thy of SOME (ops, _) => ops | NONE => no_operations);
val operations = global_operations o Proof_Context.theory_of;
fun augment t ctxt = #augment (operations ctxt) t ctxt;
fun implicit_vars ctxt t = #implicit_vars (operations ctxt) ctxt t;
fun global_purge thy t = #purge (global_operations thy) thy t;
val purge = global_purge o Proof_Context.theory_of;
end;