1(*  Title:      Pure/soft_type_system.ML
2    Author:     Alexander Krauss
3    Author:     Makarius
4
5Support for a soft-type system within the Isabelle logical framework.
6*)
7
8signature SOFT_TYPE_SYSTEM =
9sig
10  type operations =
11    {augment: term -> Proof.context -> Proof.context,
12     implicit_vars: Proof.context -> term -> (string * typ) list,
13     purge: theory -> term -> term}
14  val setup: operations -> theory -> theory
15  val augment: term -> Proof.context -> Proof.context
16  val implicit_vars: Proof.context -> term -> (string * typ) list
17  val global_purge: theory -> term -> term
18  val purge: Proof.context -> term -> term
19end;
20
21structure Soft_Type_System: SOFT_TYPE_SYSTEM =
22struct
23
24(* operations *)
25
26type operations =
27  {
28    (*extend the proof context by additional information present in the
29      given term, e.g. assumptions about variables*)
30    augment: term -> Proof.context -> Proof.context,
31
32    (*variables from the term that are implicitly introduced into the
33      context via this statement*)
34    implicit_vars: Proof.context -> term -> (string * typ) list,
35
36    (*purge soft type annotations encoded in a term*)
37    purge: theory -> term -> term
38  };
39
40val no_operations: operations =
41 {augment = K I,
42  implicit_vars = K (K []),
43  purge = K I};
44
45
46(* theory data *)
47
48structure Data = Theory_Data
49(
50  type T = (operations * stamp) option;
51  val empty = NONE;
52  val extend = I;
53  fun merge (data as SOME (_, s), SOME (_, s')) =
54        if s = s' then data
55        else error "Cannot merge theories with different soft-type systems"
56    | merge data = merge_options data;
57);
58
59fun setup operations =
60  Data.map (fn data =>
61    (case data of
62      NONE => SOME (operations, stamp ())
63    | SOME _ => error "Duplicate setup of soft-type system"));
64
65
66(* get operations *)
67
68fun global_operations thy =
69  (case Data.get thy of SOME (ops, _) => ops | NONE => no_operations);
70
71val operations = global_operations o Proof_Context.theory_of;
72
73fun augment t ctxt = #augment (operations ctxt) t ctxt;
74fun implicit_vars ctxt t = #implicit_vars (operations ctxt) ctxt t;
75
76fun global_purge thy t = #purge (global_operations thy) thy t;
77val purge = global_purge o Proof_Context.theory_of;
78
79end;
80