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