# HG changeset patch # User wenzelm # Date 1537477518 -7200 # Node ID 287bb00371c1b069cbb1cebd9b6308b09ef19a02 # Parent e2858770997a5f44b0b971a0f8b9abe80aa00770# Parent cef000855cf4f8e6c354ef92c4516a4a9add099f merged diff -r e2858770997a -r 287bb00371c1 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Thu Sep 20 18:20:02 2018 +0100 +++ b/src/Pure/Thy/export_theory.ML Thu Sep 20 23:05:18 2018 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/Thy/export_theory.ML Author: Makarius -Export foundational theory content. +Export foundational theory content and locale/class structure. *) signature EXPORT_THEORY = @@ -13,28 +13,63 @@ structure Export_Theory: EXPORT_THEORY = struct -(* names for bound variables *) +(* standardization of variables: only frees and named bounds *) local - fun declare_names (Abs (_, _, b)) = declare_names b - | declare_names (t $ u) = declare_names t #> declare_names u - | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c) - | declare_names (Free (x, _)) = Name.declare x - | declare_names _ = I; + +fun declare_names (Abs (_, _, b)) = declare_names b + | declare_names (t $ u) = declare_names t #> declare_names u + | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c) + | declare_names (Free (x, _)) = Name.declare x + | declare_names _ = I; + +fun variant_abs bs (Abs (x, T, t)) = + let + val names = fold Name.declare bs (declare_names t Name.context); + val x' = #1 (Name.variant x names); + val t' = variant_abs (x' :: bs) t; + in Abs (x', T, t') end + | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u + | variant_abs _ t = t; + +in + +fun standard_vars used = + let + fun zero_var_indexes tm = + Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm; - fun variant_abs bs (Abs (x, T, t)) = - let - val names = fold Name.declare bs (declare_names t Name.context); - val x' = #1 (Name.variant x names); - val t' = variant_abs (x' :: bs) t; - in Abs (x', T, t') end - | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u - | variant_abs _ t = t; -in - val named_bounds = variant_abs []; + fun unvarifyT ty = ty |> Term.map_atyps + (fn TVar ((a, _), S) => TFree (a, S) + | T as TFree (a, _) => + if Name.is_declared used a then T + else raise TYPE (Logic.bad_fixed a, [ty], [])); + + fun unvarify tm = tm |> Term.map_aterms + (fn Var ((x, _), T) => Free (x, T) + | t as Free (x, _) => + if Name.is_declared used x then t + else raise TERM (Logic.bad_fixed x, [tm]) + | t => t); + + in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end; + +val standard_vars_global = standard_vars Name.context; + end; +(* free variables: not declared in the context *) + +val is_free = not oo Name.is_declared; + +fun add_frees used = + fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I); + +fun add_tfrees used = + (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); + + (* locale support *) fun locale_axioms thy loc = @@ -141,55 +176,58 @@ (* consts *) val encode_const = - let open XML.Encode Term_XML.Encode in - pair (option encode_infix) (pair (list string) (pair typ (option (term o named_bounds)))) - end; + let open XML.Encode Term_XML.Encode + in pair (option encode_infix) (pair (list string) (pair typ (option term))) end; fun export_const c (T, abbrev) = let val syntax = get_infix_const thy_ctxt c; val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts; - val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts); + val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts); val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T')); - in SOME (encode_const (syntax, (args, (T', abbrev')))) end; + in encode_const (syntax, (args, (T', abbrev'))) end; val _ = - export_entities "consts" export_const Sign.const_space + export_entities "consts" (SOME oo export_const) Sign.const_space (#constants (Consts.dest (Sign.consts_of thy))); (* axioms and facts *) - fun standard_prop_of raw_thm = + fun prop_of raw_thm = let val thm = raw_thm |> Thm.transfer thy |> Thm.check_hyps (Context.Theory thy) |> Thm.strip_shyps; val prop = thm - |> Thm.full_prop_of - |> Term_Subst.zero_var_indexes; + |> Thm.full_prop_of; in (Thm.extra_shyps thm, prop) end; - fun encode_prop (Ss, prop) = + fun encode_prop used (Ss, raw_prop) = let - val prop' = Logic.unvarify_global (named_bounds prop); - val typargs = rev (Term.add_tfrees prop' []); - val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss; - val args = rev (Term.add_frees prop' []); + val prop = standard_vars used raw_prop; + val args = rev (add_frees used prop []); + val typargs = rev (add_tfrees used prop []); + val used' = fold (Name.declare o #1) typargs used; + val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss; in - (sorts @ typargs, args, prop') |> + (sorts @ typargs, args, prop) |> let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) term end end; - val encode_fact = XML.Encode.list encode_prop o map standard_prop_of; + fun encode_axiom used t = encode_prop used ([], t); + + val encode_fact_single = encode_prop Name.context o prop_of; + val encode_fact_multi = XML.Encode.list (encode_prop Name.context) o map prop_of; val _ = - export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space - (Theory.axioms_of thy); + export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) + Theory.axiom_space (Theory.axioms_of thy); val _ = - export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of) + export_entities "facts" (K (SOME o encode_fact_multi)) + (Facts.space_of o Global_Theory.facts_of) (Facts.dest_static true [] (Global_Theory.facts_of thy)); @@ -197,13 +235,12 @@ val encode_class = let open XML.Encode Term_XML.Encode - in pair (list (pair string typ)) (list (term o named_bounds)) end; + in pair (list (pair string typ)) (list encode_fact_single) end; fun export_class name = (case try (Axclass.get_info thy) name of NONE => ([], []) - | SOME {params, axioms, ...} => - (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms)) + | SOME {params, axioms, ...} => (params, axioms)) |> encode_class |> SOME; val _ = @@ -231,18 +268,20 @@ (* locales *) - fun encode_locale loc ({type_params, params, ...}: Locale.content) = + fun encode_locale used = + let open XML.Encode Term_XML.Encode + in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end; + + fun export_locale loc ({type_params, params, ...}: Locale.content) = let val axioms = locale_axioms thy loc; val args = map #1 params; - val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ axioms) []); - val encode = - let open XML.Encode Term_XML.Encode - in triple (list (pair string sort)) (list (pair string typ)) (list term) end; - in encode (typargs, args, axioms) end; + val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params)); + val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context; + in encode_locale used (typargs, args, axioms) end; val _ = - export_entities "locales" (SOME oo encode_locale) Locale.locale_space + export_entities "locales" (SOME oo export_locale) Locale.locale_space (Locale.dest_locales thy); diff -r e2858770997a -r 287bb00371c1 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Thu Sep 20 18:20:02 2018 +0100 +++ b/src/Pure/Thy/export_theory.scala Thu Sep 20 23:05:18 2018 +0200 @@ -328,12 +328,12 @@ /* type classes */ sealed case class Class( - entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term]) + entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop]) { def cache(cache: Term.Cache): Class = Class(entity.cache(cache), params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), - axioms.map(cache.term(_))) + axioms.map(_.cache(cache))) } def read_classes(provider: Export.Provider): List[Class] = @@ -344,7 +344,7 @@ { import XML.Decode._ import Term_XML.Decode._ - pair(list(pair(string, typ)), list(term))(body) + pair(list(pair(string, typ)), list(decode_prop))(body) } Class(entity, params, axioms) }) @@ -356,13 +356,13 @@ entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], - axioms: List[Term.Term]) + axioms: List[Prop]) { def cache(cache: Term.Cache): Locale = Locale(entity.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), - axioms.map(cache.term(_))) + axioms.map(_.cache(cache))) } def read_locales(provider: Export.Provider): List[Locale] = @@ -373,7 +373,7 @@ { import XML.Decode._ import Term_XML.Decode._ - triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body) + triple(list(pair(string, sort)), list(pair(string, typ)), list(decode_prop))(body) } Locale(entity, typargs, args, axioms) }) diff -r e2858770997a -r 287bb00371c1 src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Sep 20 18:20:02 2018 +0100 +++ b/src/Pure/drule.ML Thu Sep 20 23:05:18 2018 +0200 @@ -220,7 +220,8 @@ fun zero_var_indexes_list [] = [] | zero_var_indexes_list ths = let - val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); + val (instT, inst) = + Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths); val tvars = fold Thm.add_tvars ths []; fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars); diff -r e2858770997a -r 287bb00371c1 src/Pure/logic.ML --- a/src/Pure/logic.ML Thu Sep 20 18:20:02 2018 +0100 +++ b/src/Pure/logic.ML Thu Sep 20 23:05:18 2018 +0200 @@ -80,6 +80,8 @@ val list_rename_params: string list -> term -> term val assum_pairs: int * term -> (term * term) list val assum_problems: int * term -> (term -> term) * term list * term + val bad_schematic: indexname -> string + val bad_fixed: string -> string val varifyT_global: typ -> typ val unvarifyT_global: typ -> typ val varify_types_global: term -> term diff -r e2858770997a -r 287bb00371c1 src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Thu Sep 20 18:20:02 2018 +0100 +++ b/src/Pure/term_subst.ML Thu Sep 20 23:05:18 2018 +0200 @@ -29,7 +29,7 @@ val instantiateT: ((indexname * sort) * typ) list -> typ -> typ val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term - val zero_var_indexes_inst: term list -> + val zero_var_indexes_inst: Name.context -> term list -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list val zero_var_indexes: term -> term val zero_var_indexes_list: term list -> term list @@ -211,21 +211,21 @@ val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used; in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end; -fun zero_var_indexes_inst ts = +fun zero_var_indexes_inst used ts = let val (instT, _) = TVars.fold (zero_var_inst TVar o #1) ((fold o fold_types o fold_atyps) (fn TVar v => TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty) - ([], Name.context); + ([], used); val (inst, _) = Vars.fold (zero_var_inst Var o #1) ((fold o fold_aterms) (fn Var (xi, T) => Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty) - ([], Name.context); + ([], used); in (instT, inst) end; -fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst ts)) ts; +fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts; val zero_var_indexes = singleton zero_var_indexes_list; end;