support for a soft-type system within the Isabelle logical framework;

--- a/src/Pure/Isar/proof.ML	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 16 15:39:32 2019 +0200
@@ -508,7 +508,8 @@
       |> map2 Conjunction.elim_balanced (map length goal_propss)
       handle THM _ => err_lost ();
     val _ =
-      Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
+      Unify.matches_list (Context.Proof ctxt)
+        (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (map Thm.prop_of (flat results))
         orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
 
     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss

--- a/src/Pure/Isar/proof_context.ML	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 16 15:39:32 2019 +0200
@@ -420,7 +420,8 @@
 fun augment t ctxt = ctxt
   |> not (Variable.is_body ctxt) ?
       Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t []))
-  |> Variable.declare_term t;
+  |> Variable.declare_term t
+  |> Soft_Type_System.augment t;
 
 
 

--- a/src/Pure/ROOT.ML	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 16 15:39:32 2019 +0200
@@ -104,6 +104,7 @@
 ML_file "context_position.ML";
 ML_file "System/options.ML";
 ML_file "config.ML";
+ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";

--- a/src/Pure/sign.ML	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/Pure/sign.ML	Tue Jul 16 15:39:32 2019 +0200
@@ -310,7 +310,9 @@
     val tm' = Term.map_types (certify_typ thy) tm;
     val T = type_check context tm';
     val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
-    val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
+    val tm'' = tm'
+      |> Consts.certify context (tsig_of thy) do_expand consts
+      |> Soft_Type_System.global_purge thy;
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
 fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/soft_type_system.ML	Tue Jul 16 15:39:32 2019 +0200
@@ -0,0 +1,79 @@
+(*  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;
+  val extend = I;
+  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;