# HG changeset patch
# User wenzelm
# Date 1267040221 -3600
# Node ID 7425aece4ee33ea5d6dd95b673c7e4942541f125
# Parent  0df9c8a37f64e0aa8c56cecf5197e9ebebefecb1
allow general mixfix syntax for type constructors;

diff -r 0df9c8a37f64 -r 7425aece4ee3 NEWS
--- a/NEWS	Wed Feb 24 07:06:39 2010 -0800
+++ b/NEWS	Wed Feb 24 20:37:01 2010 +0100
@@ -38,6 +38,8 @@
 and ML_command "set Syntax.trace_ast" help to diagnose syntax
 problems.
 
+* Type constructors admit general mixfix syntax, not just infix.
+
 
 *** Pure ***
 
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 24 20:37:01 2010 +0100
@@ -13,14 +13,14 @@
   \end{matharray}
 
   \begin{rail}
-    'typedecl' typespec infix?
+    'typedecl' typespec mixfix?
     ;
     'typedef' altname? abstype '=' repset
     ;
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec infix?
+    abstype: typespec mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
@@ -367,7 +367,7 @@
     'rep\_datatype' ('(' (name +) ')')? (term +)
     ;
 
-    dtspec: parname? typespec infix? '=' (cons + '|')
+    dtspec: parname? typespec mixfix? '=' (cons + '|')
     ;
     cons: name ( type * ) mixfix?
   \end{rail}
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 24 20:37:01 2010 +0100
@@ -244,11 +244,9 @@
 section {* Mixfix annotations *}
 
 text {* Mixfix annotations specify concrete \emph{inner syntax} of
-  Isabelle types and terms.  Some commands such as @{command
-  "typedecl"} admit infixes only, while @{command "definition"} etc.\
-  support the full range of general mixfixes and binders.  Fixed
-  parameters in toplevel theorem statements, locale specifications
-  also admit mixfix annotations.
+  Isabelle types and terms.  Locally fixed parameters in toplevel
+  theorem statements, locale specifications etc.\ also admit mixfix
+  annotations.
 
   \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
   \begin{rail}
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Feb 24 20:37:01 2010 +0100
@@ -959,9 +959,9 @@
   \end{matharray}
 
   \begin{rail}
-    'types' (typespec '=' type infix? +)
+    'types' (typespec '=' type mixfix? +)
     ;
-    'typedecl' typespec infix?
+    'typedecl' typespec mixfix?
     ;
     'arities' (nameref '::' arity +)
     ;
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 20:37:01 2010 +0100
@@ -33,14 +33,14 @@
   \end{matharray}
 
   \begin{rail}
-    'typedecl' typespec infix?
+    'typedecl' typespec mixfix?
     ;
     'typedef' altname? abstype '=' repset
     ;
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec infix?
+    abstype: typespec mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
@@ -372,7 +372,7 @@
     'rep\_datatype' ('(' (name +) ')')? (term +)
     ;
 
-    dtspec: parname? typespec infix? '=' (cons + '|')
+    dtspec: parname? typespec mixfix? '=' (cons + '|')
     ;
     cons: name ( type * ) mixfix?
   \end{rail}
@@ -906,6 +906,9 @@
       \item[iterations] sets how many sets of assignments are
         generated for each particular size.
 
+      \item[no\_assms] specifies whether assumptions in
+        structured proofs should be ignored.
+
     \end{description}
 
     These option can be given within square brackets.
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 20:37:01 2010 +0100
@@ -266,10 +266,9 @@
 %
 \begin{isamarkuptext}%
 Mixfix annotations specify concrete \emph{inner syntax} of
-  Isabelle types and terms.  Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\
-  support the full range of general mixfixes and binders.  Fixed
-  parameters in toplevel theorem statements, locale specifications
-  also admit mixfix annotations.
+  Isabelle types and terms.  Locally fixed parameters in toplevel
+  theorem statements, locale specifications etc.\ also admit mixfix
+  annotations.
 
   \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
   \begin{rail}
diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Feb 24 20:37:01 2010 +0100
@@ -996,9 +996,9 @@
   \end{matharray}
 
   \begin{rail}
-    'types' (typespec '=' type infix? +)
+    'types' (typespec '=' type mixfix? +)
     ;
-    'typedecl' typespec infix?
+    'typedecl' typespec mixfix?
     ;
     'arities' (nameref '::' arity +)
     ;
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -2079,7 +2079,7 @@
 local structure P = OuterParse and K = OuterKeyword in
 
 val datatype_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
     (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
 
 fun mk_datatype args =
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -731,7 +731,7 @@
   in (names, specs) end;
 
 val parse_datatype_decl =
-  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
     (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
 
 val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -296,7 +296,7 @@
 val quotspec_parser =
     OuterParse.and_list1
      ((OuterParse.type_args -- OuterParse.binding) --
-        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
+        OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
          (OuterParse.$$$ "/" |-- OuterParse.term))
 
 val _ = OuterKeyword.keyword "/"
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Tools/typedef.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -255,7 +255,7 @@
     (Scan.optional (P.$$$ "(" |--
         ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
           P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
-      (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+      (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
       Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
     >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
         Toplevel.print o Toplevel.theory_to_proof
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -291,7 +291,7 @@
   || Scan.succeed [];
 
 val domain_decl =
-  (type_args' -- P.binding -- P.opt_infix) --
+  (type_args' -- P.binding -- P.opt_mixfix) --
     (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 
 val domains_decl =
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -700,7 +700,7 @@
 val parse_domain_iso :
     (string list * binding * mixfix * string * (binding * binding) option)
       parser =
-  (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) --
+  (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
     >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
 
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -340,7 +340,7 @@
   Scan.optional (P.$$$ "(" |--
       ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
         --| P.$$$ ")") (true, NONE) --
-    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
 
 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -167,7 +167,7 @@
   Scan.optional (P.$$$ "(" |--
       ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
         --| P.$$$ ")") (true, NONE) --
-    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
 
 fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -104,13 +104,13 @@
 
 val _ =
   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
-    (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
+    (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
       Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
-      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
+      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
       >> (Toplevel.theory o Sign.add_tyabbrs o
         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
 
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/Pure/Isar/outer_parse.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -72,8 +72,6 @@
   val typ: string parser
   val mixfix: mixfix parser
   val mixfix': mixfix parser
-  val opt_infix: mixfix parser
-  val opt_infix': mixfix parser
   val opt_mixfix: mixfix parser
   val opt_mixfix': mixfix parser
   val where_: string parser
@@ -279,8 +277,6 @@
 
 val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
 val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
-val opt_infix = opt_annotation !!! (infxl || infxr || infx);
-val opt_infix' = opt_annotation I (infxl || infxr || infx);
 val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
 val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
 
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/Pure/Syntax/mixfix.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -101,20 +101,26 @@
 
 fun syn_ext_types type_decls =
   let
-    fun mk_infix sy t p1 p2 p3 =
-      SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
-        [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
+    fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+    fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
 
     fun mfix_of (_, _, NoSyn) = NONE
-      | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
-      | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
-      | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
-      | mfix_of (t, _, _) =
-          error ("Bad mixfix declaration for type: " ^ quote t);  (* FIXME printable!? *)
+      | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
+      | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
+      | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
+      | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
+      | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
+      | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
 
-    val mfix = map_filter mfix_of type_decls;
+    fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
+          if SynExt.mfix_args sy = n then ()
+          else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
+      | check_args _ NONE = ();
+
+    val mfix = map mfix_of type_decls;
+    val _ = map2 check_args type_decls mfix;
     val xconsts = map #1 type_decls;
-  in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
+  in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
 
 
 (* syn_ext_consts *)
@@ -140,7 +146,7 @@
       | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
       | mfix_of (c, ty, Binder (sy, p, q)) =
           [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
-      | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c);
+      | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);   (* FIXME printable c (!?) *)
 
     fun binder (c, _, Binder _) = SOME (binder_name c, c)
       | binder _ = NONE;
diff -r 0df9c8a37f64 -r 7425aece4ee3 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 07:06:39 2010 -0800
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 20:37:01 2010 +0100
@@ -28,6 +28,8 @@
   val cargs: string
   val any: string
   val sprop: string
+  datatype mfix = Mfix of string * typ * string * int list * int
+  val err_in_mfix: string -> mfix -> 'a
   val typ_to_nonterm: typ -> string
   datatype xsymb =
     Delim of string |
@@ -37,7 +39,6 @@
   datatype xprod = XProd of string * xsymb list * string * int
   val chain_pri: int
   val delims_of: xprod list -> string list list
-  datatype mfix = Mfix of string * typ * string * int list * int
   datatype syn_ext =
     SynExt of {
       xprods: xprod list,