src/Pure/Thy/thy_parse.ML
changeset 558 c4092ae47210
parent 476 836cad329311
child 570 6333c181a3f7
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Aug 19 15:38:18 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Aug 19 15:38:50 1994 +0200
     1.3 @@ -3,9 +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 sigclass (?)
    1.10  *)
    1.11  
    1.12  infix 5 -- --$$ $$-- ^^;
    1.13 @@ -46,6 +43,12 @@
    1.14    val sort: token list -> string * token list
    1.15    val opt_infix: token list -> string * token list
    1.16    val opt_mixfix: token list -> string * token list
    1.17 +  val parens: string -> string
    1.18 +  val brackets: string -> string
    1.19 +  val mk_list: string list -> string
    1.20 +  val mk_big_list: string list -> string
    1.21 +  val mk_pair: string * string -> string
    1.22 +  val mk_triple: string * string * string -> string
    1.23    type syntax
    1.24    val make_syntax: string list ->
    1.25      (string * (token list -> (string * string) * token list)) list -> syntax
    1.26 @@ -79,6 +82,8 @@
    1.27  
    1.28  fun eof_err () = error "Unexpected end-of-file";
    1.29  
    1.30 +(*similar to Prolog's cut: reports any syntax error instead of
    1.31 +  backtracking through a superior ||*)
    1.32  fun !! parse toks = parse toks
    1.33    handle SYNTAX_ERROR (s1, s2, n) => error ("Syntax error on line " ^
    1.34      string_of_int n ^ ": " ^ s1 ^ " expected and " ^ s2 ^ " was found");
    1.35 @@ -149,14 +154,14 @@
    1.36  
    1.37  fun cat s1 s2 = s1 ^ " " ^ s2;
    1.38  
    1.39 -val pars = parents "(" ")";
    1.40 -val brackets = parents "[" "]";
    1.41 +val parens = enclose "(" ")";
    1.42 +val brackets = enclose "[" "]";
    1.43  
    1.44  val mk_list = brackets o commas;
    1.45  val mk_big_list = brackets o space_implode ",\n ";
    1.46  
    1.47 -fun mk_pair (x, y) = pars (commas [x, y]);
    1.48 -fun mk_triple (x, y, z) = pars (commas [x, y, z]);
    1.49 +fun mk_pair (x, y) = parens (commas [x, y]);
    1.50 +fun mk_triple (x, y, z) = parens (commas [x, y, z]);
    1.51  fun mk_triple1 ((x, y), z) = mk_triple (x, y, z);
    1.52  fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
    1.53  
    1.54 @@ -177,11 +182,9 @@
    1.55  
    1.56  (* classes *)
    1.57  
    1.58 -fun mk_subclass (c, cs) = mk_triple ("[]", c, cs);
    1.59 -
    1.60  val subclass = name -- optional ("<" $$-- !! name_list1) "[]";
    1.61  
    1.62 -val class_decls = repeat1 (subclass >> mk_subclass) >> mk_big_list;
    1.63 +val class_decls = repeat1 (subclass >> mk_pair) >> mk_big_list;
    1.64  
    1.65  
    1.66  (* arities *)
    1.67 @@ -211,9 +214,7 @@
    1.68  val mixfix = string -- !! (opt_pris -- optional nat "max_pri")
    1.69    >> (cat "Mixfix" o mk_triple2);
    1.70  
    1.71 -fun opt_syn fx =
    1.72 -  "(" $$-- fx --$$ ")" ||
    1.73 -  empty >> K "NoSyn";
    1.74 +fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "NoSyn";
    1.75  
    1.76  val opt_infix = opt_syn (infxl || infxr);
    1.77  val opt_mixfix = opt_syn (mixfix || infxl || infxr || binder);
    1.78 @@ -227,7 +228,7 @@
    1.79  fun mk_type_decl (((xs, t), None), syn) =
    1.80        [(mk_triple (t, string_of_int (length xs), syn), false)]
    1.81    | mk_type_decl (((xs, t), Some rhs), syn) =
    1.82 -      [(pars (commas [t, mk_list xs, rhs, syn]), true)];
    1.83 +      [(parens (commas [t, mk_list xs, rhs, syn]), true)];
    1.84  
    1.85  fun mk_type_decls tys =
    1.86    "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.87 @@ -309,14 +310,6 @@
    1.88  val axclass_decl = subclass -- repeat (ident -- !! string) >> mk_axclass_decl;
    1.89  
    1.90  
    1.91 -(* sigclass *)
    1.92 -
    1.93 -fun mk_sigclass_decl ((c, cs), consts) =
    1.94 -  (mk_pair (c, cs) ^ "\n" ^ consts, [strip_quotes c ^ "I"]);
    1.95 -
    1.96 -val sigclass_decl = subclass -- optional const_decls "[]" >> mk_sigclass_decl;
    1.97 -
    1.98 -
    1.99  (* instance *)
   1.100  
   1.101  fun mk_witness (axths, opt_tac) =
   1.102 @@ -331,7 +324,7 @@
   1.103  
   1.104  val opt_witness =
   1.105    optional ("(" $$-- list1 axm_or_thm --$$ ")") [] --
   1.106 -  optional (verbatim >> (pars o cat "Some" o pars)) "None"
   1.107 +  optional (verbatim >> (parens o cat "Some" o parens)) "None"
   1.108    >> mk_witness;
   1.109  
   1.110  val instance_decl =
   1.111 @@ -388,8 +381,13 @@
   1.112  
   1.113  (* theory definition *)
   1.114  
   1.115 -fun mk_structure tname ((thy_name, old_thys), Some (extxt, postxt, mltxt)) =
   1.116 -      if (thy_name = tname) then
   1.117 +fun mk_structure tname ((thy_name, old_thys), opt_txts) =
   1.118 +  if thy_name <> tname then
   1.119 +    error ("Filename \"" ^ tname ^ ".thy\" and theory name "
   1.120 +      ^ quote thy_name ^ " are different")
   1.121 +  else
   1.122 +    (case opt_txts of
   1.123 +      Some (extxt, postxt, mltxt) =>
   1.124          "structure " ^ thy_name ^ " =\n\
   1.125          \struct\n\
   1.126          \\n\
   1.127 @@ -412,18 +410,13 @@
   1.128          \\n\
   1.129          \end;\n\
   1.130          \end;\n"
   1.131 -      else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \""
   1.132 -                  ^ thy_name ^ "\" are different")
   1.133 -  | mk_structure tname ((thy_name, old_thys), None) =
   1.134 -      if (thy_name = tname) then
   1.135 +    | None =>
   1.136          "structure " ^ thy_name ^ " =\n\
   1.137          \struct\n\
   1.138          \\n\
   1.139          \val thy = (" ^ old_thys ^ " false);\n\
   1.140          \\n\
   1.141 -        \end;\n"
   1.142 -      else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \""
   1.143 -                  ^ thy_name ^ "\" are different");
   1.144 +        \end;\n");
   1.145  
   1.146  fun theory_defn sectab tname =
   1.147    header -- optional (extension sectab >> Some) None -- eof
   1.148 @@ -462,9 +455,8 @@
   1.149    section "MLtrans" "|> add_trfuns" mltrans,
   1.150    ("MLtext", verbatim >> rpair ""),
   1.151    axm_section "rules" "|> add_axioms" axiom_decls,
   1.152 -  axm_section "defns" "|> add_defns" axiom_decls,
   1.153 +  axm_section "defs" "|> add_defs" axiom_decls,
   1.154    axm_section "axclass" "|> add_axclass" axclass_decl,
   1.155 -  axm_section "sigclass" "|> add_sigclass" sigclass_decl,
   1.156    ("instance", instance_decl)];
   1.157  
   1.158