--- a/NEWS Tue Aug 14 11:37:58 2012 +0200
+++ b/NEWS Tue Aug 14 11:43:08 2012 +0200
@@ -29,6 +29,12 @@
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.
+* Command 'typ' supports an additional variant with explicit sort
+constraint, to infer and check the most general type conforming to a
+given given sort. Example (in HOL):
+
+ typ "_ * _ * bool * unit" :: finite
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Aug 14 11:37:58 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Aug 14 11:43:08 2012 +0200
@@ -47,7 +47,7 @@
internal logical entities in a human-readable fashion.
@{rail "
- @@{command typ} @{syntax modes}? @{syntax type}
+ @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
;
@@{command term} @{syntax modes}? @{syntax term}
;
@@ -65,8 +65,15 @@
\begin{description}
- \item @{command "typ"}~@{text \<tau>} reads and prints types of the
- meta-logic according to the current theory or proof context.
+ \item @{command "typ"}~@{text \<tau>} reads and prints a type expression
+ according to the current context.
+
+ \item @{command "typ"}~@{text "\<tau> :: s"} uses type-inference to
+ determine the most general way to make @{text "\<tau>"} conform to sort
+ @{text "s"}. For concrete @{text "\<tau>"} this checks if the type
+ belongs to that sort. Dummy type parameters ``@{text "_"}''
+ (underscore) are assigned to fresh type variables with most general
+ sorts, according the the principles of type-inference.
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
read, type-check and print terms or propositions according to the
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Aug 14 11:37:58 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Aug 14 11:43:08 2012 +0200
@@ -75,6 +75,11 @@
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
+\rail@endbar
\rail@end
\rail@begin{2}{}
\rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
@@ -139,8 +144,15 @@
\begin{description}
- \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints types of the
- meta-logic according to the current theory or proof context.
+ \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints a type expression
+ according to the current context.
+
+ \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s{\isaliteral{22}{\isachardoublequote}}} uses type-inference to
+ determine the most general way to make \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} conform to sort
+ \isa{{\isaliteral{22}{\isachardoublequote}}s{\isaliteral{22}{\isachardoublequote}}}. For concrete \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} this checks if the type
+ belongs to that sort. Dummy type parameters ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}''
+ (underscore) are assigned to fresh type variables with most general
+ sorts, according the the principles of type-inference.
\item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}
read, type-check and print terms or propositions according to the
--- a/src/Pure/Isar/isar_cmd.ML Tue Aug 14 11:37:58 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Aug 14 11:43:08 2012 +0200
@@ -75,7 +75,8 @@
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
- val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
+ val print_type: (string list * (string * string option)) ->
+ Toplevel.transition -> Toplevel.transition
val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
Toplevel.transition -> Toplevel.transition
@@ -494,9 +495,19 @@
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
end;
-fun string_of_type ctxt s =
- let val T = Syntax.read_typ ctxt s
- in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
+fun string_of_type ctxt (s, NONE) =
+ let val T = Syntax.read_typ ctxt s
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
+ | string_of_type ctxt (s1, SOME s2) =
+ let
+ val ctxt' = Config.put show_sorts true ctxt;
+ val raw_T = Syntax.parse_typ ctxt' s1;
+ val S = Syntax.read_sort ctxt' s2;
+ val T =
+ Syntax.check_term ctxt'
+ (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
+ |> Logic.dest_type;
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
--- a/src/Pure/Isar/isar_syn.ML Tue Aug 14 11:37:58 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Aug 14 11:43:08 2012 +0200
@@ -902,7 +902,8 @@
val _ =
Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
- (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
+ (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
+ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
val _ =
Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"