notation for dummy sort;
authorwenzelm
Sun Feb 25 12:59:08 2018 +0100 (23 months ago ago)
changeset 6771917874d43d3b3
parent 67717 5a1b299fe4af
child 67720 b342f96e47b5
child 67721 5348bea4accd
notation for dummy sort;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/Syntax/syntax_phases.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Sat Feb 24 17:21:35 2018 +0100
     1.2 +++ b/NEWS	Sun Feb 25 12:59:08 2018 +0100
     1.3 @@ -176,6 +176,12 @@
     1.4  (e.g. use 'find_theorems' or 'try' to figure this out).
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* The inner syntax category "sort" now includes notation "_" for the
    1.10 +dummy sort: it is effectively ignored in type-inference.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Clarifed theorem names:
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Feb 24 17:21:35 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Feb 25 12:59:08 2018 +0100
     2.3 @@ -724,7 +724,7 @@
     2.4      & \<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> \\
     2.5    @{syntax_def (inner) type_name} & = & \<open>id  |  longid\<close> \\\\
     2.6  
     2.7 -  @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
     2.8 +  @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
     2.9      & \<open>|\<close> & \<^verbatim>\<open>{\<close> @{syntax class_name} \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> @{syntax class_name} \<^verbatim>\<open>}\<close> \\
    2.10    @{syntax_def (inner) class_name} & = & \<open>id  |  longid\<close> \\
    2.11    \end{supertabular}
    2.12 @@ -803,6 +803,9 @@
    2.13    \<^item> Dummy variables (written as underscore) may occur in different
    2.14    roles.
    2.15  
    2.16 +    \<^descr> A sort ``\<open>_\<close>'' refers to a vacuous constraint for type variables, which
    2.17 +    is effectively ignored in type-inference.
    2.18 +
    2.19      \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
    2.20      parameter, which is filled-in according to the most general type produced
    2.21      by the type-checking phase.
     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Feb 24 17:21:35 2018 +0100
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Feb 25 12:59:08 2018 +0100
     3.3 @@ -106,7 +106,8 @@
     3.4        | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
     3.5        | classes _ = err ();
     3.6  
     3.7 -    fun sort (Const ("_topsort", _)) = []
     3.8 +    fun sort (Const ("_dummy_sort", _)) = dummyS
     3.9 +      | sort (Const ("_topsort", _)) = []
    3.10        | sort (Const ("_sort", _) $ cs) = classes cs
    3.11        | sort (Const (s, _)) = [class s]
    3.12        | sort _ = err ();
    3.13 @@ -506,10 +507,12 @@
    3.14      fun classes [c] = class c
    3.15        | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
    3.16    in
    3.17 -    (case S of
    3.18 -      [] => Syntax.const "_topsort"
    3.19 -    | [c] => class c
    3.20 -    | cs => Syntax.const "_sort" $ classes cs)
    3.21 +    if S = dummyS then Syntax.const "_dummy_sort"
    3.22 +    else
    3.23 +      (case S of
    3.24 +        [] => Syntax.const "_topsort"
    3.25 +      | [c] => class c
    3.26 +      | cs => Syntax.const "_sort" $ classes cs)
    3.27    end;
    3.28  
    3.29  
     4.1 --- a/src/Pure/pure_thy.ML	Sat Feb 24 17:21:35 2018 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Sun Feb 25 12:59:08 2018 +0100
     4.3 @@ -105,6 +105,7 @@
     4.4      ("",            typ "class_name => sort",          Mixfix.mixfix "_"),
     4.5      ("_class_name", typ "id => class_name",            Mixfix.mixfix "_"),
     4.6      ("_class_name", typ "longid => class_name",        Mixfix.mixfix "_"),
     4.7 +    ("_dummy_sort", typ "sort",                        Mixfix.mixfix "'_"),
     4.8      ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
     4.9      ("_sort",       typ "classes => sort",             Mixfix.mixfix "{_}"),
    4.10      ("",            typ "class_name => classes",       Mixfix.mixfix "_"),