--- a/NEWS Sat Oct 06 16:41:22 2007 +0200
+++ b/NEWS Sat Oct 06 16:50:04 2007 +0200
@@ -1337,6 +1337,11 @@
quasi-functional intermediate checkpoint, both in interactive and
batch mode.
+* Isar: simplified interfaces for outer syntax. Renamed
+OuterSyntax.add_keywords to OuterSyntax.keywords. Removed
+OuterSyntax.add_parsers -- this functionality is now included in
+OuterSyntax.command etc. INCOMPATIBILITY.
+
* Simplifier: the simpset of a running simplification process now
contains a proof context (cf. Simplifier.the_context), which is the
very context that the initial simpset has been retrieved from (by
--- a/src/HOL/Import/import_syntax.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML Sat Oct 06 16:50:04 2007 +0200
@@ -5,7 +5,7 @@
signature HOL4_IMPORT_SYNTAX =
sig
- type token = OuterSyntax.token
+ type token = OuterLex.token
type command = token list -> (theory -> theory) * token list
val import_segment: token list -> (theory -> theory) * token list
@@ -32,7 +32,7 @@
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
struct
-type token = OuterSyntax.token
+type token = OuterLex.token
type command = token list -> (theory -> theory) * token list
local structure P = OuterParse and K = OuterKeyword in
@@ -222,61 +222,59 @@
fun fl_dump toks = Scan.succeed flush_dump toks
val append_dump = (P.verbatim || P.string) >> add_dump
-val parsers =
- [OuterSyntax.command "import_segment"
+fun setup () =
+ (OuterSyntax.keywords[">"];
+ OuterSyntax.command "import_segment"
"Set import segment name"
- K.thy_decl (import_segment >> Toplevel.theory),
+ K.thy_decl (import_segment >> Toplevel.theory);
OuterSyntax.command "import_theory"
"Set default HOL4 theory name"
- K.thy_decl (import_theory >> Toplevel.theory),
+ K.thy_decl (import_theory >> Toplevel.theory);
OuterSyntax.command "end_import"
"End HOL4 import"
- K.thy_decl (end_import >> Toplevel.theory),
+ K.thy_decl (end_import >> Toplevel.theory);
OuterSyntax.command "skip_import_dir"
"Sets caching directory for skipping importing"
- K.thy_decl (skip_import_dir >> Toplevel.theory),
+ K.thy_decl (skip_import_dir >> Toplevel.theory);
OuterSyntax.command "skip_import"
"Switches skipping importing on or off"
- K.thy_decl (skip_import >> Toplevel.theory),
+ K.thy_decl (skip_import >> Toplevel.theory);
OuterSyntax.command "setup_theory"
"Setup HOL4 theory replaying"
- K.thy_decl (setup_theory >> Toplevel.theory),
+ K.thy_decl (setup_theory >> Toplevel.theory);
OuterSyntax.command "end_setup"
"End HOL4 setup"
- K.thy_decl (end_setup >> Toplevel.theory),
+ K.thy_decl (end_setup >> Toplevel.theory);
OuterSyntax.command "setup_dump"
"Setup the dump file name"
- K.thy_decl (set_dump >> Toplevel.theory),
+ K.thy_decl (set_dump >> Toplevel.theory);
OuterSyntax.command "append_dump"
"Add text to dump file"
- K.thy_decl (append_dump >> Toplevel.theory),
+ K.thy_decl (append_dump >> Toplevel.theory);
OuterSyntax.command "flush_dump"
"Write the dump to file"
- K.thy_decl (fl_dump >> Toplevel.theory),
+ K.thy_decl (fl_dump >> Toplevel.theory);
OuterSyntax.command "ignore_thms"
"Theorems to ignore in next HOL4 theory import"
- K.thy_decl (ignore_thms >> Toplevel.theory),
+ K.thy_decl (ignore_thms >> Toplevel.theory);
OuterSyntax.command "type_maps"
"Map HOL4 type names to existing Isabelle/HOL type names"
- K.thy_decl (type_maps >> Toplevel.theory),
+ K.thy_decl (type_maps >> Toplevel.theory);
OuterSyntax.command "def_maps"
"Map HOL4 constant names to their primitive definitions"
- K.thy_decl (def_maps >> Toplevel.theory),
+ K.thy_decl (def_maps >> Toplevel.theory);
OuterSyntax.command "thm_maps"
"Map HOL4 theorem names to existing Isabelle/HOL theorem names"
- K.thy_decl (thm_maps >> Toplevel.theory),
+ K.thy_decl (thm_maps >> Toplevel.theory);
OuterSyntax.command "const_renames"
"Rename HOL4 const names"
- K.thy_decl (const_renames >> Toplevel.theory),
+ K.thy_decl (const_renames >> Toplevel.theory);
OuterSyntax.command "const_moves"
"Rename HOL4 const names to other HOL4 constants"
- K.thy_decl (const_moves >> Toplevel.theory),
+ K.thy_decl (const_moves >> Toplevel.theory);
OuterSyntax.command "const_maps"
"Map HOL4 const names to existing Isabelle/HOL const names"
- K.thy_decl (const_maps >> Toplevel.theory)]
-
-fun setup () = (OuterSyntax.add_keywords[">"];
- OuterSyntax.add_parsers parsers)
+ K.thy_decl (const_maps >> Toplevel.theory));
end
--- a/src/HOL/Library/Eval.thy Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Library/Eval.thy Sat Oct 06 16:50:04 2007 +0200
@@ -213,14 +213,11 @@
*}
ML {*
-val valueP =
OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
(Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
-- OuterParse.term
>> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
(Eval.evaluate_cmd some_name t)));
-
-val _ = OuterSyntax.add_parsers [valueP];
*}
end
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Oct 06 16:50:04 2007 +0200
@@ -947,10 +947,8 @@
(* syntax und parsing *)
structure P = OuterParse and K = OuterKeyword;
-val atom_declP =
+val _ =
OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
(Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
-val _ = OuterSyntax.add_parsers [atom_declP];
-
end;
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:50:04 2007 +0200
@@ -511,22 +511,21 @@
local structure P = OuterParse and K = OuterKeyword in
-val nominal_inductiveP =
+val _ = OuterSyntax.keywords ["avoids"];
+
+val _ =
OuterSyntax.command "nominal_inductive"
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
(P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
(P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
-val equivarianceP =
+val _ =
OuterSyntax.command "equivariance"
"prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
(P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
(fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
-val _ = OuterSyntax.add_keywords ["avoids"];
-val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
-
end;
end
--- a/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -2094,12 +2094,10 @@
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in add_nominal_datatype false names specs end;
-val nominal_datatypeP =
+val _ =
OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
(P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
-val _ = OuterSyntax.add_parsers [nominal_datatypeP];
-
end;
end
--- a/src/HOL/Nominal/nominal_primrec.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Sat Oct 06 16:50:04 2007 +0200
@@ -416,6 +416,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["invariant", "freshness_context"];
+
val parser1 = P.$$$ "freshness_context" |-- P.$$$ ":" |-- (P.term >> SOME);
val parser2 =
P.$$$ "invariant" |-- P.$$$ ":" |--
@@ -434,16 +436,13 @@
val primrec_decl =
options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-val primrecP =
+val _ =
OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
(primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
Toplevel.print o Toplevel.theory_to_proof
((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
(map P.triple_swap eqns))));
-val _ = OuterSyntax.add_parsers [primrecP];
-val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
-
end;
--- a/src/HOL/Orderings.thy Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Orderings.thy Sat Oct 06 16:50:04 2007 +0200
@@ -346,7 +346,7 @@
(Context.cases (print_structures o ProofContext.init) print_structures)
(print_structures o Proof.context_of));
-val printP =
+val _ =
OuterSyntax.improper_command "print_orders"
"print order structures available to transitivity reasoner" OuterKeyword.diag
(Scan.succeed (Toplevel.no_timing o print));
@@ -354,11 +354,10 @@
(** Setup **)
-val setup = let val _ = OuterSyntax.add_parsers [printP] in
- Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
- "normalisation of algebraic structure")] #>
- Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
- end;
+val setup =
+ Method.add_methods
+ [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+ Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
end;
--- a/src/HOL/Tools/datatype_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -908,6 +908,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
+
val datatype_decl =
Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
(P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
@@ -919,7 +921,7 @@
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in snd o add_datatype false names specs end;
-val datatypeP =
+val _ =
OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
(P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
@@ -932,14 +934,10 @@
fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
-val rep_datatypeP =
+val _ =
OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
(rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
-
-val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
-val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
-
end;
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Oct 06 16:50:04 2007 +0200
@@ -302,13 +302,12 @@
|> by_pat_completeness_simp
|> termination_by_lexicographic_order
-val funP =
+val _ =
OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
(fundef_parser fun_config
>> (fn ((config, fixes), (flags, statements)) =>
(Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
-val _ = OuterSyntax.add_parsers [funP];
end
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -268,24 +268,22 @@
local structure P = OuterParse and K = OuterKeyword in
-val functionP =
+val _ = OuterSyntax.keywords ["sequential", "otherwise"];
+
+val _ =
OuterSyntax.command "function" "define general recursive functions" K.thy_goal
(fundef_parser default_config
>> (fn ((config, fixes), (flags, statements)) =>
Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
#> Toplevel.print));
-val terminationP =
+val _ =
OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
(P.opt_target -- Scan.option P.term
>> (fn (target, name) =>
Toplevel.print o
Toplevel.local_theory_to_proof target (setup_termination_proof name)));
-val _ = OuterSyntax.add_parsers [functionP];
-val _ = OuterSyntax.add_parsers [terminationP];
-val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
-
end;
--- a/src/HOL/Tools/inductive_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -923,6 +923,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["monos"];
+
(* FIXME tmp *)
fun flatten_specification specs = specs |> maps
(fn (a, (concl, [])) => concl |> map
@@ -945,22 +947,15 @@
val ind_decl = gen_ind_decl add_ind_def;
-val inductiveP =
- OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
-val coinductiveP =
- OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
-
-
-val inductive_casesP =
+val _ =
OuterSyntax.command "inductive_cases"
"create simplified instances of elimination rules (improper)" K.thy_script
(P.opt_target -- P.and_list1 SpecParse.spec
>> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
-val _ = OuterSyntax.add_keywords ["monos"];
-val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
-
end;
end;
--- a/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -543,14 +543,12 @@
val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
-val inductive_setP =
+val _ =
OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
-val coinductive_setP =
+val _ =
OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
-val _ = OuterSyntax.add_parsers [inductive_setP, coinductive_setP];
-
end;
end;
--- a/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -350,15 +350,13 @@
val primrec_decl =
opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-val primrecP =
+val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
(primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
Toplevel.theory (snd o
(if unchecked then add_primrec_unchecked else add_primrec) alt_name
(map P.triple_swap eqns))));
-val _ = OuterSyntax.add_parsers [primrecP];
-
end;
end;
--- a/src/HOL/Tools/recdef_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -295,6 +295,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
+
val hints =
P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
@@ -303,7 +305,7 @@
P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
-val recdefP =
+val _ =
OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
(recdef_decl >> Toplevel.theory);
@@ -313,21 +315,17 @@
Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
-val defer_recdefP =
+val _ =
OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
(defer_recdef_decl >> Toplevel.theory);
-val recdef_tcP =
+val _ =
OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
(P.opt_target --
SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn (((loc, thm_name), name), i) =>
Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
-
-val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
-val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
-
end;
end;
--- a/src/HOL/Tools/record_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -607,7 +607,7 @@
val types = map snd flds';
val (args,rest) = splitargs (map fst flds') fargs;
val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
- val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
+ val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
argtypes 0;
val varifyT = varifyT midx;
val vartypes = map varifyT types;
@@ -654,12 +654,12 @@
gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
-val parse_translation =
+val parse_translation =
[("_record_update", record_update_tr),
("_update_name", update_name_tr)];
-val adv_parse_translation =
+val adv_parse_translation =
[("_record",adv_record_tr),
("_record_scheme",adv_record_scheme_tr),
("_record_type",adv_record_type_tr),
@@ -762,7 +762,7 @@
in Syntax.term_of_typ (! Syntax.show_sorts)
(Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
- fun match rT T = (Sign.typ_match thy (varifyT rT,T)
+ fun match rT T = (Sign.typ_match thy (varifyT rT,T)
Vartab.empty);
in if !print_record_type_abbr
@@ -876,8 +876,8 @@
val f_x = Free (f',fT)$(Free (x,T'));
fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
| is_constr _ = false;
- fun subst (t as u$w) = if Free (f',fT)=u
- then if is_constr w then f_x
+ fun subst (t as u$w) = if Free (f',fT)=u
+ then if is_constr w then f_x
else raise TERM ("abstract_over_fun_app",[t])
else subst u$subst w
| subst (Abs (x,T,t)) = (Abs (x,T,subst t))
@@ -885,12 +885,12 @@
val t'' = abstract_over (f_x,subst t');
val vars = strip_qnt_vars "all" t'';
val bdy = strip_qnt_body "all" t'';
-
+
in list_abs ((x,T')::vars,bdy) end
| abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
(* Generates a theorem of the kind:
- * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
- *)
+ * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
+ *)
fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
let
val rT = domain_type fT;
@@ -900,16 +900,16 @@
fun app_bounds 0 t = t$Bound 0
| app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
-
+
val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
val prop = Logic.mk_equals
(list_all ((f,fT)::vars,
app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
list_all ((fst r,rT)::vars,
- app_bounds (n - 1) ((Free P)$Bound n)));
+ app_bounds (n - 1) ((Free P)$Bound n)));
val prove_standard = quick_and_dirty_prove true thy;
val thm = prove_standard [] prop (fn prems =>
- EVERY [rtac equal_intr_rule 1,
+ EVERY [rtac equal_intr_rule 1,
Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
in thm end
@@ -928,14 +928,14 @@
(trm as Abs _) =>
(case rec_id (~1) T of
"" => NONE
- | n => if T=T'
+ | n => if T=T'
then (let
- val P=cterm_of thy (abstract_over_fun_app trm);
+ val P=cterm_of thy (abstract_over_fun_app trm);
val thm = mk_fun_apply_eq trm thy;
val PV = cterm_of thy (hd (term_vars (prop_of thm)));
val thm' = cterm_instantiate [(PV,P)] thm;
in SOME thm' end handle TERM _ => NONE)
- else NONE)
+ else NONE)
| _ => NONE))
end
@@ -951,7 +951,7 @@
(* [thm] is the same as all_thm *)
| NONE => extsplits)
val thms'=K_comp_convs@thms;
- val ss' = (Simplifier.inherit_context ss simpset
+ val ss' = (Simplifier.inherit_context ss simpset
addsimps thms'
addsimprocs [record_split_f_more_simproc]);
in
@@ -992,8 +992,8 @@
NONE => NONE
| SOME u_name
=> if u_name = s
- then (case mk_eq_terms r of
- NONE =>
+ then (case mk_eq_terms r of
+ NONE =>
let
val rv = ("r",rT)
val rb = Bound 0
@@ -1064,7 +1064,7 @@
in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
else ((sprout,skeleton),vars);
- fun is_upd_same (sprout,skeleton) u
+ fun is_upd_same (sprout,skeleton) u
((K_rec as Const ("Record.K_record",_))$
((sel as Const (s,_))$r)) =
if (unsuffix updateN u) = s andalso (seed s sprout) = r
@@ -1074,17 +1074,17 @@
fun init_seed r = ((r,Bound 0), [("r", rT)]);
- fun add (n:string) f fmaps =
+ fun add (n:string) f fmaps =
(case AList.lookup (op =) fmaps n of
NONE => AList.update (op =) (n,[f]) fmaps
- | SOME fs => AList.update (op =) (n,f::fs) fmaps)
+ | SOME fs => AList.update (op =) (n,f::fs) fmaps)
- fun comps (n:string) T fmaps =
+ fun comps (n:string) T fmaps =
(case AList.lookup (op =) fmaps n of
- SOME fs =>
+ SOME fs =>
foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
| NONE => error ("record_upd_simproc.comps"))
-
+
(* mk_updterm returns either
* - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
* where vars are the bound variables in the skeleton
@@ -1119,7 +1119,7 @@
val kv = (n, kT);
val kb = Bound (length vars);
val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
- in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
+ in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
end)
else
(case rest (u::already) r of
@@ -1149,7 +1149,7 @@
val kv = (n, kT)
val kb = Bound (length vars)
val (sprout',vars') = grow u uT k kT (kv::vars) sprout
- val fmaps' = add n kb fmaps
+ val fmaps' = add n kb fmaps
in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
,vars',fmaps',sprout') end))
end
@@ -1161,7 +1161,7 @@
=> SOME (prove_split_simp thy ss rT
(list_all(vars,(equals rT$trm$trm'))))
| _ => NONE)
- end
+ end
| _ => NONE))
end
@@ -1625,7 +1625,7 @@
val refls = map mkrefl fields_more;
val dest_convs' = map mk_meta_eq dest_convs;
val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
-
+
val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
fun mkthm (udef,(fld_refl,thms)) =
@@ -1664,7 +1664,7 @@
val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
- val (([inject',induct',cases',surjective',split_meta'],
+ val (([inject',induct',cases',surjective',split_meta'],
[dest_convs',upd_convs']),
thm_thy) =
defs_thy
@@ -1915,7 +1915,7 @@
||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
[make_spec, fields_spec, extend_spec, truncate_spec])
- |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
+ |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
fold Code.add_default_func sel_defs
#> fold Code.add_default_func upd_defs
#> fold Code.add_default_func derived_defs
@@ -2276,12 +2276,10 @@
P.type_args -- P.name --
(P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
-val recordP =
+val _ =
OuterSyntax.command "record" "define extensible record" K.thy_decl
(record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
-val _ = OuterSyntax.add_parsers [recordP];
-
end;
end;
--- a/src/HOL/Tools/refute_isar.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/refute_isar.ML Sat Oct 06 16:50:04 2007 +0200
@@ -7,7 +7,7 @@
syntax.
*)
-structure RefuteIsar =
+structure RefuteIsar: sig end =
struct
(* ------------------------------------------------------------------------- *)
@@ -56,7 +56,7 @@
fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
- val refute_cmd = OuterSyntax.improper_command "refute"
+ val _ = OuterSyntax.improper_command "refute"
"try to find a model that refutes a given subgoal"
OuterKeyword.diag refute_parser;
@@ -101,15 +101,9 @@
fun refute_params_parser tokens =
(refute_params_scan_args tokens) |>> refute_params_trans;
- val refute_params_cmd = OuterSyntax.command "refute_params"
+ val _ = OuterSyntax.command "refute_params"
"show/store default parameters for the 'refute' command"
OuterKeyword.thy_decl refute_params_parser;
end;
-(* ------------------------------------------------------------------------- *)
-(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's *)
-(* outer syntax *)
-(* ------------------------------------------------------------------------- *)
-
-OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];
--- a/src/HOL/Tools/res_atp.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Sat Oct 06 16:50:04 2007 +0200
@@ -969,8 +969,8 @@
isar_atp_writeonly (ctxt, chain_ths, goal))
end;
-val _ = OuterSyntax.add_parsers
- [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
+val _ =
+ OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
end;
--- a/src/HOL/Tools/specification_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -244,7 +244,7 @@
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
-val specificationP =
+val _ =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
(specification_decl >> (fn (cos,alt_props) =>
Toplevel.print o (Toplevel.theory_to_proof
@@ -255,14 +255,12 @@
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
-val ax_specificationP =
+val _ =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
(ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
Toplevel.print o (Toplevel.theory_to_proof
(process_spec (SOME axname) cos alt_props))))
-val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
-
end
--- a/src/HOL/Tools/typedef_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -273,7 +273,9 @@
local structure P = OuterParse and K = OuterKeyword in
-val typedeclP =
+val _ = OuterSyntax.keywords ["morphisms"];
+
+val _ =
OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
(P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
Toplevel.theory (add_typedecls [(t, vs, mx)])));
@@ -289,14 +291,10 @@
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
-val typedefP =
+val _ =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
-
-val _ = OuterSyntax.add_keywords ["morphisms"];
-val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
-
end;
end;
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -481,10 +481,15 @@
add_rename aut source_aut rename_f;
-(* parsers *)
+(* outer syntax *)
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
+ "outputs", "internals", "states", "initially", "transitions", "pre",
+ "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
+ "rename"];
+
val actionlist = P.list1 P.term;
val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
@@ -520,21 +525,10 @@
(P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
>> mk_rename_decl;
-val automatonP =
+val _ =
OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
(ioa_decl >> Toplevel.theory);
end;
-
-(* setup outer syntax *)
-
-val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
- "outputs", "internals", "states", "initially", "transitions", "pre",
- "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
- "rename"];
-
-val _ = OuterSyntax.add_parsers [automatonP];
-
-
end;
--- a/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML Sat Oct 06 16:50:04 2007 +0200
@@ -99,12 +99,10 @@
local structure P = OuterParse and K = OuterKeyword in
-val constsP =
+val _ =
OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
(Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
-val _ = OuterSyntax.add_parsers [constsP];
-
end;
end;
--- a/src/HOLCF/Tools/domain/domain_extender.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat Oct 06 16:50:04 2007 +0200
@@ -146,6 +146,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["lazy"];
+
val dest_decl =
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
(P.name >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
@@ -170,14 +172,10 @@
>> (fn (opt_name, doms) =>
(case opt_name of NONE => space_implode "_" (map (#1 o #1) doms) | SOME s => s, doms));
-val domainP =
+val _ =
OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
(domains_decl >> (Toplevel.theory o add_domain));
-
-val _ = OuterSyntax.add_keywords ["lazy"];
-val _ = OuterSyntax.add_parsers [domainP];
-
-end; (* local structure *)
+end;
end;
--- a/src/HOLCF/Tools/fixrec_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -299,19 +299,17 @@
(* this builds a parser for a new keyword, fixrec, whose functionality
is defined by add_fixrec *)
-val fixrecP =
+val _ =
OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
(fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
(* fixpat parser *)
val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
-val fixpatP =
+val _ =
OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
(fixpat_decl >> (Toplevel.theory o add_fixpat));
-val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
+end;
-end; (* local structure *)
-
-end; (* struct *)
+end;
--- a/src/HOLCF/Tools/pcpodef_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -184,7 +184,7 @@
local structure P = OuterParse and K = OuterKeyword in
-(* copied from HOL/Tools/typedef_package.ML *)
+(* cf. HOL/Tools/typedef_package.ML *)
val typedef_proof_decl =
Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
@@ -196,18 +196,16 @@
(if pcpo then pcpodef_proof else cpodef_proof)
((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
-val pcpodefP =
+val _ =
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
-val cpodefP =
+val _ =
OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
-val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
-
end;
end;
--- a/src/Provers/classical.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Provers/classical.ML Sat Oct 06 16:50:04 2007 +0200
@@ -1084,7 +1084,7 @@
(** outer syntax **)
-val print_clasetP =
+val _ =
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
OuterKeyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
@@ -1092,7 +1092,4 @@
(Context.cases print_claset print_local_claset)
(print_local_claset o Proof.context_of)))));
-val _ = OuterSyntax.add_parsers [print_clasetP];
-
-
end;
--- a/src/Pure/Proof/extraction.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Sat Oct 06 16:50:04 2007 +0200
@@ -759,7 +759,7 @@
val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
-val realizersP =
+val _ =
OuterSyntax.command "realizers"
"specify realizers for primitive axioms / theorems, together with correctness proof"
K.thy_decl
@@ -768,23 +768,21 @@
(map (fn (((a, vs), s1), s2) =>
(PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
-val realizabilityP =
+val _ =
OuterSyntax.command "realizability"
"add equations characterizing realizability" K.thy_decl
(Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
-val typeofP =
+val _ =
OuterSyntax.command "extract_type"
"add equations characterizing type of extracted program" K.thy_decl
(Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
-val extractP =
+val _ =
OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
(Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
(fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
-val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
-
val etype_of = etype_of o add_syntax;
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 06 16:50:04 2007 +0200
@@ -231,36 +231,36 @@
local structure P = OuterParse and K = OuterKeyword in
-val undoP = (*undo without output*)
+fun undoP () = (*undo without output*)
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-val restartP =
+fun restartP () =
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
-val kill_proofP =
+fun kill_proofP () =
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
-val inform_file_processedP =
+fun inform_file_processedP () =
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
(P.name >> (fn file => Toplevel.no_timing o
Toplevel.init_empty (vacuous_inform_file_processed file) o
Toplevel.kill o
Toplevel.init_empty (proper_inform_file_processed file)));
-val inform_file_retractedP =
+fun inform_file_retractedP () =
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
(P.name >> (Toplevel.no_timing oo
(fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
-val process_pgipP =
+fun process_pgipP () =
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
(P.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
-fun init_outer_syntax () = OuterSyntax.add_parsers
+fun init_outer_syntax () = List.app (fn f => f ())
[undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 06 16:50:04 2007 +0200
@@ -1125,21 +1125,13 @@
end
-local
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
-val process_pgipP =
+fun init_outer_syntax () =
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
(OuterParse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
-in
-
- fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
-
-end
-
-
(* init *)
--- a/src/Pure/Tools/invoke.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/invoke.ML Sat Oct 06 16:50:04 2007 +0200
@@ -115,7 +115,7 @@
local structure P = OuterParse and K = OuterKeyword in
-val invokeP =
+val _ =
OuterSyntax.command "invoke"
"schematic invocation of locale expression in proof context"
(K.tag_proof K.prf_goal)
@@ -123,8 +123,6 @@
>> (fn (((name, expr), (insts, _)), fixes) =>
Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
-val _ = OuterSyntax.add_parsers [invokeP];
-
end;
end;
--- a/src/Pure/Tools/named_thms.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/named_thms.ML Sat Oct 06 16:50:04 2007 +0200
@@ -36,10 +36,10 @@
val setup =
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
-val _ = OuterSyntax.add_parsers
- [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
+val _ =
+ OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
OuterKeyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
- Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))];
+ Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
end;
--- a/src/Pure/codegen.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/codegen.ML Sat Oct 06 16:50:04 2007 +0200
@@ -1100,6 +1100,8 @@
structure P = OuterParse and K = OuterKeyword;
+val _ = OuterSyntax.keywords ["attach", "file", "contains"];
+
fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
(snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
@@ -1107,7 +1109,7 @@
Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
(P.verbatim >> strip_whitespace));
-val assoc_typeP =
+val _ =
OuterSyntax.command "types_code"
"associate types with target language types" K.thy_decl
(Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
@@ -1115,7 +1117,7 @@
(fn ((name, mfx), aux) => (name, (parse_mixfix
(Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
-val assoc_constP =
+val _ =
OuterSyntax.command "consts_code"
"associate constants with target language code" K.thy_decl
(Scan.repeat1
@@ -1152,12 +1154,12 @@
else map_modules (Symtab.update (module, gr)) thy)
end));
-val code_libraryP =
+val _ =
OuterSyntax.command "code_library"
"generates code for terms (one structure for each theory)" K.thy_decl
(parse_code true);
-val code_moduleP =
+val _ =
OuterSyntax.command "code_module"
"generates code for terms (single structure, incremental)" K.thy_decl
(parse_code false);
@@ -1174,13 +1176,13 @@
(P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
-val test_paramsP =
+val _ =
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
(P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
(fn fs => Toplevel.theory (fn thy =>
map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
-val testP =
+val _ =
OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
(Scan.option (P.$$$ "[" |-- P.list1
( parse_test_params >> (fn f => fn thy => apfst (f thy))
@@ -1191,15 +1193,10 @@
(get_test_params (Toplevel.theory_of st), [])) g [] |>
pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
-val valueP =
+val _ =
OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
(P.term >> (Toplevel.no_timing oo print_evaluated_term));
-val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
-
-val _ = OuterSyntax.add_parsers
- [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
-
end;
val auto_quickcheck = Codegen.auto_quickcheck;
--- a/src/Tools/code/code_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/code/code_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -558,14 +558,14 @@
-- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
) >> (fn (raw_cs, seris) => cmd raw_cs seris));
-val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
+val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
val (codeK, code_thmsK, code_depsK, code_propsK) =
("export_code", "code_thms", "code_deps", "code_props");
in
-val codeP =
+val _ =
OuterSyntax.improper_command codeK "generate executable code for constants"
K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
@@ -574,24 +574,22 @@
of SOME f => (writeln "Now generating code..."; f thy)
| NONE => error ("Bad directive " ^ quote cmd);
-val code_thmsP =
+val _ =
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
(Scan.repeat P.term
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
-val code_depsP =
+val _ =
OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
(Scan.repeat P.term
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-val code_propsP =
+val _ =
OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
-val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
-
end; (*local*)
end; (*struct*)
--- a/src/Tools/code/code_target.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/code/code_target.ML Sat Oct 06 16:50:04 2007 +0200
@@ -2091,7 +2091,10 @@
val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
-val code_classP =
+
+val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
+
+val _ =
OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
parse_multi_syntax P.xname
(Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
@@ -2100,7 +2103,7 @@
fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
);
-val code_instanceP =
+val _ =
OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
((P.minus >> K true) || Scan.succeed false)
@@ -2108,55 +2111,50 @@
fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
);
-val code_typeP =
+val _ =
OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
parse_multi_syntax P.xname (parse_syntax I)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
);
-val code_constP =
+val _ =
OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
parse_multi_syntax P.term (parse_syntax fst)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
);
-val code_monadP =
+val _ =
OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
P.term -- P.term -- P.term
>> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory
(add_haskell_monad raw_run raw_mbind raw_kbind))
);
-val code_reservedP =
+val _ =
OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
P.name -- Scan.repeat1 P.name
>> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
);
-val code_modulenameP =
+val _ =
OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
P.name -- Scan.repeat1 (P.name -- P.name)
>> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
);
-val code_moduleprologP =
+val _ =
OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
>> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
);
-val code_exceptionP =
+val _ =
OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl (
Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
);
-val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK];
-
-val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
- code_reservedP, code_modulenameP, code_moduleprologP, code_monadP, code_exceptionP];
-
(*including serializer defaults*)
val setup =
--- a/src/Tools/induct.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/induct.ML Sat Oct 06 16:50:04 2007 +0200
@@ -161,10 +161,10 @@
|> Pretty.chunks |> Pretty.writeln
end;
-val _ = OuterSyntax.add_parsers [
+val _ =
OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
- Toplevel.keep (print_rules o Toplevel.context_of)))];
+ Toplevel.keep (print_rules o Toplevel.context_of)));
(* access rules *)
--- a/src/Tools/nbe.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Tools/nbe.ML Sat Oct 06 16:50:04 2007 +0200
@@ -410,12 +410,10 @@
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val nbeP =
+val _ =
OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
(opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
-val _ = OuterSyntax.add_parsers [nbeP];
-
end;
end;
--- a/src/ZF/Tools/datatype_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -422,11 +422,9 @@
val coind_prefix = if coind then "co" else "";
-val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
+val _ = OuterSyntax.command (coind_prefix ^ "datatype")
("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
-val _ = OuterSyntax.add_parsers [inductiveP];
-
end;
end;
--- a/src/ZF/Tools/ind_cases.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML Sat Oct 06 16:50:04 2007 +0200
@@ -76,15 +76,11 @@
local structure P = OuterParse and K = OuterKeyword in
-val ind_cases =
- P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
- >> (Toplevel.theory o inductive_cases);
-
-val inductive_casesP =
+val _ =
OuterSyntax.command "inductive_cases"
- "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
-
-val _ = OuterSyntax.add_parsers [inductive_casesP];
+ "create simplified instances of elimination rules (improper)" K.thy_script
+ (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ >> (Toplevel.theory o inductive_cases));
end;
--- a/src/ZF/Tools/induct_tacs.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sat Oct 06 16:50:04 2007 +0200
@@ -188,6 +188,8 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
+
val rep_datatype_decl =
(P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
(P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
@@ -195,13 +197,10 @@
Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
-val rep_datatypeP =
+val _ =
OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
(rep_datatype_decl >> Toplevel.theory);
-val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
-val _ = OuterSyntax.add_parsers [rep_datatypeP];
-
end;
end;
--- a/src/ZF/Tools/inductive_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -576,6 +576,9 @@
local structure P = OuterParse and K = OuterKeyword in
+val _ = OuterSyntax.keywords
+ ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
+
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
#1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
@@ -590,13 +593,9 @@
Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
>> (Toplevel.theory o mk_ind);
-val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
+val _ = OuterSyntax.command (co_prefix ^ "inductive")
("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
-val _ = OuterSyntax.add_keywords
- ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
-val _ = OuterSyntax.add_parsers [inductiveP];
-
end;
end;
--- a/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -203,18 +203,12 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
+structure P = OuterParse and K = OuterKeyword;
-val primrecP =
+val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
-
-val _ = OuterSyntax.add_parsers [primrecP];
+ (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+ >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
end;
-end;
-
-
--- a/src/ZF/Tools/typechk.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/typechk.ML Sat Oct 06 16:50:04 2007 +0200
@@ -118,10 +118,10 @@
Args.del -- Args.colon >> K (I, TC_del)]
(fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
-val _ = OuterSyntax.add_parsers
- [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
+val _ =
+ OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
- Toplevel.keep (print_tcset o Toplevel.context_of)))];
+ Toplevel.keep (print_tcset o Toplevel.context_of)));
(* theory setup *)