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