moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
authorwenzelm
Thu Jan 19 21:22:24 2006 +0100 (2006-01-19)
changeset 18719dca3ae4f6dd6
parent 18718 d01837224eaf
child 18720 dd1ebba12151
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Jan 19 21:22:23 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Jan 19 21:22:24 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Mixfix declarations, infixes, binders. Also parts of the Pure syntax.
     1.8 +Mixfix declarations, infixes, binders.
     1.9  *)
    1.10  
    1.11  signature MIXFIX0 =
    1.12 @@ -32,12 +32,6 @@
    1.13    val fix_mixfix: string -> mixfix -> mixfix
    1.14    val unlocalize_mixfix: mixfix -> mixfix
    1.15    val mixfix_args: mixfix -> int
    1.16 -  val pure_nonterms: string list
    1.17 -  val pure_syntax: (string * string * mixfix) list
    1.18 -  val pure_syntax_output: (string * string * mixfix) list
    1.19 -  val pure_appl_syntax: (string * string * mixfix) list
    1.20 -  val pure_applC_syntax: (string * string * mixfix) list
    1.21 -  val pure_xsym_syntax: (string * string * mixfix) list
    1.22  end;
    1.23  
    1.24  signature MIXFIX =
    1.25 @@ -225,79 +219,4 @@
    1.26        mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
    1.27    end;
    1.28  
    1.29 -
    1.30 -
    1.31 -(** Pure syntax **)
    1.32 -
    1.33 -val pure_nonterms =
    1.34 -  (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
    1.35 -    SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
    1.36 -    "asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]);
    1.37 -
    1.38 -val pure_syntax =
    1.39 - [("_lambda",     "[pttrns, 'a] => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
    1.40 -  ("_abs",        "'a",                        NoSyn),
    1.41 -  ("",            "'a => " ^ SynExt.args,      Delimfix "_"),
    1.42 -  ("_args",       "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
    1.43 -  ("",            "id => idt",                 Delimfix "_"),
    1.44 -  ("_idtdummy",   "idt",                       Delimfix "'_"),
    1.45 -  ("_idtyp",      "[id, type] => idt",         Mixfix ("_::_", [], 0)),
    1.46 -  ("_idtypdummy", "type => idt",               Mixfix ("'_()::_", [], 0)),
    1.47 -  ("",            "idt => idt",                Delimfix "'(_')"),
    1.48 -  ("",            "idt => idts",               Delimfix "_"),
    1.49 -  ("_idts",       "[idt, idts] => idts",       Mixfix ("_/ _", [1, 0], 0)),
    1.50 -  ("",            "idt => pttrn",              Delimfix "_"),
    1.51 -  ("",            "pttrn => pttrns",           Delimfix "_"),
    1.52 -  ("_pttrns",     "[pttrn, pttrns] => pttrns", Mixfix ("_/ _", [1, 0], 0)),
    1.53 -  ("",            "id => aprop",               Delimfix "_"),
    1.54 -  ("",            "longid => aprop",           Delimfix "_"),
    1.55 -  ("",            "var => aprop",              Delimfix "_"),
    1.56 -  ("_DDDOT",      "aprop",                     Delimfix "..."),
    1.57 -  ("_aprop",      "aprop => prop",             Delimfix "PROP _"),
    1.58 -  ("_asm",        "prop => asms",              Delimfix "_"),
    1.59 -  ("_asms",       "[prop, asms] => asms",      Delimfix "_;/ _"),
    1.60 -  ("_bigimpl",    "[asms, prop] => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    1.61 -  ("_ofclass",    "[type, logic] => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.62 -  ("_mk_ofclass", "_",                         NoSyn),
    1.63 -  ("_TYPE",       "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
    1.64 -  ("",            "id => logic",               Delimfix "_"),
    1.65 -  ("",            "longid => logic",           Delimfix "_"),
    1.66 -  ("",            "var => logic",              Delimfix "_"),
    1.67 -  ("_DDDOT",      "logic",                     Delimfix "..."),
    1.68 -  ("_constify",   "num => num_const",          Delimfix "_"),
    1.69 -  ("_indexnum",   "num_const => index",        Delimfix "\\<^sub>_"),
    1.70 -  ("_index",      "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
    1.71 -  ("_indexdefault", "index",                   Delimfix ""),
    1.72 -  ("_indexvar",   "index",                     Delimfix "'\\<index>"),
    1.73 -  ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
    1.74 -
    1.75 -val pure_syntax_output =
    1.76 - [("prop", "prop => prop", Mixfix ("_", [0], 0)),
    1.77 -  ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))];
    1.78 -
    1.79 -val pure_appl_syntax =
    1.80 - [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),
    1.81 -  ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))];
    1.82 -
    1.83 -val pure_applC_syntax =
    1.84 - [("",       "'a => cargs",                  Delimfix "_"),
    1.85 -  ("_cargs", "['a, cargs] => cargs",         Mixfix ("_/ _", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri)),
    1.86 -  ("_applC", "[('b => 'a), cargs] => logic", Mixfix ("(1_/ _)", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri - 1)),
    1.87 -  ("_applC", "[('b => 'a), cargs] => aprop", Mixfix ("(1_/ _)", [SynExt.max_pri, SynExt.max_pri], SynExt.max_pri - 1))];
    1.88 -
    1.89 -val pure_xsym_syntax =
    1.90 - [("fun",      "[type, type] => type",  Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    1.91 -  ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    1.92 -  ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [SynExt.max_pri, 0], SynExt.max_pri)),
    1.93 -  ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
    1.94 -  ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
    1.95 -  ("_idtypdummy", "type => idt",        Mixfix ("'_()\\<Colon>_", [], 0)),
    1.96 -  ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    1.97 -  ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
    1.98 -  ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    1.99 -  ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
   1.100 -  ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   1.101 -  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   1.102 -  ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
   1.103 -
   1.104  end;