Re: [isabelle] Vector type syntax



On 05/02/18 12:57, Lawrence Paulson wrote:
>> On 1 Feb 2018, at 12:57, Dominique Unruh <unruh at ut.ee> wrote:
>>
>> The constraints imposed by ^ are relatively half-hearted in any case. The following types are accepted:
>>
>> typ "real^real"
>> type_synonym 'a id = "'a"
>> typ "real^('n::{finite,wellorder} id)"
>> typ "real^('n::{wellorder} id)"
>>
>> The reason is that the parse translation adds the ::{finite} constraint only if the second argument to ^ is a type variable.
>>
>> It feels to me that no enforcement might be better than such half-hearted enforcement.

I usually also prefer a clear situation, without too much builtin magic
(here the silent addition of a sort constraint due to concrete syntax).
But this appears to be infeasible now ...


> The following is not allowed: as the second occurrence of ’n is assigned a different sort from the first. This is not how sort assignment normally works, so I think we should see if there is some way to obtain more natural behaviour without forcing hundreds of theorem statements to be altered.

Systematic counting with the included ch-vec_syntax in
Isabelle/5348bea4accd + AFP/e9f2114df805 (excluding very_slow sessions)
yields the following results:

3273 T ^ 'a (type variable)
2920 T ^ U (other type)
6193 total


>   fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n"

Maybe the following ch-dummy_sort is already sufficient (cf.
Isabelle/17874d43d3b3). With that you can write:

  fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"

The dummmy sort looks syntactically like a sort constraint, and the vec
syntax translation will not add anything. Later the sort disappears, and
type inference proceeds as usual.


	Makarius
# HG changeset patch
# User wenzelm
# Date 1519570933 -3600
#      Sun Feb 25 16:02:13 2018 +0100
# Node ID c114051a18cc1c97978e101b308e4c180c6d1ec2
# Parent  5348bea4accdc357f1248e62ea4331c0392f7e60
test

diff -r 5348bea4accd -r c114051a18cc src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 25 15:44:46 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 25 16:02:13 2018 +0100
@@ -44,16 +44,24 @@
 parse_translation \<open>
   let
     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
-    fun finite_vec_tr [t, u] =
-      (case Term_Position.strip_positions u of
-        v as Free (x, _) =>
-          if Lexicon.is_tid x then
-            vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
-              Syntax.const @{class_syntax finite})
-          else vec t u
-      | _ => vec t u)
+    fun finite_vec_tr ctxt [t, u] =
+      let
+        fun warn s =
+          if Context_Position.is_visible ctxt
+          then warning ("FIXME " ^ s ^ Position.here (Position.thread_data ()))
+          else ();
+      in
+        (case Term_Position.strip_positions u of
+          v as Free (x, _) =>
+            if Lexicon.is_tid x then
+              (warn "vec1";
+              vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
+                Syntax.const @{class_syntax finite}))
+            else (warn "vec2"; vec t u)
+        | _ => (warn "vec3"; vec t u))
+      end;
   in
-    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+    [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
   end
 \<close>
 
# HG changeset patch
# User wenzelm
# Date 1519559948 -3600
#      Sun Feb 25 12:59:08 2018 +0100
# Node ID 17874d43d3b3d0b4fbbd14fca0818ab88031373f
# Parent  5a1b299fe4af77c7ceabf068df0eff2ddcfa94e4
notation for dummy sort;

diff -r 5a1b299fe4af -r 17874d43d3b3 NEWS
--- 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:
diff -r 5a1b299fe4af -r 17874d43d3b3 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.
diff -r 5a1b299fe4af -r 17874d43d3b3 src/Pure/Syntax/syntax_phases.ML
--- 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;
 
 
diff -r 5a1b299fe4af -r 17874d43d3b3 src/Pure/pure_thy.ML
--- 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 "_"),


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.