src/Pure/Thy/thy_parse.ML
changeset 451 9ebdead316e0
parent 425 c42f384c89de
child 476 836cad329311
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Jul 06 12:51:27 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Jul 06 14:39:32 1994 +0200
     1.3 @@ -3,6 +3,9 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  The parser for theory files.
     1.7 +
     1.8 +TODO:
     1.9 +  remove sigclass (?)
    1.10  *)
    1.11  
    1.12  infix 5 -- --$$ $$-- ^^;
    1.13 @@ -41,6 +44,8 @@
    1.14      -> token list -> 'a list * token list
    1.15    val name: token list -> string * token list
    1.16    val sort: token list -> string * token list
    1.17 +  val opt_infix: token list -> string * token list
    1.18 +  val opt_mixfix: token list -> string * token list
    1.19    type syntax
    1.20    val make_syntax: string list ->
    1.21      (string * (token list -> (string * string) * token list)) list -> syntax
    1.22 @@ -312,7 +317,7 @@
    1.23  val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl;
    1.24  
    1.25  
    1.26 -(* subclass, instance *)
    1.27 +(* instance *)
    1.28  
    1.29  fun mk_witness (axths, opt_tac) =
    1.30    mk_list (keyfilter axths false) ^ "\n" ^
    1.31 @@ -323,19 +328,17 @@
    1.32    string >> rpair false ||
    1.33    long_id >> rpair true;
    1.34  
    1.35 +
    1.36  val opt_witness =
    1.37    optional ("(" $$-- list1 axm_or_thm --$$ ")") [] --
    1.38    optional (verbatim >> (pars o cat "Some" o pars)) "None"
    1.39    >> mk_witness;
    1.40  
    1.41 -
    1.42 -val subclass_decl =
    1.43 -  name --$$ "<" -- name -- opt_witness
    1.44 -  >> (fn ((c1, c2), witn) => mk_pair (c1, c2) ^ "\n" ^ witn);
    1.45 -
    1.46  val instance_decl =
    1.47 -  name --$$ "::" -- arity -- opt_witness
    1.48 -  >> (fn ((t, (ss, s)), wit) => mk_triple (t, ss, s) ^ "\n" ^ wit);
    1.49 +  (name --$$ "<" -- name >> (pair "|> add_inst_subclass" o mk_pair) ||
    1.50 +    name --$$ "::" -- arity >> (pair "|> add_inst_arity" o mk_triple2))
    1.51 +  -- opt_witness
    1.52 +  >> (fn ((x, y), z) => (cat_lines [x, y, z], ""));
    1.53  
    1.54  
    1.55  
    1.56 @@ -345,8 +348,9 @@
    1.57    lexicon * (token list -> (string * string) * token list) Symtab.table;
    1.58  
    1.59  fun make_syntax keywords sects =
    1.60 -  (make_lexicon keywords, Symtab.make sects handle Symtab.DUPS dups
    1.61 -    => error ("Duplicate sections in thy syntax: " ^ commas_quote dups));
    1.62 +  (make_lexicon (map fst sects @ keywords),
    1.63 +    Symtab.make sects handle Symtab.DUPS dups =>
    1.64 +      error ("Duplicate sections in theory file syntax: " ^ commas_quote dups));
    1.65  
    1.66  
    1.67  (* header *)
    1.68 @@ -438,11 +442,8 @@
    1.69  
    1.70  
    1.71  val pure_keywords =
    1.72 - ["classes", "default", "types", "arities", "consts", "syntax",
    1.73 -  "translations", "MLtrans", "MLtext", "rules", "defns", "axclass",
    1.74 -  "sigclass", "subclass", "instance", "end", "ML", "mixfix", "infixr",
    1.75 -  "infixl", "binder", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
    1.76 -  "==", "=>", "<="];
    1.77 + ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<",
    1.78 +   "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.79  
    1.80  val pure_sections =
    1.81   [section "classes" "|> add_classes" class_decls,
    1.82 @@ -458,8 +459,7 @@
    1.83    axm_section "defns" "|> add_defns" axiom_decls,
    1.84    axm_section "axclass" "|> add_axclass" axclass_decl,
    1.85    axm_section "sigclass" "|> add_sigclass" sigclass_decl,
    1.86 -  section "subclass" "|> add_subclass" subclass_decl,
    1.87 -  section "instance" "|> add_instance" instance_decl];
    1.88 +  ("instance", instance_decl)];
    1.89  
    1.90  
    1.91  end;