src/Pure/Thy/syntax.ML
author clasohm
Tue, 26 Oct 1993 22:24:20 +0100
changeset 81 4cc5a34292a9
parent 74 208ab8773a73
child 123 0a2f744e008a
permissions -rw-r--r--
corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Thy/syntax.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and Markus Wenzel, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
Definition of theory syntax together with translation to ML code.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
signature THYSYN =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
 sig
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
    10
  datatype BaseType = Thy  of string
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
    11
                    | File of string
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
    12
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
   val read: string list -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
functor ThySynFUN (Parse: PARSE): THYSYN =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
(*-------------- OBJECT TO STRING TRANSLATION ---------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
fun parent s = "(" ^ s ^ ")";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    26
fun pair(a, b) = parent(a ^ ", " ^ b);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    28
fun pair_quote(a, b) = pair(quote a, quote b);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    30
fun pair_quote2(a, b) = pair(a, quote b);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
fun bracket s = "[" ^ s ^ "]";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val comma = space_implode ", ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val bracket_comma = bracket o comma;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val big_bracket_comma = bracket o space_implode ",\n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
fun big_bracket_comma_ind ind strs = bracket (space_implode (",\n" ^ ind) strs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    42
val bracket_comma_quote = bracket_comma o (map quote);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*------------------- ABSTRACT SYNTAX FUNCTIONS ---------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
datatype mixfix = Mixfix of string * string * string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
                | Delimfix of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
                | Infixl of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
                | Infixr of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
                | Binder of string * string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
                | TInfixl of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
                | TInfixr of string;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
datatype pfix_or_mfix = Pref of string | Mixf of string;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun pm_proj(Pref s) = s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  | pm_proj(Mixf s) = s;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
fun split_decls l =
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    62
    let val (p, m) = partition (fn Pref _ => true | _ => false) l;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    in (big_bracket_comma_ind "   " (map pm_proj p), map pm_proj m) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
fun delim_mix (s, None) = Delimfix(s)
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    66
  | delim_mix (s, Some(l, n)) = Mixfix(s, l, n);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    68
fun mixfix (sy, c, ty, l, n) =  "Mixfix(" ^ comma[quote sy, c, ty, l, n] ^ ")";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    70
fun infixrl(ty, c, n) = parent(comma[ty, c, n]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    72
fun binder(sy, c, ty, n) = "Binder(" ^ comma[quote sy, c, ty, "0", n] ^ ")";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    74
fun delimfix (sy, c, ty) = "Delimfix(" ^ comma[quote sy, c, ty] ^ ")";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
fun tinfixrl (ty, n) = "(" ^ comma[ty, ty, n] ^ ")";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    78
fun mk_mfix((c, ty), mfix) =
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    79
      let val cs = quote c and tys = quote ty
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
      in case mfix of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
           Mixfix(sy, l, n) => mixfix (sy, tys, cs, l, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
         | Infixr(n) => "Infixr" ^ infixrl(cs, tys, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
         | Infixl(n) => "Infixl" ^ infixrl(cs, tys, n)
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    84
         | Binder(sy, n) => binder(sy, tys, cs, n)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
         | TInfixl(n) => "TInfixl" ^ tinfixrl(cs, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
         | TInfixr(n) => "TInfixr" ^ tinfixrl(cs, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
         | Delimfix(sy) => delimfix(sy, tys, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    91
fun mk_mixfix((cs, ty), None) =
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    92
      [Pref(pair(bracket_comma_quote cs, quote ty))]
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    93
  | mk_mixfix((c::cs, ty), Some(mfix)) =
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    94
      Mixf(mk_mfix((c, ty), mfix)) :: mk_mixfix((cs, ty), Some(mfix))
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    95
  | mk_mixfix(([], _), _) = [];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    97
fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_quote ts, n))]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  | mk_type_decl((t::ts, n), Some(tinfix)) =
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
    99
      [Pref(pair(bracket(quote t), n)), Mixf(mk_mfix((t, n), tinfix))] @
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
      mk_type_decl((ts, n), Some(tinfix))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  | mk_type_decl(([], n), Some(tinfix)) = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
fun mk_extension (((((((cl, def), (ty, tinfix)), ar), (co, mfix)), tr), ax), ml) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  ((cl, def, ty, ar, co, ax), big_bracket_comma_ind "    " tinfix,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
    big_bracket_comma_ind "     " mfix, big_bracket_comma_ind "     " tr, ml);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   108
fun add_val((id, _), s) = "val " ^ id ^ " = get_axiom thy " ^ quote id ^ "\n" ^ s;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
fun mk_rules ps =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  let
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   112
    val axs = big_bracket_comma_ind "  " (map pair_quote ps);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
    val vals = foldr add_val (ps, "")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  in
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   115
    axs ^ "\n\n" ^ vals
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
74
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   118
fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   119
                        ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
fun mk_sext mfix trans =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
  "Some (NewSext {\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
\   mixfix =\n    " ^ mfix ^ ",\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
\   xrules =\n    " ^ trans ^ ",\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
\   parse_ast_translation = parse_ast_translation,\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
\   parse_translation = parse_translation,\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
\   print_translation = print_translation,\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
\   print_ast_translation = print_ast_translation})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
fun mk_simple_sext mfix =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
  "Some (Syntax.simple_sext\n   " ^ mfix ^ ")";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
fun mk_ext ((cl, def, ty, ar, co, ax), sext) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
  " (" ^ space_implode ",\n  " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
fun mk_ext_thy (base, name, ext, sext) =
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   138
  "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
val preamble =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
  "\nlocal\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  \ val parse_ast_translation = []\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
  \ val parse_translation = []\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
  \ val print_translation = []\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
  \ val print_ast_translation = []\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  \in\n\n\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
  \(**** begin of user section ****)\n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val postamble = "\n(**** end of user section ****)\n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
fun mk_structure ((name, base), Some (ext, tinfix, mfix, trans, ml)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
        val noext = ("[]", "[]", "[]", "[]", "[]", "[]");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
        val basethy =
74
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   155
          if tinfix = "[]" then base ^ (quote name)
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   156
          else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
        val sext =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
          if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
          else mk_sext mfix trans;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   160
        val thy = "val thy = " ^ mk_ext_thy (basethy, name, ext, sext);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
      in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
        mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
      end
74
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   164
  | mk_structure ((name, base), None) =
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   165
      mk_struct (name, "\nval thy = " ^ base ^ (quote name));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   167
datatype BaseType = Thy  of string
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   168
                  | File of string;
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   169
74
208ab8773a73 changes in Readthy:
clasohm
parents: 20
diff changeset
   170
fun merge thys =
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   171
  let fun make_list (Thy t :: ts) =
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   172
            ("Thy \"" ^ t ^ "\"") :: make_list ts
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   173
        | make_list (File t :: ts) =
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   174
            ("File \"" ^ t ^ "\"") :: make_list ts
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   175
        | make_list [] = []
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   176
  in "base_on " ^ (bracket (space_implode "," (make_list thys))) ^ " " end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
(*------------------------ PARSERS -------------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
open Parse
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*------------------- VARIOUS PARSERS ----------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   187
val emptyl = empty >> K "[]";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   189
val ids  =  list_of1 id >> bracket_comma_quote;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
(* -> "[id1, id2, ..., idn]" *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
val stgorids =  list_of1 (stg || id);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   194
val sort =    id >> (bracket o quote)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
           || "{" $$-- (ids || emptyl) --$$ "}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
(* -> "[id]"
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   197
   -> "[id1, ..., idn]"  *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
val infxl = "infixl" $$-- !! nat
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
and infxr = "infixr" $$-- !! nat
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
(*------------------- CLASSES PARSER ----------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   208
val class  =  (id >> quote) -- ( "<" $$-- (!! ids)  ||  emptyl)   >> pair;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(* -> "(id, [id1, ..., idn])"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
   ||
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
   -> "(id, [])"  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
val classes =  "classes" $$-- !!(repeat1 class) >> bracket_comma
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
            || emptyl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   219
(* "[(id, [..]), ..., (id, [...])]" *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
(*------------------- DEFAULT PARSER ---------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
val default =  "default" $$-- !!sort
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
           ||  emptyl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
(* -> "[]"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
   -> "[id]"
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   231
   -> "[id1, ..., idn]"  *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
(*-------------------- TYPES  PARSER  ----------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
val type_decl =  stgorids -- nat;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val tyinfix =  infxl  >> (Some o TInfixl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
            || infxr  >> (Some o TInfixr);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
val type_infix =   "(" $$-- !! (tyinfix --$$ ")")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
               || empty                           >> K None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
val types =  "types" $$--
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
                !! (repeat1 (type_decl -- type_infix >> mk_type_decl))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
                >> (split_decls o flat)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
          || empty >> (K ("[]", []));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
  (* ==> ("[(id, nat), ... ]", [strg, ...]) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
(*-------------------- ARITIES PARSER ----------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
val sorts =  list_of sort >> bracket_comma;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(* -> "[[id1, ...], ..., [id, ...]]" *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   262
val arity =  id                           >> (fn s => pair("[]", quote s))
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   263
          || "(" $$-- sorts --$$")" -- id >> (fn (l, s) => pair(l, quote s));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   265
(* -> "([], id)"
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   266
   -> "([[id, ..], ..., [id, ..]], id)" *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   268
val tys = stgorids >> bracket_comma_quote;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val arities =  "arities" $$-- !! (repeat1 (tys --$$ "::" -- arity >> pair))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
               >> bracket_comma
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
            || emptyl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   274
(* -> "[([id, ..], ([[id, ...], ...], id))]" *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
(*--------------------- CONSTS PARSER ---------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
val natlist = "[" $$--  !!(list_of nat --$$ "]") >> bracket_comma
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   280
            || empty                             >> K "[]";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
  (* "[nat, ...]"  || "[]" *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
val prio_opt =  natlist -- nat  >> Some
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
             || empty           >> K None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
val mfix =  stg -- !! prio_opt            >> delim_mix
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
         || infxl                         >> Infixl
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
         || infxr                         >> Infixr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
         || "binder" $$-- !!(stg -- nat)  >> Binder
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
val const_decl = stgorids -- !! ("::" $$-- stg);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
(*("[exid, ...]", stg)  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
val mixfix =  "(" $$-- !! (mfix --$$ ")")  >> Some
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
           || empty                        >> K None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(* (s, e, l, n) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
val consts = "consts" $$--
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
                 !! (repeat1 (const_decl -- mixfix >> mk_mixfix))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
                 >> (split_decls o flat)
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   308
           || empty >> K ("[]", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
(* ("[([exid, ...], stg), ....]", [strg, ..])  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
(*---------------- TRANSLATIONS PARSER --------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   315
val xpat = "(" $$-- id --$$ ")" -- stg >> pair_quote
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   316
         || stg >> (fn s => pair_quote ("logic", s));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val arrow = $$ "=>" >> K " |-> "
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
         || $$ "<=" >> K " <-| "
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
         || $$ "==" >> K " <-> ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
val xrule = xpat -- !! (arrow -- xpat) >> (fn (xp1, (a, xp2)) => xp1 ^ a ^ xp2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
val translations = "translations" $$-- !! (repeat1 xrule)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
                 || empty;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
(*------------------- RULES PARSER -----------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
val rules  = "rules" $$-- !! (repeat1 (id -- !! stg) >> mk_rules)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
           || emptyl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
(* "[(id, stg), ...]" *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   335
(*----------------------- BASE PARSER -------------------------*)
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   336
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   337
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   338
fun base toks =
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   339
  let fun make_thy (b, toks) = (Thy b, toks);
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   340
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   341
      fun make_file (b, toks) = (File b, toks);
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   342
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   343
      val (b, toks) = make_thy (id toks)
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   344
                      handle _ => make_file (stg toks)
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   345
  in (b, toks) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
(*----------------------- ML_TEXT -------------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
20
e6fb60365db9 Pure/Thy/syntax.ML
wenzelm
parents: 0
diff changeset
   350
val mltxt =  txt || empty >> K "";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
(*---------------------------------------------------------*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
val extension = "+" $$-- !! (classes -- default -- types -- arities
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
                             -- consts -- translations -- rules --$$ "end" -- mltxt)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
                       >> (Some o mk_extension)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
              || empty >> K None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 74
diff changeset
   361
val bases = base -- repeat("+" $$-- base) >> op:: ;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
val theoryDef = !!(id --$$ "=" -- (bases >> merge) -- extension)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
                >> mk_structure;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
val read = reader theoryDef
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369