# HG changeset patch # User wenzelm # Date 1266250671 -3600 # Node ID ed24ba6f69aabc7c0102f55aa5e4aeacf6db7b58 # Parent c1ad622e90e47f4865992e5ae53c129309596ff2 discontinued unnamed infix syntax; diff -r c1ad622e90e4 -r ed24ba6f69aa NEWS --- 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 *** diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOL/Import/xmlconv.ML --- 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 diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOL/Tools/typedef.ML --- 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)" diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOLCF/Tools/Domain/domain_extender.ML --- 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)) diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOLCF/Tools/Domain/domain_syntax.ML --- 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)); diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOLCF/Tools/cont_consts.ML --- 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; diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOLCF/Tools/pcpodef.ML --- 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 diff -r c1ad622e90e4 -r ed24ba6f69aa src/HOLCF/Tools/repdef.ML --- 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 diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/Isar/object_logic.ML --- 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') diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/Isar/outer_parse.ML --- 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)))) diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/Isar/proof_context.ML --- 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 diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/Syntax/mixfix.ML --- 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', []) [] ([], []) diff -r c1ad622e90e4 -r ed24ba6f69aa src/Pure/sign.ML --- 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 => diff -r c1ad622e90e4 -r ed24ba6f69aa src/ZF/ind_syntax.ML --- 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;