--- a/NEWS Sat Feb 24 17:21:35 2018 +0100
+++ b/NEWS Sun Feb 25 12:59:08 2018 +0100
@@ -176,6 +176,12 @@
(e.g. use 'find_theorems' or 'try' to figure this out).
+*** Pure ***
+
+* The inner syntax category "sort" now includes notation "_" for the
+dummy sort: it is effectively ignored in type-inference.
+
+
*** HOL ***
* Clarifed theorem names:
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Feb 25 12:59:08 2018 +0100
@@ -724,7 +724,7 @@
& \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
@{syntax_def (inner) type_name} & = & \<open>id | longid\<close> \\\\
- @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
+ @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
& \<open>|\<close> & \<^verbatim>\<open>{\<close> @{syntax class_name} \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> @{syntax class_name} \<^verbatim>\<open>}\<close> \\
@{syntax_def (inner) class_name} & = & \<open>id | longid\<close> \\
\end{supertabular}
@@ -803,6 +803,9 @@
\<^item> Dummy variables (written as underscore) may occur in different
roles.
+ \<^descr> A sort ``\<open>_\<close>'' refers to a vacuous constraint for type variables, which
+ is effectively ignored in type-inference.
+
\<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
parameter, which is filled-in according to the most general type produced
by the type-checking phase.
--- a/src/Pure/Syntax/syntax_phases.ML Sat Feb 24 17:21:35 2018 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Feb 25 12:59:08 2018 +0100
@@ -106,7 +106,8 @@
| classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
| classes _ = err ();
- fun sort (Const ("_topsort", _)) = []
+ fun sort (Const ("_dummy_sort", _)) = dummyS
+ | sort (Const ("_topsort", _)) = []
| sort (Const ("_sort", _) $ cs) = classes cs
| sort (Const (s, _)) = [class s]
| sort _ = err ();
@@ -506,10 +507,12 @@
fun classes [c] = class c
| classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
in
- (case S of
- [] => Syntax.const "_topsort"
- | [c] => class c
- | cs => Syntax.const "_sort" $ classes cs)
+ if S = dummyS then Syntax.const "_dummy_sort"
+ else
+ (case S of
+ [] => Syntax.const "_topsort"
+ | [c] => class c
+ | cs => Syntax.const "_sort" $ classes cs)
end;
--- a/src/Pure/pure_thy.ML Sat Feb 24 17:21:35 2018 +0100
+++ b/src/Pure/pure_thy.ML Sun Feb 25 12:59:08 2018 +0100
@@ -105,6 +105,7 @@
("", typ "class_name => sort", Mixfix.mixfix "_"),
("_class_name", typ "id => class_name", Mixfix.mixfix "_"),
("_class_name", typ "longid => class_name", Mixfix.mixfix "_"),
+ ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"),
("_topsort", typ "sort", Mixfix.mixfix "{}"),
("_sort", typ "classes => sort", Mixfix.mixfix "{_}"),
("", typ "class_name => classes", Mixfix.mixfix "_"),