# HG changeset patch # User wenzelm # Date 1002047013 -7200 # Node ID 201b3f76c7b72c2c37e9c2c24ec684186e717a71 # Parent e4314c06a2a31c5e31d7d69c5a35aff70853ef1d support non-oriented infix; diff -r e4314c06a2a3 -r 201b3f76c7b7 doc-src/IsarRef/syntax.tex --- 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 ')' ; diff -r e4314c06a2a3 -r 201b3f76c7b7 src/HOLCF/cont_consts.ML --- 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)) diff -r e4314c06a2a3 -r 201b3f76c7b7 src/Pure/Isar/isar_syn.ML --- 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", "|", "\\", "\\", "\\", "\\", "\\"]; diff -r e4314c06a2a3 -r 201b3f76c7b7 src/Pure/Isar/outer_parse.ML --- 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 *) diff -r e4314c06a2a3 -r 201b3f76c7b7 src/Pure/Syntax/mixfix.ML --- 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)) =>