--- 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 ***
--- 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}
--- 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}
--- 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 +)
;
--- 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.
--- 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}
--- 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 +)
;
--- 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 =
--- 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;
--- 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 "/"
--- 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
--- 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 =
--- 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));
--- 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)) =
--- 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)) =
--- 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))));
--- 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);
--- 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;
--- 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,