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