--- a/doc-src/IsarRef/syntax.tex Mon Oct 01 21:53:50 2001 +0200
+++ b/doc-src/IsarRef/syntax.tex Tue Oct 02 20:23:33 2001 +0200
@@ -248,7 +248,7 @@
\indexouternonterm{infix}\indexouternonterm{mixfix}
\begin{rail}
- infix: '(' ('infixl' | 'infixr') string? nat ')'
+ infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
;
mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
;
--- a/src/HOLCF/cont_consts.ML Mon Oct 01 21:53:50 2001 +0200
+++ b/src/HOLCF/cont_consts.ML Tue Oct 02 20:23:33 2001 +0200
@@ -38,7 +38,8 @@
foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun")
[t,Variable arg]))
(Constant name1,vnames))]
- @(case mx of InfixlName _ => [extra_parse_rule]
+ @(case mx of InfixName _ => [extra_parse_rule]
+ | InfixlName _ => [extra_parse_rule]
| InfixrName _ => [extra_parse_rule] | _ => []) end;
@@ -48,7 +49,9 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun fix_mixfix (syn , T, mx as Infixl p ) =
+fun fix_mixfix (syn , T, mx as Infix p ) =
+ (Syntax.const_name syn mx, T, InfixName (syn, p))
+ | fix_mixfix (syn , T, mx as Infixl p ) =
(Syntax.const_name syn mx, T, InfixlName (syn, p))
| fix_mixfix (syn , T, mx as Infixr p ) =
(Syntax.const_name syn mx, T, InfixrName (syn, p))
--- a/src/Pure/Isar/isar_syn.ML Mon Oct 01 21:53:50 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Oct 02 20:23:33 2001 +0200
@@ -676,7 +676,7 @@
val keywords =
["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
"<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
- "files", "in", "infixl", "infixr", "is", "output", "overloaded",
+ "files", "in", "infix", "infixl", "infixr", "is", "output", "overloaded",
"|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
"\\<rightleftharpoons>", "\\<subseteq>"];
--- a/src/Pure/Isar/outer_parse.ML Mon Oct 01 21:53:50 2001 +0200
+++ b/src/Pure/Isar/outer_parse.ML Tue Oct 02 20:23:33 2001 +0200
@@ -202,6 +202,7 @@
(* mixfix annotations *)
+val infx = $$$ "infix" |-- !!! (nat >> Syntax.Infix || string -- nat >> Syntax.InfixName);
val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName);
val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName);
@@ -220,11 +221,11 @@
fun opt_fix guard fix =
Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
-val opt_infix = opt_fix !!! (infxl || infxr);
-val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr);
+val opt_infix = opt_fix !!! (infxl || infxr || infx);
+val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
-val opt_infix' = opt_fix I (infxl || infxr);
-val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr);
+val opt_infix' = opt_fix I (infxl || infxr || infx);
+val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
(* consts *)
--- a/src/Pure/Syntax/mixfix.ML Mon Oct 01 21:53:50 2001 +0200
+++ b/src/Pure/Syntax/mixfix.ML Tue Oct 02 20:23:33 2001 +0200
@@ -11,8 +11,10 @@
NoSyn |
Mixfix of string * int list * int |
Delimfix of string |
+ InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
+ Infix of int |
Infixl of int |
Infixr of int |
Binder of string * int * int
@@ -54,8 +56,10 @@
NoSyn |
Mixfix of string * int list * int |
Delimfix of string |
+ InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
+ Infix of int |
Infixl of int |
Infixr of int |
Binder of string * int * int;
@@ -72,19 +76,24 @@
val strip_esc = implode o strip o Symbol.explode;
-fun type_name t (InfixlName _) = t
+fun type_name t (InfixName _) = t
+ | type_name t (InfixlName _) = t
| type_name t (InfixrName _) = t
+ | type_name t (Infix _) = strip_esc t
| type_name t (Infixl _) = strip_esc t
| type_name t (Infixr _) = strip_esc t
| type_name t _ = t;
-fun const_name c (InfixlName _) = c
+fun const_name c (InfixName _) = c
+ | const_name c (InfixlName _) = c
| const_name c (InfixrName _) = c
+ | const_name c (Infix _) = "op " ^ strip_esc c
| const_name c (Infixl _) = "op " ^ strip_esc c
| const_name c (Infixr _) = "op " ^ strip_esc c
| const_name c _ = c;
-fun fix_mixfix c (Infixl p) = (InfixlName (c, p))
+fun fix_mixfix c (Infix p) = (InfixName (c, p))
+ | fix_mixfix c (Infixl p) = (InfixlName (c, p))
| fix_mixfix c (Infixr p) = (InfixrName (c, p))
| fix_mixfix _ mx = mx;
@@ -111,8 +120,10 @@
let val t = name_of decl in
(case decl of
(_, _, NoSyn) => None
+ | (_, 2, InfixName (sy, p)) => Some (mk_infix sy t (p + 1) (p + 1) p)
| (_, 2, InfixlName (sy, p)) => Some (mk_infix sy t p (p + 1) p)
| (_, 2, InfixrName (sy, p)) => Some (mk_infix sy t (p + 1) p p)
+ | (sy, 2, Infix p) => Some (mk_infix sy t (p + 1) (p + 1) p)
| (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
| (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
| _ => error ("Bad mixfix declaration for type " ^ quote t))
@@ -143,8 +154,10 @@
(_, _, NoSyn) => []
| (_, ty, Mixfix (sy, ps, p)) => [SynExt.Mfix (sy, ty, c, ps, p)]
| (_, ty, Delimfix sy) => [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
+ | (_, ty, InfixName (sy, p)) => mk_infix sy ty c (p + 1) (p + 1) p
| (_, ty, InfixlName (sy, p)) => mk_infix sy ty c p (p + 1) p
| (_, ty, InfixrName (sy, p)) => mk_infix sy ty c (p + 1) p p
+ | (sy, ty, Infix p) => mk_infix sy ty c (p + 1) (p + 1) p
| (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p
| (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p
| (_, ty, Binder (sy, p, q)) =>