moved parts of OuterParse to SpecParse;
authorwenzelm
Fri Jan 19 22:08:08 2007 +0100 (2007-01-19)
changeset 221016d13239d5f52
parent 22100 33d7468302bb
child 22102 a89ef7144729
moved parts of OuterParse to SpecParse;
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/old_inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/HOLCF/fixrec_package.ML
src/Pure/ProofGeneral/parsing.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/invoke.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:07 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:08 2007 +0100
     1.3 @@ -426,7 +426,7 @@
     1.4      (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
     1.5  
     1.6  val primrec_decl =
     1.7 -  options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
     1.8 +  options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
     1.9  
    1.10  val primrecP =
    1.11    OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:07 2007 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:08 2007 +0100
     2.3 @@ -1030,9 +1030,9 @@
     2.4  
     2.5  val rep_datatype_decl =
     2.6    Scan.option (Scan.repeat1 P.name) --
     2.7 -    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
     2.8 -    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
     2.9 -    (P.$$$ "induction" |-- P.!!! P.xthm);
    2.10 +    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
    2.11 +    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
    2.12 +    (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
    2.13  
    2.14  fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
    2.15  
     3.1 --- a/src/HOL/Tools/old_inductive_package.ML	Fri Jan 19 22:08:07 2007 +0100
     3.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Fri Jan 19 22:08:08 2007 +0100
     3.3 @@ -888,8 +888,8 @@
     3.4  fun ind_decl coind =
     3.5    Scan.repeat1 P.term --
     3.6    (P.$$$ "intros" |--
     3.7 -    P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
     3.8 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
     3.9 +    P.!!! (Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop))) --
    3.10 +  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
    3.11    >> (Toplevel.theory o mk_ind coind);
    3.12  
    3.13  val inductiveP =
    3.14 @@ -900,7 +900,7 @@
    3.15  
    3.16  
    3.17  val ind_cases =
    3.18 -  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    3.19 +  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
    3.20    >> (Toplevel.theory o inductive_cases);
    3.21  
    3.22  val inductive_casesP =
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jan 19 22:08:07 2007 +0100
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Jan 19 22:08:08 2007 +0100
     4.3 @@ -321,7 +321,7 @@
     4.4        P.name >> pair false) --| P.$$$ ")")) (false, "");
     4.5  
     4.6  val primrec_decl =
     4.7 -  opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
     4.8 +  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
     4.9  
    4.10  val primrecP =
    4.11    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
     5.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 19 22:08:07 2007 +0100
     5.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jan 19 22:08:08 2007 +0100
     5.3 @@ -314,7 +314,7 @@
     5.4  
     5.5  val recdef_decl =
     5.6    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
     5.7 -  P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints
     5.8 +  P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
     5.9    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    5.10  
    5.11  val recdefP =
    5.12 @@ -324,7 +324,7 @@
    5.13  
    5.14  val defer_recdef_decl =
    5.15    P.name -- Scan.repeat1 P.prop --
    5.16 -  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
    5.17 +  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
    5.18    >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
    5.19  
    5.20  val defer_recdefP =
    5.21 @@ -333,8 +333,8 @@
    5.22  
    5.23  val recdef_tcP =
    5.24    OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
    5.25 -    (P.opt_locale_target --
    5.26 -      P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    5.27 +    (P.opt_target --
    5.28 +      SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    5.29        >> (fn (((loc, thm_name), name), i) =>
    5.30          Toplevel.print o Toplevel.local_theory_to_proof loc (recdef_tc thm_name name i)));
    5.31  
     6.1 --- a/src/HOL/Tools/specification_package.ML	Fri Jan 19 22:08:07 2007 +0100
     6.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Jan 19 22:08:08 2007 +0100
     6.3 @@ -241,7 +241,7 @@
     6.4  
     6.5  val specification_decl =
     6.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
     6.7 -          Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
     6.8 +          Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
     6.9  
    6.10  val specificationP =
    6.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    6.12 @@ -252,7 +252,7 @@
    6.13  val ax_specification_decl =
    6.14      P.name --
    6.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    6.16 -           Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
    6.17 +           Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
    6.18  
    6.19  val ax_specificationP =
    6.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
     7.1 --- a/src/HOLCF/fixrec_package.ML	Fri Jan 19 22:08:07 2007 +0100
     7.2 +++ b/src/HOLCF/fixrec_package.ML	Fri Jan 19 22:08:08 2007 +0100
     7.3 @@ -291,7 +291,7 @@
     7.4  
     7.5  local structure P = OuterParse and K = OuterKeyword in
     7.6  
     7.7 -val fixrec_eqn = P.opt_thm_name ":" -- P.prop;
     7.8 +val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop;
     7.9  
    7.10  val fixrec_strict = P.opt_keyword "permissive" >> not;
    7.11  
    7.12 @@ -304,7 +304,7 @@
    7.13      (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
    7.14  
    7.15  (* fixpat parser *)
    7.16 -val fixpat_decl = P.opt_thm_name ":" -- Scan.repeat1 P.prop;
    7.17 +val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
    7.18  
    7.19  val fixpatP =
    7.20    OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
     8.1 --- a/src/Pure/ProofGeneral/parsing.ML	Fri Jan 19 22:08:07 2007 +0100
     8.2 +++ b/src/Pure/ProofGeneral/parsing.ML	Fri Jan 19 22:08:08 2007 +0100
     8.3 @@ -129,8 +129,8 @@
     8.4  
     8.5              val thmnameP = (* see isar_syn.ML/theoremsP *)
     8.6                  let
     8.7 -                    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
     8.8 -                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
     8.9 +                    val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1)
    8.10 +                    val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x)
    8.11                  in
    8.12                      theoremsP
    8.13                  end
    8.14 @@ -150,8 +150,8 @@
    8.15                     | "classes"   => named_item P.name "class"
    8.16                     | "classrel"  => named_item P.name "class"
    8.17                     | "consts"    => named_item (P.const >> #1) "term"
    8.18 -                   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
    8.19 -                   | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
    8.20 +                   | "axioms"    => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem"
    8.21 +                   | "defs"      => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem"
    8.22                     | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
    8.23                     | "theorems"  => named_item thmnameP "thmset"
    8.24                     | "lemmas"    => named_item thmnameP "thmset"
    8.25 @@ -164,17 +164,17 @@
    8.26      fun xmls_of_thy_goal (name,toks,str) =
    8.27          let
    8.28              (* see isar_syn.ML/gen_theorem *)
    8.29 -         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
    8.30 +         val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp);
    8.31           val general_statement =
    8.32 -            statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
    8.33 +            statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement);
    8.34  
    8.35              val gen_theoremP =
    8.36 -                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
    8.37 -                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
    8.38 +                P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
    8.39 +                 Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) --
    8.40                                   general_statement >> (fn ((locale, a), (elems, concl)) =>
    8.41                                                           fst a) (* a : (bstring * Args.src list) *)
    8.42  
    8.43 -            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
    8.44 +            val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "")
    8.45  	    val thmname = nameparse "opengoal" "theorem" nameP toks
    8.46          in
    8.47              [D.Opengoal {thmname=SOME thmname, text=str},
     9.1 --- a/src/Pure/Tools/class_package.ML	Fri Jan 19 22:08:07 2007 +0100
     9.2 +++ b/src/Pure/Tools/class_package.ML	Fri Jan 19 22:08:08 2007 +0100
     9.3 @@ -560,7 +560,7 @@
     9.4  val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
     9.5  
     9.6  val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
     9.7 -val class_bodyP = P.!!! (Scan.repeat1 P.locale_element);
     9.8 +val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
     9.9  
    9.10  val parse_arity =
    9.11    (P.xname --| P.$$$ "::" -- P.!!! P.arity)
    9.12 @@ -582,7 +582,7 @@
    9.13    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    9.14        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    9.15             >> instance_sort_e
    9.16 -      || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
    9.17 +      || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    9.18             >> (fn (arities, defs) => instance_arity_e arities defs)
    9.19      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    9.20  
    10.1 --- a/src/Pure/Tools/invoke.ML	Fri Jan 19 22:08:07 2007 +0100
    10.2 +++ b/src/Pure/Tools/invoke.ML	Fri Jan 19 22:08:08 2007 +0100
    10.3 @@ -119,7 +119,7 @@
    10.4    OuterSyntax.command "invoke"
    10.5      "schematic invocation of locale expression in proof context"
    10.6      (K.tag_proof K.prf_goal)
    10.7 -    (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes
    10.8 +    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
    10.9        >> (fn (((name, expr), insts), fixes) =>
   10.10            Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
   10.11  
    11.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Jan 19 22:08:07 2007 +0100
    11.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Jan 19 22:08:08 2007 +0100
    11.3 @@ -417,9 +417,9 @@
    11.4  val datatype_decl =
    11.5    (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
    11.6    P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
    11.7 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
    11.8 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
    11.9 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
   11.10 +  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
   11.11 +  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
   11.12 +  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   11.13    >> (Toplevel.theory o mk_datatype);
   11.14  
   11.15  val coind_prefix = if coind then "co" else "";
    12.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jan 19 22:08:07 2007 +0100
    12.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 19 22:08:08 2007 +0100
    12.3 @@ -82,7 +82,7 @@
    12.4  local structure P = OuterParse and K = OuterKeyword in
    12.5  
    12.6  val ind_cases =
    12.7 -  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    12.8 +  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
    12.9    >> (Toplevel.theory o inductive_cases);
   12.10  
   12.11  val inductive_casesP =
    13.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Jan 19 22:08:07 2007 +0100
    13.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Jan 19 22:08:08 2007 +0100
    13.3 @@ -199,10 +199,10 @@
    13.4  local structure P = OuterParse and K = OuterKeyword in
    13.5  
    13.6  val rep_datatype_decl =
    13.7 -  (P.$$$ "elimination" |-- P.!!! P.xthm) --
    13.8 -  (P.$$$ "induction" |-- P.!!! P.xthm) --
    13.9 -  (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
   13.10 -  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
   13.11 +  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
   13.12 +  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
   13.13 +  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
   13.14 +  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
   13.15    >> (fn (((x, y), z), w) => rep_datatype x y z w);
   13.16  
   13.17  val rep_datatypeP =
    14.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jan 19 22:08:07 2007 +0100
    14.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 19 22:08:08 2007 +0100
    14.3 @@ -590,11 +590,11 @@
    14.4    (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
    14.5        ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
    14.6    (P.$$$ "intros" |--
    14.7 -    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
    14.8 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
    14.9 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] --
   14.10 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
   14.11 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
   14.12 +    P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
   14.13 +  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
   14.14 +  Scan.optional (P.$$$ "con_defs" |-- P.!!! SpecParse.xthms1) [] --
   14.15 +  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
   14.16 +  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   14.17    >> (Toplevel.theory o mk_ind);
   14.18  
   14.19  val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
    15.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Jan 19 22:08:07 2007 +0100
    15.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Jan 19 22:08:08 2007 +0100
    15.3 @@ -205,7 +205,7 @@
    15.4  
    15.5  local structure P = OuterParse and K = OuterKeyword in
    15.6  
    15.7 -val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
    15.8 +val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
    15.9  
   15.10  val primrecP =
   15.11    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl