# HG changeset patch # User wenzelm # Date 1563284372 -7200 # Node ID b2bedb022a75804bf11800829fe55aa9e5fb301a # Parent 6d96ee03b62e823293ea20fc72f7950ffa08a672 support for a soft-type system within the Isabelle logical framework; diff -r 6d96ee03b62e -r b2bedb022a75 src/Pure/Isar/proof.ML --- 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 diff -r 6d96ee03b62e -r b2bedb022a75 src/Pure/Isar/proof_context.ML --- 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; diff -r 6d96ee03b62e -r b2bedb022a75 src/Pure/ROOT.ML --- 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"; diff -r 6d96ee03b62e -r b2bedb022a75 src/Pure/sign.ML --- 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; diff -r 6d96ee03b62e -r b2bedb022a75 src/Pure/soft_type_system.ML --- /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;