added 'subclass' section;
authorwenzelm
Thu Jun 16 12:07:40 1994 +0200 (1994-06-16)
changeset 425c42f384c89de
parent 424 f9d7e4fe141a
child 426 767367131b47
added 'subclass' section;
minor internal cleanups;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Jun 16 12:06:56 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Jun 16 12:07:40 1994 +0200
     1.3 @@ -3,10 +3,6 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  The parser for theory files.
     1.7 -
     1.8 -TODO:
     1.9 -  remove quote in syn_err (?)
    1.10 -  check: names vs names1
    1.11  *)
    1.12  
    1.13  infix 5 -- --$$ $$-- ^^;
    1.14 @@ -233,7 +229,7 @@
    1.15    \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.16  
    1.17  
    1.18 -val old_type_decl = names -- nat -- opt_infix >> mk_old_type_decl;
    1.19 +val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
    1.20  
    1.21  val type_args =
    1.22    type_var >> (fn x => [x]) ||
    1.23 @@ -310,16 +306,15 @@
    1.24  
    1.25  (* sigclass *)
    1.26  
    1.27 -fun mk_sigclass_decl ((c, cs), consts) = 
    1.28 +fun mk_sigclass_decl ((c, cs), consts) =
    1.29    (mk_pair (c, cs) ^ "\n" ^ consts, [strip_quotes c ^ "I"]);
    1.30  
    1.31  val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl;
    1.32  
    1.33  
    1.34 -(* instance *)
    1.35 +(* subclass, instance *)
    1.36  
    1.37 -fun mk_instance_decl ((((t, ss), c), axths), opt_tac) =
    1.38 -  mk_triple (t, ss, c) ^ "\n" ^
    1.39 +fun mk_witness (axths, opt_tac) =
    1.40    mk_list (keyfilter axths false) ^ "\n" ^
    1.41    mk_list (keyfilter axths true) ^ "\n" ^
    1.42    opt_tac;
    1.43 @@ -328,11 +323,19 @@
    1.44    string >> rpair false ||
    1.45    long_id >> rpair true;
    1.46  
    1.47 -val instance_decl =
    1.48 -  name --$$ "::" -- optional ("(" $$-- sort_list1 --$$")") "[]" -- name --
    1.49 +val opt_witness =
    1.50    optional ("(" $$-- list1 axm_or_thm --$$ ")") [] --
    1.51    optional (verbatim >> (pars o cat "Some" o pars)) "None"
    1.52 -  >> mk_instance_decl;
    1.53 +  >> mk_witness;
    1.54 +
    1.55 +
    1.56 +val subclass_decl =
    1.57 +  name --$$ "<" -- name -- opt_witness
    1.58 +  >> (fn ((c1, c2), witn) => mk_pair (c1, c2) ^ "\n" ^ witn);
    1.59 +
    1.60 +val instance_decl =
    1.61 +  name --$$ "::" -- arity -- opt_witness
    1.62 +  >> (fn ((t, (ss, s)), wit) => mk_triple (t, ss, s) ^ "\n" ^ wit);
    1.63  
    1.64  
    1.65  
    1.66 @@ -342,14 +345,14 @@
    1.67    lexicon * (token list -> (string * string) * token list) Symtab.table;
    1.68  
    1.69  fun make_syntax keywords sects =
    1.70 -  (make_lexicon keywords, Symtab.make sects handle Symtab.DUPS names
    1.71 -    => error ("Duplicate sections in thy syntax: " ^ commas_quote names));
    1.72 +  (make_lexicon keywords, Symtab.make sects handle Symtab.DUPS dups
    1.73 +    => error ("Duplicate sections in thy syntax: " ^ commas_quote dups));
    1.74  
    1.75  
    1.76  (* header *)
    1.77  
    1.78  fun mk_header (thy_name, bases) =
    1.79 -  (thy_name, "(base_on " ^ mk_list bases ^ " " ^ quote thy_name ^ ")");
    1.80 +  (thy_name, "base_on " ^ mk_list bases ^ " " ^ quote thy_name);
    1.81  
    1.82  val base =
    1.83    ident >> (cat "Thy" o quote) ||
    1.84 @@ -385,13 +388,13 @@
    1.85        "structure " ^ thy_name ^ " =\n\
    1.86        \struct\n\
    1.87        \\n\
    1.88 -      \local\n"              ^ " open Mixfix;\n"  (* FIXME tmp *)
    1.89 +      \local\n"
    1.90        ^ trfun_defs ^ "\n\
    1.91        \in\n\
    1.92        \\n"
    1.93        ^ mltxt ^ "\n\
    1.94        \\n\
    1.95 -      \val thy = " ^ old_thys ^ "\n\n\
    1.96 +      \val thy = (" ^ old_thys ^ " true)\n\n\
    1.97        \|> add_trfuns\n"
    1.98        ^ trfun_args ^ "\n\
    1.99        \\n"
   1.100 @@ -408,7 +411,7 @@
   1.101        "structure " ^ thy_name ^ " =\n\
   1.102        \struct\n\
   1.103        \\n\
   1.104 -      \val thy = " ^ old_thys ^ ";\n\
   1.105 +      \val thy = (" ^ old_thys ^ " false);\n\
   1.106        \\n\
   1.107        \end;\n";
   1.108  
   1.109 @@ -437,8 +440,8 @@
   1.110  val pure_keywords =
   1.111   ["classes", "default", "types", "arities", "consts", "syntax",
   1.112    "translations", "MLtrans", "MLtext", "rules", "defns", "axclass",
   1.113 -  "sigclass", "instance", "end", "ML", "mixfix", "infixr", "infixl",
   1.114 -  "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
   1.115 +  "sigclass", "subclass", "instance", "end", "ML", "mixfix", "infixr",
   1.116 +  "infixl", "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
   1.117    "==", "=>", "<="];
   1.118  
   1.119  val pure_sections =
   1.120 @@ -455,6 +458,7 @@
   1.121    axm_section "defns" "|> add_defns" axiom_decls,
   1.122    axm_section "axclass" "|> add_axclass" axclass_decl,
   1.123    axm_section "sigclass" "|> add_sigclass" sigclass_decl,
   1.124 +  section "subclass" "|> add_subclass" subclass_decl,
   1.125    section "instance" "|> add_instance" instance_decl];
   1.126  
   1.127