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;
     1 (*  Title:      Pure/soft_type_system.ML
     2     Author:     Alexander Krauss
     3     Author:     Makarius
     4 
     5 Support for a soft-type system within the Isabelle logical framework.
     6 *)
     7 
     8 signature SOFT_TYPE_SYSTEM =
     9 sig
    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
    19 end;
    20 
    21 structure Soft_Type_System: SOFT_TYPE_SYSTEM =
    22 struct
    23 
    24 (* operations *)
    25 
    26 type 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 
    40 val no_operations: operations =
    41  {augment = K I,
    42   implicit_vars = K (K []),
    43   purge = K I};
    44 
    45 
    46 (* theory data *)
    47 
    48 structure 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 
    59 fun 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 
    68 fun global_operations thy =
    69   (case Data.get thy of SOME (ops, _) => ops | NONE => no_operations);
    70 
    71 val operations = global_operations o Proof_Context.theory_of;
    72 
    73 fun augment t ctxt = #augment (operations ctxt) t ctxt;
    74 fun implicit_vars ctxt t = #implicit_vars (operations ctxt) ctxt t;
    75 
    76 fun global_purge thy t = #purge (global_operations thy) thy t;
    77 val purge = global_purge o Proof_Context.theory_of;
    78 
    79 end;