--- a/NEWS Mon Feb 15 15:50:41 2010 +0100
+++ b/NEWS Mon Feb 15 17:17:51 2010 +0100
@@ -9,6 +9,9 @@
* Code generator: details of internal data cache have no impact on
the user space functionality any longer.
+* Discontinued unnamed infix syntax (legacy feature for many years) --
+need to specify constant name and syntax separately.
+
*** HOL ***
--- a/src/HOL/Import/xmlconv.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOL/Import/xmlconv.ML Mon Feb 15 17:17:51 2010 +0100
@@ -221,9 +221,6 @@
| xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
| xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
| xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
- | xml_of_mixfix (Infix i) = wrap "infix" xml_of_int i
- | xml_of_mixfix (Infixl i) = wrap "infixl" xml_of_int i
- | xml_of_mixfix (Infixr i) = wrap "infixr" xml_of_int i
| xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
fun mixfix_of_xml e =
@@ -235,9 +232,6 @@
| "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml)
| "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)
| "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
- | "infix" => unwrap Infix int_of_xml
- | "infixl" => unwrap Infixl int_of_xml
- | "infixr" => unwrap Infixr int_of_xml
| "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
| _ => parse_err "mixfix"
) e
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Feb 15 17:17:51 2010 +0100
@@ -651,7 +651,7 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
+ let val full_tname = Sign.full_name tmp_thy tname
in
(case duplicates (op =) tvs of
[] =>
@@ -675,10 +675,10 @@
val _ =
(case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
[] => ()
- | vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [(Sign.full_name_path tmp_thy tname'
- (Binding.map_name (Syntax.const_name mx') cname),
- map (dtyp_of_typ new_dts) cargs')],
+ | vs => error ("Extra type variables on rhs: " ^ commas vs));
+ val c = Sign.full_name_path tmp_thy tname' cname;
+ in
+ (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
@@ -686,14 +686,12 @@
val (constrs', constr_syntax', sorts') =
fold prep_constr constrs ([], [], sorts)
-
in
case duplicates (op =) (map fst constrs') of
- [] =>
- (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
- map DtTFree tvs, constrs'))],
+ [] =>
+ (dts' @ [(i, (Sign.full_name tmp_thy tname, map DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
- | dups => error ("Duplicate constructors " ^ commas dups ^
+ | dups => error ("Duplicate constructors " ^ commas dups ^
" in datatype " ^ quote (Binding.str_of tname))
end;
--- a/src/HOL/Tools/typedef.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Mon Feb 15 17:17:51 2010 +0100
@@ -55,7 +55,7 @@
structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
val interpretation = Typedef_Interpretation.interpretation;
-fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
+fun prepare_typedef prep_term def name (tname, vs, mx) raw_set opt_morphs thy =
let
val _ = Theory.requires thy "Typedef" "typedefs";
val ctxt = ProofContext.init thy;
@@ -79,7 +79,6 @@
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
|> map TFree;
- val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -125,7 +124,7 @@
in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
fun typedef_result inhabited =
- ObjectLogic.typedecl (t, vs, mx)
+ ObjectLogic.typedecl (tname, vs, mx)
#> snd
#> Sign.add_consts_i
[(Rep_name, newT --> oldT, NoSyn),
@@ -252,8 +251,7 @@
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name),
- (t, vs, mx), A, morphs);
+ typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Feb 15 17:17:51 2010 +0100
@@ -160,7 +160,7 @@
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,args,mx) =
- ((Syntax.const_name mx (Binding.name_of con)),
+ (Binding.name_of con, (* FIXME preverse binding (!?) *)
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
@@ -235,7 +235,7 @@
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,args,mx) =
- ((Syntax.const_name mx (Binding.name_of con)),
+ (Binding.name_of con, (* FIXME preverse binding (!?) *)
ListPair.map (fn ((lazy,sel,tp),vn) =>
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Mon Feb 15 17:17:51 2010 +0100
@@ -28,7 +28,7 @@
open Domain_Library;
infixr 5 -->; infixr 6 ->>;
-fun calc_syntax
+fun calc_syntax (* FIXME authentic syntax *)
(definitional : bool)
(dtypeprod : typ)
((dname : string, typevars : typ list),
@@ -115,7 +115,7 @@
local open Syntax in
local
- fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
+ fun c_ast con mx = Constant (Binding.name_of con); (* FIXME proper const syntax *)
fun expvar n = Variable ("e"^(string_of_int n));
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
(string_of_int m));
--- a/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 17:17:51 2010 +0100
@@ -53,19 +53,8 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
-
-fun fix_mixfix (syn , T, mx as Infix p ) =
- (const_binding mx syn, T, InfixName (Binding.name_of syn, p))
- | fix_mixfix (syn , T, mx as Infixl p ) =
- (const_binding mx syn, T, InfixlName (Binding.name_of syn, p))
- | fix_mixfix (syn , T, mx as Infixr p ) =
- (const_binding mx syn, T, InfixrName (Binding.name_of syn, p))
- | fix_mixfix decl = decl;
-
-fun transform decl =
+fun transform (c, T, mx) =
let
- val (c, T, mx) = fix_mixfix decl;
val c1 = Binding.name_of c;
val c2 = "_cont_" ^ c1;
val n = Syntax.mixfix_args mx
@@ -78,9 +67,9 @@
fun is_contconst (_,_,NoSyn ) = false
| is_contconst (_,_,Binder _) = false
-| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
- handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name mx (Binding.name_of c)));
+| is_contconst (c,T,mx ) =
+ cfun_arity T >= Syntax.mixfix_args mx
+ handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
(* add_consts(_i) *)
@@ -94,6 +83,7 @@
thy
|> Sign.add_consts_i
(normal_decls @ map first transformed_decls @ map second transformed_decls)
+ (* FIXME authentic syntax *)
|> Sign.add_trrules_i (maps third transformed_decls)
end;
--- a/src/HOLCF/Tools/pcpodef.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Mon Feb 15 17:17:51 2010 +0100
@@ -153,7 +153,7 @@
fun declare_type_name a =
Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-fun prepare prep_term name (t, vs, mx) raw_set opt_morphs thy =
+fun prepare prep_term name (tname, vs, mx) raw_set opt_morphs thy =
let
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
val ctxt = ProofContext.init thy;
@@ -168,7 +168,6 @@
(*lhs*)
val defS = Sign.defaultS thy;
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
- val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -346,7 +345,7 @@
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
+ ((def, the_default t opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
--- a/src/HOLCF/Tools/repdef.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Mon Feb 15 17:17:51 2010 +0100
@@ -59,7 +59,7 @@
(prep_term: Proof.context -> 'a -> term)
(def: bool)
(name: binding)
- (typ as (t, vs, mx) : binding * string list * mixfix)
+ (typ as (tname, vs, mx) : binding * string list * mixfix)
(raw_defl: 'a)
(opt_morphs: (binding * binding) option)
(thy: theory)
@@ -79,7 +79,6 @@
val defS = Sign.defaultS thy;
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
val lhs_sorts = map snd lhs_tfrees;
- val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -172,8 +171,7 @@
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- repdef_cmd
- ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
+ repdef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
--- a/src/Pure/Isar/object_logic.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/Isar/object_logic.ML Mon Feb 15 17:17:51 2010 +0100
@@ -84,10 +84,9 @@
(* typedecl *)
-fun typedecl (a, vs, mx) thy =
+fun typedecl (b, vs, mx) thy =
let
val base_sort = get_base_sort thy;
- val b = Binding.map_name (Syntax.type_name mx) a;
val _ = has_duplicates (op =) vs andalso
error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
val name = Sign.full_name thy b;
@@ -95,7 +94,7 @@
val T = Type (name, map (fn v => TFree (v, [])) vs);
in
thy
- |> Sign.add_types [(a, n, mx)]
+ |> Sign.add_types [(b, n, mx)]
|> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
|> pair T
end;
@@ -106,7 +105,7 @@
local
fun gen_add_judgment add_consts (b, T, mx) thy =
- let val c = Sign.full_name thy (Binding.map_name (Syntax.const_name mx) b) in
+ let val c = Sign.full_name thy b in
thy
|> add_consts [(b, T, mx)]
|> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
--- a/src/Pure/Isar/outer_parse.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/Isar/outer_parse.ML Mon Feb 15 17:17:51 2010 +0100
@@ -266,9 +266,9 @@
!!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
-val infx = $$$ "infix" |-- !!! (nat >> Infix || string -- nat >> InfixName);
-val infxl = $$$ "infixl" |-- !!! (nat >> Infixl || string -- nat >> InfixlName);
-val infxr = $$$ "infixr" |-- !!! (nat >> Infixr || string -- nat >> InfixrName);
+val infx = $$$ "infix" |-- !!! (string -- nat >> InfixName);
+val infxl = $$$ "infixl" |-- !!! (string -- nat >> InfixlName);
+val infxr = $$$ "infixr" |-- !!! (string -- nat >> InfixrName);
val binder = $$$ "binder" |--
!!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
--- a/src/Pure/Isar/proof_context.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Feb 15 17:17:51 2010 +0100
@@ -966,19 +966,18 @@
local
fun prep_vars prep_typ internal =
- fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
+ fold_map (fn (b, raw_T, mx) => fn ctxt =>
let
- val raw_x = Name.of_binding raw_b;
- val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
+ val x = Name.of_binding b;
val _ = Syntax.is_identifier (no_skolem internal x) orelse
- error ("Illegal variable name: " ^ quote x);
+ error ("Illegal variable name: " ^ quote (Binding.str_of b));
fun cond_tvars T =
if internal then T
else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
- val var = (Binding.map_name (K x) raw_b, opt_T, mx);
- in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
+ val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
+ in ((b, opt_T, mx), ctxt') end);
in
--- a/src/Pure/Syntax/mixfix.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML Mon Feb 15 17:17:51 2010 +0100
@@ -13,9 +13,6 @@
InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
- Infix of int | (*obsolete*)
- Infixl of int | (*obsolete*)
- Infixr of int | (*obsolete*)
Binder of string * int * int |
Structure
val binder_name: string -> string
@@ -27,9 +24,6 @@
val literal: string -> mixfix
val no_syn: 'a * 'b -> 'a * 'b * mixfix
val pretty_mixfix: mixfix -> Pretty.T
- val type_name: mixfix -> string -> string
- val const_name: mixfix -> string -> string
- val const_mixfix: string -> mixfix -> string * mixfix
val mixfix_args: mixfix -> int
val mixfixT: mixfix -> typ
end;
@@ -54,9 +48,6 @@
InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
- Infix of int | (*obsolete*)
- Infixl of int | (*obsolete*)
- Infixr of int | (*obsolete*)
Binder of string * int * int |
Structure;
@@ -84,9 +75,6 @@
| pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
| pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
| pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
- | pretty_mixfix (Infix p) = parens (Pretty.breaks [keyword "infix", int p])
- | pretty_mixfix (Infixl p) = parens (Pretty.breaks [keyword "infixl", int p])
- | pretty_mixfix (Infixr p) = parens (Pretty.breaks [keyword "infixr", int p])
| pretty_mixfix (Binder (s, p1, p2)) =
parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
| pretty_mixfix Structure = parens [keyword "structure"];
@@ -96,47 +84,12 @@
(* syntax specifications *)
-fun strip ("'" :: c :: cs) = c :: strip cs
- | strip ["'"] = []
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
-
-val strip_esc = implode o strip o Symbol.explode;
-
-fun deprecated c = (legacy_feature ("Unnamed infix operator " ^ quote c); c);
-
-fun type_name (InfixName _) = I
- | type_name (InfixlName _) = I
- | type_name (InfixrName _) = I
- | type_name (Infix _) = deprecated o strip_esc
- | type_name (Infixl _) = deprecated o strip_esc
- | type_name (Infixr _) = deprecated o strip_esc
- | type_name _ = I;
-
-fun const_name (InfixName _) = I
- | const_name (InfixlName _) = I
- | const_name (InfixrName _) = I
- | const_name (Infix _) = prefix "op " o deprecated o strip_esc
- | const_name (Infixl _) = prefix "op " o deprecated o strip_esc
- | const_name (Infixr _) = prefix "op " o deprecated o strip_esc
- | const_name _ = I;
-
-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;
-
-fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
-
fun mixfix_args NoSyn = 0
| mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
| mixfix_args (Delimfix sy) = SynExt.mfix_args sy
| mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
| mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
| mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
- | mixfix_args (Infix _) = 2
- | mixfix_args (Infixl _) = 2
- | mixfix_args (Infixr _) = 2
| mixfix_args (Binder _) = 1
| mixfix_args Structure = 0;
@@ -148,27 +101,19 @@
fun syn_ext_types type_decls =
let
- fun name_of (t, _, mx) = type_name mx t;
-
fun mk_infix sy t p1 p2 p3 =
SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
[SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
- fun mfix_of decl =
- 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))
- end;
+ fun mfix_of (_, _, NoSyn) = NONE
+ | mfix_of (t, 2, InfixName (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
+ | mfix_of (t, 2, InfixlName (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
+ | mfix_of (t, 2, InfixrName (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
+ | mfix_of (t, _, _) =
+ error ("Bad mixfix declaration for type: " ^ quote t); (* FIXME printable!? *)
val mfix = map_filter mfix_of type_decls;
- val xconsts = map name_of type_decls;
+ val xconsts = map #1 type_decls;
in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
@@ -179,8 +124,6 @@
fun syn_ext_consts is_logtype const_decls =
let
- fun name_of (c, _, mx) = const_name mx c;
-
fun mk_infix sy ty c p1 p2 p3 =
[SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
@@ -189,33 +132,27 @@
[Type ("idts", []), ty2] ---> ty3
| binder_typ c _ = error ("Bad type of binder: " ^ quote c);
- fun mfix_of decl =
- let val c = name_of decl in
- (case decl of
- (_, _, 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)) =>
- [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
- | _ => error ("Bad mixfix declaration for const: " ^ quote c))
- end;
+ fun mfix_of (_, _, NoSyn) = []
+ | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)]
+ | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
+ | mfix_of (c, ty, InfixName (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
+ | mfix_of (c, ty, InfixlName (sy, p)) = mk_infix sy ty c p (p + 1) p
+ | mfix_of (c, ty, InfixrName (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);
fun binder (c, _, Binder _) = SOME (binder_name c, c)
| binder _ = NONE;
val mfix = maps mfix_of const_decls;
- val xconsts = map name_of const_decls;
+ val xconsts = map #1 const_decls;
val binders = map_filter binder const_decls;
- val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o
- apsnd K o SynTrans.mk_binder_tr);
- val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o
- apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
+ val binder_trs = binders
+ |> map (SynExt.stamp_trfun binder_stamp o apsnd K o SynTrans.mk_binder_tr);
+ val binder_trs' = binders
+ |> map (SynExt.stamp_trfun binder_stamp o
+ apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
in
SynExt.syn_ext' true is_logtype
mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
--- a/src/Pure/sign.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/Pure/sign.ML Mon Feb 15 17:17:51 2010 +0100
@@ -434,7 +434,7 @@
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
- val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
+ val decls = map (fn (a, n, _) => (a, n)) types;
val tsig' = fold (Type.add_type naming) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -450,12 +450,11 @@
(* add type abbreviations *)
-fun gen_add_tyabbr parse_typ (a, vs, rhs, mx) thy =
+fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val ctxt = ProofContext.init thy;
- val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
- val b = Binding.map_name (Syntax.type_name mx) a;
+ val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
@@ -471,8 +470,7 @@
let
val ctxt = ProofContext.init thy;
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
- handle ERROR msg =>
- cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name mx c));
+ handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
@@ -500,10 +498,8 @@
let
val ctxt = ProofContext.init thy;
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
- fun prep (raw_b, raw_T, raw_mx) =
+ fun prep (b, raw_T, mx) =
let
- val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
- val b = Binding.map_name (K mx_name) raw_b;
val c = full_name thy b;
val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
--- a/src/ZF/ind_syntax.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/ZF/ind_syntax.ML Mon Feb 15 17:17:51 2010 +0100
@@ -65,15 +65,14 @@
| dest_mem _ = error "Constructor specifications must have the form x:A";
(*read a constructor specification*)
-fun read_construct ctxt (id, sprems, syn) =
+fun read_construct ctxt (id: string, sprems, syn: mixfix) =
let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
|> Syntax.check_terms ctxt
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT
handle TERM _ => error
"Bad variable in constructor specification"
- val name = Syntax.const_name syn id
- in ((id,T,syn), name, args, prems) end;
+ in ((id,T,syn), id, args, prems) end;
val read_constructs = map o map o read_construct;