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