src/Pure/pure_thy.ML
changeset 62752 d09d71223e7a
parent 62529 8b7bdfc09f3b
child 62761 5c672b22dcc2
     1.1 --- a/src/Pure/pure_thy.ML	Tue Mar 29 20:53:52 2016 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Mar 29 21:17:29 2016 +0200
     1.3 @@ -22,18 +22,24 @@
     1.4  
     1.5  val qualify = Binding.qualify true Context.PureN;
     1.6  
     1.7 +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
     1.8 +fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
     1.9 +fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);
    1.10 +fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
    1.11 +fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
    1.12 +
    1.13  
    1.14  (* application syntax variants *)
    1.15  
    1.16  val appl_syntax =
    1.17 - [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
    1.18 -  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    1.19 + [("_appl", typ "('b => 'a) => args => logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
    1.20 +  ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
    1.21  
    1.22  val applC_syntax =
    1.23 - [("",       typ "'a => cargs",                  Delimfix "_"),
    1.24 -  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
    1.25 -  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
    1.26 -  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
    1.27 + [("",       typ "'a => cargs",                  delimfix "_"),
    1.28 +  ("_cargs", typ "'a => cargs => cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
    1.29 +  ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
    1.30 +  ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
    1.31  
    1.32  structure Old_Appl_Syntax = Theory_Data
    1.33  (
    1.34 @@ -81,120 +87,120 @@
    1.35          "class_name"]))
    1.36    #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
    1.37    #> Sign.add_syntax Syntax.mode_default
    1.38 -   [("",            typ "prop' => prop",               Delimfix "_"),
    1.39 -    ("",            typ "logic => any",                Delimfix "_"),
    1.40 -    ("",            typ "prop' => any",                Delimfix "_"),
    1.41 -    ("",            typ "logic => logic",              Delimfix "'(_')"),
    1.42 -    ("",            typ "prop' => prop'",              Delimfix "'(_')"),
    1.43 -    ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
    1.44 -    ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
    1.45 +   [("",            typ "prop' => prop",               delimfix "_"),
    1.46 +    ("",            typ "logic => any",                delimfix "_"),
    1.47 +    ("",            typ "prop' => any",                delimfix "_"),
    1.48 +    ("",            typ "logic => logic",              delimfix "'(_')"),
    1.49 +    ("",            typ "prop' => prop'",              delimfix "'(_')"),
    1.50 +    ("_constrain",  typ "logic => type => logic",      mixfix ("_::_", [4, 0], 3)),
    1.51 +    ("_constrain",  typ "prop' => type => prop'",      mixfix ("_::_", [4, 0], 3)),
    1.52      ("_ignore_type", typ "'a",                         NoSyn),
    1.53 -    ("",            typ "tid_position => type",        Delimfix "_"),
    1.54 -    ("",            typ "tvar_position => type",       Delimfix "_"),
    1.55 -    ("",            typ "type_name => type",           Delimfix "_"),
    1.56 -    ("_type_name",  typ "id => type_name",             Delimfix "_"),
    1.57 -    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
    1.58 -    ("_ofsort",     typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
    1.59 -    ("_ofsort",     typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
    1.60 -    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
    1.61 -    ("",            typ "class_name => sort",          Delimfix "_"),
    1.62 -    ("_class_name", typ "id => class_name",            Delimfix "_"),
    1.63 -    ("_class_name", typ "longid => class_name",        Delimfix "_"),
    1.64 -    ("_topsort",    typ "sort",                        Delimfix "{}"),
    1.65 -    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
    1.66 -    ("",            typ "class_name => classes",       Delimfix "_"),
    1.67 -    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
    1.68 -    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
    1.69 -    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    1.70 -    ("",            typ "type => types",               Delimfix "_"),
    1.71 -    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
    1.72 -    ("\<^type>fun", typ "type => type => type",        Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
    1.73 -    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
    1.74 -    ("",            typ "type => type",                Delimfix "'(_')"),
    1.75 -    ("\<^type>dummy", typ "type",                      Delimfix "'_"),
    1.76 +    ("",            typ "tid_position => type",        delimfix "_"),
    1.77 +    ("",            typ "tvar_position => type",       delimfix "_"),
    1.78 +    ("",            typ "type_name => type",           delimfix "_"),
    1.79 +    ("_type_name",  typ "id => type_name",             delimfix "_"),
    1.80 +    ("_type_name",  typ "longid => type_name",         delimfix "_"),
    1.81 +    ("_ofsort",     typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
    1.82 +    ("_ofsort",     typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
    1.83 +    ("_dummy_ofsort", typ "sort => type",              mixfix ("'_()::_", [0], 1000)),
    1.84 +    ("",            typ "class_name => sort",          delimfix "_"),
    1.85 +    ("_class_name", typ "id => class_name",            delimfix "_"),
    1.86 +    ("_class_name", typ "longid => class_name",        delimfix "_"),
    1.87 +    ("_topsort",    typ "sort",                        delimfix "{}"),
    1.88 +    ("_sort",       typ "classes => sort",             delimfix "{_}"),
    1.89 +    ("",            typ "class_name => classes",       delimfix "_"),
    1.90 +    ("_classes",    typ "class_name => classes => classes", delimfix "_,_"),
    1.91 +    ("_tapp",       typ "type => type_name => type",   mixfix ("_ _", [1000, 0], 1000)),
    1.92 +    ("_tappl",      typ "type => types => type_name => type", delimfix "((1'(_,/ _')) _)"),
    1.93 +    ("",            typ "type => types",               delimfix "_"),
    1.94 +    ("_types",      typ "type => types => types",      delimfix "_,/ _"),
    1.95 +    ("\<^type>fun", typ "type => type => type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
    1.96 +    ("_bracket",    typ "types => type => type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
    1.97 +    ("",            typ "type => type",                delimfix "'(_')"),
    1.98 +    ("\<^type>dummy", typ "type",                      delimfix "'_"),
    1.99      ("_type_prop",  typ "'a",                          NoSyn),
   1.100 -    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
   1.101 +    ("_lambda",     typ "pttrns => 'a => logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
   1.102      ("_abs",        typ "'a",                          NoSyn),
   1.103 -    ("",            typ "'a => args",                  Delimfix "_"),
   1.104 -    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
   1.105 -    ("",            typ "id_position => idt",          Delimfix "_"),
   1.106 -    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
   1.107 -    ("_idtyp",      typ "id_position => type => idt",  Mixfix ("_::_", [], 0)),
   1.108 -    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
   1.109 -    ("",            typ "idt => idt",                  Delimfix "'(_')"),
   1.110 -    ("",            typ "idt => idts",                 Delimfix "_"),
   1.111 -    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
   1.112 -    ("",            typ "idt => pttrn",                Delimfix "_"),
   1.113 -    ("",            typ "pttrn => pttrns",             Delimfix "_"),
   1.114 -    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
   1.115 -    ("",            typ "aprop => aprop",              Delimfix "'(_')"),
   1.116 -    ("",            typ "id_position => aprop",        Delimfix "_"),
   1.117 -    ("",            typ "longid_position => aprop",    Delimfix "_"),
   1.118 -    ("",            typ "var_position => aprop",       Delimfix "_"),
   1.119 -    ("_DDDOT",      typ "aprop",                       Delimfix "\<dots>"),
   1.120 -    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
   1.121 -    ("_asm",        typ "prop => asms",                Delimfix "_"),
   1.122 -    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
   1.123 -    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
   1.124 -    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   1.125 +    ("",            typ "'a => args",                  delimfix "_"),
   1.126 +    ("_args",       typ "'a => args => args",          delimfix "_,/ _"),
   1.127 +    ("",            typ "id_position => idt",          delimfix "_"),
   1.128 +    ("_idtdummy",   typ "idt",                         delimfix "'_"),
   1.129 +    ("_idtyp",      typ "id_position => type => idt",  mixfix ("_::_", [], 0)),
   1.130 +    ("_idtypdummy", typ "type => idt",                 mixfix ("'_()::_", [], 0)),
   1.131 +    ("",            typ "idt => idt",                  delimfix "'(_')"),
   1.132 +    ("",            typ "idt => idts",                 delimfix "_"),
   1.133 +    ("_idts",       typ "idt => idts => idts",         mixfix ("_/ _", [1, 0], 0)),
   1.134 +    ("",            typ "idt => pttrn",                delimfix "_"),
   1.135 +    ("",            typ "pttrn => pttrns",             delimfix "_"),
   1.136 +    ("_pttrns",     typ "pttrn => pttrns => pttrns",   mixfix ("_/ _", [1, 0], 0)),
   1.137 +    ("",            typ "aprop => aprop",              delimfix "'(_')"),
   1.138 +    ("",            typ "id_position => aprop",        delimfix "_"),
   1.139 +    ("",            typ "longid_position => aprop",    delimfix "_"),
   1.140 +    ("",            typ "var_position => aprop",       delimfix "_"),
   1.141 +    ("_DDDOT",      typ "aprop",                       delimfix "\<dots>"),
   1.142 +    ("_aprop",      typ "aprop => prop",               delimfix "PROP _"),
   1.143 +    ("_asm",        typ "prop => asms",                delimfix "_"),
   1.144 +    ("_asms",       typ "prop => asms => asms",        delimfix "_;/ _"),
   1.145 +    ("_bigimpl",    typ "asms => prop => prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
   1.146 +    ("_ofclass",    typ "type => logic => prop",       delimfix "(1OFCLASS/(1'(_,/ _')))"),
   1.147      ("_mk_ofclass", typ "dummy",                       NoSyn),
   1.148 -    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
   1.149 -    ("",            typ "id_position => logic",        Delimfix "_"),
   1.150 -    ("",            typ "longid_position => logic",    Delimfix "_"),
   1.151 -    ("",            typ "var_position => logic",       Delimfix "_"),
   1.152 -    ("_DDDOT",      typ "logic",                       Delimfix "\<dots>"),
   1.153 +    ("_TYPE",       typ "type => logic",               delimfix "(1TYPE/(1'(_')))"),
   1.154 +    ("",            typ "id_position => logic",        delimfix "_"),
   1.155 +    ("",            typ "longid_position => logic",    delimfix "_"),
   1.156 +    ("",            typ "var_position => logic",       delimfix "_"),
   1.157 +    ("_DDDOT",      typ "logic",                       delimfix "\<dots>"),
   1.158      ("_strip_positions", typ "'a", NoSyn),
   1.159 -    ("_position",   typ "num_token => num_position",   Delimfix "_"),
   1.160 -    ("_position",   typ "float_token => float_position", Delimfix "_"),
   1.161 -    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
   1.162 -    ("_constify",   typ "float_position => float_const", Delimfix "_"),
   1.163 -    ("_index",      typ "logic => index",              Delimfix "(00\<^bsub>_\<^esub>)"),
   1.164 -    ("_indexdefault", typ "index",                     Delimfix ""),
   1.165 -    ("_indexvar",   typ "index",                       Delimfix "'\<index>"),
   1.166 +    ("_position",   typ "num_token => num_position",   delimfix "_"),
   1.167 +    ("_position",   typ "float_token => float_position", delimfix "_"),
   1.168 +    ("_constify",   typ "num_position => num_const",   delimfix "_"),
   1.169 +    ("_constify",   typ "float_position => float_const", delimfix "_"),
   1.170 +    ("_index",      typ "logic => index",              delimfix "(00\<^bsub>_\<^esub>)"),
   1.171 +    ("_indexdefault", typ "index",                     delimfix ""),
   1.172 +    ("_indexvar",   typ "index",                       delimfix "'\<index>"),
   1.173      ("_struct",     typ "index => logic",              NoSyn),
   1.174      ("_update_name", typ "idt",                        NoSyn),
   1.175      ("_constrainAbs", typ "'a",                        NoSyn),
   1.176 -    ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
   1.177 -    ("_position_sort", typ "tvar => tvar_position",    Delimfix "_"),
   1.178 -    ("_position",   typ "id => id_position",           Delimfix "_"),
   1.179 -    ("_position",   typ "longid => longid_position",   Delimfix "_"),
   1.180 -    ("_position",   typ "var => var_position",         Delimfix "_"),
   1.181 -    ("_position",   typ "str_token => str_position",   Delimfix "_"),
   1.182 -    ("_position",   typ "string_token => string_position", Delimfix "_"),
   1.183 -    ("_position",   typ "cartouche => cartouche_position", Delimfix "_"),
   1.184 +    ("_position_sort", typ "tid => tid_position",      delimfix "_"),
   1.185 +    ("_position_sort", typ "tvar => tvar_position",    delimfix "_"),
   1.186 +    ("_position",   typ "id => id_position",           delimfix "_"),
   1.187 +    ("_position",   typ "longid => longid_position",   delimfix "_"),
   1.188 +    ("_position",   typ "var => var_position",         delimfix "_"),
   1.189 +    ("_position",   typ "str_token => str_position",   delimfix "_"),
   1.190 +    ("_position",   typ "string_token => string_position", delimfix "_"),
   1.191 +    ("_position",   typ "cartouche => cartouche_position", delimfix "_"),
   1.192      ("_type_constraint_", typ "'a",                    NoSyn),
   1.193 -    ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
   1.194 -    ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
   1.195 -    ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
   1.196 -    ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
   1.197 -    ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
   1.198 -    ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
   1.199 -    ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
   1.200 -    ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
   1.201 -    (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
   1.202 -    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   1.203 -    (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
   1.204 -    (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
   1.205 +    ("_context_const", typ "id_position => logic",     delimfix "CONST _"),
   1.206 +    ("_context_const", typ "id_position => aprop",     delimfix "CONST _"),
   1.207 +    ("_context_const", typ "longid_position => logic", delimfix "CONST _"),
   1.208 +    ("_context_const", typ "longid_position => aprop", delimfix "CONST _"),
   1.209 +    ("_context_xconst", typ "id_position => logic",    delimfix "XCONST _"),
   1.210 +    ("_context_xconst", typ "id_position => aprop",    delimfix "XCONST _"),
   1.211 +    ("_context_xconst", typ "longid_position => logic", delimfix "XCONST _"),
   1.212 +    ("_context_xconst", typ "longid_position => aprop", delimfix "XCONST _"),
   1.213 +    (const "Pure.dummy_pattern", typ "aprop",          delimfix "'_"),
   1.214 +    ("_sort_constraint", typ "type => prop",           delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   1.215 +    (const "Pure.term", typ "logic => prop",           delimfix "TERM _"),
   1.216 +    (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))]
   1.217    #> Sign.add_syntax Syntax.mode_default applC_syntax
   1.218    #> Sign.add_syntax (Print_Mode.ASCII, true)
   1.219 -   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ => _)", [1, 0], 0)),
   1.220 -    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ => _)", [0, 0], 0)),
   1.221 -    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3%_./ _)", [0, 3], 3)),
   1.222 -    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("==", 2)),
   1.223 -    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
   1.224 -    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("==>", 1)),
   1.225 -    ("_DDDOT",            typ "aprop",                  Delimfix "..."),
   1.226 -    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   1.227 -    ("_DDDOT",            typ "logic",                  Delimfix "...")]
   1.228 +   [(tycon "fun",         typ "type => type => type",   mixfix ("(_/ => _)", [1, 0], 0)),
   1.229 +    ("_bracket",          typ "types => type => type",  mixfix ("([_]/ => _)", [0, 0], 0)),
   1.230 +    ("_lambda",           typ "pttrns => 'a => logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
   1.231 +    (const "Pure.eq",     typ "'a => 'a => prop",       infix_ ("==", 2)),
   1.232 +    (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
   1.233 +    (const "Pure.imp",    typ "prop => prop => prop",   infixr_ ("==>", 1)),
   1.234 +    ("_DDDOT",            typ "aprop",                  delimfix "..."),
   1.235 +    ("_bigimpl",          typ "asms => prop => prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   1.236 +    ("_DDDOT",            typ "logic",                  delimfix "...")]
   1.237    #> Sign.add_syntax ("", false)
   1.238 -   [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   1.239 +   [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
   1.240    #> Sign.add_consts
   1.241 -   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
   1.242 -    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
   1.243 -    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
   1.244 +   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
   1.245 +    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
   1.246 +    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
   1.247      (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
   1.248      (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
   1.249 -    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
   1.250 +    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")]
   1.251    #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
   1.252    #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
   1.253    #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []