renamed InfixName to Infix etc.;
authorwenzelm
Mon Feb 15 18:03:42 2010 +0100 (2010-02-15)
changeset 351300991c84e8dcf
parent 35129 ed24ba6f69aa
child 35131 7e24282f2dd7
renamed InfixName to Infix etc.;
NEWS
src/HOL/Import/xmlconv.ML
src/HOLCF/Tools/cont_consts.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Mon Feb 15 17:17:51 2010 +0100
     1.2 +++ b/NEWS	Mon Feb 15 18:03:42 2010 +0100
     1.3 @@ -10,7 +10,9 @@
     1.4  the user space functionality any longer.
     1.5  
     1.6  * Discontinued unnamed infix syntax (legacy feature for many years) --
     1.7 -need to specify constant name and syntax separately.
     1.8 +need to specify constant name and syntax separately.  Internal ML
     1.9 +datatype constructors have been renamed from InfixName to Infix etc.
    1.10 +Minor INCOMPATIBILITY.
    1.11  
    1.12  
    1.13  *** HOL ***
     2.1 --- a/src/HOL/Import/xmlconv.ML	Mon Feb 15 17:17:51 2010 +0100
     2.2 +++ b/src/HOL/Import/xmlconv.ML	Mon Feb 15 18:03:42 2010 +0100
     2.3 @@ -218,9 +218,9 @@
     2.4    | xml_of_mixfix Structure = wrap_empty "structure"
     2.5    | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
     2.6    | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
     2.7 -  | xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args
     2.8 -  | xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args
     2.9 -  | xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args
    2.10 +  | xml_of_mixfix (Infix args) = wrap "infix" (xml_of_pair xml_of_string xml_of_int) args
    2.11 +  | xml_of_mixfix (Infixl args) = wrap "infixl" (xml_of_pair xml_of_string xml_of_int) args
    2.12 +  | xml_of_mixfix (Infixr args) = wrap "infixr" (xml_of_pair xml_of_string xml_of_int) args
    2.13    | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
    2.14                                    
    2.15  fun mixfix_of_xml e = 
    2.16 @@ -229,9 +229,9 @@
    2.17         | "structure" => unwrap_empty Structure 
    2.18         | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
    2.19         | "delimfix" => unwrap Delimfix string_of_xml
    2.20 -       | "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml) 
    2.21 -       | "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml)  
    2.22 -       | "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml)
    2.23 +       | "infix" => unwrap Infix (pair_of_xml string_of_xml int_of_xml) 
    2.24 +       | "infixl" => unwrap Infixl (pair_of_xml string_of_xml int_of_xml)  
    2.25 +       | "infixr" => unwrap Infixr (pair_of_xml string_of_xml int_of_xml)
    2.26         | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
    2.27         | _ => parse_err "mixfix"
    2.28      ) e
     3.1 --- a/src/HOLCF/Tools/cont_consts.ML	Mon Feb 15 17:17:51 2010 +0100
     3.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Mon Feb 15 18:03:42 2010 +0100
     3.3 @@ -40,9 +40,9 @@
     3.4          fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg])
     3.5            vnames (Constant name1))] @
     3.6      (case mx of
     3.7 -      InfixName _ => [extra_parse_rule]
     3.8 -    | InfixlName _ => [extra_parse_rule]
     3.9 -    | InfixrName _ => [extra_parse_rule]
    3.10 +      Infix _ => [extra_parse_rule]
    3.11 +    | Infixl _ => [extra_parse_rule]
    3.12 +    | Infixr _ => [extra_parse_rule]
    3.13      | _ => [])
    3.14    end;
    3.15  
     4.1 --- a/src/Pure/Isar/outer_parse.ML	Mon Feb 15 17:17:51 2010 +0100
     4.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Feb 15 18:03:42 2010 +0100
     4.3 @@ -266,9 +266,9 @@
     4.4    !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
     4.5      Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
     4.6  
     4.7 -val infx = $$$ "infix" |-- !!! (string -- nat >> InfixName);
     4.8 -val infxl = $$$ "infixl" |-- !!! (string -- nat >> InfixlName);
     4.9 -val infxr = $$$ "infixr" |-- !!! (string -- nat >> InfixrName);
    4.10 +val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
    4.11 +val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
    4.12 +val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
    4.13  
    4.14  val binder = $$$ "binder" |--
    4.15    !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
     5.1 --- a/src/Pure/Syntax/mixfix.ML	Mon Feb 15 17:17:51 2010 +0100
     5.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon Feb 15 18:03:42 2010 +0100
     5.3 @@ -10,9 +10,9 @@
     5.4      NoSyn |
     5.5      Mixfix of string * int list * int |
     5.6      Delimfix of string |
     5.7 -    InfixName of string * int |
     5.8 -    InfixlName of string * int |
     5.9 -    InfixrName of string * int |
    5.10 +    Infix of string * int |
    5.11 +    Infixl of string * int |
    5.12 +    Infixr of string * int |
    5.13      Binder of string * int * int |
    5.14      Structure
    5.15    val binder_name: string -> string
    5.16 @@ -45,9 +45,9 @@
    5.17    NoSyn |
    5.18    Mixfix of string * int list * int |
    5.19    Delimfix of string |
    5.20 -  InfixName of string * int |
    5.21 -  InfixlName of string * int |
    5.22 -  InfixrName of string * int |
    5.23 +  Infix of string * int |
    5.24 +  Infixl of string * int |
    5.25 +  Infixr of string * int |
    5.26    Binder of string * int * int |
    5.27    Structure;
    5.28  
    5.29 @@ -72,9 +72,9 @@
    5.30    | pretty_mixfix (Mixfix (s, ps, p)) =
    5.31        parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
    5.32    | pretty_mixfix (Delimfix s) = parens [quoted s]
    5.33 -  | pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    5.34 -  | pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    5.35 -  | pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    5.36 +  | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    5.37 +  | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    5.38 +  | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    5.39    | pretty_mixfix (Binder (s, p1, p2)) =
    5.40        parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
    5.41    | pretty_mixfix Structure = parens [keyword "structure"];
    5.42 @@ -87,9 +87,9 @@
    5.43  fun mixfix_args NoSyn = 0
    5.44    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
    5.45    | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
    5.46 -  | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
    5.47 -  | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
    5.48 -  | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
    5.49 +  | mixfix_args (Infix (sy, _)) = 2 + SynExt.mfix_args sy
    5.50 +  | mixfix_args (Infixl (sy, _)) = 2 + SynExt.mfix_args sy
    5.51 +  | mixfix_args (Infixr (sy, _)) = 2 + SynExt.mfix_args sy
    5.52    | mixfix_args (Binder _) = 1
    5.53    | mixfix_args Structure = 0;
    5.54  
    5.55 @@ -106,9 +106,9 @@
    5.56          [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
    5.57  
    5.58      fun mfix_of (_, _, NoSyn) = NONE
    5.59 -      | mfix_of (t, 2, InfixName (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
    5.60 -      | mfix_of (t, 2, InfixlName (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
    5.61 -      | mfix_of (t, 2, InfixrName (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
    5.62 +      | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
    5.63 +      | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
    5.64 +      | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
    5.65        | mfix_of (t, _, _) =
    5.66            error ("Bad mixfix declaration for type: " ^ quote t);  (* FIXME printable!? *)
    5.67  
    5.68 @@ -135,9 +135,9 @@
    5.69      fun mfix_of (_, _, NoSyn) = []
    5.70        | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)]
    5.71        | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
    5.72 -      | mfix_of (c, ty, InfixName (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
    5.73 -      | mfix_of (c, ty, InfixlName (sy, p)) = mk_infix sy ty c p (p + 1) p
    5.74 -      | mfix_of (c, ty, InfixrName (sy, p)) = mk_infix sy ty c (p + 1) p p
    5.75 +      | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
    5.76 +      | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
    5.77 +      | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
    5.78        | mfix_of (c, ty, Binder (sy, p, q)) =
    5.79            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
    5.80        | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c);
     6.1 --- a/src/Pure/Syntax/syntax.ML	Mon Feb 15 17:17:51 2010 +0100
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Feb 15 18:03:42 2010 +0100
     6.3 @@ -450,9 +450,9 @@
     6.4  fun guess_infix (Syntax ({gram, ...}, _)) c =
     6.5    (case Parser.guess_infix_lr gram c of
     6.6      SOME (s, l, r, j) => SOME
     6.7 -     (if l then Mixfix.InfixlName (s, j)
     6.8 -      else if r then Mixfix.InfixrName (s, j)
     6.9 -      else Mixfix.InfixName (s, j))
    6.10 +     (if l then Mixfix.Infixl (s, j)
    6.11 +      else if r then Mixfix.Infixr (s, j)
    6.12 +      else Mixfix.Infix (s, j))
    6.13    | NONE => NONE);
    6.14  
    6.15  
    6.16 @@ -914,8 +914,8 @@
    6.17  
    6.18  end;
    6.19  
    6.20 -structure BasicSyntax: BASIC_SYNTAX = Syntax;
    6.21 -open BasicSyntax;
    6.22 +structure Basic_Syntax: BASIC_SYNTAX = Syntax;
    6.23 +open Basic_Syntax;
    6.24  
    6.25  forget_structure "Ast";
    6.26  forget_structure "SynExt";
     7.1 --- a/src/Pure/pure_thy.ML	Mon Feb 15 17:17:51 2010 +0100
     7.2 +++ b/src/Pure/pure_thy.ML	Mon Feb 15 18:03:42 2010 +0100
     7.3 @@ -313,7 +313,7 @@
     7.4      (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
     7.5      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     7.6      ("Pure.term",   typ "logic => prop",               Delimfix "TERM _"),
     7.7 -    ("Pure.conjunction", typ "prop => prop => prop",   InfixrName ("&&&", 2))]
     7.8 +    ("Pure.conjunction", typ "prop => prop => prop",   Infixr ("&&&", 2))]
     7.9    #> Sign.add_syntax_i applC_syntax
    7.10    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    7.11     [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    7.12 @@ -325,9 +325,9 @@
    7.13      ("_idtypdummy", typ "type => idt",         Mixfix ("'_()\\<Colon>_", [], 0)),
    7.14      ("_type_constraint_", typ "'a",            NoSyn),
    7.15      ("_lambda",  typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    7.16 -    ("==",       typ "'a => 'a => prop",       InfixrName ("\\<equiv>", 2)),
    7.17 +    ("==",       typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
    7.18      ("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    7.19 -    ("==>",      typ "prop => prop => prop",   InfixrName ("\\<Longrightarrow>", 1)),
    7.20 +    ("==>",      typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    7.21      ("_DDDOT",   typ "aprop",                  Delimfix "\\<dots>"),
    7.22      ("_bigimpl", typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    7.23      ("_DDDOT",   typ "logic",                  Delimfix "\\<dots>")]
    7.24 @@ -336,7 +336,7 @@
    7.25    #> Sign.add_modesyntax_i ("HTML", false)
    7.26     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    7.27    #> Sign.add_consts_i
    7.28 -   [(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)),
    7.29 +   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
    7.30      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    7.31      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    7.32      (Binding.name "prop", typ "prop => prop", NoSyn),