# HG changeset patch # User wenzelm # Date 1443217284 -7200 # Node ID 28eb608b9b5902e36a7b134118fba9b5ff4f76a7 # Parent b77bf45efe21c9da659a94d4bdcd19b0b8d90cda# Parent 64a5bce1f49859f67bf459a1f1c9183e226b87f1 merged diff -r b77bf45efe21 -r 28eb608b9b59 NEWS --- a/NEWS Fri Sep 25 16:54:31 2015 +0200 +++ b/NEWS Fri Sep 25 23:41:24 2015 +0200 @@ -177,6 +177,9 @@ *** Pure *** +* Command 'print_definitions' prints dependencies of definitional +specifications. This functionality used to be part of 'print_theory'. + * The vacuous fact "TERM x" may be established "by fact" or as `TERM x` as well, not just "by this" or "." as before. @@ -194,6 +197,13 @@ *** HOL *** +* The 'typedef' command has been upgraded from a partially checked +"axiomatization", to a full definitional specification that takes the +global collection of overloaded constant / type definitions into +account. Type definitions with open dependencies on overloaded +definitions need to be specified as "typedef (overloaded)". This +provides extra robustness in theory construction. Rare INCOMPATIBILITY. + * Qualification of various formal entities in the libraries is done more uniformly via "context begin qualified definition ... end" instead of old-style "hide_const (open) ...". Consequently, both the defined @@ -319,6 +329,10 @@ *** ML *** +* The auxiliary module Pure/display.ML has been eliminated. Its +elementary thm print operations are now in Pure/more_thm.ML and thus +called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. + * Simproc programming interfaces have been simplified: Simplifier.make_simproc and Simplifier.define_simproc supersede various forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that diff -r b77bf45efe21 -r 28eb608b9b59 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Sep 25 23:41:24 2015 +0200 @@ -662,12 +662,12 @@ binding * term -> theory -> (string * thm) * theory"} \\ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory"} \\ - @{index_ML Thm.add_def: "Proof.context -> bool -> bool -> + @{index_ML Thm.add_def: "Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Theory.add_deps: "Proof.context -> string -> - string * typ -> (string * typ) list -> theory -> theory"} \\ + @{index_ML Theory.add_deps: "Defs.context -> string -> + Defs.entry -> Defs.entry list -> theory -> theory"} \\ \end{mldecls} \begin{description} @@ -766,7 +766,7 @@ \item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\ \<^vec>d\<^sub>\"} declares dependencies of a named specification for constant @{text "c\<^sub>\"}, relative to existing specifications for constants @{text - "\<^vec>d\<^sub>\"}. + "\<^vec>d\<^sub>\"}. This also works for type constructors. \end{description} \ diff -r b77bf45efe21 -r 28eb608b9b59 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 23:41:24 2015 +0200 @@ -932,7 +932,7 @@ \end{matharray} @{rail \ - @@{command (HOL) record} @{syntax typespec_sorts} '=' \ + @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \ (@{syntax type} '+')? (constdecl +) ; constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? @@ -1100,61 +1100,90 @@ text \See @{file "~~/src/HOL/ex/Records.thy"}, for example.\ -section \Typedef axiomatization \label{sec:hol-typedef}\ +section \Semantic subtype definitions \label{sec:hol-typedef}\ text \ \begin{matharray}{rcl} @{command_def (HOL) "typedef"} & : & @{text "local_theory \ proof(prove)"} \\ \end{matharray} - A Gordon/HOL-style type definition is a certain axiom scheme that - identifies a new type with a subset of an existing type. More - precisely, the new type is defined by exhibiting an existing type - @{text \}, a set @{text "A :: \ set"}, and a theorem that proves - @{prop "\x. x \ A"}. Thus @{text A} is a non-empty subset of @{text - \}, and the new type denotes this subset. New functions are - postulated that establish an isomorphism between the new type and - the subset. In general, the type @{text \} may involve type - variables @{text "\\<^sub>1, \, \\<^sub>n"} which means that the type definition - produces a type constructor @{text "(\\<^sub>1, \, \\<^sub>n) t"} depending on - those type arguments. - - The axiomatization can be considered a ``definition'' in the sense of the - particular set-theoretic interpretation of HOL @{cite pitts93}, where the - universe of types is required to be downwards-closed wrt.\ arbitrary - non-empty subsets. Thus genuinely new types introduced by @{command - "typedef"} stay within the range of HOL models by construction. - - In contrast, the command @{command_ref type_synonym} from Isabelle/Pure - merely introduces syntactic abbreviations, without any logical - significance. Thus it is more faithful to the idea of a genuine type - definition, but less powerful in practice. + A type definition identifies a new type with a non-empty subset of an + existing type. More precisely, the new type is defined by exhibiting an + existing type @{text \}, a set @{text "A :: \ set"}, and proving @{prop + "\x. x \ A"}. Thus @{text A} is a non-empty subset of @{text \}, and the + new type denotes this subset. New functions are postulated that establish + an isomorphism between the new type and the subset. In general, the type + @{text \} may involve type variables @{text "\\<^sub>1, \, \\<^sub>n"} which means + that the type definition produces a type constructor @{text "(\\<^sub>1, \, \\<^sub>n) + t"} depending on those type arguments. @{rail \ - @@{command (HOL) typedef} abs_type '=' rep_set + @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set + ; + @{syntax_def "overloaded"}: ('(' @'overloaded' ')') ; abs_type: @{syntax typespec_sorts} @{syntax mixfix}? ; rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? \} + To understand the concept of type definition better, we need to recount + its somewhat complex history. The HOL logic goes back to the ``Simple + Theory of Types'' (STT) of A. Church @{cite "church40"}, which is further + explained in the book by P. Andrews @{cite "andrews86"}. The overview + article by W. Farmer @{cite "Farmer:2008"} points out the ``seven + virtues'' of this relatively simple family of logics. STT has only ground + types, without polymorphism and without type definitions. + + \medskip M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by + adding schematic polymorphism (type variables and type constructors) and a + facility to introduce new types as semantic subtypes from existing types. + This genuine extension of the logic was explained semantically by A. Pitts + in the book of the original Cambridge HOL88 system @{cite "pitts93"}. Type + definitions work in this setting, because the general model-theory of STT + is restricted to models that ensure that the universe of type + interpretations is closed by forming subsets (via predicates taken from + the logic). + + \medskip Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded + constant definitions @{cite "Wenzel:1997:TPHOL" and + "Haftmann-Wenzel:2006:classes"}, which are actually a concept of + Isabelle/Pure and do not depend on particular set-theoretic semantics of + HOL. Over many years, there was no formal checking of semantic type + definitions in Isabelle/HOL versus syntactic constant definitions in + Isabelle/Pure. So the @{command typedef} command was described as + ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some + local checks of the given type and its representing set. + + Recent clarification of overloading in the HOL logic proper @{cite + "Kuncar-Popescu:2015"} demonstrate how the dissimilar concepts of constant + definitions versus type definitions may be understood uniformly. This + requires an interpretation of Isabelle/HOL that substantially reforms the + set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic + view on polymorphism and interpreting only ground types in the + set-theoretic sense of HOL88. Moreover, type-constructors may be + explicitly overloaded, e.g.\ by making the subset depend on type-class + parameters (cf.\ \secref{sec:class}). This is semantically like a + dependent type: the meaning relies on the operations provided by different + type-class instances. + \begin{description} - \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} produces an - axiomatization (\secref{sec:axiomatizations}) for a type definition in the - background theory of the current context, depending on a non-emptiness - result of the set @{text A} that needs to be proven here. The set @{text - A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} as specified on the - LHS, but no term variables. - - Even though a local theory specification, the newly introduced type - constructor cannot depend on parameters or assumptions of the - context: this is structurally impossible in HOL. In contrast, the - non-emptiness proof may use local assumptions in unusual situations, - which could result in different interpretations in target contexts: - the meaning of the bijection between the representing set @{text A} - and the new type @{text t} may then change in different application - contexts. + \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} defines a + new type @{text "(\\<^sub>1, \, \\<^sub>n) t"} from the set @{text A} over an existing + type. The set @{text A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} + as specified on the LHS, but no term variables. Non-emptiness of @{text A} + needs to be proven on the spot, in order to turn the internal conditional + characterization into usable theorems. + + The ``@{text "(overloaded)"}'' option allows the @{command + "typedef"} specification to depend on constants that are not (yet) + specified and thus left open as parameters, e.g.\ type-class parameters. + + Within a local theory specification, the newly introduced type constructor + cannot depend on parameters or assumptions of the context: this is + syntactically impossible in HOL. The non-emptiness proof may formally + depend on local assumptions, but this has little practical relevance. For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced type @{text t} is accompanied by a pair of morphisms to relate it to @@ -1163,11 +1192,11 @@ Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification allows to provide alternative names. - The core axiomatization uses the locale predicate @{const - type_definition} as defined in Isabelle/HOL. Various basic - consequences of that are instantiated accordingly, re-using the - locale facts with names derived from the new type constructor. Thus - the generic @{thm type_definition.Rep} is turned into the specific + The logical characterization of @{command typedef} uses the predicate of + locale @{const type_definition} that is defined in Isabelle/HOL. Various + basic consequences of that are instantiated accordingly, re-using the + locale facts with names derived from the new type constructor. Thus the + generic theorem @{thm type_definition.Rep} is turned into the specific @{text "Rep_t"}, for example. Theorems @{thm type_definition.Rep}, @{thm @@ -1191,27 +1220,8 @@ subsubsection \Examples\ -text \Type definitions permit the introduction of abstract data - types in a safe way, namely by providing models based on already - existing types. Given some abstract axiomatic description @{text P} - of a type, this involves two steps: - - \begin{enumerate} - - \item Find an appropriate type @{text \} and subset @{text A} which - has the desired properties @{text P}, and make a type definition - based on this representation. - - \item Prove that @{text P} holds for @{text \} by lifting @{text P} - from the representation. - - \end{enumerate} - - You can later forget about the representation and work solely in - terms of the abstract properties @{text P}. - - \medskip The following trivial example pulls a three-element type - into existence within the formal logical environment of HOL.\ +text \The following trivial example pulls a three-element type into +existence within the formal logical environment of Isabelle/HOL.\ (*<*)experiment begin(*>*) typedef three = "{(True, True), (True, False), (False, True)}" @@ -1299,8 +1309,9 @@ \end{matharray} @{rail \ - @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '=' - quot_type \ quot_morphisms? quot_parametric? + @@{command (HOL) quotient_type} @{syntax "overloaded"}? \ + @{syntax typespec} @{syntax mixfix}? '=' quot_type \ + quot_morphisms? quot_parametric? ; quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term} ; diff -r b77bf45efe21 -r 28eb608b9b59 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Sep 25 23:41:24 2015 +0200 @@ -462,6 +462,7 @@ text \ \begin{matharray}{rcl} @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -475,6 +476,7 @@ @{rail \ (@@{command print_theory} | + @@{command print_definitions} | @@{command print_methods} | @@{command print_attributes} | @@{command print_theorems} | @@ -504,6 +506,12 @@ \item @{command "print_theory"} prints the main logical content of the background theory; the ``@{text "!"}'' option indicates extra verbosity. + \item @{command "print_definitions"} prints dependencies of definitional + specifications within the background theory, which may be constants + \secref{sec:consts} or types (\secref{sec:types-pure}, + \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra + verbosity. + \item @{command "print_methods"} prints all proof methods available in the current theory context; the ``@{text "!"}'' option indicates extra verbosity. diff -r b77bf45efe21 -r 28eb608b9b59 src/Doc/manual.bib --- a/src/Doc/manual.bib Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Doc/manual.bib Fri Sep 25 23:41:24 2015 +0200 @@ -601,6 +601,17 @@ year = 1993, pages = {213-248}} +@article{Farmer:2008, + author = {William M. Farmer}, + title = {The seven virtues of simple type theory}, + journal = {J. Applied Logic}, + volume = {6}, + number = {3}, + pages = {267--286}, + year = {2008}, + url = {http://dx.doi.org/10.1016/j.jal.2007.11.001}, +} + @InProceedings{felty91a, Author = {Amy Felty}, Title = {A Logic Program for Transforming Sequent Proofs to Natural @@ -679,6 +690,14 @@ publisher = CUP, note = {Translated by Yves Lafont and Paul Taylor}} +@TechReport{Gordon:1985:HOL, + author = {M. J. C. Gordon}, + title = {{HOL}: A machine oriented formulation of higher order logic}, + institution = {University of Cambridge Computer Laboratory}, + year = 1985, + number = 68 +} + @Book{mgordon-hol, editor = {M. J. C. Gordon and T. F. Melham}, title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, @@ -978,6 +997,20 @@ note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} } +@inproceedings{Kuncar-Popescu:2015, + author = {Ondrej Kuncar and Andrei Popescu}, + title = {A Consistent Foundation for {Isabelle/HOL}}, + editor = {Christian Urban and Xingyuan Zhang}, + booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} + 2015, Nanjing, China, August 24-27, 2015, Proceedings}, + year = {2015}, + url = {http://dx.doi.org/10.1007/978-3-319-22102-1_16}, + series = {Lecture Notes in Computer Science}, + volume = {9236}, + publisher = {Springer}, + year = {2015}, +} + @Book{kunen80, author = {Kenneth Kunen}, title = {Set Theory: An Introduction to Independence Proofs}, diff -r b77bf45efe21 -r 28eb608b9b59 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 23:41:24 2015 +0200 @@ -151,7 +151,7 @@ fun check_syntax ctxt thm expected = let val obtained = - Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm; + Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm; in if obtained <> expected then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.") diff -r b77bf45efe21 -r 28eb608b9b59 src/FOLP/classical.ML --- a/src/FOLP/classical.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/FOLP/classical.ML Fri Sep 25 23:41:24 2015 +0200 @@ -124,10 +124,10 @@ fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = writeln (cat_lines - (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @ - ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @ - ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @ - ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs)); + (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @ + ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @ + ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @ + ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs)); fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; diff -r b77bf45efe21 -r 28eb608b9b59 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/FOLP/simp.ML Fri Sep 25 23:41:24 2015 +0200 @@ -306,8 +306,8 @@ fun print_ss ctxt (SS{congs,simps,...}) = writeln (cat_lines - (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @ - ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps)); + (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @ + ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps)); (* Rewriting with conditionals *) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Datatype_Examples/Misc_N2M.thy --- a/src/HOL/Datatype_Examples/Misc_N2M.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Datatype_Examples/Misc_N2M.thy Fri Sep 25 23:41:24 2015 +0200 @@ -11,6 +11,9 @@ imports "~~/src/HOL/Library/BNF_Axiomatization" begin +declare [[typedef_overloaded]] + + locale misc begin diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Datatype_Examples/Stream_Processor.thy --- a/src/HOL/Datatype_Examples/Stream_Processor.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Fri Sep 25 23:41:24 2015 +0200 @@ -12,6 +12,9 @@ imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization" begin +declare [[typedef_overloaded]] + + section {* Continuous Functions on Streams *} datatype ('a, 'b, 'c) sp\<^sub>\ = Get "'a \ ('a, 'b, 'c) sp\<^sub>\" | Put "'b" "'c" diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Eisbach/Eisbach_Tools.thy --- a/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 23:41:24 2015 +0200 @@ -31,7 +31,7 @@ (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) (fn ctxt => fn (tok, thms) => (* FIXME proper formatting!? *) - Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #> + Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #> setup_trace_method @{binding print_term} (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) (fn ctxt => fn (tok, t) => diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/HOLCF/Porder.thy --- a/src/HOL/HOLCF/Porder.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/HOLCF/Porder.thy Fri Sep 25 23:41:24 2015 +0200 @@ -8,6 +8,9 @@ imports Main begin +declare [[typedef_overloaded]] + + subsection {* Type class for partial orders *} class below = diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 25 23:41:24 2015 +0200 @@ -165,7 +165,7 @@ let val name = #1 typ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy - |> Typedef.add_typedef_global typ set opt_bindings tac + |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings tac val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/IMP/Abs_State.thy --- a/src/HOL/IMP/Abs_State.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/IMP/Abs_State.thy Fri Sep 25 23:41:24 2015 +0200 @@ -19,7 +19,7 @@ hide_type st --"hide previous def to avoid long names" -quotient_type 'a st = "('a::top) st_rep" / eq_st +quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st morphisms rep_st St by (metis eq_st_def equivpI reflpI sympI transpI) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Import/import_rule.ML Fri Sep 25 23:41:24 2015 +0200 @@ -222,7 +222,8 @@ Typedef.make_morphisms (Binding.name tycname) (SOME (Binding.name rep_name, Binding.name abs_name)) val ((_, typedef_info), thy') = - Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c + Typedef.add_typedef_global {overloaded = false} + (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy val aty = #abs_type (#1 typedef_info) val th = freezeT thy' (#type_definition (#2 typedef_info)) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Fri Sep 25 23:41:24 2015 +0200 @@ -47,7 +47,7 @@ end -quotient_type 'a fract = "'a :: idom \ 'a" / partial: "fractrel" +quotient_type (overloaded) 'a fract = "'a :: idom \ 'a" / partial: "fractrel" by(rule part_equivp_fractrel) subsubsection \Representation and basic operations\ diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 23:41:24 2015 +0200 @@ -21,7 +21,7 @@ fun drop_fact_warning ctxt = Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Display.string_of_thm ctxt) + Thm.string_of_thm ctxt) (* general theorem normalizations *) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Old_SMT/old_smt_solver.ML --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 23:41:24 2015 +0200 @@ -105,7 +105,7 @@ fun trace_assms ctxt = Old_SMT_Config.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) + Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) = let @@ -327,7 +327,7 @@ if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0 then tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" - (map (Display.pretty_thm ctxt o snd) wthms))) + (map (Thm.pretty_thm ctxt o snd) wthms))) else () end diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 23:41:24 2015 +0200 @@ -72,7 +72,7 @@ fun pretty_goal ctxt thms t = [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] |> not (null thms) ? cons (Pretty.big_list "assumptions:" - (map (Display.pretty_thm ctxt) thms)) + (map (Thm.pretty_thm ctxt) thms)) fun try_apply ctxt thms = let diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Polynomial.thy Fri Sep 25 23:41:24 2015 +0200 @@ -52,7 +52,7 @@ subsection \Definition of type @{text poly}\ -typedef 'a poly = "{f :: nat \ 'a::zero. \\<^sub>\ n. f n = 0}" +typedef (overloaded) 'a poly = "{f :: nat \ 'a::zero. \\<^sub>\ n. f n = 0}" morphisms coeff Abs_poly by (auto intro!: ALL_MOST) setup_lifting type_definition_poly diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Quotient_Type.thy --- a/src/HOL/Library/Quotient_Type.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Quotient_Type.thy Fri Sep 25 23:41:24 2015 +0200 @@ -62,7 +62,7 @@ definition (in eqv) "quot = {{x. a \ x} | a. True}" -typedef 'a quot = "quot :: 'a::eqv set set" +typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" unfolding quot_def by blast lemma quotI [intro]: "{x. a \ x} \ quot" diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/RBT.thy Fri Sep 25 23:41:24 2015 +0200 @@ -10,7 +10,7 @@ subsection \Type definition\ -typedef ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}" +typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}" morphisms impl_of RBT proof - have "RBT_Impl.Empty \ ?rbt" by simp diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/Saturated.thy --- a/src/HOL/Library/Saturated.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/Saturated.thy Fri Sep 25 23:41:24 2015 +0200 @@ -12,7 +12,7 @@ subsection \The type of saturated naturals\ -typedef ('a::len) sat = "{.. len_of TYPE('a)}" +typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}" morphisms nat_of Abs_sat by auto diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 25 23:41:24 2015 +0200 @@ -35,9 +35,9 @@ fun mk_b name user_b = (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) |> Binding.qualify false (Binding.name_of b); - val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; - val (bd_type_Tname, lthy) = - Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; + val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy; + val (bd_type_Tname, lthy) = lthy + |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn); val T = Type (Tname, map TFree vars); val bd_type_T = Type (bd_type_Tname, map TFree deads); val lives = map TFree (filter_out (member (op =) deads) vars); diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Sep 25 23:41:24 2015 +0200 @@ -375,8 +375,8 @@ (case find_thms_split splitths 1 th of NONE => (writeln (cat_lines - (["th:", Display.string_of_thm ctxt th, "split ths:"] @ - map (Display.string_of_thm ctxt) splitths @ ["\n--"])); + (["th:", Thm.string_of_thm ctxt th, "split ths:"] @ + map (Thm.string_of_thm ctxt) splitths @ ["\n--"])); error "splitto: cannot find variable to split on") | SOME v => let @@ -1342,7 +1342,7 @@ fun say s = if !tracing then writeln s else (); fun print_thms ctxt s L = - say (cat_lines (s :: map (Display.string_of_thm ctxt) L)); + say (cat_lines (s :: map (Thm.string_of_thm ctxt) L)); fun print_term ctxt s t = say (cat_lines [s, Syntax.string_of_term ctxt t]); @@ -1458,7 +1458,7 @@ val cntxt = Simplifier.prems_of ctxt val _ = print_thms ctxt "cntxt:" cntxt val _ = say "cong rule:" - val _ = say (Display.string_of_thm ctxt thm) + val _ = say (Thm.string_of_thm ctxt thm) (* Unquantified eliminate *) fun uq_eliminate (thm,imp) = let val tych = Thm.cterm_of ctxt @@ -2390,7 +2390,7 @@ fun trace_thms ctxt s L = - if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L)) + if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L)) else (); fun trace_cterm ctxt s ct = diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Matrix_LP/Matrix.thy --- a/src/HOL/Matrix_LP/Matrix.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Matrix_LP/Matrix.thy Fri Sep 25 23:41:24 2015 +0200 @@ -13,7 +13,7 @@ definition "matrix = {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}" -typedef 'a matrix = "matrix :: (nat \ nat \ 'a::zero) set" +typedef (overloaded) 'a matrix = "matrix :: (nat \ nat \ 'a::zero) set" unfolding matrix_def proof show "(\j i. 0) \ {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}" diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Sep 25 23:41:24 2015 +0200 @@ -9,7 +9,8 @@ definition bcontfun :: "('a::topological_space \ 'b::metric_space) set" where "bcontfun = {f. continuous_on UNIV f \ bounded (range f)}" -typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \ 'b::metric_space) set" +typedef (overloaded) ('a, 'b) bcontfun = + "bcontfun :: ('a::topological_space \ 'b::metric_space) set" by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) lemma bcontfunE: diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri Sep 25 23:41:24 2015 +0200 @@ -6,6 +6,9 @@ "avoids" begin +declare [[typedef_overloaded]] + + section {* Permutations *} (*======================*) @@ -3378,7 +3381,7 @@ definition "ABS = ABS_set" -typedef ('x,'a) ABS ("\_\_" [1000,1000] 1000) = +typedef ('x, 'a) ABS ("\_\_" [1000,1000] 1000) = "ABS::('x\('a noption)) set" morphisms Rep_ABS Abs_ABS unfolding ABS_def diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Sep 25 23:41:24 2015 +0200 @@ -586,7 +586,7 @@ val (typedefs, thy6) = thy4 |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => - Typedef.add_typedef_global + Typedef.add_typedef_global {overloaded = false} (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 23:41:24 2015 +0200 @@ -156,7 +156,7 @@ fold (fn thm => Data.map (flag thm)) thms_to_be_added context end handle EQVT_FORM s => - error (Display.string_of_thm (Context.proof_of context) orig_thm ^ + error (Thm.string_of_thm (Context.proof_of context) orig_thm ^ " does not comply with the form of an equivariance lemma (" ^ s ^").") diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 23:41:24 2015 +0200 @@ -78,7 +78,7 @@ Pretty.chunks (map (fn (b, th) => Pretty.block [Binding.pretty b, Pretty.str ":", Pretty.brk 1, - Display.pretty_thm ctxt th]) + Thm.pretty_thm ctxt th]) defs), Pretty.str "Verification conditions:", diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 25 23:41:24 2015 +0200 @@ -359,7 +359,7 @@ map (rpair (mk_type thy prfx ty)) flds) fldtys in case get_type thy prfx s of NONE => - Record.add_record ([], Binding.name s) NONE + Record.add_record {overloaded = false} ([], Binding.name s) NONE (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy | SOME (rT, cmap) => (case get_record_info thy rT of @@ -388,8 +388,7 @@ (ids, case get_type thy prfx s of SOME _ => thy - | NONE => Typedecl.typedecl_global - (Binding.name s, [], NoSyn) thy |> snd); + | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd); fun term_of_expr thy prfx types pfuns = diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Sep 25 23:41:24 2015 +0200 @@ -198,9 +198,8 @@ val final_fqn = Sign.full_name thy binding val tyargs = List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int) - val thy' = - Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy - |> snd + val (_, thy') = + Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy val typ_map_entry = (thf_type, (final_fqn, arity)) val ty_map' = typ_map_entry :: ty_map in (ty_map', thy') end diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 25 23:41:24 2015 +0200 @@ -1923,7 +1923,8 @@ ||>> variant_tfrees fp_b_names; fun add_fake_type spec = - Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); + Typedecl.basic_typedecl {final = true} + (type_binding_of_spec spec, num_As, mixfix_of_spec spec); val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy; diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 23:41:24 2015 +0200 @@ -159,7 +159,7 @@ val ((name, info), (lthy, lthy_old)) = lthy |> Local_Theory.open_target |> snd - |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac + |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; in diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 23:41:24 2015 +0200 @@ -202,14 +202,14 @@ raise QUOT_ERROR [Pretty.block [Pretty.str "The Quotient theorem has extra assumptions:", Pretty.brk 1, - Display.pretty_thm ctxt quot_thm]] + Thm.pretty_thm ctxt quot_thm]] else () val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient handle TERM _ => raise QUOT_ERROR [Pretty.block [Pretty.str "The Quotient theorem is not of the right form:", Pretty.brk 1, - Display.pretty_thm ctxt quot_thm]] + Thm.pretty_thm ctxt quot_thm]] val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt val (rty, qty) = quot_thm_rty_qty quot_thm_fixed val rty_tfreesT = Term.add_tfree_namesT rty [] @@ -837,13 +837,13 @@ handle TERM _ => raise PCR_ERROR [Pretty.block [Pretty.str "The pcr definiton theorem is not a plain meta equation:", Pretty.brk 1, - Display.pretty_thm ctxt pcrel_def]] + Thm.pretty_thm ctxt pcrel_def]] val pcr_const_def = head_of def_lhs val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq)) handle TERM _ => raise PCR_ERROR [Pretty.block [Pretty.str "The pcr_cr equation theorem is not a plain equation:", Pretty.brk 1, - Display.pretty_thm ctxt pcr_cr_eq]] + Thm.pretty_thm ctxt pcr_cr_eq]] val (pcr_const_eq, eqs) = strip_comb eq_lhs fun is_eq (Const (@{const_name HOL.eq}, _)) = true | is_eq _ = false @@ -853,7 +853,7 @@ [Pretty.block [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:", Pretty.brk 1, - Display.pretty_thm ctxt pcr_cr_eq]] + Thm.pretty_thm ctxt pcr_cr_eq]] else [] val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then [Pretty.block diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 25 23:41:24 2015 +0200 @@ -186,8 +186,8 @@ | tacf prems = error (cat_lines ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: - Display.string_of_thm ctxt st :: - "Premises:" :: map (Display.string_of_thm ctxt) prems)) + Thm.string_of_thm ctxt st :: + "Premises:" :: map (Thm.string_of_thm ctxt) prems)) in case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of SOME (th, _) => th @@ -395,7 +395,7 @@ val cls = if has_too_many_clauses ctxt (Thm.concl_of th) then (trace_msg ctxt (fn () => - "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) + "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths) else cnf_aux (th, ths) in (cls, !ctxt_ref) end @@ -652,7 +652,7 @@ |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^ - Display.string_of_thm ctxt th) + Thm.string_of_thm ctxt th) | _ => ())) end @@ -751,8 +751,8 @@ val horns = make_horns (cls @ ths) val _ = trace_msg ctxt (fn () => cat_lines ("meson method called:" :: - map (Display.string_of_thm ctxt) (cls @ ths) @ - ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) + map (Thm.string_of_thm ctxt) (cls @ ths) @ + ["clauses:"] @ map (Thm.string_of_thm ctxt) horns)) in THEN_ITER_DEEPEN iter_deepen_limit (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 23:41:24 2015 +0200 @@ -170,7 +170,7 @@ val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th) in Thm.equal_elim eqth th end handle THM (msg, _, _) => - (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^ + (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^ "\nException message: " ^ msg); (* A type variable of sort "{}" will make "abstraction" fail. *) TrueI) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 23:41:24 2015 +0200 @@ -134,11 +134,11 @@ end handle Option.Option => (trace_msg ctxt (fn () => - "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) | TYPE _ => (trace_msg ctxt (fn () => - "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = let val a = Metis_Name.toString a in @@ -149,7 +149,7 @@ SOME _ => NONE (* type instantiations are forbidden *) | NONE => SOME (a, t) (* internal Metis var? *))) end - val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) + val _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) val (vars, tms) = ListPair.unzip (map_filter subst_translation substs) @@ -269,8 +269,8 @@ let val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => - " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\ - \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) + " isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\ + \ isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2) in (* Trivial cases where one operand is type info *) if Thm.eq_thm (TrueI, i_th1) then @@ -369,7 +369,7 @@ val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst') val eq_terms = map (apply2 (Thm.cterm_of ctxt)) (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) @@ -462,7 +462,7 @@ val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) |> flexflex_first_order ctxt |> resynchronize ctxt fol_th - val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th) val _ = trace_msg ctxt (fn () => "=============================================") in (fol_th, th) :: th_pairs diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 23:41:24 2015 +0200 @@ -160,7 +160,7 @@ val dischargers = map (fst o snd) th_cls_pairs val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls + val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_of_string Strict type_enc val (sym_tab, axioms, ord_info, concealed) = @@ -172,7 +172,7 @@ | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (K "ISABELLE CLAUSES") - val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms + val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms val _ = trace_msg ctxt (K "METIS CLAUSES") val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") @@ -200,7 +200,7 @@ val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used + val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used val (used_th_cls_pairs, unused_th_cls_pairs) = List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs val unused_ths = maps (snd o snd) unused_th_cls_pairs @@ -217,7 +217,7 @@ (); (case result of (_, ith) :: _ => - (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) | _ => (trace_msg ctxt (K "Metis: No result"); [])) end @@ -251,7 +251,7 @@ val unused = Unsynchronized.ref [] val type_encs = if null type_encs0 then partial_type_encs else type_encs0 val _ = trace_msg ctxt (fn () => - "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths)) val type_encs = type_encs |> maps unalias_type_enc val combs = (lam_trans = combsN) fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1 diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 25 23:41:24 2015 +0200 @@ -186,7 +186,7 @@ |> Sign.parent_path |> fold_map (fn (((name, mx), tvs), c) => - Typedef.add_typedef_global (name, tvs, mx) + Typedef.add_typedef_global {overloaded = false} (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (fn ctxt => resolve_tac ctxt [exI] 1 THEN diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 23:41:24 2015 +0200 @@ -355,7 +355,7 @@ fun print_intros ctxt gr consts = tracing (cat_lines (map (fn const => "Constant " ^ const ^ "has intros:\n" ^ - cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts)) + cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts)) (* translation of moded predicates *) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 23:41:24 2015 +0200 @@ -23,14 +23,14 @@ tracing (msg ^ (cat_lines (map (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ - commas (map (Display.string_of_thm_global thy) intros)) intross))) + commas (map (Thm.string_of_thm_global thy) intros)) intross))) else () fun print_specs options thy specs = if show_intermediate_results options then map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ - (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs + (cat_lines (map (Thm.string_of_thm_global thy) thms)) ^ "\n") specs |> cat_lines |> tracing else () diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 23:41:24 2015 +0200 @@ -1079,7 +1079,7 @@ error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^ " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^ " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^ - " in " ^ Display.string_of_thm ctxt' th) + " in " ^ Thm.string_of_thm ctxt' th) in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end fun instantiate_typ th = let diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 23:41:24 2015 +0200 @@ -130,11 +130,11 @@ let val _ = writeln ("predicate: " ^ pred) val _ = writeln ("introrules: ") - val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm)) + val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm)) (rev (Core_Data.intros_of ctxt pred)) () in if Core_Data.has_elim ctxt pred then - writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred)) + writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred)) else writeln ("no elimrule defined") end @@ -1295,7 +1295,7 @@ else error ("Format of introduction rule is invalid: tuples must be expanded:" ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ - (Display.string_of_thm_global thy intro)) + (Thm.string_of_thm_global thy intro)) | _ => true val prems = Logic.strip_imp_prems (prop_of intro) fun check_prem (Prem t) = forall check_arg args @@ -1387,7 +1387,7 @@ (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val _ = if show_intermediate_results options then - tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames))) + tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames))) else () val (preds, all_vs, param_vs, all_modes, clauses) = prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 23:41:24 2015 +0200 @@ -217,7 +217,7 @@ val _ = if show_intermediate_results options then tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^ - commas (map (Display.string_of_thm_global thy) spec)) + commas (map (Thm.string_of_thm_global thy) spec)) else () in spec diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 23:41:24 2015 +0200 @@ -310,7 +310,7 @@ fun rewrite_intro thy intro = let fun lookup_pred t = lookup thy (Fun_Pred.get thy) t - (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*) + (*val _ = tracing ("Rewriting intro " ^ Thm.string_of_thm_global thy intro)*) val intro_t = Logic.unvarify_global (Thm.prop_of intro) val (prems, concl) = Logic.strip_horn intro_t val frees = map fst (Term.add_frees intro_t []) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 23:41:24 2015 +0200 @@ -192,7 +192,7 @@ fun print_specs options thy msg ths = if show_intermediate_results options then - (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths))) + (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths))) else () @@ -209,7 +209,7 @@ map (rewrite_intros ctxt) specs else error ("unexpected specification for constant " ^ quote constname ^ ":\n" - ^ commas (map (quote o Display.string_of_thm_global thy) specs)) + ^ commas (map (quote o Thm.string_of_thm_global thy) specs)) val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros val _ = print_specs options thy "normalized intros" intros diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 23:41:24 2015 +0200 @@ -306,7 +306,7 @@ val (_, ts) = strip_comb t in trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^ - " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) + " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm) THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1 THEN (trace_tac ctxt options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 25 23:41:24 2015 +0200 @@ -6,14 +6,17 @@ signature QUOTIENT_TYPE = sig - val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory - - val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option * thm option) -> Proof.context -> Proof.state - - val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) * - (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state + val add_quotient_type: {overloaded: bool} -> + ((string list * binding * mixfix) * (typ * term * bool) * + ((binding * binding) option * thm option)) * thm -> local_theory -> + Quotient_Info.quotients * local_theory + val quotient_type: {overloaded: bool} -> + (string list * binding * mixfix) * (typ * term * bool) * + ((binding * binding) option * thm option) -> Proof.context -> Proof.state + val quotient_type_cmd: {overloaded: bool} -> + (((((string list * binding) * mixfix) * string) * (bool * string)) * + (binding * binding) option) * (Facts.ref * Token.src list) option -> + Proof.context -> Proof.state end; structure Quotient_Type: QUOTIENT_TYPE = @@ -40,12 +43,12 @@ (* makes the new type definitions and proves non-emptyness *) -fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = +fun typedef_make overloaded (vs, qty_name, mx, rel, rty) equiv_thm lthy = let fun typedef_tac ctxt = EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef overloaded (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end @@ -152,7 +155,8 @@ end (* main function for constructing a quotient type *) -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy = +fun add_quotient_type overloaded + (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy = let val part_equiv = if partial @@ -161,7 +165,7 @@ (* generates the typedef *) val ((_, typedef_info), lthy1) = - typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy + typedef_make overloaded (vs, qty_name, mx, rel, rty) part_equiv lthy (* abs and rep functions from the typedef *) val Abs_ty = #abs_type (#1 typedef_info) @@ -290,7 +294,7 @@ relations are equivalence relations *) -fun quotient_type quot lthy = +fun quotient_type overloaded quot lthy = let (* sanity check *) val _ = sanity_check quot @@ -307,12 +311,12 @@ val goal = (mk_goal o #2) quot - fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm) + fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm) in Proof.theorem NONE after_qed [[(goal, [])]] lthy end -fun quotient_type_cmd spec lthy = +fun quotient_type_cmd overloaded spec lthy = let fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy = let @@ -330,7 +334,7 @@ val (spec', _) = parse_spec spec lthy in - quotient_type spec' lthy + quotient_type overloaded spec' lthy end @@ -340,11 +344,11 @@ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type} "quotient type definitions (require equivalence proofs)" (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) - (Parse.type_args -- Parse.binding -- + (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |-- Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) -- Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) -- - Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) - >> quotient_type_cmd) + Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)) + >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec)) end diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 23:41:24 2015 +0200 @@ -23,7 +23,7 @@ fun drop_fact_warning ctxt = SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Display.string_of_thm ctxt) + Thm.string_of_thm ctxt) (* general theorem normalizations *) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 23:41:24 2015 +0200 @@ -103,7 +103,7 @@ fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) + Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) = let diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 23:41:24 2015 +0200 @@ -89,7 +89,7 @@ val ctxt = ctxt |> Config.put show_markup true val assms = op @ assmsp val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") - val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) + val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) val concl = Syntax.pretty_term ctxt concl in tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/choice_specification.ML Fri Sep 25 23:41:24 2015 +0200 @@ -148,7 +148,7 @@ fun add_final (thm, thy) = if name = "" then (thm, thy) - else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); + else (writeln (" " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm); Global_Theory.store_thm (Binding.name name, thm) thy) in swap args diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/inductive.ML Fri Sep 25 23:41:24 2015 +0200 @@ -236,7 +236,7 @@ (Pretty.str "(co)inductives:" :: map (Pretty.mark_str o #1) (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))), - Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] + Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)] end |> Pretty.writeln_chunks; @@ -269,7 +269,7 @@ dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm)) | _ => thm) - end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); + end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm); val mono_add = Thm.declaration_attribute (fn thm => fn context => diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Fri Sep 25 23:41:24 2015 +0200 @@ -298,7 +298,7 @@ val _ = if Context_Position.is_really_visible ctxt then warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^ - "\n" ^ Display.string_of_thm ctxt thm) + "\n" ^ Thm.string_of_thm ctxt thm) else (); in tab end; diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Sep 25 23:41:24 2015 +0200 @@ -303,11 +303,11 @@ @{const_name Rings.divide}] a | _ => (if Context_Position.is_visible ctxt then - warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm) + warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)) | _ => (if Context_Position.is_visible ctxt then - warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm) + warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm) else (); false)); (* substitute new for occurrences of old in a term, incrementing bound *) diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/record.ML Fri Sep 25 23:41:24 2015 +0200 @@ -26,8 +26,8 @@ val get_info: theory -> string -> info option val the_info: theory -> string -> info val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list - val add_record: (string * sort) list * binding -> (typ list * string) option -> - (binding * typ * mixfix) list -> theory -> theory + val add_record: {overloaded: bool} -> (string * sort) list * binding -> + (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory val last_extT: typ -> (string * typ list) option val dest_recTs: typ -> (string * typ list) list @@ -55,7 +55,7 @@ signature ISO_TUPLE_SUPPORT = sig - val add_iso_tuple_type: binding * (string * sort) list -> + val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list -> typ * typ -> theory -> (term * term) * theory val mk_cons_tuple: term * term -> term val dest_cons_tuple: term -> term * term @@ -93,13 +93,13 @@ |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT)) end -fun do_typedef raw_tyco repT raw_vs thy = +fun do_typedef overloaded raw_tyco repT raw_vs thy = let val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; val vs = map (Proof_Context.check_tfree ctxt) raw_vs; in thy - |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn) + |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn) (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; @@ -117,13 +117,13 @@ fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u) | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]); -fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy = +fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy = let val repT = HOLogic.mk_prodT (leftT, rightT); val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) = thy - |> do_typedef b repT alphas + |> do_typedef overloaded b repT alphas ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*) val typ_ctxt = Proof_Context.init_global typ_thy; @@ -1499,7 +1499,7 @@ in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end); -fun extension_definition name fields alphas zeta moreT more vars thy = +fun extension_definition overloaded name fields alphas zeta moreT more vars thy = let val ctxt = Proof_Context.init_global thy; @@ -1525,7 +1525,7 @@ let val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; val ((_, cons), thy') = thy - |> Iso_Tuple_Support.add_iso_tuple_type + |> Iso_Tuple_Support.add_iso_tuple_type overloaded (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right); in @@ -1808,7 +1808,7 @@ (* definition *) -fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 = +fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 = let val ctxt0 = Proof_Context.init_global thy0; @@ -1867,7 +1867,7 @@ extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) = thy0 |> Sign.qualified_path false binding - |> extension_definition extension_name fields alphas_ext zeta moreT more vars; + |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars; val ext_ctxt = Proof_Context.init_global ext_thy; val _ = timing_msg ext_ctxt "record preparing definitions"; @@ -2277,7 +2277,7 @@ in -fun add_record (params, binding) raw_parent raw_fields thy = +fun add_record overloaded (params, binding) raw_parent raw_fields thy = let val ctxt = Proof_Context.init_global thy; fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T) @@ -2327,11 +2327,11 @@ err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields; val _ = if null errs then () else error (cat_lines errs); in - thy |> definition (params, binding) parent parents bfields + thy |> definition overloaded (params, binding) parent parents bfields end handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding); -fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy = +fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy = let val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; @@ -2339,7 +2339,7 @@ val (parent, ctxt2) = read_parent raw_parent ctxt1; val (fields, ctxt3) = read_fields raw_fields ctxt2; val params' = map (Proof_Context.check_tfree ctxt3) params; - in thy |> add_record (params', binding) parent fields end; + in thy |> add_record overloaded (params', binding) parent fields end; end; @@ -2348,9 +2348,10 @@ val _ = Outer_Syntax.command @{command_keyword record} "define extensible record" - (Parse.type_args_constrained -- Parse.binding -- + (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) -- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) -- Scan.repeat1 Parse.const_binding) - >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z))); + >> (fn ((overloaded, x), (y, z)) => + Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z))); end; diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/sat.ML Fri Sep 25 23:41:24 2015 +0200 @@ -155,9 +155,9 @@ let val _ = cond_tracing ctxt (fn () => - "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^ + "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^ - ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^ + ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")") (* the two literals used for resolution *) @@ -176,7 +176,7 @@ val _ = cond_tracing ctxt - (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm) + (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm) (* Gamma1, Gamma2 |- False *) val c_new = @@ -186,7 +186,7 @@ val _ = cond_tracing ctxt (fn () => - "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^ + "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")") diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Tools/typedef.ML Fri Sep 25 23:41:24 2015 +0200 @@ -20,16 +20,17 @@ val default_bindings: binding -> bindings val make_bindings: binding -> bindings option -> bindings val make_morphisms: binding -> (binding * binding) option -> bindings - val add_typedef: binding * (string * sort) list * mixfix -> + val overloaded: bool Config.T + val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix -> term -> bindings option -> (Proof.context -> tactic) -> local_theory -> (string * info) * local_theory - val add_typedef_global: binding * (string * sort) list * mixfix -> + val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix -> term -> bindings option -> (Proof.context -> tactic) -> theory -> (string * info) * theory - val typedef: binding * (string * sort) list * mixfix -> term -> bindings option -> - local_theory -> Proof.state - val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option -> - local_theory -> Proof.state + val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix -> + term -> bindings option -> local_theory -> Proof.state + val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix -> + string -> bindings option -> local_theory -> Proof.state end; structure Typedef: TYPEDEF = @@ -98,6 +99,8 @@ (* primitive typedef axiomatization -- for fresh typedecl *) +val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false); + fun mk_inhabited A = let val T = HOLogic.dest_setT (Term.fastype_of A) in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end; @@ -109,7 +112,7 @@ (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT); in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end; -fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy = +fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy = let (* errors *) @@ -118,11 +121,13 @@ val lhs_tfrees = Term.add_tfreesT newT []; val rhs_tfrees = Term.add_tfreesT oldT []; val _ = - (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => () + (case fold (remove (op =)) lhs_tfrees rhs_tfrees of + [] => () | extras => error ("Extra type variables in representing set: " ^ show_names extras)); val _ = - (case Term.add_frees A [] of [] => [] + (case Term.add_frees A [] of [] => + [] | xs => error ("Illegal variables in representing set: " ^ show_names xs)); @@ -132,15 +137,38 @@ |> Local_Theory.background_theory_result (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>> Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn)); + val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy); + val defs_context = Proof_Context.defs_context consts_lthy; - val typedef_deps = Term.add_consts A []; + val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A []; + val A_types = + (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A []; + val typedef_deps = A_consts @ A_types; + + val newT_dep = Theory.type_dep (dest_Type newT); val ((axiom_name, axiom), axiom_lthy) = consts_lthy |> Local_Theory.background_theory_result (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##> - Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##> - Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps); + Theory.add_deps defs_context "" newT_dep typedef_deps ##> + Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##> + Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]); + val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy); + val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep)); + val _ = + if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then () + else + error (Pretty.string_of (Pretty.chunks + [Pretty.paragraph + (Pretty.text "Type definition with open dependencies, use" @ + [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1, + Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @ + Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."), + Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT], + Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 :: + Pretty.commas + (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))])) in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end; @@ -164,7 +192,7 @@ (* prepare_typedef *) -fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy = +fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy = let val bname = Binding.name_of name; @@ -187,7 +215,7 @@ val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args; val (newT, typedecl_lthy) = lthy - |> Typedecl.typedecl (name, args, mx) + |> Typedecl.typedecl {final = false} (name, args, mx) ||> Variable.declare_term set; val Type (full_name, _) = newT; @@ -198,7 +226,7 @@ val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings; val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy - |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set; + |> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set; val alias_lthy = typedef_lthy |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC)) @@ -262,18 +290,18 @@ (* add_typedef: tactic interface *) -fun add_typedef typ set opt_bindings tac lthy = +fun add_typedef overloaded typ set opt_bindings tac lthy = let val ((goal, _, typedef_result), lthy') = - prepare_typedef Syntax.check_term typ set opt_bindings lthy; + prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy; val inhabited = Goal.prove lthy' [] [] goal (tac o #context) |> Goal.norm_result lthy' |> Thm.close_derivation; in typedef_result inhabited lthy' end; -fun add_typedef_global typ set opt_bindings tac = +fun add_typedef_global overloaded typ set opt_bindings tac = Named_Target.theory_init - #> add_typedef typ set opt_bindings tac + #> add_typedef overloaded typ set opt_bindings tac #> Local_Theory.exit_result_global (apsnd o transform_info); @@ -281,11 +309,11 @@ local -fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy = +fun gen_typedef prep_term prep_constraint overloaded (b, raw_args, mx) set opt_bindings lthy = let val args = map (apsnd (prep_constraint lthy)) raw_args; val ((goal, goal_pat, typedef_result), lthy') = - prepare_typedef prep_term (b, args, mx) set opt_bindings lthy; + prepare_typedef prep_term overloaded (b, args, mx) set opt_bindings lthy; fun after_qed [[th]] = snd o typedef_result th; in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end; @@ -303,10 +331,14 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_keyword typedef} "HOL type definition (requires non-emptiness proof)" - (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- + (Parse_Spec.overloaded -- Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) - >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy => - typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy)); + >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy => + typedef_cmd {overloaded = overloaded} (t, vs, mx) A + (SOME (make_morphisms t opt_morphs)) lthy)); + + +val overloaded = typedef_overloaded; end; diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/Word/Word.thy Fri Sep 25 23:41:24 2015 +0200 @@ -18,7 +18,7 @@ subsection {* Type definition *} -typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}" +typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}" morphisms uint Abs_word by auto lemma uint_nonnegative: diff -r b77bf45efe21 -r 28eb608b9b59 src/HOL/ex/PER.thy --- a/src/HOL/ex/PER.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/HOL/ex/PER.thy Fri Sep 25 23:41:24 2015 +0200 @@ -154,7 +154,7 @@ definition "quot = {{x. a \ x}| a::'a::partial_equiv. True}" -typedef 'a quot = "quot :: 'a::partial_equiv set set" +typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set" unfolding quot_def by blast lemma quotI [intro]: "{x. a \ x} \ quot" diff -r b77bf45efe21 -r 28eb608b9b59 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 23:41:24 2015 +0200 @@ -349,7 +349,7 @@ fun trace_thm ctxt msgs th = (if Config.get ctxt LA_Data.trace - then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th])) + then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th])) else (); th); fun trace_term ctxt msgs t = @@ -468,8 +468,8 @@ if LA_Logic.is_False fls then () else (tracing (cat_lines - (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @ - ["Proved:", Display.string_of_thm ctxt fls, ""])); + (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @ + ["Proved:", Thm.string_of_thm ctxt fls, ""])); warning "Linear arithmetic should have refuted the assumptions.\n\ \Please inform Tobias Nipkow.") in fls end diff -r b77bf45efe21 -r 28eb608b9b59 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Provers/blast.ML Fri Sep 25 23:41:24 2015 +0200 @@ -484,7 +484,7 @@ | cond_tracing false _ = (); fun TRACE ctxt rl tac i st = - (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st); + (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st); (*Resolution/matching tactics: if upd then the proof state may be updated. Matching makes the tactics more deterministic in the presence of Vars.*) @@ -509,13 +509,13 @@ handle ElimBadPrem => (*reject: prems don't preserve conclusion*) (if Context_Position.is_visible ctxt then - warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0) + warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0) else (); Option.NONE) | ElimBadConcl => (*ignore: conclusion is not just a variable*) (cond_tracing (Config.get ctxt trace) (fn () => "Ignoring ill-formed elimination rule:\n" ^ - "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0); + "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0); Option.NONE); diff -r b77bf45efe21 -r 28eb608b9b59 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Provers/classical.ML Fri Sep 25 23:41:24 2015 +0200 @@ -282,7 +282,7 @@ fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; fun delete x = delete_tagged_list (joinrules x); -fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th); +fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); fun make_elim ctxt th = if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th @@ -290,7 +290,7 @@ fun warn_thm ctxt msg th = if Context_Position.is_really_visible ctxt - then warning (msg ^ Display.string_of_thm ctxt th) else (); + then warning (msg ^ Thm.string_of_thm ctxt th) else (); fun warn_rules ctxt msg rules (r: rule) = Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true); @@ -634,7 +634,7 @@ fun print_claset ctxt = let val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; - val pretty_thms = map (Display.pretty_thm_item ctxt o #1) o Item_Net.content; + val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content; in [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Sep 25 23:41:24 2015 +0200 @@ -532,9 +532,9 @@ register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> - register_config Goal_Display.show_consts_raw #> - register_config Display.show_hyps_raw #> - register_config Display.show_tags_raw #> + register_config Thm.show_consts_raw #> + register_config Thm.show_hyps_raw #> + register_config Thm.show_tags_raw #> register_config Pattern.unify_trace_failure_raw #> register_config Unify.trace_bound_raw #> register_config Unify.search_bound_raw #> diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/bundle.ML Fri Sep 25 23:41:24 2015 +0200 @@ -124,7 +124,7 @@ fun print_bundles verbose ctxt = let - val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; + val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; fun prt_fact (ths, []) = map prt_thm ths | prt_fact (ths, atts) = Pretty.enclose "(" ")" diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/calculation.ML Fri Sep 25 23:41:24 2015 +0200 @@ -41,7 +41,7 @@ fun print_rules ctxt = let - val pretty_thm = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm_item ctxt; val (trans, sym) = get_rules ctxt; in [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)), @@ -137,8 +137,8 @@ fun calculate prep_rules final raw_rules int state = let val ctxt = Proof.context_of state; - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thm_item = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thm_item = Thm.pretty_thm_item ctxt; val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl); diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/class.ML Fri Sep 25 23:41:24 2015 +0200 @@ -599,7 +599,7 @@ fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts) | matchings _ = I; val tvartab = (fold o fold_aterms) matchings ts Vartab.empty - handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e); + handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e); val inst = map_type_tvar (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end; @@ -657,7 +657,7 @@ val primary_constraints = map (apsnd (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; val algebra = Sign.classes_of thy - |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy) + |> fold (fn tyco => Sorts.add_arities (Context.Theory thy) (tyco, map (fn class => (class, map snd vs)) sort)) tycos; val consts = Sign.consts_of thy; val improve_constraints = AList.lookup (op =) diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/code.ML Fri Sep 25 23:41:24 2015 +0200 @@ -443,11 +443,11 @@ exception BAD_THM of string; fun bad_thm msg = raise BAD_THM msg; fun error_thm f thy (thm, proper) = f (thm, proper) - handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); + handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); fun error_abs_thm f thy thm = f thm - handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); + handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); fun warning_thm f thy (thm, proper) = SOME (f (thm, proper)) - handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE) + handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE) fun try_thm f thm_proper = SOME (f thm_proper) handle BAD_THM _ => NONE; @@ -764,7 +764,7 @@ val (thms, propers) = split_list eqns; val _ = map (fn thm => if c = const_eqn thy thm then () else error ("Wrong head of code equation,\nexpected constant " - ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms; + ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms; fun tvars_of T = rev (Term.add_tvarsT T []); val vss = map (tvars_of o snd o head_eqn) thms; fun inter_sorts vs = @@ -794,7 +794,7 @@ val _ = assert_abs_eqn thy (SOME tyco) abs_thm; val _ = if c = const_abs_eqn thy abs_thm then () else error ("Wrong head of abstract code equation,\nexpected constant " - ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm); + ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm); in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; fun constrain_cert_thm thy sorts cert_thm = @@ -888,12 +888,12 @@ fun pretty_cert thy (cert as Nothing _) = [Pretty.str "(not implemented)"] | pretty_cert thy (cert as Equations _) = - (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd) + (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd) o these o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = [Syntax.pretty_term_global thy (Logic.varify_types_global t)] | pretty_cert thy (Abstract (abs_thm, _)) = - [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; + [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; end; @@ -927,7 +927,7 @@ fun cert_of_eqns_preprocess ctxt functrans c = let fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) - (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns); + (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns); val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) (); in tap (tracing "before function transformation") @@ -1010,7 +1010,7 @@ val exec = the_exec thy; fun pretty_equations const thms = (Pretty.block o Pretty.fbreaks) - (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms); + (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); fun pretty_function (const, Eqns_Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy)) | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) @@ -1096,7 +1096,7 @@ fun drop (thm', proper') = if (proper orelse not proper') andalso matches_args (args_of thm') then (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ - Display.string_of_thm_global thy thm') else (); true) + Thm.string_of_thm_global thy thm') else (); true) else false; in (thm, proper) :: filter_out drop eqns end; fun natural_order eqns = diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/context_rules.ML Fri Sep 25 23:41:24 2015 +0200 @@ -121,7 +121,7 @@ fun prt_kind (i, b) = Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") (map_filter (fn (_, (k, th)) => - if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) + if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE) (sort (int_ord o apply2 fst) rules)); in Pretty.writeln_chunks (map prt_kind rule_kinds) end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/element.ML Fri Sep 25 23:41:24 2015 +0200 @@ -152,7 +152,7 @@ let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; - val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; + val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt; fun prt_binding (b, atts) = Attrib.pretty_binding ctxt (b, if show_attribs then atts else []); diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Sep 25 23:41:24 2015 +0200 @@ -162,7 +162,7 @@ val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result - (Thm.add_def lthy2 false false + (Thm.add_def (Proof_Context.defs_context lthy2) false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); in ((lhs, def), lthy3) end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Fri Sep 25 23:41:24 2015 +0200 @@ -238,12 +238,12 @@ Proof_Context.pretty_local_facts verbose (Toplevel.context_of st) else let - val thy = Toplevel.theory_of st; + val ctxt = Toplevel.context_of st; val prev_thys = (case Toplevel.previous_context_of st of SOME prev => [Proof_Context.theory_of prev] - | NONE => Theory.parents_of thy); - in Proof_Display.pretty_theorems_diff verbose prev_thys thy end; + | NONE => Theory.parents_of (Proof_Context.theory_of ctxt)); + in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end; (* print theorems, terms, types etc. *) diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Fri Sep 25 23:41:24 2015 +0200 @@ -22,7 +22,8 @@ val _ = Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix - >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); + >> (fn ((args, a), mx) => + Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" @@ -767,7 +768,13 @@ Outer_Syntax.command @{command_keyword print_theory} "print logical theory contents" (Parse.opt_bang >> (fn b => - Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of))); + Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); + +val _ = + Outer_Syntax.command @{command_keyword print_definitions} + "print dependencies of definitional theory content" + (Parse.opt_bang >> (fn b => + Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command @{command_keyword print_syntax} diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/local_defs.ML Fri Sep 25 23:41:24 2015 +0200 @@ -176,7 +176,7 @@ fun print_rules ctxt = Pretty.writeln (Pretty.big_list "definitional rewrite rules:" - (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); + (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context); val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context); diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/method.ML Fri Sep 25 23:41:24 2015 +0200 @@ -218,7 +218,7 @@ fun trace ctxt rules = if Config.get ctxt rule_trace andalso not (null rules) then - Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) + Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) |> Pretty.string_of |> tracing else (); diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/object_logic.ML Fri Sep 25 23:41:24 2015 +0200 @@ -87,10 +87,13 @@ local fun gen_add_judgment add_consts (b, T, mx) thy = - let val c = Sign.full_name thy b in - thy - |> add_consts [(b, T, mx)] - |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy') + let + val c = Sign.full_name thy b; + val thy' = thy |> add_consts [(b, T, mx)]; + val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c); + in + thy' + |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) [] |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => if is_some judgment then error "Attempt to redeclare object-logic judgment" else (base_sort, SOME c, atomize_rulify)) diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Sep 25 23:41:24 2015 +0200 @@ -257,9 +257,9 @@ [prem] => if Thm.concl_of th aconv thesis andalso Logic.strip_assums_concl prem aconv thesis then th - else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th) + else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th) | [] => error "Goal solved -- nothing guessed" - | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th)); + | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th)); fun result tac facts ctxt = let @@ -308,7 +308,7 @@ val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); - fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); + fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; val rule = Thm.incr_indexes (maxidx + 1) raw_rule; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/parse_spec.ML Fri Sep 25 23:41:24 2015 +0200 @@ -29,6 +29,7 @@ val obtains: Element.obtains parser val general_statement: (Element.context list * Element.statement) parser val statement_keyword: string parser + val overloaded: bool parser end; structure Parse_Spec: PARSE_SPEC = @@ -155,4 +156,10 @@ val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows"; + +(* options *) + +val overloaded = + Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false; + end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/proof.ML Fri Sep 25 23:41:24 2015 +0200 @@ -495,7 +495,7 @@ error "Bad background theory of goal state"; val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); - fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); + fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal); val th = (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) @@ -511,7 +511,7 @@ handle THM _ => err_lost (); val _ = Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results)) - orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th); + orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th); fun recover_result ([] :: pss) thss = [] :: recover_result pss thss | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Sep 25 23:41:24 2015 +0200 @@ -44,6 +44,7 @@ val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T + val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string @@ -286,7 +287,7 @@ val tsig_of = #1 o #tsig o rep_data; val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; -fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt); +fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt); val consts_of = #1 o #consts o rep_data; val cases_of = #cases o rep_data; @@ -322,6 +323,8 @@ val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; +fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt)); + val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; @@ -346,7 +349,7 @@ map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in if Type.eq_tsig (thy_tsig, global_tsig) then tsig - else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) + else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in @@ -393,8 +396,8 @@ fun pretty_fact ctxt = let - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thms = map (Display.pretty_thm_item ctxt); + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) @@ -552,7 +555,7 @@ fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) - in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end; + in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end; in @@ -577,8 +580,9 @@ local -fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt) - (not (abbrev_mode ctxt)) (consts_of ctxt); +fun certify_consts ctxt = + Consts.certify (Context.Proof ctxt) (tsig_of ctxt) + (not (abbrev_mode ctxt)) (consts_of ctxt); fun expand_binds ctxt = let @@ -761,7 +765,7 @@ t |> expand_abbrevs ctxt |> (fn t' => - #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t') + #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg); in diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/proof_display.ML Fri Sep 25 23:41:24 2015 +0200 @@ -12,10 +12,10 @@ val pp_term: (unit -> theory) -> term -> Pretty.T val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T val pp_cterm: (unit -> theory) -> cterm -> Pretty.T - val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list - val pretty_theorems: bool -> theory -> Pretty.T list - val pretty_full_theory: bool -> theory -> Pretty.T - val print_theory: theory -> unit + val pretty_theory: bool -> Proof.context -> Pretty.T + val pretty_definitions: bool -> Proof.context -> Pretty.T + val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list + val pretty_theorems: bool -> Proof.context -> Pretty.T list val string_of_rule: Proof.context -> string -> thm -> string val pretty_goal_header: thm -> Pretty.T val string_of_goal: Proof.context -> thm -> string @@ -31,7 +31,7 @@ structure Proof_Display: PROOF_DISPLAY = struct -(* toplevel pretty printing *) +(** toplevel pretty printing **) fun pp_context ctxt = (if Config.get ctxt Proof_Context.debug then @@ -48,7 +48,7 @@ | NONE => Syntax.init_pretty_global (mk_thy ())); fun pp_thm mk_thy th = - Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; + Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T); fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t); @@ -57,30 +57,165 @@ fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct); -(* theorems and theory *) + +(** theory content **) + +fun pretty_theory verbose ctxt = + let + val thy = Proof_Context.theory_of ctxt; + + fun prt_cls c = Syntax.pretty_sort ctxt [c]; + fun prt_sort S = Syntax.pretty_sort ctxt S; + fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); + fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); + val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; + fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); + val prt_term_no_vars = prt_term o Logic.unvarify_global; + fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; + + fun pretty_classrel (c, []) = prt_cls c + | pretty_classrel (c, cs) = Pretty.block + (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); + + fun pretty_default S = Pretty.block + [Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; + + val tfrees = map (fn v => TFree (v, [])); + fun pretty_type syn (t, Type.LogicalType n) = + if syn then NONE + else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) + | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) = + if syn <> syn' then NONE + else SOME (Pretty.block + [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) + | pretty_type syn (t, Type.Nonterminal) = + if not syn then NONE + else SOME (prt_typ (Type (t, []))); + + val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); + + fun pretty_abbrev (c, (ty, t)) = Pretty.block + (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); + + fun pretty_axm (a, t) = + Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; -fun pretty_theorems_diff verbose prev_thys thy = + val tsig = Sign.tsig_of thy; + val consts = Sign.consts_of thy; + val {const_space, constants, constraints} = Consts.dest consts; + val {classes, default, types, ...} = Type.rep_tsig tsig; + val type_space = Type.type_space tsig; + val (class_space, class_algebra) = classes; + val classes = Sorts.classes_of class_algebra; + val arities = Sorts.arities_of class_algebra; + + val clsses = + Name_Space.extern_entries verbose ctxt class_space + (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) + |> map (apfst #1); + val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1); + val arties = + Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities) + |> map (apfst #1); + + val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; + val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; + val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; + val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; + + val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); + in + Pretty.chunks + [Pretty.big_list "classes:" (map pretty_classrel clsses), + pretty_default default, + Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), + Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), + Pretty.big_list "type arities:" (pretty_arities arties), + Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), + Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), + Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), + Pretty.big_list "axioms:" (map pretty_axm axms), + Pretty.block + (Pretty.breaks (Pretty.str "oracles:" :: + map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] + end; + + +(* theorems *) + +fun pretty_theorems_diff verbose prev_thys ctxt = let - val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy); - val facts = Global_Theory.facts_of thy; + val pretty_fact = Proof_Context.pretty_fact ctxt; + val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts; val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss)); in if null prts then [] else [Pretty.big_list "theorems:" prts] end; -fun pretty_theorems verbose thy = - pretty_theorems_diff verbose (Theory.parents_of thy) thy; +fun pretty_theorems verbose ctxt = + pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt; + + +(* definitions *) + +fun pretty_definitions verbose ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val context = Proof_Context.defs_context ctxt; + + val const_space = Proof_Context.const_space ctxt; + val type_space = Proof_Context.type_space ctxt; + val item_space = fn Defs.Const => const_space | Defs.Type => type_space; + fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c; + + fun extern_item (kind, name) = + let val xname = Name_Space.extern ctxt (item_space kind) name + in (xname, (kind, name)) end; + + fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) = + (case Defs.item_kind_ord (kind1, kind2) of + EQUAL => string_ord (xname1, xname2) + | ord => ord); + + fun sort_items f = sort (extern_item_ord o apply2 f); + + fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args); -fun pretty_full_theory verbose thy = - Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy); + fun pretty_reduct (lhs, rhs) = Pretty.block + ([pretty_entry lhs, Pretty.str " ->", Pretty.brk 2] @ + Pretty.commas (map pretty_entry (sort_items fst rhs))); + + fun pretty_restrict (entry, name) = + Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); + + val defs = Theory.defs_of thy; + val {restricts, reducts} = Defs.dest defs; -val print_theory = Pretty.writeln o pretty_full_theory false; + val (reds1, reds2) = + filter_out (prune_item o #1 o #1) reducts + |> map (fn (lhs, rhs) => + (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) + |> sort_items (#1 o #1) + |> filter_out (null o #2) + |> List.partition (Defs.plain_args o #2 o #1); + val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1); + in + Pretty.big_list "definitions:" + (map (Pretty.text_fold o single) + [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1), + Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2), + Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)]) + end; + + + +(** proof items **) (* refinement rule *) fun pretty_rule ctxt s thm = Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), - Pretty.fbrk, Display.pretty_thm ctxt thm]; + Pretty.fbrk, Thm.pretty_thm ctxt thm]; val string_of_rule = Pretty.string_of ooo pretty_rule; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/runtime.ML Fri Sep 25 23:41:24 2015 +0200 @@ -119,7 +119,7 @@ (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts)) | THM (msg, i, thms) => raised exn ("THM " ^ string_of_int i) - (msg :: robust_context context Display.string_of_thm thms) + (msg :: robust_context context Thm.string_of_thm thms) | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); in [((i, msg), id)] end) and sorted_msgs context exn = diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/token.ML Fri Sep 25 23:41:24 2015 +0200 @@ -498,7 +498,7 @@ | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => - Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths)) + Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); fun pretty_src ctxt src = diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Isar/typedecl.ML Fri Sep 25 23:41:24 2015 +0200 @@ -7,9 +7,12 @@ signature TYPEDECL = sig val read_constraint: Proof.context -> string option -> sort - val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory - val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory - val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory + val basic_typedecl: {final: bool} -> binding * int * mixfix -> + local_theory -> string * local_theory + val typedecl: {final: bool} -> binding * (string * sort) list * mixfix -> + local_theory -> typ * local_theory + val typedecl_global: {final: bool} -> binding * (string * sort) list * mixfix -> + theory -> typ * theory val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory @@ -35,13 +38,6 @@ |> pair name end; -fun basic_typedecl (b, n, mx) lthy = - basic_decl (fn name => - Sign.add_type lthy (b, n, NoSyn) #> - (case Object_Logic.get_base_sort lthy of - SOME S => Axclass.arity_axiomatization (name, replicate n S, S) - | NONE => I)) (b, n, mx) lthy; - (* global type -- without dependencies on type parameters of the context *) @@ -61,21 +57,39 @@ commas_quote (map (Syntax.string_of_typ lthy) bad_args)); in T end; +fun final_type (b, n) lthy = + let + val c = Local_Theory.full_name lthy b; + val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); + in + Local_Theory.background_theory + (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy + end; + +fun basic_typedecl {final} (b, n, mx) lthy = + lthy + |> basic_decl (fn name => + Sign.add_type lthy (b, n, NoSyn) #> + (case Object_Logic.get_base_sort lthy of + SOME S => Axclass.arity_axiomatization (name, replicate n S, S) + | NONE => I)) (b, n, mx) + ||> final ? final_type (b, n); + (* type declarations *) -fun typedecl (b, raw_args, mx) lthy = +fun typedecl {final} (b, raw_args, mx) lthy = let val T = global_type lthy (b, raw_args) in lthy - |> basic_typedecl (b, length raw_args, mx) + |> basic_typedecl {final = final} (b, length raw_args, mx) |> snd |> Variable.declare_typ T |> pair T end; -fun typedecl_global decl = +fun typedecl_global {final} decl = Named_Target.theory_init - #> typedecl decl + #> typedecl {final = final} decl #> Local_Theory.exit_result_global Morphism.typ; @@ -121,4 +135,3 @@ #> Local_Theory.exit_result_global (K I); end; - diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Proof/reconstruct.ML Fri Sep 25 23:41:24 2015 +0200 @@ -254,8 +254,8 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2 - (Envir.norm_term bigenv) p)) cs))) + Thm.pretty_flexpair (Syntax.init_pretty_global thy) + (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then let diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Pure.thy Fri Sep 25 23:41:24 2015 +0200 @@ -74,8 +74,8 @@ and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" - and "help" "print_commands" "print_options" "print_context" - "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules" + and "help" "print_commands" "print_options" "print_context" "print_theory" + "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_dependencies" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/ROOT --- a/src/Pure/ROOT Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/ROOT Fri Sep 25 23:41:24 2015 +0200 @@ -247,7 +247,6 @@ "context_position.ML" "conv.ML" "defs.ML" - "display.ML" "drule.ML" "envir.ML" "facts.ML" diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/ROOT.ML Fri Sep 25 23:41:24 2015 +0200 @@ -170,8 +170,8 @@ use "envir.ML"; use "consts.ML"; use "primitive_defs.ML"; +use "sign.ML"; use "defs.ML"; -use "sign.ML"; use "term_sharing.ML"; use "pattern.ML"; use "unify.ML"; @@ -195,7 +195,6 @@ use "raw_simplifier.ML"; use "conjunction.ML"; use "assumption.ML"; -use "display.ML"; (* Isar -- Intelligible Semi-Automated Reasoning *) diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Sep 25 23:41:24 2015 +0200 @@ -65,7 +65,7 @@ val is_pretty_global: Proof.context -> bool val set_pretty_global: bool -> Proof.context -> Proof.context val init_pretty_global: theory -> Proof.context - val init_pretty: Context.pretty -> Proof.context + val init_pretty: Context.generic -> Proof.context val pretty_term_global: theory -> term -> Pretty.T val pretty_typ_global: theory -> typ -> Pretty.T val pretty_sort_global: theory -> sort -> Pretty.T @@ -324,7 +324,7 @@ fun is_pretty_global ctxt = Config.get ctxt pretty_global; val set_pretty_global = Config.put pretty_global; val init_pretty_global = set_pretty_global true o Proof_Context.init_global; -val init_pretty = Context.pretty_context init_pretty_global; +val init_pretty = Context.cases init_pretty_global I; val pretty_term_global = pretty_term o init_pretty_global; val pretty_typ_global = pretty_typ o init_pretty_global; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Tools/class_deps.ML --- a/src/Pure/Tools/class_deps.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Tools/class_deps.ML Fri Sep 25 23:41:24 2015 +0200 @@ -29,7 +29,7 @@ Graph_Display.content_node (Name_Space.extern ctxt space c) (Class.pretty_specification (Proof_Context.theory_of ctxt) c); in - Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra + Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra |> #2 |> Sorts.classes_of |> Graph.dest |> map (fn ((c, _), ds) => ((c, node c), ds)) end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Sep 25 23:41:24 2015 +0200 @@ -462,7 +462,7 @@ in fun pretty_thm ctxt (thmref, thm) = - Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]); + Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]); fun pretty_theorems state opt_limit rem_dups raw_criteria = let diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/axclass.ML Fri Sep 25 23:41:24 2015 +0200 @@ -82,25 +82,25 @@ Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels, proven_arities = proven_arities, inst_params = inst_params}; -structure Data = Theory_Data_PP +structure Data = Theory_Data' ( type T = data; val empty = make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty)); val extend = I; - fun merge pp + fun merge old_thys (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1, proven_arities = proven_arities1, inst_params = inst_params1}, Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2, proven_arities = proven_arities2, inst_params = inst_params2}) = let - val ctxt = Syntax.init_pretty pp; + val old_ctxt = Syntax.init_pretty_global (fst old_thys); val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); val params' = if null params1 then params2 else - fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p) + fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p) params2 params1; (*see Theory.at_begin hook for transitive closure of classrels and arity completion*) @@ -596,6 +596,9 @@ fun class_const c = (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); +fun class_const_dep c = + ((Defs.Const, Logic.const_of_class c), [Term.aT []]); + in val classrel_axiomatization = @@ -614,7 +617,7 @@ thy |> Sign.primitive_class (bclass, super) |> classrel_axiomatization (map (fn c => (class, c)) super) - |> Theory.add_deps_global "" (class_const class) (map class_const super) + |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super) end; end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/consts.ML Fri Sep 25 23:41:24 2015 +0200 @@ -27,7 +27,7 @@ val intern: T -> xstring -> string val intern_syntax: T -> xstring -> string val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list - val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) + val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ val declare: Context.generic -> binding * typ -> T -> T @@ -155,11 +155,11 @@ (* certify *) -fun certify pp tsig do_expand consts = +fun certify context tsig do_expand consts = let fun err msg (c, T) = raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ - Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []); + Syntax.string_of_typ (Syntax.init_pretty context) T, [], []); val certT = Type.cert_typ tsig; fun cert tm = let @@ -272,9 +272,8 @@ fun abbreviate context tsig mode (b, raw_rhs) consts = let - val pp = Context.pretty_generic context; - val cert_term = certify pp tsig false consts; - val expand_term = certify pp tsig true consts; + val cert_term = certify context tsig false consts; + val expand_term = certify context tsig true consts; val force_expand = mode = Print_Mode.internal; val _ = Term.exists_subterm Term.is_Var raw_rhs andalso diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/context.ML --- a/src/Pure/context.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/context.ML Fri Sep 25 23:41:24 2015 +0200 @@ -31,14 +31,11 @@ type theory_id val theory_id: theory -> theory_id val timing: bool Unsynchronized.ref - type pretty val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_id_name: theory_id -> string val theory_name: theory -> string val PureN: string - val display_name: theory_id -> string - val display_names: theory -> string list val pretty_thy: theory -> Pretty.T val string_of_thy: theory -> string val pretty_abbrev_thy: theory -> Pretty.T @@ -52,7 +49,7 @@ val subthy_id: theory_id * theory_id -> bool val subthy: theory * theory -> bool val finish_thy: theory -> theory - val begin_thy: (theory -> pretty) -> string -> theory list -> theory + val begin_thy: string -> theory list -> theory (*proof context*) val raw_transfer: theory -> Proof.context -> Proof.context (*certificate*) @@ -77,11 +74,6 @@ val proof_map: (generic -> generic) -> Proof.context -> Proof.context val theory_of: generic -> theory (*total*) val proof_of: generic -> Proof.context (*total*) - (*pretty printing context*) - val pretty: Proof.context -> pretty - val pretty_global: theory -> pretty - val pretty_generic: generic -> pretty - val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context (*thread data*) val thread_data: unit -> generic option val the_thread_data: unit -> generic @@ -97,7 +89,7 @@ structure Theory_Data: sig val declare: Position.T -> Any.T -> (Any.T -> Any.T) -> - (pretty -> Any.T * Any.T -> Any.T) -> serial + (theory * theory -> Any.T * Any.T -> Any.T) -> serial val get: serial -> (Any.T -> 'a) -> theory -> 'a val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory end @@ -114,55 +106,9 @@ (*** theory context ***) -(** theory data **) - -(* data kinds and access methods *) - -val timing = Unsynchronized.ref false; - (*private copy avoids potential conflict of table exceptions*) structure Datatab = Table(type key = int val ord = int_ord); -datatype pretty = Pretty of Any.T; - -local - -type kind = - {pos: Position.T, - empty: Any.T, - extend: Any.T -> Any.T, - merge: pretty -> Any.T * Any.T -> Any.T}; - -val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); - -fun invoke name f k x = - (case Datatab.lookup (Synchronized.value kinds) k of - SOME kind => - if ! timing andalso name <> "" then - Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) - (fn () => f kind x) - else f kind x - | NONE => raise Fail "Invalid theory data identifier"); - -in - -fun invoke_empty k = invoke "" (K o #empty) k (); -val invoke_extend = invoke "extend" #extend; -fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp); - -fun declare_theory_data pos empty extend merge = - let - val k = serial (); - val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; - val _ = Synchronized.change kinds (Datatab.update (k, kind)); - in k end; - -val extend_data = Datatab.map invoke_extend; -fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data; - -end; - - (** datatype theory **) @@ -288,6 +234,51 @@ +(** theory data **) + +(* data kinds and access methods *) + +val timing = Unsynchronized.ref false; + +local + +type kind = + {pos: Position.T, + empty: Any.T, + extend: Any.T -> Any.T, + merge: theory * theory -> Any.T * Any.T -> Any.T}; + +val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); + +fun invoke name f k x = + (case Datatab.lookup (Synchronized.value kinds) k of + SOME kind => + if ! timing andalso name <> "" then + Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) + (fn () => f kind x) + else f kind x + | NONE => raise Fail "Invalid theory data identifier"); + +in + +fun invoke_empty k = invoke "" (K o #empty) k (); +val invoke_extend = invoke "extend" #extend; +fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys); + +fun declare_theory_data pos empty extend merge = + let + val k = serial (); + val kind = {pos = pos, empty = empty, extend = extend, merge = merge}; + val _ = Synchronized.change kinds (Datatab.update (k, kind)); + in k end; + +val extend_data = Datatab.map invoke_extend; +fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data; + +end; + + + (** build theories **) (* primitives *) @@ -325,12 +316,12 @@ local -fun merge_thys pp (thy1, thy2) = +fun merge_thys (thy1, thy2) = let val ids = merge_ids thy1 thy2; val history = make_history "" 0; val ancestry = make_ancestry [] []; - val data = merge_data (pp thy1) (data_of thy1, data_of thy2); + val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2); in create_thy ids history ancestry data end; fun maximal_thys thys = @@ -338,7 +329,7 @@ in -fun begin_thy pp name imports = +fun begin_thy name imports = if name = "" then error ("Bad theory name: " ^ quote name) else let @@ -351,7 +342,7 @@ (case parents of [] => error "Missing theory imports" | [thy] => extend_thy thy - | thy :: thys => Library.foldl (merge_thys pp) (thy, thys)); + | thy :: thys => Library.foldl merge_thys (thy, thys)); val history = make_history name 0; val ancestry = make_ancestry parents ancestors; @@ -498,17 +489,6 @@ val proof_of = cases Proof_Context.init_global I; -(* pretty printing context *) - -exception PRETTY of generic; - -val pretty_generic = Pretty o PRETTY; -val pretty = pretty_generic o Proof; -val pretty_global = pretty_generic o Theory; - -fun pretty_context init (Pretty (PRETTY context)) = cases init I context; - - (** thread data **) @@ -551,12 +531,12 @@ (** theory data **) -signature THEORY_DATA_PP_ARGS = +signature THEORY_DATA'_ARGS = sig type T val empty: T val extend: T -> T - val merge: Context.pretty -> T * T -> T + val merge: theory * theory -> T * T -> T end; signature THEORY_DATA_ARGS = @@ -575,7 +555,7 @@ val map: (T -> T) -> theory -> theory end; -functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA = +functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA = struct type T = Data.T; @@ -586,7 +566,7 @@ (Position.thread_data ()) (Data Data.empty) (fn Data x => Data (Data.extend x)) - (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2))); + (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2))); val get = Context.Theory_Data.get kind (fn Data x => x); val put = Context.Theory_Data.put kind Data; @@ -595,7 +575,7 @@ end; functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = - Theory_Data_PP + Theory_Data' ( type T = Data.T; val empty = Data.empty; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/defs.ML --- a/src/Pure/defs.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/defs.ML Fri Sep 25 23:41:24 2015 +0200 @@ -7,39 +7,76 @@ signature DEFS = sig - val pretty_const: Proof.context -> string * typ list -> Pretty.T + datatype item_kind = Const | Type + type item = item_kind * string + type entry = item * typ list + val item_kind_ord: item_kind * item_kind -> order val plain_args: typ list -> bool + type context = Proof.context * (Name_Space.T * Name_Space.T) + val global_context: theory -> context + val space: context -> item_kind -> Name_Space.T + val pretty_item: context -> item -> Pretty.T + val pretty_args: Proof.context -> typ list -> Pretty.T list + val pretty_entry: context -> entry -> Pretty.T type T type spec = {def: string option, description: string, pos: Position.T, lhs: typ list, - rhs: (string * typ list) list} - val all_specifications_of: T -> (string * spec list) list - val specifications_of: T -> string -> spec list + rhs: entry list} + val all_specifications_of: T -> (item * spec list) list + val specifications_of: T -> item -> spec list val dest: T -> - {restricts: ((string * typ list) * string) list, - reducts: ((string * typ list) * (string * typ list) list) list} + {restricts: (entry * string) list, + reducts: (entry * entry list) list} val empty: T - val merge: Proof.context -> T * T -> T - val define: Proof.context -> bool -> string option -> string -> - string * typ list -> (string * typ list) list -> T -> T -end + val merge: context -> T * T -> T + val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T + val get_deps: T -> item -> (typ list * entry list) list +end; structure Defs: DEFS = struct -(* type arguments *) +(* specification items *) + +datatype item_kind = Const | Type; +type item = item_kind * string; +type entry = item * typ list; -type args = typ list; +fun item_kind_ord (Const, Type) = LESS + | item_kind_ord (Type, Const) = GREATER + | item_kind_ord _ = EQUAL; + +structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord); + + +(* pretty printing *) + +type context = Proof.context * (Name_Space.T * Name_Space.T) -fun pretty_const ctxt (c, args) = - let - val prt_args = - if null args then [] - else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; - in Pretty.block (Pretty.str c :: prt_args) end; +fun global_context thy = + (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy)); + +fun space ((ctxt, spaces): context) kind = + if kind = Const then #1 spaces else #2 spaces; + +fun pretty_item (context as (ctxt, _)) (kind, name) = + let val prt_name = Name_Space.pretty ctxt (space context kind) name in + if kind = Const then prt_name + else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name] + end; + +fun pretty_args ctxt args = + if null args then [] + else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; + +fun pretty_entry context (c, args) = + Pretty.block (pretty_item context c :: pretty_args (#1 context) args); + + +(* type arguments *) fun plain_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args); @@ -62,32 +99,32 @@ {def: string option, description: string, pos: Position.T, - lhs: args, - rhs: (string * args) list}; + lhs: typ list, + rhs: entry list}; type def = {specs: spec Inttab.table, (*source specifications*) - restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) - reducts: (args * (string * args) list) list}; (*specifications as reduction system*) + restricts: (typ list * string) list, (*global restrictions imposed by incomplete patterns*) + reducts: (typ list * entry list) list}; (*specifications as reduction system*) fun make_def (specs, restricts, reducts) = {specs = specs, restricts = restricts, reducts = reducts}: def; fun map_def c f = - Symtab.default (c, make_def (Inttab.empty, [], [])) #> - Symtab.map_entry c (fn {specs, restricts, reducts}: def => + Itemtab.default (c, make_def (Inttab.empty, [], [])) #> + Itemtab.map_entry c (fn {specs, restricts, reducts}: def => make_def (f (specs, restricts, reducts))); -datatype T = Defs of def Symtab.table; +datatype T = Defs of def Itemtab.table; fun lookup_list which defs c = - (case Symtab.lookup defs c of + (case Itemtab.lookup defs c of SOME (def: def) => which def | NONE => []); fun all_specifications_of (Defs defs) = - (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs); + (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs); fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; @@ -96,56 +133,58 @@ fun dest (Defs defs) = let - val restricts = Symtab.fold (fn (c, {restricts, ...}) => + val restricts = Itemtab.fold (fn (c, {restricts, ...}) => fold (fn (args, description) => cons ((c, args), description)) restricts) defs []; - val reducts = Symtab.fold (fn (c, {reducts, ...}) => + val reducts = Itemtab.fold (fn (c, {reducts, ...}) => fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; in {restricts = restricts, reducts = reducts} end; -val empty = Defs Symtab.empty; +val empty = Defs Itemtab.empty; (* specifications *) -fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = +fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => i = j orelse disjoint_args (Ts, Us) orelse - error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^ + error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^ " " ^ quote a ^ Position.here pos_a ^ "\n" ^ " " ^ quote b ^ Position.here pos_b)); -fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = +fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = let val specs' = - Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1; + Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2)) + specs2 specs1; in make_def (specs', restricts, reducts) end; -fun update_specs c spec = map_def c (fn (specs, restricts, reducts) => - (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts))); +fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) => + (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts))); (* normalized dependencies: reduction with well-formedness check *) local -val prt = Pretty.string_of oo pretty_const; -fun err ctxt (c, args) (d, Us) s1 s2 = - error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); +val prt = Pretty.string_of oo pretty_entry; -fun acyclic ctxt (c, args) (d, Us) = +fun err context (c, args) (d, Us) s1 s2 = + error (s1 ^ " dependency of " ^ prt context (c, args) ^ " -> " ^ prt context (d, Us) ^ s2); + +fun acyclic context (c, args) (d, Us) = c <> d orelse is_none (match_args (args, Us)) orelse - err ctxt (c, args) (d, Us) "Circular" ""; + err context (c, args) (d, Us) "Circular" ""; -fun wellformed ctxt defs (c, args) (d, Us) = +fun wellformed context defs (c, args) (d, Us) = plain_args Us orelse (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of SOME (Ts, description) => - err ctxt (c, args) (d, Us) "Malformed" - ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")") + err context (c, args) (d, Us) "Malformed" + ("\n(restriction " ^ prt context (d, Ts) ^ " from " ^ quote description ^ ")") | NONE => true); -fun reduction ctxt defs const deps = +fun reduction context defs const deps = let fun reduct Us (Ts, rhs) = (case match_args (Ts, Us) of @@ -158,67 +197,69 @@ if forall (is_none o #1) reds then NONE else SOME (fold_rev (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); - val _ = forall (acyclic ctxt const) (the_default deps deps'); + val _ = forall (acyclic context const) (the_default deps deps'); in deps' end; in -fun normalize ctxt = +fun normalize context = let fun norm_update (c, {reducts, ...}: def) (changed, defs) = let val reducts' = reducts |> map (fn (args, deps) => - (args, perhaps (reduction ctxt defs (c, args)) deps)); + (args, perhaps (reduction context defs (c, args)) deps)); in if reducts = reducts' then (changed, defs) else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) end; fun norm_all defs = - (case Symtab.fold norm_update defs (false, defs) of + (case Itemtab.fold norm_update defs (false, defs) of (true, defs') => norm_all defs' | (false, _) => defs); fun check defs (c, {reducts, ...}: def) = - reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps); - in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end; + reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps); + in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end; -fun dependencies ctxt (c, args) restr deps = +fun dependencies context (c, args) restr deps = map_def c (fn (specs, restricts, reducts) => let val restricts' = Library.merge (op =) (restricts, restr); val reducts' = insert (op =) (args, deps) reducts; in (specs, restricts', reducts') end) - #> normalize ctxt; + #> normalize context; end; (* merge *) -fun merge ctxt (Defs defs1, Defs defs2) = +fun merge context (Defs defs1, Defs defs2) = let fun add_deps (c, args) restr deps defs = if AList.defined (op =) (reducts_of defs c) args then defs - else dependencies ctxt (c, args) restr deps defs; + else dependencies context (c, args) restr deps defs; fun add_def (c, {restricts, reducts, ...}: def) = fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; in - Defs (Symtab.join join_specs (defs1, defs2) - |> normalize ctxt |> Symtab.fold add_def defs2) + Defs (Itemtab.join (join_specs context) (defs1, defs2) + |> normalize context |> Itemtab.fold add_def defs2) end; (* define *) -fun define ctxt unchecked def description (c, args) deps (Defs defs) = +fun define context unchecked def description (c, args) deps (Defs defs) = let val pos = Position.thread_data (); val restr = if plain_args args orelse - (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false) + (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false) then [] else [(args, description)]; val spec = (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); - val defs' = defs |> update_specs c spec; - in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end; + val defs' = defs |> update_specs context c spec; + in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end; + +fun get_deps (Defs defs) c = reducts_of defs c; end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/display.ML --- a/src/Pure/display.ML Fri Sep 25 16:54:31 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,205 +0,0 @@ -(* Title: Pure/display.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Makarius - -Printing of theorems, results etc. -*) - -signature BASIC_DISPLAY = -sig - val show_consts: bool Config.T - val show_hyps_raw: Config.raw - val show_hyps: bool Config.T - val show_tags_raw: Config.raw - val show_tags: bool Config.T -end; - -signature DISPLAY = -sig - include BASIC_DISPLAY - val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T - val pretty_thm: Proof.context -> thm -> Pretty.T - val pretty_thm_item: Proof.context -> thm -> Pretty.T - val pretty_thm_global: theory -> thm -> Pretty.T - val string_of_thm: Proof.context -> thm -> string - val string_of_thm_global: theory -> thm -> string - val pretty_full_theory: bool -> theory -> Pretty.T list -end; - -structure Display: DISPLAY = -struct - -(** options **) - -val show_consts = Goal_Display.show_consts; - -val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false); -val show_hyps = Config.bool show_hyps_raw; - -val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false); -val show_tags = Config.bool show_tags_raw; - - - -(** print thm **) - -fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; -val pretty_tags = Pretty.list "[" "]" o map pretty_tag; - -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = - let - val show_tags = Config.get ctxt show_tags; - val show_hyps = Config.get ctxt show_hyps; - - val th = raw_th - |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt))) - |> perhaps (try Thm.strip_shyps); - - val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th; - val extra_shyps = Thm.extra_shyps th; - val tags = Thm.get_tags th; - val tpairs = Thm.tpairs_of th; - - val q = if quote then Pretty.quote else I; - val prt_term = q o Syntax.pretty_term ctxt; - - - val hlen = length extra_shyps + length hyps + length tpairs; - val hsymbs = - if hlen = 0 then [] - else if show_hyps orelse show_hyps' then - [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ - map (Syntax.pretty_sort ctxt) extra_shyps)] - else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; - val tsymbs = - if null tags orelse not show_tags then [] - else [Pretty.brk 1, pretty_tags tags]; - in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; - -fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; -fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; - -fun pretty_thm_global thy = - pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; - -val string_of_thm = Pretty.string_of oo pretty_thm; -val string_of_thm_global = Pretty.string_of oo pretty_thm_global; - - - -(** print theory **) - -(* pretty_full_theory *) - -fun pretty_full_theory verbose thy = - let - val ctxt = Syntax.init_pretty_global thy; - - fun prt_cls c = Syntax.pretty_sort ctxt [c]; - fun prt_sort S = Syntax.pretty_sort ctxt S; - fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); - fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); - val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; - fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); - val prt_term_no_vars = prt_term o Logic.unvarify_global; - fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; - val prt_const' = Defs.pretty_const ctxt; - - fun pretty_classrel (c, []) = prt_cls c - | pretty_classrel (c, cs) = Pretty.block - (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); - - fun pretty_default S = Pretty.block - [Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; - - val tfrees = map (fn v => TFree (v, [])); - fun pretty_type syn (t, (Type.LogicalType n)) = - if syn then NONE - else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) - | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) = - if syn <> syn' then NONE - else SOME (Pretty.block - [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) - | pretty_type syn (t, Type.Nonterminal) = - if not syn then NONE - else SOME (prt_typ (Type (t, []))); - - val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); - - fun pretty_abbrev (c, (ty, t)) = Pretty.block - (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); - - fun pretty_axm (a, t) = - Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; - - fun pretty_finals reds = Pretty.block - (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds)); - - fun pretty_reduct (lhs, rhs) = Pretty.block - ([prt_const' lhs, Pretty.str " ->", Pretty.brk 2] @ - Pretty.commas (map prt_const' (sort_by #1 rhs))); - - fun pretty_restrict (const, name) = - Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); - - val defs = Theory.defs_of thy; - val {restricts, reducts} = Defs.dest defs; - val tsig = Sign.tsig_of thy; - val consts = Sign.consts_of thy; - val {const_space, constants, constraints} = Consts.dest consts; - val extern_const = Name_Space.extern ctxt const_space; - val {classes, default, types, ...} = Type.rep_tsig tsig; - val (class_space, class_algebra) = classes; - val classes = Sorts.classes_of class_algebra; - val arities = Sorts.arities_of class_algebra; - - val clsses = - Name_Space.extern_entries verbose ctxt class_space - (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) - |> map (apfst #1); - val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1); - val arties = - Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities) - |> map (apfst #1); - - val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; - val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; - val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; - val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; - - val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); - - fun prune_const c = not verbose andalso Consts.is_concealed consts c; - val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts - |> map (fn (lhs, rhs) => - (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) - |> sort_by (#1 o #1) - |> List.partition (null o #2) - ||> List.partition (Defs.plain_args o #2 o #1); - val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1); - in - [Pretty.strs ("names:" :: Context.display_names thy)] @ - [Pretty.big_list "classes:" (map pretty_classrel clsses), - pretty_default default, - Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), - Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), - Pretty.big_list "type arities:" (pretty_arities arties), - Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), - Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), - Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), - Pretty.big_list "axioms:" (map pretty_axm axms), - Pretty.block - (Pretty.breaks (Pretty.str "oracles:" :: - map Pretty.mark_str (Thm.extern_oracles verbose ctxt))), - Pretty.big_list "definitions:" - [pretty_finals reds0, - Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), - Pretty.big_list "overloaded:" (map pretty_reduct reds2), - Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] - end; - -end; - -structure Basic_Display: BASIC_DISPLAY = Display; -open Basic_Display; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/global_theory.ML Fri Sep 25 23:41:24 2015 +0200 @@ -205,9 +205,9 @@ fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy => let - val ctxt = Syntax.init_pretty_global thy; + val context as (ctxt, _) = Defs.global_context thy; val prop = prep ctxt (b, raw_prop); - val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy; + val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy; val thm = def |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/goal_display.ML Fri Sep 25 23:41:24 2015 +0200 @@ -11,9 +11,6 @@ val goals_limit: int Config.T val show_main_goal_raw: Config.raw val show_main_goal: bool Config.T - val show_consts_raw: Config.raw - val show_consts: bool Config.T - val pretty_flexpair: Proof.context -> term * term -> Pretty.T val pretty_goals: Proof.context -> thm -> Pretty.T list val pretty_goal: Proof.context -> thm -> Pretty.T val string_of_goal: Proof.context -> thm -> string @@ -28,12 +25,6 @@ val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here}); val show_main_goal = Config.bool show_main_goal_raw; -val show_consts_raw = Config.declare_option ("show_consts", @{here}); -val show_consts = Config.bool show_consts_raw; - -fun pretty_flexpair ctxt (t, u) = Pretty.block - [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; - (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) @@ -107,7 +98,7 @@ Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A]; val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A); - val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt); + val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt); val pretty_consts = pretty_list "constants:" prt_consts o consts_of; val pretty_vars = pretty_list "variables:" prt_vars o vars_of; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/more_thm.ML Fri Sep 25 23:41:24 2015 +0200 @@ -9,6 +9,9 @@ signature BASIC_THM = sig include BASIC_THM + val show_consts: bool Config.T + val show_hyps: bool Config.T + val show_tags: bool Config.T structure Ctermtab: TABLE structure Thmtab: TABLE val aconvc: cterm * cterm -> bool @@ -72,7 +75,7 @@ val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory - val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory + val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list @@ -105,6 +108,19 @@ val kind: string -> attribute val register_proofs: thm list -> theory -> theory val join_theory_proofs: theory -> unit + val show_consts_raw: Config.raw + val show_consts: bool Config.T + val show_hyps_raw: Config.raw + val show_hyps: bool Config.T + val show_tags_raw: Config.raw + val show_tags: bool Config.T + val pretty_flexpair: Proof.context -> term * term -> Pretty.T + val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T + val pretty_thm: Proof.context -> thm -> Pretty.T + val pretty_thm_item: Proof.context -> thm -> Pretty.T + val pretty_thm_global: theory -> thm -> Pretty.T + val string_of_thm: Proof.context -> thm -> string + val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = @@ -290,12 +306,8 @@ (case undeclared_hyps context th of [] => th | undeclared => - let - val ctxt = Context.cases Syntax.init_pretty_global I context; - in - error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" - (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared))) - end); + error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" + (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); @@ -475,13 +487,13 @@ fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; -fun add_def ctxt unchecked overloaded (b, prop) thy = +fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); - val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy; + val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = @@ -491,7 +503,7 @@ in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = - add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy; + add_def (Defs.global_context thy) unchecked overloaded arg thy; @@ -590,6 +602,70 @@ Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy))); + +(** print theorems **) + +(* options *) + +val show_consts_raw = Config.declare_option ("show_consts", @{here}); +val show_consts = Config.bool show_consts_raw; + +val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false); +val show_hyps = Config.bool show_hyps_raw; + +val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false); +val show_tags = Config.bool show_tags_raw; + + +(* pretty_thm etc. *) + +fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; +val pretty_tags = Pretty.list "[" "]" o map pretty_tag; + +fun pretty_flexpair ctxt (t, u) = Pretty.block + [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; + +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = + let + val show_tags = Config.get ctxt show_tags; + val show_hyps = Config.get ctxt show_hyps; + + val th = raw_th + |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt))) + |> perhaps (try Thm.strip_shyps); + + val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; + val extra_shyps = Thm.extra_shyps th; + val tags = Thm.get_tags th; + val tpairs = Thm.tpairs_of th; + + val q = if quote then Pretty.quote else I; + val prt_term = q o Syntax.pretty_term ctxt; + + + val hlen = length extra_shyps + length hyps + length tpairs; + val hsymbs = + if hlen = 0 then [] + else if show_hyps orelse show_hyps' then + [Pretty.brk 2, Pretty.list "[" "]" + (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @ + map (Syntax.pretty_sort ctxt) extra_shyps)] + else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; + val tsymbs = + if null tags orelse not show_tags then [] + else [Pretty.brk 1, pretty_tags tags]; + in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; + +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; +fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; + +fun pretty_thm_global thy = + pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; + +val string_of_thm = Pretty.string_of oo pretty_thm; +val string_of_thm_global = Pretty.string_of oo pretty_thm_global; + + open Thm; end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/pure_thy.ML Fri Sep 25 23:41:24 2015 +0200 @@ -66,6 +66,10 @@ (Binding.make ("prop", @{here}), 0, NoSyn), (Binding.make ("itself", @{here}), 1, NoSyn), (Binding.make ("dummy", @{here}), 0, NoSyn)] + #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) [] + #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) [] + #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) [] + #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) [] #> Sign.add_nonterminals_global (map (fn name => Binding.make (name, @{here})) (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", @@ -194,11 +198,11 @@ (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")] - #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") [] - #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") [] - #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") [] - #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") [] - #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") [] + #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) [] + #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) [] + #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) [] + #> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) [] + #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) [] #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/sign.ML Fri Sep 25 23:41:24 2015 +0200 @@ -62,7 +62,7 @@ val certify_sort: theory -> sort -> sort val certify_typ: theory -> typ -> typ val certify_typ_mode: Type.mode -> theory -> typ -> typ - val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int + val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int val certify_term: theory -> term -> term * typ * int val cert_term: theory -> term -> term val cert_prop: theory -> term -> term @@ -133,20 +133,20 @@ fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts}; -structure Data = Theory_Data_PP +structure Data = Theory_Data' ( type T = sign; fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts); val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty); - fun merge pp (sign1, sign2) = + fun merge old_thys (sign1, sign2) = let val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1; val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2; val syn = Syntax.merge_syntax (syn1, syn2); - val tsig = Type.merge_tsig pp (tsig1, tsig2); + val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2); val consts = Consts.merge (consts1, consts2); in make_sign (syn, tsig, consts) end; ); @@ -257,7 +257,7 @@ (* certify wrt. type signature *) val arity_number = Type.arity_number o tsig_of; -fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy); +fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy); val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; @@ -269,14 +269,14 @@ local -fun type_check pp tm = +fun type_check context tm = let fun err_appl bs t T u U = let val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); - val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U; + val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U; in raise TYPE (msg, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T @@ -306,20 +306,19 @@ in -fun certify' prop pp do_expand consts thy tm = +fun certify' prop context do_expand consts thy tm = let val _ = check_vars tm; val tm' = Term.map_types (certify_typ thy) tm; - val T = type_check pp 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 pp (tsig_of thy) do_expand consts tm'; + val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm'; in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end; -fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy; -fun cert_term_abbrev thy = - #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy; +fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy; +fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy; val cert_term = #1 oo certify_term; -fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy; +fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy; end; @@ -474,10 +473,10 @@ |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; fun primitive_classrel arg thy = - thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg); + thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg); fun primitive_arity arg thy = - thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg); + thy |> map_tsig (Type.add_arity (Context.Theory thy) arg); (* add translation functions *) diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/simplifier.ML Fri Sep 25 23:41:24 2015 +0200 @@ -162,8 +162,8 @@ fun pretty_simpset verbose ctxt = let val pretty_term = Syntax.pretty_term ctxt; - val pretty_thm = Display.pretty_thm ctxt; - val pretty_thm_item = Display.pretty_thm_item ctxt; + val pretty_thm = Thm.pretty_thm ctxt; + val pretty_thm_item = Thm.pretty_thm_item ctxt; fun pretty_simproc (name, lhss) = Pretty.block diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/sorts.ML Fri Sep 25 23:41:24 2015 +0200 @@ -38,15 +38,15 @@ val minimize_sort: algebra -> sort -> sort val complete_sort: algebra -> sort -> sort val minimal_sorts: algebra -> sort list -> sort Ord_List.T - val add_class: Context.pretty -> class * class list -> algebra -> algebra - val add_classrel: Context.pretty -> class * class -> algebra -> algebra - val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra + val add_class: Context.generic -> class * class list -> algebra -> algebra + val add_classrel: Context.generic -> class * class -> algebra -> algebra + val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra val empty_algebra: algebra - val merge_algebra: Context.pretty -> algebra * algebra -> algebra - val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option) + val merge_algebra: Context.generic -> algebra * algebra -> algebra + val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option) -> algebra -> (sort -> sort) * algebra type class_error - val class_error: Context.pretty -> class_error -> string + val class_error: Context.generic -> class_error -> string exception CLASS_ERROR of class_error val has_instance: algebra -> string -> sort -> bool val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*) @@ -188,16 +188,16 @@ fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c); -fun err_cyclic_classes pp css = +fun err_cyclic_classes context css = error (cat_lines (map (fn cs => - "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css)); + "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty context) cs) css)); -fun add_class pp (c, cs) = map_classes (fn classes => +fun add_class context (c, cs) = map_classes (fn classes => let val classes' = classes |> Graph.new_node (c, serial ()) handle Graph.DUP dup => err_dup_class dup; val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs) - handle Graph.CYCLES css => err_cyclic_classes pp css; + handle Graph.CYCLES css => err_cyclic_classes context css; in classes'' end); @@ -208,14 +208,14 @@ fun for_classes _ NONE = "" | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2]; -fun err_conflict pp t cc (c, Ss) (c', Ss') = - let val ctxt = Syntax.init_pretty pp in +fun err_conflict context t cc (c, Ss) (c', Ss') = + let val ctxt = Syntax.init_pretty context in error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n " ^ Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n " ^ Syntax.string_of_arity ctxt (t, Ss', [c'])) end; -fun coregular pp algebra t (c, Ss) ars = +fun coregular context algebra t (c, Ss) ars = let fun conflict (c', Ss') = if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then @@ -225,62 +225,62 @@ else NONE; in (case get_first conflict ars of - SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') + SOME ((c1, c2), (c', Ss')) => err_conflict context t (SOME (c1, c2)) (c, Ss) (c', Ss') | NONE => (c, Ss) :: ars) end; fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c); -fun insert pp algebra t (c, Ss) ars = +fun insert context algebra t (c, Ss) ars = (case AList.lookup (op =) ars c of - NONE => coregular pp algebra t (c, Ss) ars + NONE => coregular context algebra t (c, Ss) ars | SOME Ss' => if sorts_le algebra (Ss, Ss') then ars else if sorts_le algebra (Ss', Ss) - then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars) - else err_conflict pp t NONE (c, Ss) (c, Ss')); + then coregular context algebra t (c, Ss) (remove (op =) (c, Ss') ars) + else err_conflict context t NONE (c, Ss) (c, Ss')); in -fun insert_ars pp algebra t = fold_rev (insert pp algebra t); +fun insert_ars context algebra t = fold_rev (insert context algebra t); -fun insert_complete_ars pp algebra (t, ars) arities = +fun insert_complete_ars context algebra (t, ars) arities = let val ars' = Symtab.lookup_list arities t - |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars); + |> fold_rev (insert_ars context algebra t) (map (complete algebra) ars); in Symtab.update (t, ars') arities end; -fun add_arities pp arg algebra = - algebra |> map_arities (insert_complete_ars pp algebra arg); +fun add_arities context arg algebra = + algebra |> map_arities (insert_complete_ars context algebra arg); -fun add_arities_table pp algebra = - Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars)); +fun add_arities_table context algebra = + Symtab.fold (fn (t, ars) => insert_complete_ars context algebra (t, ars)); end; (* classrel *) -fun rebuild_arities pp algebra = algebra |> map_arities (fn arities => +fun rebuild_arities context algebra = algebra |> map_arities (fn arities => Symtab.empty - |> add_arities_table pp algebra arities); + |> add_arities_table context algebra arities); -fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes => +fun add_classrel context rel = rebuild_arities context o map_classes (fn classes => classes |> Graph.add_edge_trans_acyclic rel - handle Graph.CYCLES css => err_cyclic_classes pp css); + handle Graph.CYCLES css => err_cyclic_classes context css); (* empty and merge *) val empty_algebra = make_algebra (Graph.empty, Symtab.empty); -fun merge_algebra pp +fun merge_algebra context (Algebra {classes = classes1, arities = arities1}, Algebra {classes = classes2, arities = arities2}) = let val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2) handle Graph.DUP c => err_dup_class c - | Graph.CYCLES css => err_cyclic_classes pp css; + | Graph.CYCLES css => err_cyclic_classes context css; val algebra0 = make_algebra (classes', Symtab.empty); val arities' = (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of @@ -288,20 +288,20 @@ | (true, false) => (*no completion*) (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) => if pointer_eq (ars1, ars2) then raise Symtab.SAME - else insert_ars pp algebra0 t ars2 ars1) + else insert_ars context algebra0 t ars2 ars1) | (false, true) => (*unary completion*) Symtab.empty - |> add_arities_table pp algebra0 arities1 + |> add_arities_table context algebra0 arities1 | (false, false) => (*binary completion*) Symtab.empty - |> add_arities_table pp algebra0 arities1 - |> add_arities_table pp algebra0 arities2); + |> add_arities_table context algebra0 arities1 + |> add_arities_table context algebra0 arities2); in make_algebra (classes', arities') end; (* algebra projections *) (* FIXME potentially violates abstract type integrity *) -fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) = +fun subalgebra context P sargs (algebra as Algebra {classes, arities}) = let val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes; fun restrict_arity t (c, Ss) = @@ -313,7 +313,7 @@ else NONE; val classes' = classes |> Graph.restrict P; val arities' = arities |> Symtab.map (map_filter o restrict_arity); - in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end; + in (restrict_sort, rebuild_arities context (make_algebra (classes', arities'))) end; @@ -326,8 +326,8 @@ No_Arity of string * class | No_Subsort of sort * sort; -fun class_error pp = - let val ctxt = Syntax.init_pretty pp in +fun class_error context = + let val ctxt = Syntax.init_pretty context in fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2] | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c]) | No_Subsort (S1, S2) => diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/term.ML --- a/src/Pure/term.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/term.ML Fri Sep 25 23:41:24 2015 +0200 @@ -107,6 +107,7 @@ val maxidx_of_typ: typ -> int val maxidx_of_typs: typ list -> int val maxidx_of_term: term -> int + val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val exists_subtype: (typ -> bool) -> typ -> bool val exists_type: (typ -> bool) -> term -> bool val exists_subterm: (term -> bool) -> term -> bool @@ -878,6 +879,12 @@ (* substructure *) +fun fold_subtypes f = + let + fun iter ty = + (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty); + in iter end; + fun exists_subtype P = let fun ex ty = P ty orelse diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/theory.ML --- a/src/Pure/theory.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/theory.ML Fri Sep 25 23:41:24 2015 +0200 @@ -23,9 +23,11 @@ val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory - val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory - val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory - val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory + val const_dep: theory -> string * typ -> Defs.entry + val type_dep: string * typ list -> Defs.entry + val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory + val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory + val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end @@ -62,7 +64,7 @@ fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; -structure Thy = Theory_Data_PP +structure Thy = Theory_Data' ( type T = thy; val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; @@ -71,14 +73,13 @@ fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) = make_thy (Position.none, 0, empty_axioms, defs, wrappers); - fun merge pp (thy1, thy2) = + fun merge old_thys (thy1, thy2) = let - val ctxt = Syntax.init_pretty pp; val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; val axioms' = empty_axioms; - val defs' = Defs.merge ctxt (defs1, defs2); + val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end; @@ -163,7 +164,7 @@ | _ => error "Bad bootstrapping of theory Pure") else let - val thy = Context.begin_thy Context.pretty_global name imports; + val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy @@ -211,35 +212,48 @@ (* dependencies *) -fun dependencies ctxt unchecked def description lhs rhs = +fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); +fun type_dep (c, args) = ((Defs.Type, c), args); + +fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let val thy = Proof_Context.theory_of ctxt; val consts = Sign.consts_of thy; - fun prep const = - let val Const (c, T) = Sign.no_vars ctxt (Const const) - in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end; - val lhs_vars = Term.add_tfreesT (#2 lhs) []; - val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => - if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs []; + fun prep (item, args) = + (case fold Term.add_tvarsT args [] of + [] => (item, map Logic.varifyT_global args) + | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); + + val lhs_vars = fold Term.add_tfreesT (snd lhs) []; + val rhs_extras = + fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v => + if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); - in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end; + in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; -fun add_deps ctxt a raw_lhs raw_rhs thy = +fun cert_entry thy ((Defs.Const, c), args) = + Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) + |> dest_Const |> const_dep thy + | cert_entry thy ((Defs.Type, c), args) = + Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; + +fun add_deps context a raw_lhs raw_rhs thy = let - val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs); - val description = if a = "" then #1 lhs ^ " axiom" else a; - in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end; + val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); + val description = if a = "" then lhs_name ^ " axiom" else a; + in thy |> map_defs (dependencies context false NONE description lhs rhs) end; -fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy; +fun add_deps_global a x y thy = + add_deps (Defs.global_context thy) a x y thy; fun specify_const decl thy = - let val (t as Const const, thy') = Sign.declare_const_global decl thy; - in (t, add_deps_global "" const [] thy') end; + let val (t, thy') = Sign.declare_const_global decl thy; + in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) @@ -271,25 +285,31 @@ local -fun check_def ctxt thy unchecked overloaded (b, tm) defs = +fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); - val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; + + val rhs_consts = + fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; + val rhs_types = + (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; + val rhs_deps = rhs_consts @ rhs_types; + val _ = check_overloading ctxt overloaded lhs_const; - in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end + in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in -fun add_def ctxt unchecked overloaded raw_axm thy = +fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy - |> map_defs (check_def ctxt thy unchecked overloaded axm) + |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Pure/type.ML --- a/src/Pure/type.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Pure/type.ML Fri Sep 25 23:41:24 2015 +0200 @@ -55,7 +55,7 @@ val cert_typ_mode: mode -> tsig -> typ -> typ val cert_typ: tsig -> typ -> typ val arity_number: tsig -> string -> int - val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list + val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list (*special treatment of type vars*) val sort_of_atyp: typ -> sort @@ -96,9 +96,9 @@ val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig val add_nonterminal: Context.generic -> binding -> tsig -> tsig val hide_type: bool -> string -> tsig -> tsig - val add_arity: Context.pretty -> arity -> tsig -> tsig - val add_classrel: Context.pretty -> class * class -> tsig -> tsig - val merge_tsig: Context.pretty -> tsig * tsig -> tsig + val add_arity: Context.generic -> arity -> tsig -> tsig + val add_classrel: Context.generic -> class * class -> tsig -> tsig + val merge_tsig: Context.generic -> tsig * tsig -> tsig end; structure Type: TYPE = @@ -321,9 +321,9 @@ | _ => error (undecl_type a)); fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) [] - | arity_sorts pp (TSig {classes, ...}) a S = + | arity_sorts context (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S - handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err); + handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err); @@ -609,7 +609,7 @@ handle TYPE (msg, _, _) => error msg; val _ = Binding.check c; val (c', space') = space |> Name_Space.declare context true c; - val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs'); + val classes' = classes |> Sorts.add_class context (c', cs'); in ((space', classes'), default, types) end); fun hide_class fully c = map_tsig (fn ((space, classes), default, types) => @@ -618,7 +618,7 @@ (* arities *) -fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => +fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let val _ = (case lookup_type tsig t of @@ -627,18 +627,18 @@ | NONE => error (undecl_type t)); val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) handle TYPE (msg, _, _) => error msg; - val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S')); + val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S')); in ((space, classes'), default, types) end); (* classrel *) -fun add_classrel pp rel tsig = +fun add_classrel context rel tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let val rel' = apply2 (cert_class tsig) rel handle TYPE (msg, _, _) => error msg; - val classes' = classes |> Sorts.add_classrel pp rel'; + val classes' = classes |> Sorts.add_classrel context rel'; in ((space, classes'), default, types) end); @@ -701,7 +701,7 @@ (* merge type signatures *) -fun merge_tsig pp (tsig1, tsig2) = +fun merge_tsig context (tsig1, tsig2) = let val (TSig {classes = (space1, classes1), default = default1, types = types1, log_types = _}) = tsig1; @@ -709,7 +709,7 @@ log_types = _}) = tsig2; val space' = Name_Space.merge (space1, space2); - val classes' = Sorts.merge_algebra pp (classes1, classes2); + val classes' = Sorts.merge_algebra context (classes1, classes2); val default' = Sorts.inter_sort classes' (default1, default2); val types' = Name_Space.merge_tables (types1, types2); in build_tsig ((space', classes'), default', types') end; diff -r b77bf45efe21 -r 28eb608b9b59 src/Sequents/prover.ML --- a/src/Sequents/prover.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Sequents/prover.ML Fri Sep 25 23:41:24 2015 +0200 @@ -63,8 +63,8 @@ fun pretty_pack ctxt = let val (safes, unsafes) = get_rules ctxt in Pretty.chunks - [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes), - Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)] + [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes), + Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)] end; val _ = @@ -82,7 +82,7 @@ (case context of Context.Proof ctxt => if Context_Position.is_really_visible ctxt then - warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th) + warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th) else () | _ => ()); in ths end diff -r b77bf45efe21 -r 28eb608b9b59 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Sequents/simpdata.ML Fri Sep 25 23:41:24 2015 +0200 @@ -38,7 +38,7 @@ | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection} | (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F} | _ => th RS @{thm iff_reflection_T}) - | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th)); + | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); (*Replace premises x=y, X<->Y by X==Y*) fun mk_meta_prems ctxt = diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri Sep 25 23:41:24 2015 +0200 @@ -517,7 +517,7 @@ |> fold (ensure_fun ctxt arities eqngr) cs |> fold (ensure_rhs ctxt arities eqngr) cs_rhss; val arities' = fold (add_arity ctxt vardeps) insts arities; - val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy) + val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy) (AList.lookup (op =) arities') (Sign.classes_of thy); val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr); fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra) diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/Code/code_printer.ML Fri Sep 25 23:41:24 2015 +0200 @@ -111,7 +111,7 @@ (** generic nonsense *) fun eqn_error thy (SOME thm) s = - error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm) + error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm) | eqn_error _ NONE s = error s; val code_presentationN = "code_presentation"; diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Sep 25 23:41:24 2015 +0200 @@ -396,7 +396,7 @@ else let val thm_msg = - Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm; + Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm; val dep_msg = if null (tl deps) then NONE else SOME ("with dependency " ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); @@ -412,7 +412,7 @@ fun not_wellsorted ctxt permissive some_thm deps ty sort e = let - val err_class = Sorts.class_error (Context.pretty ctxt) e; + val err_class = Sorts.class_error (Context.Proof ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ Syntax.string_of_sort ctxt sort; diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/coherent.ML Fri Sep 25 23:41:24 2015 +0200 @@ -175,7 +175,7 @@ let val _ = cond_trace ctxt (fn () => - Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms))); + Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms))); val th' = Drule.implies_elim_list (Thm.instantiate diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/induct.ML Fri Sep 25 23:41:24 2015 +0200 @@ -207,7 +207,7 @@ fun pretty_rules ctxt kind rs = let val thms = map snd (Item_Net.content rs) - in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end; + in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end; (* context data *) diff -r b77bf45efe21 -r 28eb608b9b59 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/Tools/nbe.ML Fri Sep 25 23:41:24 2015 +0200 @@ -50,17 +50,17 @@ let val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) of SOME ofclass_eq => ofclass_eq - | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm); + | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val (T, class) = case try Logic.dest_of_class ofclass of SOME T_class => T_class - | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm); + | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val tvar = case try Term.dest_TVar T of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort) then tvar - else error ("Bad sort: " ^ Display.string_of_thm_global thy thm) - | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm); + else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm) + | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm); val _ = if Term.add_tvars eqn [] = [tvar] then () - else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm); + else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm); val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); @@ -69,7 +69,7 @@ | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then () - else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm); + else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm); in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end; local diff -r b77bf45efe21 -r 28eb608b9b59 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Sep 25 23:41:24 2015 +0200 @@ -319,7 +319,7 @@ if ! Ind_Syntax.trace then writeln (cat_lines (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @ - ["raw_induct:", Display.string_of_thm ctxt1 raw_induct])) + ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct])) else (); @@ -352,7 +352,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct) + writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct) else (); @@ -429,7 +429,7 @@ val dummy = if ! Ind_Syntax.trace then - writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma) + writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma) else (); diff -r b77bf45efe21 -r 28eb608b9b59 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Fri Sep 25 16:54:31 2015 +0200 +++ b/src/ZF/Tools/typechk.ML Fri Sep 25 23:41:24 2015 +0200 @@ -26,7 +26,7 @@ fun add_rule ctxt th (tcs as TC {rules, net}) = if member Thm.eq_thm_prop rules th then - (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs) + (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs) else TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net}; @@ -34,7 +34,7 @@ if member Thm.eq_thm_prop rules th then TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net, rules = remove Thm.eq_thm_prop th rules} - else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs); + else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs); (* generic data *) @@ -61,7 +61,7 @@ fun print_tcset ctxt = let val TC {rules, ...} = tcset_of ctxt in Pretty.writeln (Pretty.big_list "type-checking rules:" - (map (Display.pretty_thm_item ctxt) rules)) + (map (Thm.pretty_thm_item ctxt) rules)) end;