--- a/Admin/isatest/isatest-stats Fri Aug 23 16:51:53 2013 +0200
+++ b/Admin/isatest/isatest-stats Fri Aug 23 21:59:29 2013 +0200
@@ -65,7 +65,6 @@
HOL-SPARK
HOL-SPARK-Examples
HOL-SPARK-Manual
- HOL-Spec_Check
HOL-Statespace
HOL-TLA
HOL-TLA-Buffer
@@ -91,6 +90,7 @@
IOA-Storage
IOA-ex
Pure
+ Spec_Check
ZF
ZF-AC
ZF-Coind
--- a/CONTRIBUTORS Fri Aug 23 16:51:53 2013 +0200
+++ b/CONTRIBUTORS Fri Aug 23 21:59:29 2013 +0200
@@ -14,7 +14,7 @@
Ephemeral interpretation in local theories.
* May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
- HOL-Spec_Check: A Quickcheck tool for Isabelle's ML environment.
+ Spec_Check: A Quickcheck tool for Isabelle/ML.
* April 2013: Stefan Berghofer, secunet Security Networks AG
Dmitriy Traytel, TUM
--- a/NEWS Fri Aug 23 16:51:53 2013 +0200
+++ b/NEWS Fri Aug 23 21:59:29 2013 +0200
@@ -86,7 +86,9 @@
* Dockable window "Timing" provides an overview of relevant command
timing information.
-* Option to skip over proofs, using implicit 'sorry' internally.
+* Action isabelle.reset-font-size resets main text area font size
+according to Isabelle/Scala plugin option "jedit_font_reset_size"
+(cf. keyboard shortcut C+0).
*** Pure ***
@@ -108,8 +110,8 @@
* Target-sensitive commands 'interpretation' and 'sublocale'.
Particulary, 'interpretation' now allows for non-persistent
-interpretation within "context ... begin ... end" blocks.
-See "isar-ref" manual for details.
+interpretation within "context ... begin ... end" blocks. See
+"isar-ref" manual for details.
* Improved locales diagnostic command 'print_dependencies'.
@@ -130,39 +132,44 @@
* Improved support for adhoc overloading of constants (see also
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
-* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.
-Use explicit 'code equation' and 'code abstract' to distinguish both when desired.
+* Attibute 'code': 'code' now declares concrete and abstract code
+equations uniformly. Use explicit 'code equation' and 'code abstract'
+to distinguish both when desired.
* Code generator:
- * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
- * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
- subsuming 'code_modulename'.
- See the Isar reference manual for syntax diagrams, and the HOL theories for examples.
+ - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
+ 'code_instance'.
+ - 'code_identifier' declares name hints for arbitrary identifiers in
+ generated code, subsuming 'code_modulename'.
+ See the isar-ref manual for syntax diagrams, and the HOL theories
+ for examples.
* Library/Polynomial.thy:
- * Use lifting for primitive definitions.
- * Explicit conversions from and to lists of coefficients, used for generated code.
- * Replaced recursion operator poly_rec by fold_coeffs.
- * Prefer pre-existing gcd operation for gcd.
- * Fact renames:
+ - Use lifting for primitive definitions.
+ - Explicit conversions from and to lists of coefficients, used for
+ generated code.
+ - Replaced recursion operator poly_rec by fold_coeffs.
+ - Prefer pre-existing gcd operation for gcd.
+ - Fact renames:
poly_eq_iff ~> poly_eq_poly_eq_iff
poly_ext ~> poly_eqI
expand_poly_eq ~> poly_eq_iff
IMCOMPATIBILTIY.
* Reification and reflection:
- * Reification is now directly available in HOL-Main in structure "Reification".
- * Reflection now handles multiple lists with variables also.
- * The whole reflection stack has been decomposed into conversions.
+ - Reification is now directly available in HOL-Main in structure
+ "Reification".
+ - Reflection now handles multiple lists with variables also.
+ - The whole reflection stack has been decomposed into conversions.
INCOMPATIBILITY.
* Weaker precendence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations. INCOMPATIBILITY.
-* Nested case expressions are now translated in a separate check
- phase rather than during parsing. The data for case combinators
- is separated from the datatype package. The declaration attribute
- "case_translation" can be used to register new case combinators:
+* Nested case expressions are now translated in a separate check phase
+rather than during parsing. The data for case combinators is separated
+from the datatype package. The declaration attribute
+"case_translation" can be used to register new case combinators:
declare [[case_translation case_combinator constructor1 ... constructorN]]
@@ -187,7 +194,6 @@
- Fact renames:
card.union_inter ~> card_Un_Int [symmetric]
card.union_disjoint ~> card_Un_disjoint
-
INCOMPATIBILITY.
* Locale hierarchy for abstract orderings and (semi)lattices.
@@ -198,37 +204,38 @@
* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.
-* Numeric types mapped by default to target language numerals:
-natural (replaces former code_numeral) and integer (replaces
-former code_int). Conversions are available as integer_of_natural /
-natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
-Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML).
-INCOMPATIBILITY.
+* Numeric types mapped by default to target language numerals: natural
+(replaces former code_numeral) and integer (replaces former code_int).
+Conversions are available as integer_of_natural / natural_of_integer /
+integer_of_nat / nat_of_integer (in HOL) and
+Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
+ML). INCOMPATIBILITY.
* Discontinued theories Code_Integer and Efficient_Nat by a more
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
-Code_Target_Nat and Code_Target_Numeral. See the tutorial on
-code generation for details. INCOMPATIBILITY.
-
-* Introduce type class "conditionally_complete_lattice": Like a complete
- lattice but does not assume the existence of the top and bottom elements.
- Allows to generalize some lemmas about reals and extended reals.
- Removed SupInf and replaced it by the instantiation of
- conditionally_complete_lattice for real. Renamed lemmas about
- conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
- to cInf_... to avoid hidding of similar complete lattice lemmas.
-
- Introduce type class linear_continuum as combination of conditionally-complete
- lattices and inner dense linorders which have more than one element.
-INCOMPATIBILITY.
-
-* Introduce type classes "no_top" and "no_bot" for orderings without top
- and bottom elements.
+Code_Target_Nat and Code_Target_Numeral. See the tutorial on code
+generation for details. INCOMPATIBILITY.
+
+* Introduce type class "conditionally_complete_lattice": Like a
+complete lattice but does not assume the existence of the top and
+bottom elements. Allows to generalize some lemmas about reals and
+extended reals. Removed SupInf and replaced it by the instantiation
+of conditionally_complete_lattice for real. Renamed lemmas about
+conditionally-complete lattice from Sup_... to cSup_... and from
+Inf_... to cInf_... to avoid hidding of similar complete lattice
+lemmas.
+
+* Introduce type class linear_continuum as combination of
+conditionally-complete lattices and inner dense linorders which have
+more than one element. INCOMPATIBILITY.
+
+* Introduce type classes "no_top" and "no_bot" for orderings without
+top and bottom elements.
* Split dense_linorder into inner_dense_order and no_top, no_bot.
* Complex_Main: Unify and move various concepts from
- HOL-Multivariate_Analysis to HOL-Complex_Main.
+HOL-Multivariate_Analysis to HOL-Complex_Main.
- Introduce type class (lin)order_topology and linear_continuum_topology.
Allows to generalize theorems about limits and order.
@@ -305,28 +312,23 @@
- Renamed option:
isar_shrink ~> isar_compress
-* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.
-
- With HOL-Spec_Check, ML developers can check specifications with the
- ML function check_property. The specifications must be of the form
- "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
- src/HOL/Spec_Check/Examples.thy.
-
-* Imperative HOL: The MREC combinator is considered legacy and no longer
-included by default. INCOMPATIBILITY, use partial_function instead, or import
-theory Legacy_Mrec as a fallback.
-
-
-*** HOL-Algebra ***
-
-* Discontinued theories src/HOL/Algebra/abstract and .../poly.
-Existing theories should be based on src/HOL/Library/Polynomial
-instead. The latter provides integration with HOL's type classes for
-rings. INCOMPATIBILITY.
+* Imperative-HOL: The MREC combinator is considered legacy and no
+longer included by default. INCOMPATIBILITY, use partial_function
+instead, or import theory Legacy_Mrec as a fallback.
+
+* HOL-Algebra: Discontinued theories src/HOL/Algebra/abstract and
+.../poly. Existing theories should be based on
+src/HOL/Library/Polynomial instead. The latter provides integration
+with HOL's type classes for rings. INCOMPATIBILITY.
*** ML ***
+* Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function
+"check_property" allows to check specifications of the form "ALL x y
+z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its
+Examples.thy in particular.
+
* More uniform naming of goal functions for skipped proofs:
Skip_Proof.prove ~> Goal.prove_sorry--- a/ROOTS Fri Aug 23 16:51:53 2013 +0200
+++ b/ROOTS Fri Aug 23 21:59:29 2013 +0200
@@ -9,3 +9,5 @@
src/LCF
src/Sequents
src/Doc
+src/Tools
+
--- a/lib/texinputs/isabelle.sty Fri Aug 23 16:51:53 2013 +0200
+++ b/lib/texinputs/isabelle.sty Fri Aug 23 21:59:29 2013 +0200
@@ -37,8 +37,6 @@
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
-\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
-\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
\newdimen\isa@parindent\newdimen\isa@parskip
--- a/src/Doc/IsarImplementation/ML.thy Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy Fri Aug 23 21:59:29 2013 +0200
@@ -667,7 +667,7 @@
ML is augmented by special syntactic entities of the following form:
@{rail "
- @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
+ @{syntax_def antiquote}: '@{' nameref args '}'
"}
Here @{syntax nameref} and @{syntax args} are regular outer syntax
@@ -682,61 +682,6 @@
scheme allows to refer to formal entities in a robust manner, with
proper static scoping and with some degree of logical checking of
small portions of the code.
-
- Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note
- \<dots>}"} augment the compilation context without generating code. The
- non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the
- effect by introducing local blocks within the pre-compilation
- environment.
-
- \medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
- perspective on Isabelle/ML antiquotations. *}
-
-text %mlantiq {*
- \begin{matharray}{rcl}
- @{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
- \end{matharray}
-
- @{rail "
- @@{ML_antiquotation let} ((term + @'and') '=' term + @'and')
- ;
- @@{ML_antiquotation note} (thmdef? thmrefs + @'and')
- "}
-
- \begin{description}
-
- \item @{text "@{let p = t}"} binds schematic variables in the
- pattern @{text "p"} by higher-order matching against the term @{text
- "t"}. This is analogous to the regular @{command_ref let} command
- in the Isar proof language. The pre-compilation environment is
- augmented by auxiliary term bindings, without emitting ML source.
-
- \item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text
- "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. This is analogous to
- the regular @{command_ref note} command in the Isar proof language.
- The pre-compilation environment is augmented by auxiliary fact
- bindings, without emitting ML source.
-
- \end{description}
-*}
-
-text %mlex {* The following artificial example gives some impression
- about the antiquotation elements introduced so far, together with
- the important @{text "@{thm}"} antiquotation defined later.
-*}
-
-ML {*
- \<lbrace>
- @{let ?t = my_term}
- @{note my_refl = reflexive [of ?t]}
- fun foo th = Thm.transitive th @{thm my_refl}
- \<rbrace>
-*}
-
-text {* The extra block delimiters do not affect the compiled code
- itself, i.e.\ function @{ML foo} is available in the present context
- of this paragraph.
*}
--- a/src/Doc/IsarImplementation/document/style.sty Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Doc/IsarImplementation/document/style.sty Fri Aug 23 21:59:29 2013 +0200
@@ -24,9 +24,6 @@
\renewcommand{\isadigit}[1]{\isamath{#1}}
-\renewcommand{\isaantiqopen}{\isasymlbrace}
-\renewcommand{\isaantiqclose}{\isasymrbrace}
-
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
\isafoldtag{FIXME}--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 23 21:59:29 2013 +0200
@@ -2140,7 +2140,7 @@
ML_file "cooper_tac.ML"
method_setup cooper = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
*} "decision procedure for linear integer arithmetic"
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 23 21:59:29 2013 +0200
@@ -2009,7 +2009,7 @@
ML_file "ferrack_tac.ML"
method_setup rferrack = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
*} "decision procedure for linear real arithmetic"
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 23 21:59:29 2013 +0200
@@ -5665,7 +5665,7 @@
ML_file "mir_tac.ML"
method_setup mir = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
*} "decision procedure for MIR arithmetic"
--- a/src/HOL/Import/import_data.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Import/import_data.ML Fri Aug 23 21:59:29 2013 +0200
@@ -87,39 +87,39 @@
const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
end
-val parser = Parse.name -- Scan.option (Parse.$$$ ":" |-- Parse.xname)
-fun add_const_attr (s1, s2) = Thm.declaration_attribute
- (fn th => Context.mapping (add_const_def s1 th s2) (fn x => x))
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "import_const") (Scan.lift parser >> add_const_attr)
- "Declare a theorem as an equality that maps the given constant"))
+val _ = Theory.setup
+ (Attrib.setup @{binding import_const}
+ (Scan.lift (Parse.name -- Scan.option (@{keyword ":"} |-- Parse.xname)) >>
+ (fn (s1, s2) => Thm.declaration_attribute
+ (fn th => Context.mapping (add_const_def s1 th s2) I)))
+ "declare a theorem as an equality that maps the given constant")
-val parser = Parse.name -- (Parse.name -- Parse.name)
-fun add_typ_attr (tyname, (absname, repname)) = Thm.declaration_attribute
- (fn th => Context.mapping (add_typ_def tyname absname repname th) (fn x => x))
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "import_type") (Scan.lift parser >> add_typ_attr)
- "Declare a type_definion theorem as a map for an imported type abs rep"))
+val _ = Theory.setup
+ (Attrib.setup @{binding import_type}
+ (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
+ (fn ((tyname, absname), repname) => Thm.declaration_attribute
+ (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
+ "declare a type_definion theorem as a map for an imported type abs rep")
-val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
- (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
-val _ = Outer_Syntax.command @{command_spec "import_type_map"}
- "map external type name to existing Isabelle/HOL type name"
- (type_map >> Toplevel.theory)
+val _ =
+ Outer_Syntax.command @{command_spec "import_type_map"}
+ "map external type name to existing Isabelle/HOL type name"
+ ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
+ (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map ty_name1 ty_name2)))
-val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
- (fn (cname1, cname2) => add_const_map cname1 cname2)
-val _ = Outer_Syntax.command @{command_spec "import_const_map"}
- "map external const name to existing Isabelle/HOL const name"
- (const_map >> Toplevel.theory)
+val _ =
+ Outer_Syntax.command @{command_spec "import_const_map"}
+ "map external const name to existing Isabelle/HOL const name"
+ ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
+ (fn (cname1, cname2) => Toplevel.theory (add_const_map cname1 cname2)))
(* Initial type and constant maps, for types and constants that are not
defined, which means their definitions do not appear in the proof dump *)
-val _ = Context.>> (Context.map_theory (
- add_typ_map "bool" @{type_name bool} o
- add_typ_map "fun" @{type_name fun} o
- add_typ_map "ind" @{type_name ind} o
- add_const_map "=" @{const_name HOL.eq} o
- add_const_map "@" @{const_name "Eps"}))
+val _ = Theory.setup
+ (add_typ_map "bool" @{type_name bool} #>
+ add_typ_map "fun" @{type_name fun} #>
+ add_typ_map "ind" @{type_name ind} #>
+ add_const_map "=" @{const_name HOL.eq} #>
+ add_const_map "@" @{const_name "Eps"})
end--- a/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 21:59:29 2013 +0200
@@ -169,8 +169,9 @@
in
val nominal_induct_method =
- Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
- avoiding -- fixing -- rule_spec) >>
+ Scan.lift (Args.mode Induct.no_simpN) --
+ (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ avoiding -- fixing -- rule_spec) >>
(fn (no_simp, (((x, y), z), w)) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));--- a/src/HOL/ROOT Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/ROOT Fri Aug 23 21:59:29 2013 +0200
@@ -741,12 +741,6 @@
options [document = false]
theories WordExamples
-session "HOL-Spec_Check" in Spec_Check = HOL +
- theories
- Spec_Check
- theories [condition = ISABELLE_POLYML]
- Examples
-
session "HOL-Statespace" in Statespace = HOL +
theories [skip_proofs = false]
StateSpaceEx--- a/src/HOL/Spec_Check/Examples.thy Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-theory Examples
-imports Spec_Check
-begin
-
-section {* List examples *}
-
-ML_command {*
-check_property "ALL xs. rev xs = xs";
-*}
-
-ML_command {*
-check_property "ALL xs. rev (rev xs) = xs";
-*}
-
-
-section {* AList Specification *}
-
-ML_command {*
-(* map_entry applies the function to the element *)
-check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
-*}
-
-ML_command {*
-(* update always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
-*}
-
-ML_command {*
-(* update always writes the value *)
-check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
-*}
-
-ML_command {*
-(* default always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
-*}
-
-ML_command {*
-(* delete always removes the entry *)
-check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
-*}
-
-ML_command {*
-(* default writes the entry iff it didn't exist *)
-check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
-*}
-
-section {* Examples on Types and Terms *}
-
-ML_command {*
-check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
-*}
-
-ML_command {*
-check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
-*}
-
-
-text {* One would think this holds: *}
-
-ML_command {*
-check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
-*}
-
-text {* But it only holds with this precondition: *}
-
-ML_command {*
-check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
-*}
-
-section {* Some surprises *}
-
-ML_command {*
-check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
-*}
-
-
-ML_command {*
-val thy = @{theory};
-check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
-*}
-
-end--- a/src/HOL/Spec_Check/README Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-This is a Quickcheck tool for Isabelle's ML environment.
-
-Authors
-
- Lukas Bulwahn
- Nicolai Schaffroth
-
-Quick Usage
-
- - Import Spec_Check.thy in your development
- - Look at examples in Examples.thy
- - write specifications with the ML invocation
- check_property "ALL x. P x"
-
-Notes
-
-Our specification-based testing tool originated from Christopher League's
-QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
-provides a rich and uniform ML platform (called Isabelle/ML), this
-testing tools is very different than the one for a typical ML developer.
-
-1. Isabelle/ML provides common data structures, which we can use in the
-tool's implementation for storing data and printing output.
-
-2. The implementation in Isabelle that will be checked with this tool
-commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
-but they do not use other integer types in ML, such as ML's Int.int,
-Word.word and others.
-
-3. As Isabelle can run heavily in parallel, we avoid reference types.
-
-4. Isabelle has special naming conventions and documentation of source
-code is only minimal to avoid parroting.
-
-Next steps:
- - Remove all references and store the neccessary random seed in the
- Isabelle's context.
- - Simplify some existing random generators.
- The original ones from Christopher League are so complicated to
- support many integer types uniformly.
-
-License
-
- The source code originated from Christopher League's QCheck, which is
- licensed under the 2-clause BSD license. The current source code is
- licensed under the compatible 3-clause BSD license of Isabelle.
-
--- a/src/HOL/Spec_Check/Spec_Check.thy Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-theory Spec_Check
-imports Main
-begin
-
-ML_file "random.ML"
-ML_file "property.ML"
-ML_file "base_generator.ML"
-ML_file "generator.ML"
-ML_file "gen_construction.ML"
-ML_file "spec_check.ML"
-ML_file "output_style.ML"
-setup Output_Style.setup
-
-end
\ No newline at end of file
--- a/src/HOL/Spec_Check/base_generator.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(* Title: HOL/Spec_Check/base_generator.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Basic random generators.
-*)
-
-signature BASE_GENERATOR =
-sig
-
-type rand
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-val new : unit -> rand
-val range : int * int -> rand -> int * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-val lift : 'a -> 'a gen
-val select : 'a vector -> 'a gen
-val choose : 'a gen vector -> 'a gen
-val choose' : (int * 'a gen) vector -> 'a gen
-val selectL : 'a list -> 'a gen
-val chooseL : 'a gen list -> 'a gen
-val chooseL' : (int * 'a gen) list -> 'a gen
-val filter : ('a -> bool) -> 'a gen -> 'a gen
-
-val zip : ('a gen * 'b gen) -> ('a * 'b) gen
-val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
-val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
-val map : ('a -> 'b) -> 'a gen -> 'b gen
-val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
-val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
-val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
-
-val flip : bool gen
-val flip' : int * int -> bool gen
-
-val list : bool gen -> 'a gen -> 'a list gen
-val option : bool gen -> 'a gen -> 'a option gen
-val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
-
-val variant : (int, 'b) co
-val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
-val cobool : (bool, 'b) co
-val colist : ('a, 'b) co -> ('a list, 'b) co
-val coopt : ('a, 'b) co -> ('a option, 'b) co
-
-type stream
-val start : rand -> stream
-val limit : int -> 'a gen -> ('a, stream) reader
-
-end
-
-structure Base_Generator : BASE_GENERATOR =
-struct
-
-(* random number engine *)
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
- let
- val t = a * seed
- in
- t - m * real (floor (t / m))
- end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
- if min > max then raise Domain (* TODO: raise its own error *)
- else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
-
-fun split r =
- let
- val r = r / a
- val r0 = real (floor r)
- val r1 = r - r0
- in
- (nextrand r0, nextrand r1)
- end
-
-(* generators *)
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-fun lift obj r = (obj, r)
-
-local (* Isabelle does not use vectors? *)
- fun explode ((freq, gen), acc) =
- List.tabulate (freq, fn _ => gen) @ acc
-in
- fun choose v r =
- let val (i, r) = range(0, Vector.length v - 1) r
- in Vector.sub (v, i) r end
- fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
- fun select v = choose (Vector.map lift v)
-end
-
-fun chooseL l = choose (Vector.fromList l)
-fun chooseL' l = choose' (Vector.fromList l)
-fun selectL l = select (Vector.fromList l)
-
-fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
-
-fun zip3 (g1, g2, g3) =
- zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
-
-fun zip4 (g1, g2, g3, g4) =
- zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
-
-fun map f g = apfst f o g
-
-fun map2 f = map f o zip
-fun map3 f = map f o zip3
-fun map4 f = map f o zip4
-
-fun filter p gen r =
- let
- fun loop (x, r) = if p x then (x, r) else loop (gen r)
- in
- loop (gen r)
- end
-
-val flip = selectL [true, false]
-fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
-
-fun list flip g r =
- case flip r of
- (true, r) => ([], r)
- | (false, r) =>
- let
- val (x,r) = g r
- val (xs,r) = list flip g r
- in (x::xs, r) end
-
-fun option flip g r =
- case flip r of
- (true, r) => (NONE, r)
- | (false, r) => map SOME g r
-
-fun vector tabulate (int, elem) r =
- let
- val (n, r) = int r
- val p = Unsynchronized.ref r
- fun g _ =
- let
- val (x,r) = elem(!p)
- in x before p := r end
- in
- (tabulate(n, g), !p)
- end
-
-type stream = rand Unsynchronized.ref * int
-
-fun start r = (Unsynchronized.ref r, 0)
-
-fun limit max gen =
- let
- fun next (p, i) =
- if i >= max then NONE
- else
- let val (x, r) = gen(!p)
- in SOME(x, (p, i+1)) before p := r end
- in
- next
- end
-
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-fun variant v g r =
- let
- fun nth (i, r) =
- let val (r1, r2) = split r
- in if i = 0 then r1 else nth (i-1, r2) end
- in
- g (nth (v, r))
- end
-
-fun arrow (cogen, gen) r =
- let
- val (r1, r2) = split r
- fun g x = fst (cogen x gen r1)
- in (g, r2) end
-
-fun cobool false = variant 0
- | cobool true = variant 1
-
-fun colist _ [] = variant 0
- | colist co (x::xs) = variant 1 o co x o colist co xs
-
-fun coopt _ NONE = variant 0
- | coopt co (SOME x) = variant 1 o co x
-
-end
---- a/src/HOL/Spec_Check/gen_construction.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(* Title: HOL/Spec_Check/gen_construction.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Constructing generators and pretty printing function for complex types.
-*)
-
-signature GEN_CONSTRUCTION =
-sig
- val register : string * (string * string) -> theory -> theory
- type mltype
- val parse_pred : string -> string * mltype
- val build_check : Proof.context -> string -> mltype * string -> string
- (*val safe_check : string -> mltype * string -> string*)
- val string_of_bool : bool -> string
- val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
-end;
-
-structure Gen_Construction : GEN_CONSTRUCTION =
-struct
-
-(* Parsing ML types *)
-
-datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
-
-(*Split string into tokens for parsing*)
-fun split s =
- let
- fun split_symbol #"(" = "( "
- | split_symbol #")" = " )"
- | split_symbol #"," = " ,"
- | split_symbol #":" = " :"
- | split_symbol c = Char.toString c
- fun is_space c = c = #" "
- in String.tokens is_space (String.translate split_symbol s) end;
-
-(*Accept anything that is not a recognized symbol*)
-val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
-
-(*Turn a type list into a nested Con*)
-fun make_con [] = raise Empty
- | make_con [c] = c
- | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
-
-(*Parse a type*)
-fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
-
-and parse_type_arg s = (parse_tuple || parse_type_single) s
-
-and parse_type_single s = (parse_con || parse_type_basic) s
-
-and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
-
-and parse_list s =
- ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
-
-and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
-
-and parse_con s = ((parse_con_nest
- || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
- || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
- >> (make_con o rev)) s
-
-and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
-
-and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
-
-and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
- >> (fn (t, tl) => Tuple (t :: tl))) s;
-
-(*Parse entire type + name*)
-fun parse_function s =
- let
- val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
- val (name, ty) = p (split s)
- val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
- val (typ, _) = Scan.finite stop parse_type ty
- in (name, typ) end;
-
-(*Create desired output*)
-fun parse_pred s =
- let
- val (name, Con ("->", t :: _)) = parse_function s
- in (name, t) end;
-
-(* Construct Generators and Pretty Printers *)
-
-(*copied from smt_config.ML *)
-fun string_of_bool b = if b then "true" else "false"
-
-fun string_of_ref f r = f (!r) ^ " ref";
-
-val initial_content = Symtab.make
- [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
- ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
- ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
- ("unit", ("gen_unit", "fn () => \"()\"")),
- ("int", ("Generator.int", "string_of_int")),
- ("real", ("Generator.real", "string_of_real")),
- ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
- ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
- ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
- ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
- ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
-
-structure Data = Theory_Data
-(
- type T = (string * string) Symtab.table
- val empty = initial_content
- val extend = I
- fun merge data : T = Symtab.merge (K true) data
-)
-
-fun data_of ctxt tycon =
- (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
- SOME data => data
- | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
-
-val generator_of = fst oo data_of
-val printer_of = snd oo data_of
-
-fun register (ty, data) = Data.map (Symtab.update (ty, data))
-
-(*
-fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
-*)
-
-fun combine dict [] = dict
- | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
-
-fun compose_generator _ Var = "Generator.int"
- | compose_generator ctxt (Con (s, types)) =
- combine (generator_of ctxt s) (map (compose_generator ctxt) types)
- | compose_generator ctxt (Tuple t) =
- let
- fun tuple_body t = space_implode ""
- (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
- compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
- fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
- in
- "fn r0 => let " ^ tuple_body t ^
- "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
- end;
-
-fun compose_printer _ Var = "Int.toString"
- | compose_printer ctxt (Con (s, types)) =
- combine (printer_of ctxt s) (map (compose_printer ctxt) types)
- | compose_printer ctxt (Tuple t) =
- let
- fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
- fun tuple_body t = space_implode " ^ \", \" ^ "
- (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
- (t ~~ (1 upto (length t))))
- in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
-
-(*produce compilable string*)
-fun build_check ctxt name (ty, spec) =
- "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
- ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
- ^ name ^ "\", Property.pred (" ^ spec ^ "));";
-
-(*produce compilable string - non-eqtype functions*)
-(*
-fun safe_check name (ty, spec) =
- let
- val default =
- (case AList.lookup (op =) (!gen_table) "->" of
- NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
- | SOME entry => entry)
- in
- (gen_table :=
- AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
- build_check name (ty, spec) before
- gen_table := AList.update (op =) ("->", default) (!gen_table))
- end;
-*)
-
-end;
---- a/src/HOL/Spec_Check/generator.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(* Title: HOL/Spec_Check/generator.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Random generators for Isabelle/ML's types.
-*)
-
-signature GENERATOR = sig
- include BASE_GENERATOR
- (* text generators *)
- val char : char gen
- val charRange : char * char -> char gen
- val charFrom : string -> char gen
- val charByType : (char -> bool) -> char gen
- val string : (int gen * char gen) -> string gen
- val substring : string gen -> substring gen
- val cochar : (char, 'b) co
- val costring : (string, 'b) co
- val cosubstring : (substring, 'b) co
- (* integer generators *)
- val int : int gen
- val int_pos : int gen
- val int_neg : int gen
- val int_nonpos : int gen
- val int_nonneg : int gen
- val coint : (int, 'b) co
- (* real generators *)
- val real : real gen
- val real_frac : real gen
- val real_pos : real gen
- val real_neg : real gen
- val real_nonpos : real gen
- val real_nonneg : real gen
- val real_finite : real gen
- (* function generators *)
- val function_const : 'c * 'b gen -> ('a -> 'b) gen
- val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
- val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
- val unit : unit gen
- val ref' : 'a gen -> 'a Unsynchronized.ref gen
- (* more generators *)
- val term : int -> term gen
- val typ : int -> typ gen
-
- val stream : stream
-end
-
-structure Generator : GENERATOR =
-struct
-
-open Base_Generator
-
-val stream = start (new())
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-(* text *)
-
-type char = Char.char
-type string = String.string
-type substring = Substring.substring
-
-
-val char = map Char.chr (range (0, Char.maxOrd))
-fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
-
-fun charFrom s =
- choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
-
-fun charByType p = filter p char
-
-val string = vector CharVector.tabulate
-
-fun substring gen r =
- let
- val (s, r') = gen r
- val (i, r'') = range (0, String.size s) r'
- val (j, r''') = range (0, String.size s - i) r''
- in
- (Substring.substring (s, i, j), r''')
- end
-
-fun cochar c =
- if Char.ord c = 0 then variant 0
- else variant 1 o cochar (Char.chr (Char.ord c div 2))
-
-fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
-
-fun costring s = cosubstring (Substring.full s)
-
-(* integers *)
-val digit = charRange (#"0", #"9")
-val nonzero = string (lift 1, charRange (#"1", #"9"))
-fun digits' n = string (range (0, n-1), digit)
-fun digits n = map2 op^ (nonzero, digits' n)
-
-val maxDigits = 64
-val ratio = 49
-
-fun pos_or_neg f r =
- let
- val (s, r') = digits maxDigits r
- in (f (the (Int.fromString s)), r') end
-
-val int_pos = pos_or_neg I
-val int_neg = pos_or_neg Int.~
-val zero = lift 0
-
-val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
-val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
-val int = chooseL [int_nonneg, int_nonpos]
-
-fun coint n =
- if n = 0 then variant 0
- else if n < 0 then variant 1 o coint (~ n)
- else variant 2 o coint (n div 2)
-
-(* reals *)
-val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
-
-fun real_frac r =
- let val (s, r') = digits r
- in (the (Real.fromString s), r') end
-
-val {exp=minExp,...} = Real.toManExp Real.minPos
-val {exp=maxExp,...} = Real.toManExp Real.posInf
-
-val ratio = 99
-
-fun mk r =
- let
- val (a, r') = digits r
- val (b, r'') = digits r'
- val (e, r''') = range (minExp div 4, maxExp div 4) r''
- val x = String.concat [a, ".", b, "E", Int.toString e]
- in
- (the (Real.fromString x), r''')
- end
-
-val real_pos = chooseL' (List.map ((pair 1) o lift)
- [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
-
-val real_neg = map Real.~ real_pos
-
-val real_zero = Real.fromInt 0
-val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
-val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
-
-val real = chooseL [real_nonneg, real_nonpos]
-
-val real_finite = filter Real.isFinite real
-
-(*alternate list generator - uses an integer generator to determine list length*)
-fun list' int gen = vector List.tabulate (int, gen);
-
-(* more function generators *)
-
-fun function_const (_, gen2) r =
- let
- val (v, r') = gen2 r
- in (fn _ => v, r') end;
-
-fun function_strict size (gen1, gen2) r =
- let
- val (def, r') = gen2 r
- val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
- in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
-
-fun function_lazy (gen1, gen2) r =
- let
- val (initial1, r') = gen1 r
- val (initial2, internal) = gen2 r'
- val seed = Unsynchronized.ref internal
- val table = Unsynchronized.ref [(initial1, initial2)]
- fun new_entry k =
- let
- val (new_val, new_seed) = gen2 (!seed)
- val _ = seed := new_seed
- val _ = table := AList.update (op =) (k, new_val) (!table)
- in new_val end
- in
- (fn v1 =>
- case AList.lookup (op =) (!table) v1 of
- NONE => new_entry v1
- | SOME v2 => v2, r')
- end;
-
-(* unit *)
-
-fun unit r = ((), r);
-
-(* references *)
-
-fun ref' gen r =
- let val (value, r') = gen r
- in (Unsynchronized.ref value, r') end;
-
-(* types and terms *)
-
-val sort_string = selectL ["sort1", "sort2", "sort3"];
-val type_string = selectL ["TCon1", "TCon2", "TCon3"];
-val tvar_string = selectL ["a", "b", "c"];
-
-val const_string = selectL ["c1", "c2", "c3"];
-val var_string = selectL ["x", "y", "z"];
-val index = selectL [0, 1, 2, 3];
-val bound_index = selectL [0, 1, 2, 3];
-
-val sort = list (flip' (1, 2)) sort_string;
-
-fun typ n =
- let
- fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
- val tfree = map TFree (zip (tvar_string, sort))
- val tvar = map TVar (zip (zip (tvar_string, index), sort))
- in
- if n = 0 then chooseL [tfree, tvar]
- else chooseL [type' (n div 2), tfree, tvar]
- end;
-
-fun term n =
- let
- val const = map Const (zip (const_string, typ 10))
- val free = map Free (zip (var_string, typ 10))
- val var = map Var (zip (zip (var_string, index), typ 10))
- val bound = map Bound bound_index
- fun abs m = map Abs (zip3 (var_string, typ 10, term m))
- fun app m = map (op $) (zip (term m, term m))
- in
- if n = 0 then chooseL [const, free, var, bound]
- else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
- end;
-
-end--- a/src/HOL/Spec_Check/output_style.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-(* Title: HOL/Spec_Check/output_style.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Output styles for presenting Spec_Check's results.
-*)
-
-signature OUTPUT_STYLE =
-sig
- val setup : theory -> theory
-end
-
-structure Output_Style : OUTPUT_STYLE =
-struct
-
-(* perl style *)
-
-val perl_style =
- Spec_Check.register_style "Perl"
- (fn ctxt => fn tag =>
- let
- val target = Config.get ctxt Spec_Check.gen_target
- val namew = Config.get ctxt Spec_Check.column_width
- val sort_examples = Config.get ctxt Spec_Check.sort_examples
- val show_stats = Config.get ctxt Spec_Check.show_stats
- val limit = Config.get ctxt Spec_Check.examples
-
- val resultw = 8
- val countw = 20
- val allw = namew + resultw + countw + 2
-
- val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
-
- fun result ({count = 0, ...}, _) _ = "dubious"
- | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
- | result ({count, tags}, badobjs) true =
- if not (null badobjs) then "FAILED"
- else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
- else "ok"
-
- fun ratio (0, _) = "(0/0 passed)"
- | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
- | ratio (count, n) =
- "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)"
-
- fun update (stats, badobjs) donep =
- "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
- StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
- StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
-
- fun status (_, result, (stats, badobjs)) =
- if Property.failure result then warning (update (stats, badobjs) false) else ()
-
- fun prtag count (tag, n) first =
- if String.isPrefix "__" tag then ("", first)
- else
- let
- val ratio = round ((real n / real count) * 100.0)
- in
- (((if first then "" else StringCvt.padRight #" " allw "\n") ^
- StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
- false)
- end
-
- fun prtags ({count, tags} : Property.stats) =
- if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
-
- fun err badobjs =
- let
- fun iter [] _ = ()
- | iter (e :: es) k =
- (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
- StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
- iter es (k + 1))
- in
- iter (maybe_sort (take limit (map_filter I badobjs))) 0
- end
-
- fun finish (stats, badobjs) =
- if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
- else (warning (update (stats, badobjs) true); err badobjs)
- in
- {status = status, finish = finish}
- end)
-
-
-(* CM style: meshes with CM output; highlighted in sml-mode *)
-
-val cm_style =
- Spec_Check.register_style "CM"
- (fn ctxt => fn tag =>
- let
- fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
- val gen_target = Config.get ctxt Spec_Check.gen_target
- val _ = writeln ("[testing " ^ tag ^ "... ")
- fun finish ({count, ...} : Property.stats, badobjs) =
- (case (count, badobjs) of
- (0, []) => warning ("no valid cases generated]")
- | (n, []) => writeln (
- if n >= gen_target then "ok]"
- else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
- | (_, es) =>
- let
- val wd = size (string_of_int (length es))
- fun each (NONE, _) = ()
- | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
- in
- (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
- end)
- in
- {status = K (), finish = finish}
- end)
-
-
-(* setup *)
-
-val setup = perl_style #> cm_style
-
-end--- a/src/HOL/Spec_Check/property.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(* Title: HOL/Spec_Check/property.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Conditional properties that can track argument distribution.
-*)
-
-signature PROPERTY =
-sig
-
-type 'a pred = 'a -> bool
-type 'a prop
-val pred : 'a pred -> 'a prop
-val pred2 : ('a * 'b) pred -> 'b -> 'a prop
-val implies : 'a pred * 'a prop -> 'a prop
-val ==> : 'a pred * 'a pred -> 'a prop
-val trivial : 'a pred -> 'a prop -> 'a prop
-val classify : 'a pred -> string -> 'a prop -> 'a prop
-val classify' : ('a -> string option) -> 'a prop -> 'a prop
-
-(*Results*)
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
-val test : 'a prop -> 'a * stats -> result * stats
-val stats : stats
-val success : result pred
-val failure : result pred
-
-end
-
-structure Property : PROPERTY =
-struct
-
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
-type 'a pred = 'a -> bool
-type 'a prop = 'a * stats -> result * stats
-
-fun success (SOME true) = true
- | success _ = false
-
-fun failure (SOME false) = true
- | failure _ = false
-
-fun apply f x = (case try f x of NONE => SOME false | some => some)
-fun pred f (x,s) = (apply f x, s)
-fun pred2 f z = pred (fn x => f (x, z))
-
-fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
-
-fun ==> (p1, p2) = implies (p1, pred p2)
-
-fun wrap trans p (x,s) =
- let val (result,s) = p (x,s)
- in (result, trans (x, result, s)) end
-
-fun classify' f =
- wrap (fn (x, result, {tags, count}) =>
- { tags =
- if is_some result then
- (case f x of
- NONE => tags
- | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
- else tags,
- count = count })
-
-fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
-
-fun trivial cond = classify cond "trivial"
-
-fun test p =
- wrap (fn (_, result, {tags, count}) =>
- { tags = tags, count = if is_some result then count + 1 else count }) p
-
-val stats = { tags = [], count = 0 }
-
-end--- a/src/HOL/Spec_Check/random.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/Spec_Check/random.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Random number engine.
-*)
-
-signature RANDOM =
-sig
- type rand
- val new : unit -> rand
- val range : int * int -> rand -> int * rand
- val split : rand -> rand * rand
-end
-
-structure Random : RANDOM =
-struct
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
- let
- val t = a * seed
- in
- t - m * real(floor(t/m))
- end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
- if min > max then raise Domain (* TODO: raise its own error *)
- else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
-
-fun split r =
- let
- val r = r / a
- val r0 = real(floor r)
- val r1 = r - r0
- in
- (nextrand r0, nextrand r1)
- end
-
-end
--- a/src/HOL/Spec_Check/spec_check.ML Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: HOL/Spec_Check/spec_check.ML
- Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
- Author: Christopher League
-
-Specification-based testing of ML programs with random values.
-*)
-
-signature SPEC_CHECK =
-sig
- val gen_target : int Config.T
- val gen_max : int Config.T
- val examples : int Config.T
- val sort_examples : bool Config.T
- val show_stats : bool Config.T
- val column_width : int Config.T
- val style : string Config.T
-
- type output_style = Proof.context -> string ->
- {status : string option * Property.result * (Property.stats * string option list) -> unit,
- finish: Property.stats * string option list -> unit}
-
- val register_style : string -> output_style -> theory -> theory
-
- val checkGen : Proof.context ->
- 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
-
- val check_property : Proof.context -> string -> unit
-end;
-
-structure Spec_Check : SPEC_CHECK =
-struct
-
-(* configurations *)
-
-val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
-val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
-val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
-
-val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
-val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
-val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
-val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
-
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-type 'a rep = ('a -> string) option
-
-type output_style = Proof.context -> string ->
- {status: string option * Property.result * (Property.stats * string option list) -> unit,
- finish: Property.stats * string option list -> unit}
-
-fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
-
-structure Style = Theory_Data
-(
- type T = output_style Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data : T = Symtab.merge (K true) data
-)
-
-fun get_style ctxt =
- let val name = Config.get ctxt style in
- (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
- SOME style => style ctxt
- | NONE => error ("No style called " ^ quote name ^ " found"))
- end
-
-fun register_style name style = Style.map (Symtab.update (name, style))
-
-
-(* testing functions *)
-
-fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
- let
- val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
-
- val {status, finish} = get_style ctxt tag
- fun status' (obj, result, (stats, badobjs)) =
- let
- val badobjs' = if Property.failure result then obj :: badobjs else badobjs
- val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
- in badobjs' end
-
- fun try_shrink (obj, result, stats') (stats, badobjs) =
- let
- fun is_failure s =
- let val (result, stats') = Property.test prop (s, stats)
- in if Property.failure result then SOME (s, result, stats') else NONE end
- in
- case get_first is_failure (shrink obj) of
- SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
- | NONE => status' (obj, result, (stats', badobjs))
- end
-
- fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
- | iter (SOME (obj, stream), (stats, badobjs)) =
- if #count stats >= Config.get ctxt gen_target then
- finish (stats, map apply_show badobjs)
- else
- let
- val (result, stats') = Property.test prop (obj, stats)
- val badobjs' = if Property.failure result then
- try_shrink (obj, result, stats') (stats, badobjs)
- else
- status' (obj, result, (stats', badobjs))
- in iter (next stream, (stats', badobjs')) end
- in
- fn stream => iter (next stream, (s0, []))
- end
-
-fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
-fun check ctxt = check' ctxt Property.stats
-fun checks ctxt = cpsCheck ctxt Property.stats
-
-fun checkGen ctxt (gen, show) (tag, prop) =
- check' ctxt {count = 0, tags = [("__GEN", 0)]}
- (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
- cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
- (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkOne ctxt show (tag, prop) obj =
- check ctxt (List.getItem, show) (tag, prop) [obj]
-
-(*call the compiler and pass resulting type string to the parser*)
-fun determine_type ctxt s =
- let
- val return = Unsynchronized.ref "return"
- val use_context : use_context =
- {tune_source = #tune_source ML_Env.local_context,
- name_space = #name_space ML_Env.local_context,
- str_of_pos = #str_of_pos ML_Env.local_context,
- print = fn r => return := r,
- error = #error ML_Env.local_context}
- val _ =
- Context.setmp_thread_data (SOME (Context.Proof ctxt))
- (fn () => Secure.use_text use_context (0, "generated code") true s) ()
- in
- Gen_Construction.parse_pred (! return)
- end;
-
-(*call the compiler and run the test*)
-fun run_test ctxt s =
- Context.setmp_thread_data (SOME (Context.Proof ctxt))
- (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
-
-(*split input into tokens*)
-fun input_split s =
- let
- fun dot c = c = #"."
- fun space c = c = #" "
- val (head, code) = Substring.splitl (not o dot) (Substring.full s)
- in
- (String.tokens space (Substring.string head),
- Substring.string (Substring.dropl dot code))
- end;
-
-(*create the function from the input*)
-fun make_fun s =
- let
- val scan_param = Scan.one (fn s => s <> ";")
- fun parameters s = Scan.repeat1 scan_param s
- val p = $$ "ALL" |-- parameters
- val (split, code) = input_split s
- val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
- val (params, _) = Scan.finite stop p split
- in "fn (" ^ commas params ^ ") => " ^ code end;
-
-(*read input and perform the test*)
-fun gen_check_property check ctxt s =
- let
- val func = make_fun s
- val (_, ty) = determine_type ctxt func
- in run_test ctxt (check ctxt "Check" (ty, func)) end;
-
-val check_property = gen_check_property Gen_Construction.build_check
-(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
-
-(*perform test for specification function*)
-fun gen_check_property_f check ctxt s =
- let
- val (name, ty) = determine_type ctxt s
- in run_test ctxt (check ctxt name (ty, s)) end;
-
-val check_property_f = gen_check_property_f Gen_Construction.build_check
-(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
-
-end;
-
-fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
---- a/src/HOL/Tools/reflection.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/HOL/Tools/reflection.ML Fri Aug 23 21:59:29 2013 +0200
@@ -65,11 +65,13 @@
val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup @{binding reify}
- (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
- Attrib.setup @{binding reflection}
- (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
+ (Attrib.add_del add_reification_eq del_reification_eq)
+ "declare reification equations" #>
+ Attrib.setup @{binding reflection}
+ (Attrib.add_del add_correctness_thm del_correctness_thm)
+ "declare reflection correctness theorems");
fun default_reify_tac ctxt user_eqs =
let--- a/src/Pure/General/antiquote.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/General/antiquote.ML Fri Aug 23 21:59:29 2013 +0200
@@ -8,15 +8,11 @@
sig
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.range |
- Open of Position.T |
- Close of Position.T
+ Antiq of Symbol_Pos.T list * Position.range
val is_text: 'a antiquote -> bool
val reports_of: ('a -> Position.report_text list) ->
'a antiquote list -> Position.report_text list
- val check_nesting: 'a antiquote list -> unit
val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
- val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
end;
@@ -28,9 +24,7 @@
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.range |
- Open of Position.T |
- Close of Position.T;
+ Antiq of Symbol_Pos.T list * Position.range;
fun is_text (Text _) = true
| is_text _ = false;
@@ -39,27 +33,7 @@
(* reports *)
fun reports_of text =
- maps
- (fn Text x => text x
- | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]
- | Open pos => [((pos, Markup.antiq), "")]
- | Close pos => [((pos, Markup.antiq), "")]);
-
-
-(* check_nesting *)
-
-fun err_unbalanced pos =
- error ("Unbalanced antiquotation block parentheses" ^ Position.here pos);
-
-fun check_nesting antiqs =
- let
- fun check [] [] = ()
- | check [] (pos :: _) = err_unbalanced pos
- | check (Open pos :: ants) ps = check ants (pos :: ps)
- | check (Close pos :: _) [] = err_unbalanced pos
- | check (Close _ :: ants) (_ :: ps) = check ants ps
- | check (_ :: ants) ps = check ants ps;
- in check antiqs [] end;
+ maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]);
(* scan *)
@@ -72,16 +46,12 @@
val scan_txt =
$$$ "@" --| Scan.ahead (~$$$ "{") ||
- Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
- andalso Symbol.is_regular s) >> single;
+ Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
val scan_ant =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
-val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
-val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
-
in
val scan_antiq =
@@ -90,8 +60,7 @@
(Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
-fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
-val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
+val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
end;
@@ -100,7 +69,7 @@
fun read (syms, pos) =
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
- SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs)
+ SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
end;--- a/src/Pure/Isar/args.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 23 21:59:29 2013 +0200
@@ -25,9 +25,9 @@
val bang: string parser
val query_colon: string parser
val bang_colon: string parser
- val parens: ('a parser) -> 'a parser
- val bracks: ('a parser) -> 'a parser
- val mode: string -> bool context_parser
+ val parens: 'a parser -> 'a parser
+ val bracks: 'a parser -> 'a parser
+ val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val name_source: string parser
val name_source_position: (Symbol_Pos.text * Position.T) parser
@@ -145,7 +145,7 @@
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
-fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
+fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val name_source = named >> Token.source_of;--- a/src/Pure/Isar/attrib.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Aug 23 21:59:29 2013 +0200
@@ -353,8 +353,8 @@
(* rule format *)
-val rule_format = Args.mode "no_asm"
- >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
+fun rule_format true = Object_Logic.rule_format_no_asm
+ | rule_format false = Object_Logic.rule_format;
val elim_format = Thm.rule_attribute (K Tactic.make_elim);
@@ -385,7 +385,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
"internal attribute" #>
setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
@@ -410,7 +410,8 @@
"named rule parameters" #>
setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
"result put into standard form (legacy)" #>
- setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
+ setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
+ "result put into canonical rule format" #>
setup (Binding.name "elim_format") (Scan.succeed elim_format)
"destruct rule turned into elimination rule format" #>
setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
@@ -426,7 +427,7 @@
setup (Binding.name "abs_def")
(Scan.succeed (Thm.rule_attribute (fn context =>
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
- "abstract over free variables of definitional theorem"));
+ "abstract over free variables of definitional theorem");
@@ -505,7 +506,7 @@
fun setup_config declare_config binding default =
let
val (config, setup) = declare_config binding default;
- val _ = Context.>> (Context.map_theory setup);
+ val _ = Theory.setup setup;
in config end;
in
@@ -530,7 +531,7 @@
fun setup_option coerce name =
let
val config = Config.declare_option name;
- val _ = Context.>> (Context.map_theory (register_config config));
+ val _ = Theory.setup (register_config config);
in coerce config end;
in
@@ -550,7 +551,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(register_config quick_and_dirty_raw #>
register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
@@ -581,6 +582,6 @@
register_config Raw_Simplifier.simp_depth_limit_raw #>
register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
register_config Raw_Simplifier.simp_debug_raw #>
- register_config Raw_Simplifier.simp_trace_raw));
+ register_config Raw_Simplifier.simp_trace_raw);
end;--- a/src/Pure/Isar/calculation.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Aug 23 21:59:29 2013 +0200
@@ -94,7 +94,7 @@
(* concrete syntax *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
"declaration of transitivity rule" #>
Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
@@ -103,7 +103,7 @@
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
- ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
+ ((Binding.empty, symmetric_thm), [sym_add])] #> snd);
--- a/src/Pure/Isar/class.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 23 21:59:29 2013 +0200
@@ -659,11 +659,11 @@
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
default_intro_tac ctxt facts;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
"back-chain introduction rules of classes" #>
Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
- "apply some intro/elim rule"));
+ "apply some intro/elim rule");
end;
--- a/src/Pure/Isar/code.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/code.ML Fri Aug 23 21:59:29 2013 +0200
@@ -320,9 +320,8 @@
#> map_history_concluded (K true))
|> SOME;
-val _ =
- Context.>> (Context.map_theory
- (Theory.at_begin continue_history #> Theory.at_end conclude_history));
+val _ = Theory.setup
+ (Theory.at_begin continue_history #> Theory.at_end conclude_history);
(* access to data dependent on abstract executable code *)
@@ -1233,7 +1232,7 @@
(* setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
val code_attribute_parser =
@@ -1247,7 +1246,7 @@
Datatype_Interpretation.init
#> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
"declare theorems for code generation"
- end));
+ end);
end; (*struct*)
--- a/src/Pure/Isar/context_rules.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Aug 23 21:59:29 2013 +0200
@@ -198,8 +198,8 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.>> (Context.map_theory
- (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
+val _ = Theory.setup
+ (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
(* concrete syntax *)
@@ -208,7 +208,7 @@
(Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
"declaration of introduction rule" #>
Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
@@ -216,6 +216,6 @@
Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
"declaration of destruction rule" #>
Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
- "remove declaration of intro/elim/dest rule"));
+ "remove declaration of intro/elim/dest rule");
end;--- a/src/Pure/Isar/isar_cmd.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Aug 23 21:59:29 2013 +0200
@@ -265,12 +265,11 @@
Proof.goal (Toplevel.proof_of (diag_state ctxt))
handle Toplevel.UNDEF => error "No goal present";
-val _ =
- Context.>> (Context.map_theory
- (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
- (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
- ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
- (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
+val _ = Theory.setup
+ (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
+ (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
+ ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
+ (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
(* print theorems *)--- a/src/Pure/Isar/locale.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 23 21:59:29 2013 +0200
@@ -613,11 +613,11 @@
val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
- "back-chain all introduction rules of locales"));
+ "back-chain all introduction rules of locales");
(*** diagnostic commands and interfaces ***)--- a/src/Pure/Isar/method.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/method.ML Fri Aug 23 21:59:29 2013 +0200
@@ -438,7 +438,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
setup (Binding.name "-") (Scan.succeed (K insert_facts))
@@ -451,7 +451,7 @@
"repeatedly apply elimination rules" #>
setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
- setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize))
+ setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
"present local premises as object-level statements" #>
setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
@@ -470,7 +470,7 @@
setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
"ML tactic as proof method" #>
setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
- "ML tactic as raw proof method"));
+ "ML tactic as raw proof method");
(*final declarations of this structure!*)--- a/src/Pure/Isar/object_logic.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/object_logic.ML Fri Aug 23 21:59:29 2013 +0200
@@ -174,7 +174,7 @@
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
-val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
+val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
(* atomize *)
--- a/src/Pure/Isar/rule_insts.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML Fri Aug 23 21:59:29 2013 +0200
@@ -163,12 +163,12 @@
(* where: named instantiation *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "where")
(Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
(fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
- "named instantiation of theorem"));
+ "named instantiation of theorem");
(* of: positional instantiation (terms only) *)
@@ -184,11 +184,11 @@
in
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "of")
(Scan.lift insts >> (fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
- "positional instantiation of theorem"));
+ "positional instantiation of theorem");
end;
@@ -341,7 +341,7 @@
(* setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
Method.setup (Binding.name "erule_tac") eres_inst_meth
"apply rule in elimination manner (dynamic instantiation)" #>
@@ -358,7 +358,7 @@
Method.setup (Binding.name "thin_tac")
(Args.goal_spec -- Scan.lift Args.name_source >>
(fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
- "remove premise (dynamic instantiation)"));
+ "remove premise (dynamic instantiation)");
end;
--- a/src/Pure/ML/ml_antiquote.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Aug 23 21:59:29 2013 +0200
@@ -7,9 +7,7 @@
signature ML_ANTIQUOTE =
sig
val variant: string -> Proof.context -> string * Proof.context
- val macro: binding -> Proof.context context_parser -> theory -> theory
val inline: binding -> string context_parser -> theory -> theory
- val declaration: string -> binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
end;
@@ -31,37 +29,32 @@
fun variant a ctxt =
let
val names = Names.get ctxt;
- val (b, names') = Name.variant a names;
+ val (b, names') = Name.variant (Name.desymbolize false a) names;
val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
(* specific antiquotations *)
-fun macro name scan = ML_Context.add_antiq name
- (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
- (Context.Proof ctxt, fn background => (K ("", ""), background)))));
-
-fun inline name scan = ML_Context.add_antiq name
- (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
+fun inline name scan =
+ ML_Context.add_antiq name
+ (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
-fun declaration kind name scan = ML_Context.add_antiq name
- (fn _ => scan >> (fn s => fn background =>
- let
- val (a, background') =
- variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
- val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
- val body = "Isabelle." ^ a;
- in (K (env, body), background') end));
-
-val value = declaration "val";
+fun value name scan =
+ ML_Context.add_antiq name
+ (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
+ let
+ val ctxt = Context.the_proof context;
+ val (a, ctxt') = variant (Binding.name_of name) ctxt;
+ val env = "val " ^ a ^ " = " ^ s ^ ";\n";
+ val body = "Isabelle." ^ a;
+ in (Context.Proof ctxt', (K (env, body))) end)));
(** misc antiquotations **)
-val _ = Context.>> (Context.map_theory
-
+val _ = Theory.setup
(inline (Binding.name "assert")
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
@@ -92,18 +85,6 @@
inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
- macro (Binding.name "let")
- (Args.context --
- Scan.lift
- (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
- >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
-
- macro (Binding.name "note")
- (Args.context :|-- (fn ctxt =>
- Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
- >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
- >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
-
value (Binding.name "ctyp") (Args.typ >> (fn T =>
"Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
@@ -120,7 +101,7 @@
(Args.context --
Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t)))));
+ ML_Syntax.atomic (ML_Syntax.print_term t))));
(* type classes *)
@@ -130,13 +111,13 @@
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "class") (class false) #>
inline (Binding.name "class_syntax") (class true) #>
inline (Binding.name "sort")
(Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
- ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
+ ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
@@ -152,7 +133,7 @@
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
in ML_Syntax.print_string res end);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "type_name")
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
inline (Binding.name "type_abbrev")
@@ -160,7 +141,7 @@
inline (Binding.name "nonterminal")
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
inline (Binding.name "type_syntax")
- (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
+ (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
(* constants *)
@@ -173,7 +154,7 @@
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
in ML_Syntax.print_string res end);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "const_name")
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
inline (Binding.name "const_abbrev")
@@ -199,7 +180,7 @@
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
quote c ^ enclose "(" ")" (commas (replicate n "_")));
val const = Const (c, Consts.instance consts (c, Ts));
- in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
+ in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
(* outer syntax *)
@@ -209,7 +190,7 @@
(f ((name, Thy_Header.the_keyword thy name), pos)
handle ERROR msg => error (msg ^ Position.here pos)));
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(value (Binding.name "keyword")
(with_keyword
(fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
@@ -227,7 +208,7 @@
(ML_Syntax.print_list ML_Syntax.print_string)))
ML_Syntax.print_position) ((name, kind), pos))
| ((name, NONE), pos) =>
- error ("Expected command keyword " ^ quote name ^ Position.here pos)))));
+ error ("Expected command keyword " ^ quote name ^ Position.here pos))));
end;
--- a/src/Pure/ML/ml_context.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Aug 23 21:59:29 2013 +0200
@@ -23,8 +23,8 @@
val get_stored_thm: unit -> thm
val ml_store_thms: string * thm list -> unit
val ml_store_thm: string * thm -> unit
- type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
- val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
+ type antiq = Proof.context -> string * string
+ val add_antiq: binding -> antiq context_parser -> theory -> theory
val check_antiq: theory -> xstring * Position.T -> string
val trace_raw: Config.raw
val trace: bool Config.T
@@ -74,7 +74,7 @@
let
val ths' = Context.>>> (Context.map_theory_result
(Global_Theory.store_thms (Binding.name name, ths)));
- val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
+ val _ = Theory.setup (Stored_Thms.put ths');
val _ =
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
@@ -82,7 +82,7 @@
else
ML_Compiler.eval true Position.none
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
- val _ = Context.>> (Context.map_theory (Stored_Thms.put []));
+ val _ = Theory.setup (Stored_Thms.put []);
in () end;
val ml_store_thms = ml_store "ML_Context.get_stored_thms";
@@ -97,11 +97,11 @@
(* antiquotation commands *)
-type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
+type antiq = Proof.context -> string * string;
structure Antiq_Parsers = Theory_Data
(
- type T = (Position.T -> antiq context_parser) Name_Space.table;
+ type T = antiq context_parser Name_Space.table;
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
@@ -117,7 +117,7 @@
val thy = Proof_Context.theory_of ctxt;
val ((xname, _), pos) = Args.dest_src src;
val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
- in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
+ in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
(* parsing and evaluation *)
@@ -154,29 +154,22 @@
then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
+ val lex = #1 (Keyword.get_lexicons ());
+ fun no_decl _ = ([], []);
+
+ fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
+ | expand (Antiquote.Antiq (ss, range)) ctxt =
+ let
+ val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+ val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
+ in (decl', ctxt') end;
+
val ctxt =
(case opt_ctxt of
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
| SOME ctxt => Context.proof_of ctxt);
- val lex = #1 (Keyword.get_lexicons ());
- fun no_decl _ = ([], []);
-
- fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
- | expand (Antiquote.Antiq (ss, range)) (scope, background) =
- let
- val context = Stack.top scope;
- val (f, context') =
- antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
- val (decl, background') = f background;
- val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
- in (decl', (Stack.map_top (K context') scope, background')) end
- | expand (Antiquote.Open _) (scope, background) =
- (no_decl, (Stack.push scope, background))
- | expand (Antiquote.Close _) (scope, background) =
- (no_decl, (Stack.pop scope, background));
-
- val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
+ val (decls, ctxt') = fold_map expand ants ctxt;
val (ml_env, ml_body) =
decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;--- a/src/Pure/ML/ml_lex.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Aug 23 21:59:29 2013 +0200
@@ -270,7 +270,7 @@
scan_ident >> token Ident ||
scan_typevar >> token TypeVar));
-val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
fun recover msg =
(recover_char ||
@@ -304,7 +304,6 @@
(SOME (false, fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
|> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
- |> tap Antiquote.check_nesting
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);--- a/src/Pure/ML/ml_thms.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/ML/ml_thms.ML Fri Aug 23 21:59:29 2013 +0200
@@ -34,46 +34,51 @@
(* attribute source *)
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "attributes")
- (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background =>
- let
- val thy = Proof_Context.theory_of background;
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "attributes")
+ (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
+ let
+ val ctxt = Context.the_proof context;
+ val thy = Proof_Context.theory_of ctxt;
- val i = serial ();
- val srcs = map (Attrib.intern_src thy) raw_srcs;
- val _ = map (Attrib.attribute background) srcs;
- val (a, background') = background
- |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
- val ml =
- ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
- string_of_int i ^ ";\n", "Isabelle." ^ a);
- in (K ml, background') end))));
+ val i = serial ();
+ val srcs = map (Attrib.intern_src thy) raw_srcs;
+ val _ = map (Attrib.attribute ctxt) srcs;
+ val (a, ctxt') = ctxt
+ |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
+ val ml =
+ ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
+ string_of_int i ^ ";\n", "Isabelle." ^ a);
+ in (Context.Proof ctxt', K ml) end))));
(* fact references *)
-fun thm_binding kind is_single thms background =
+fun thm_binding kind is_single context thms =
let
- val initial = null (get_thmss background);
- val (name, background') = ML_Antiquote.variant kind background;
- val background'' = cons_thms ((name, is_single), thms) background';
+ val ctxt = Context.the_proof context;
+
+ val initial = null (get_thmss ctxt);
+ val (name, ctxt') = ML_Antiquote.variant kind ctxt;
+ val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
val ml_body = "Isabelle." ^ name;
- fun decl ctxt =
+ fun decl final_ctxt =
if initial then
let
- val binds = get_thmss ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
+ val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
in (ml_env, ml_body) end
else ("", ml_body);
- in (decl, background'') end;
+ in (Context.Proof ctxt'', decl) end;
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "thm") (K (Attrib.thm >> (thm_binding "thm" true o single))) #>
- ML_Context.add_antiq (Binding.name "thms") (K (Attrib.thms >> thm_binding "thms" false))));
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "thm")
+ (Scan.depend (fn context =>
+ Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
+ ML_Context.add_antiq (Binding.name "thms")
+ (Scan.depend (fn context =>
+ Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
(* ad-hoc goals *)
@@ -82,27 +87,28 @@
val by = Args.$$$ "by";
val goal = Scan.unless (by || and_) Args.name_source;
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "lemma")
- (fn _ => Args.context -- Args.mode "open" --
- Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
- (by |-- Method.parse -- Scan.option Method.parse)) >>
- (fn ((ctxt, is_open), (raw_propss, methods)) =>
- let
- val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
- val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
- fun after_qed res goal_ctxt =
- Proof_Context.put_thms false (Auto_Bind.thisN,
- SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "lemma")
+ (Scan.depend (fn context =>
+ Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
+ (by |-- Method.parse -- Scan.option Method.parse) >>
+ (fn ((is_open, raw_propss), methods) =>
+ let
+ val ctxt = Context.proof_of context;
- val ctxt' = ctxt
- |> Proof.theorem NONE after_qed propss
- |> Proof.global_terminal_proof methods;
- val thms =
- Proof_Context.get_fact ctxt'
- (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
- in thm_binding "lemma" (length (flat propss) = 1) thms end))));
+ val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+ val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
+ fun after_qed res goal_ctxt =
+ Proof_Context.put_thms false (Auto_Bind.thisN,
+ SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+
+ val ctxt' = ctxt
+ |> Proof.theorem NONE after_qed propss
+ |> Proof.global_terminal_proof methods;
+ val thms =
+ Proof_Context.get_fact ctxt'
+ (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
+ in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
end;
--- a/src/Pure/Proof/extraction.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 23 21:59:29 2013 +0200
@@ -422,7 +422,7 @@
(** Pure setup **)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(add_types [("prop", ([], NONE))] #>
add_typeof_eqns
@@ -469,7 +469,7 @@
Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
"specify theorems to be expanded during extraction" #>
Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
- "specify definitions to be expanded during extraction"));
+ "specify definitions to be expanded during extraction");
(**** extract program ****)--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Aug 23 21:59:29 2013 +0200
@@ -190,7 +190,7 @@
in rew' #> Option.map (rpair Proofterm.no_skel) end;
fun rprocs b = [rew b];
-val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
+val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
(**** apply rewriting function to all terms in proof ****)
--- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 21:59:29 2013 +0200
@@ -807,14 +807,14 @@
(* setup translations *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Sign.parse_ast_translation
[("_context_const", const_ast_tr true),
("_context_xconst", const_ast_tr false)] #>
Sign.typed_print_translation
[("_type_prop", type_prop_tr'),
("\\<^const>TYPE", type_tr'),
- ("_type_constraint_", type_constraint_tr')]));
+ ("_type_constraint_", type_constraint_tr')]);
--- a/src/Pure/Thy/latex.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/latex.ML Fri Aug 23 21:59:29 2013 +0200
@@ -99,9 +99,7 @@
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
| Antiquote.Antiq (ss, _) =>
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
- (output_symbols (map Symbol_Pos.symbol ss))
- | Antiquote.Open _ => "{\\isaantiqopen}"
- | Antiquote.Close _ => "{\\isaantiqclose}");
+ (output_symbols (map Symbol_Pos.symbol ss)));
end;
--- a/src/Pure/Thy/present.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/present.ML Fri Aug 23 21:59:29 2013 +0200
@@ -52,8 +52,8 @@
fun merge _ = empty;
);
-val _ = Context.>> (Context.map_theory
- (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
+val _ = Theory.setup
+ (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
val session_name = #name o Browser_Info.get;
val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;--- a/src/Pure/Thy/rail.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/rail.ML Fri Aug 23 21:59:29 2013 +0200
@@ -263,11 +263,10 @@
in
-val _ =
- Context.>> (Context.map_theory
- (Thy_Output.antiquotation (Binding.name "rail")
- (Scan.lift (Parse.source_position Parse.string))
- (fn {state, ...} => output_rules state o read)));
+val _ = Theory.setup
+ (Thy_Output.antiquotation (Binding.name "rail")
+ (Scan.lift (Parse.source_position Parse.string))
+ (fn {state, ...} => output_rules state o read));
end;
--- a/src/Pure/Thy/term_style.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/term_style.ML Fri Aug 23 21:59:29 2013 +0200
@@ -91,11 +91,11 @@
| sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
| sub_term t = t;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup "lhs" (style_lhs_rhs fst) #>
setup "rhs" (style_lhs_rhs snd) #>
setup "prem" style_prem #>
setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup "sub" (Scan.succeed (K sub_term))));
+ setup "sub" (Scan.succeed (K sub_term)));
end;
--- a/src/Pure/Thy/thy_load.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Fri Aug 23 21:59:29 2013 +0200
@@ -275,9 +275,8 @@
(* document antiquotation *)
-val _ =
- Context.>> (Context.map_theory
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+val _ = Theory.setup
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
(fn {context = ctxt, ...} => fn (name, pos) =>
let
val dir = master_directory (Proof_Context.theory_of ctxt);
@@ -290,7 +289,7 @@
space_explode "/" name
|> map Thy_Output.verb_text
|> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
- end)));
+ end));
(* global master path *)--- a/src/Pure/Thy/thy_output.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 23 21:59:29 2013 +0200
@@ -178,9 +178,7 @@
fun eval_antiquote lex state (txt, pos) =
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
- | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
- | expand (Antiquote.Open _) = ""
- | expand (Antiquote.Close _) = "";
+ | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
@@ -444,25 +442,24 @@
(* options *)
-val _ =
- Context.>> (Context.map_theory
- (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
- add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
- add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
- add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
- add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
- add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
- add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
- add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
- add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
- add_option (Binding.name "display") (Config.put display o boolean) #>
- add_option (Binding.name "break") (Config.put break o boolean) #>
- add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
- add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
- add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
- add_option (Binding.name "indent") (Config.put indent o integer) #>
- add_option (Binding.name "source") (Config.put source o boolean) #>
- add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
+val _ = Theory.setup
+ (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
+ add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
+ add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
+ add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
+ add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
+ add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
+ add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
+ add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
+ add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
+ add_option (Binding.name "display") (Config.put display o boolean) #>
+ add_option (Binding.name "break") (Config.put break o boolean) #>
+ add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
+ add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
+ add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+ add_option (Binding.name "indent") (Config.put indent o integer) #>
+ add_option (Binding.name "source") (Config.put source o boolean) #>
+ add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
(* basic pretty printing *)
@@ -566,22 +563,21 @@
in
-val _ =
- Context.>> (Context.map_theory
- (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
- basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
- basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
- basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
- basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
- basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
- basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
- basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
- basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
- basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
- basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory));
+val _ = Theory.setup
+ (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+ basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
+ basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
+ basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
+ basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
+ basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+ basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+ basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
+ basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
+ basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
+ basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+ basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
+ basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
+ basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
end;
@@ -602,10 +598,9 @@
in
-val _ =
- Context.>> (Context.map_theory
- (goal_state (Binding.name "goals") true #>
- goal_state (Binding.name "subgoals") false));
+val _ = Theory.setup
+ (goal_state (Binding.name "goals") true #>
+ goal_state (Binding.name "subgoals") false);
end;
@@ -614,9 +609,8 @@
val _ = Keyword.define ("by", NONE); (*overlap with command category*)
-val _ =
- Context.>> (Context.map_theory
- (antiquotation (Binding.name "lemma")
+val _ = Theory.setup
+ (antiquotation (Binding.name "lemma")
(Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
(fn {source, context, ...} => fn (prop, methods) =>
let
@@ -626,7 +620,7 @@
val _ = context
|> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
- in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
+ in output context (maybe_pretty_source pretty_term context prop_src [prop]) end));
(* ML text *)
@@ -651,20 +645,19 @@
in
-val _ =
- Context.>> (Context.map_theory
- (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
- ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
- ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_struct")
- (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+val _ = Theory.setup
+ (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
+ ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
+ ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
+ ml_text (Binding.name "ML_struct")
+ (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
- ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
- (fn pos => fn txt =>
- ML_Lex.read Position.none ("ML_Env.check_functor " ^
- ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
+ ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
+ (fn pos => fn txt =>
+ ML_Lex.read Position.none ("ML_Env.check_functor " ^
+ ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
- ml_text (Binding.name "ML_text") (K (K []))));
+ ml_text (Binding.name "ML_text") (K (K [])));
end;
--- a/src/Pure/axclass.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/axclass.ML Fri Aug 23 21:59:29 2013 +0200
@@ -264,9 +264,8 @@
else SOME (map_proven_arities (K arities') thy)
end;
-val _ = Context.>> (Context.map_theory
- (Theory.at_begin complete_classrels #>
- Theory.at_begin complete_arities));
+val _ = Theory.setup
+ (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
val _ = Proofterm.install_axclass_proofs
{classrel_proof = Thm.proof_of oo the_classrel,--- a/src/Pure/pure_thy.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/pure_thy.ML Fri Aug 23 21:59:29 2013 +0200
@@ -56,7 +56,7 @@
val token_markers =
["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
Sign.add_types_global
@@ -221,6 +221,6 @@
#> Sign.hide_const false "Pure.conjunction"
#> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
#> fold (fn (a, prop) =>
- snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
+ snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
end;--- a/src/Pure/simplifier.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/simplifier.ML Fri Aug 23 21:59:29 2013 +0200
@@ -129,10 +129,10 @@
(* global simprocs *)
fun Addsimprocs args =
- Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt addsimprocs args)));
+ Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
fun Delsimprocs args =
- Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt delsimprocs args)));
+ Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
@@ -154,13 +154,11 @@
fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
val the_simproc = Name_Space.get o get_simprocs;
-val _ =
- Context.>> (Context.map_theory
- (ML_Antiquote.value (Binding.name "simproc")
- (Args.context -- Scan.lift (Parse.position Args.name)
- >> (fn (ctxt, name) =>
- "Simplifier.the_simproc ML_context " ^
- ML_Syntax.print_string (check_simproc ctxt name)))));
+val _ = Theory.setup
+ (ML_Antiquote.value (Binding.name "simproc")
+ (Args.context -- Scan.lift (Parse.position Args.name)
+ >> (fn (ctxt, name) =>
+ "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
(* define simprocs *)
@@ -327,14 +325,14 @@
(* setup attributes *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
"declaration of Simplifier congruence rule" #>
Attrib.setup (Binding.name "simproc") simproc_att
"declaration of simplification procedures" #>
- Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
+ Attrib.setup (Binding.name "simplified") simplified "simplified rule");
--- a/src/Pure/theory.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Pure/theory.ML Fri Aug 23 21:59:29 2013 +0200
@@ -15,6 +15,7 @@
val merge: theory * theory -> theory
val merge_list: theory list -> theory
val requires: theory -> string -> string -> unit
+ val setup: (theory -> theory) -> unit
val get_markup: theory -> Markup.T
val axiom_space: theory -> Name_Space.T
val axiom_table: theory -> term Symtab.table
@@ -59,6 +60,8 @@
if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
+fun setup f = Context.>> (Context.map_theory f);
+
(** datatype thy **)--- a/src/Tools/Code/code_runtime.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Aug 23 21:59:29 2013 +0200
@@ -51,14 +51,14 @@
datatype truth = Holds;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Code_Target.extend_target (target, (Code_ML.target_SML, K I))
#> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
#> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
#> Code_Target.add_reserved target this
- #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
+ #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
(*avoid further pervasive infix names*)
val trace = Unsynchronized.ref false;
@@ -247,12 +247,15 @@
in
-fun ml_code_antiq raw_const background =
+fun ml_code_antiq context raw_const =
let
- val const = Code.check_const (Proof_Context.theory_of background) raw_const;
- val is_first = is_first_occ background;
- val background' = register_const const background;
- in (print_code is_first const, background') end;
+ val ctxt = Context.the_proof context;
+ val thy = Proof_Context.theory_of ctxt;
+
+ val const = Code.check_const thy raw_const;
+ val is_first = is_first_occ ctxt;
+ val ctxt' = register_const const ctxt;
+ in (Context.Proof ctxt', print_code is_first const) end;
end; (*local*)
@@ -342,9 +345,9 @@
(** Isar setup **)
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
+val _ = Theory.setup
+ (ML_Context.add_antiq @{binding code}
+ (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
local
@@ -383,7 +386,7 @@
fun notify_val (string, value) =
let
val _ = #enterVal ML_Env.name_space (string, value);
- val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
+ val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
in () end;
fun abort _ = error "Only value bindings allowed.";--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/ROOT Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,9 @@
+session WWW_Find in WWW_Find = Pure +
+ theories [condition = ISABELLE_POLYML] WWW_Find
+
+session Spec_Check in Spec_Check = Pure +
+ theories
+ Spec_Check
+ theories [condition = ISABELLE_POLYML]
+ Examples
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/Examples.thy Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,83 @@
+theory Examples
+imports Spec_Check
+begin
+
+section {* List examples *}
+
+ML_command {*
+check_property "ALL xs. rev xs = xs";
+*}
+
+ML_command {*
+check_property "ALL xs. rev (rev xs) = xs";
+*}
+
+
+section {* AList Specification *}
+
+ML_command {*
+(* map_entry applies the function to the element *)
+check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
+*}
+
+ML_command {*
+(* update always results in an entry *)
+check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
+*}
+
+ML_command {*
+(* update always writes the value *)
+check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
+*}
+
+ML_command {*
+(* default always results in an entry *)
+check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
+*}
+
+ML_command {*
+(* delete always removes the entry *)
+check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
+*}
+
+ML_command {*
+(* default writes the entry iff it didn't exist *)
+check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
+*}
+
+section {* Examples on Types and Terms *}
+
+ML_command {*
+check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
+*}
+
+ML_command {*
+check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
+*}
+
+
+text {* One would think this holds: *}
+
+ML_command {*
+check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
+*}
+
+text {* But it only holds with this precondition: *}
+
+ML_command {*
+check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
+*}
+
+section {* Some surprises *}
+
+ML_command {*
+check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
+*}
+
+
+ML_command {*
+val thy = @{theory};
+check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
+*}
+
+end--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/README Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,47 @@
+This is a Quickcheck tool for Isabelle/ML.
+
+Authors
+
+ Lukas Bulwahn
+ Nicolai Schaffroth
+
+Quick Usage
+
+ - Import Spec_Check.thy in your development
+ - Look at examples in Examples.thy
+ - write specifications with the ML invocation
+ check_property "ALL x. P x"
+
+Notes
+
+Our specification-based testing tool originated from Christopher League's
+QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
+provides a rich and uniform ML platform (called Isabelle/ML), this
+testing tools is very different than the one for a typical ML developer.
+
+1. Isabelle/ML provides common data structures, which we can use in the
+tool's implementation for storing data and printing output.
+
+2. The implementation in Isabelle that will be checked with this tool
+commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
+but they do not use other integer types in ML, such as ML's Int.int,
+Word.word and others.
+
+3. As Isabelle can run heavily in parallel, we avoid reference types.
+
+4. Isabelle has special naming conventions and documentation of source
+code is only minimal to avoid parroting.
+
+Next steps:
+ - Remove all references and store the neccessary random seed in the
+ Isabelle's context.
+ - Simplify some existing random generators.
+ The original ones from Christopher League are so complicated to
+ support many integer types uniformly.
+
+License
+
+ The source code originated from Christopher League's QCheck, which is
+ licensed under the 2-clause BSD license. The current source code is
+ licensed under the compatible 3-clause BSD license of Isabelle.
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/Spec_Check.thy Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,13 @@
+theory Spec_Check
+imports Pure
+begin
+
+ML_file "random.ML"
+ML_file "property.ML"
+ML_file "base_generator.ML"
+ML_file "generator.ML"
+ML_file "gen_construction.ML"
+ML_file "spec_check.ML"
+ML_file "output_style.ML"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/base_generator.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,201 @@
+(* Title: Tools/Spec_Check/base_generator.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Basic random generators.
+*)
+
+signature BASE_GENERATOR =
+sig
+
+type rand
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+val new : unit -> rand
+val range : int * int -> rand -> int * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+val lift : 'a -> 'a gen
+val select : 'a vector -> 'a gen
+val choose : 'a gen vector -> 'a gen
+val choose' : (int * 'a gen) vector -> 'a gen
+val selectL : 'a list -> 'a gen
+val chooseL : 'a gen list -> 'a gen
+val chooseL' : (int * 'a gen) list -> 'a gen
+val filter : ('a -> bool) -> 'a gen -> 'a gen
+
+val zip : ('a gen * 'b gen) -> ('a * 'b) gen
+val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
+val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
+val map : ('a -> 'b) -> 'a gen -> 'b gen
+val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
+val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
+val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
+
+val flip : bool gen
+val flip' : int * int -> bool gen
+
+val list : bool gen -> 'a gen -> 'a list gen
+val option : bool gen -> 'a gen -> 'a option gen
+val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
+
+val variant : (int, 'b) co
+val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
+val cobool : (bool, 'b) co
+val colist : ('a, 'b) co -> ('a list, 'b) co
+val coopt : ('a, 'b) co -> ('a option, 'b) co
+
+type stream
+val start : rand -> stream
+val limit : int -> 'a gen -> ('a, stream) reader
+
+end
+
+structure Base_Generator : BASE_GENERATOR =
+struct
+
+(* random number engine *)
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+ let
+ val t = a * seed
+ in
+ t - m * real (floor (t / m))
+ end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+ if min > max then raise Domain (* TODO: raise its own error *)
+ else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
+
+fun split r =
+ let
+ val r = r / a
+ val r0 = real (floor r)
+ val r1 = r - r0
+ in
+ (nextrand r0, nextrand r1)
+ end
+
+(* generators *)
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+fun lift obj r = (obj, r)
+
+local (* Isabelle does not use vectors? *)
+ fun explode ((freq, gen), acc) =
+ List.tabulate (freq, fn _ => gen) @ acc
+in
+ fun choose v r =
+ let val (i, r) = range(0, Vector.length v - 1) r
+ in Vector.sub (v, i) r end
+ fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
+ fun select v = choose (Vector.map lift v)
+end
+
+fun chooseL l = choose (Vector.fromList l)
+fun chooseL' l = choose' (Vector.fromList l)
+fun selectL l = select (Vector.fromList l)
+
+fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
+
+fun zip3 (g1, g2, g3) =
+ zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
+
+fun zip4 (g1, g2, g3, g4) =
+ zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
+
+fun map f g = apfst f o g
+
+fun map2 f = map f o zip
+fun map3 f = map f o zip3
+fun map4 f = map f o zip4
+
+fun filter p gen r =
+ let
+ fun loop (x, r) = if p x then (x, r) else loop (gen r)
+ in
+ loop (gen r)
+ end
+
+val flip = selectL [true, false]
+fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
+
+fun list flip g r =
+ case flip r of
+ (true, r) => ([], r)
+ | (false, r) =>
+ let
+ val (x,r) = g r
+ val (xs,r) = list flip g r
+ in (x::xs, r) end
+
+fun option flip g r =
+ case flip r of
+ (true, r) => (NONE, r)
+ | (false, r) => map SOME g r
+
+fun vector tabulate (int, elem) r =
+ let
+ val (n, r) = int r
+ val p = Unsynchronized.ref r
+ fun g _ =
+ let
+ val (x,r) = elem(!p)
+ in x before p := r end
+ in
+ (tabulate(n, g), !p)
+ end
+
+type stream = rand Unsynchronized.ref * int
+
+fun start r = (Unsynchronized.ref r, 0)
+
+fun limit max gen =
+ let
+ fun next (p, i) =
+ if i >= max then NONE
+ else
+ let val (x, r) = gen(!p)
+ in SOME(x, (p, i+1)) before p := r end
+ in
+ next
+ end
+
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+fun variant v g r =
+ let
+ fun nth (i, r) =
+ let val (r1, r2) = split r
+ in if i = 0 then r1 else nth (i-1, r2) end
+ in
+ g (nth (v, r))
+ end
+
+fun arrow (cogen, gen) r =
+ let
+ val (r1, r2) = split r
+ fun g x = fst (cogen x gen r1)
+ in (g, r2) end
+
+fun cobool false = variant 0
+ | cobool true = variant 1
+
+fun colist _ [] = variant 0
+ | colist co (x::xs) = variant 1 o co x o colist co xs
+
+fun coopt _ NONE = variant 0
+ | coopt co (SOME x) = variant 1 o co x
+
+end
+--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/gen_construction.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,179 @@
+(* Title: Tools/Spec_Check/gen_construction.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Constructing generators and pretty printing function for complex types.
+*)
+
+signature GEN_CONSTRUCTION =
+sig
+ val register : string * (string * string) -> theory -> theory
+ type mltype
+ val parse_pred : string -> string * mltype
+ val build_check : Proof.context -> string -> mltype * string -> string
+ (*val safe_check : string -> mltype * string -> string*)
+ val string_of_bool : bool -> string
+ val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
+end;
+
+structure Gen_Construction : GEN_CONSTRUCTION =
+struct
+
+(* Parsing ML types *)
+
+datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
+
+(*Split string into tokens for parsing*)
+fun split s =
+ let
+ fun split_symbol #"(" = "( "
+ | split_symbol #")" = " )"
+ | split_symbol #"," = " ,"
+ | split_symbol #":" = " :"
+ | split_symbol c = Char.toString c
+ fun is_space c = c = #" "
+ in String.tokens is_space (String.translate split_symbol s) end;
+
+(*Accept anything that is not a recognized symbol*)
+val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
+
+(*Turn a type list into a nested Con*)
+fun make_con [] = raise Empty
+ | make_con [c] = c
+ | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
+
+(*Parse a type*)
+fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
+
+and parse_type_arg s = (parse_tuple || parse_type_single) s
+
+and parse_type_single s = (parse_con || parse_type_basic) s
+
+and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
+
+and parse_list s =
+ ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
+
+and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
+
+and parse_con s = ((parse_con_nest
+ || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
+ || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
+ >> (make_con o rev)) s
+
+and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
+
+and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
+
+and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
+ >> (fn (t, tl) => Tuple (t :: tl))) s;
+
+(*Parse entire type + name*)
+fun parse_function s =
+ let
+ val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
+ val (name, ty) = p (split s)
+ val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+ val (typ, _) = Scan.finite stop parse_type ty
+ in (name, typ) end;
+
+(*Create desired output*)
+fun parse_pred s =
+ let
+ val (name, Con ("->", t :: _)) = parse_function s
+ in (name, t) end;
+
+(* Construct Generators and Pretty Printers *)
+
+(*copied from smt_config.ML *)
+fun string_of_bool b = if b then "true" else "false"
+
+fun string_of_ref f r = f (!r) ^ " ref";
+
+val initial_content = Symtab.make
+ [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
+ ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
+ ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
+ ("unit", ("gen_unit", "fn () => \"()\"")),
+ ("int", ("Generator.int", "string_of_int")),
+ ("real", ("Generator.real", "string_of_real")),
+ ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
+ ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
+ ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
+ ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
+ ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
+
+structure Data = Theory_Data
+(
+ type T = (string * string) Symtab.table
+ val empty = initial_content
+ val extend = I
+ fun merge data : T = Symtab.merge (K true) data
+)
+
+fun data_of ctxt tycon =
+ (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
+ SOME data => data
+ | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
+
+val generator_of = fst oo data_of
+val printer_of = snd oo data_of
+
+fun register (ty, data) = Data.map (Symtab.update (ty, data))
+
+(*
+fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
+*)
+
+fun combine dict [] = dict
+ | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
+
+fun compose_generator _ Var = "Generator.int"
+ | compose_generator ctxt (Con (s, types)) =
+ combine (generator_of ctxt s) (map (compose_generator ctxt) types)
+ | compose_generator ctxt (Tuple t) =
+ let
+ fun tuple_body t = space_implode ""
+ (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
+ compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
+ fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+ in
+ "fn r0 => let " ^ tuple_body t ^
+ "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
+ end;
+
+fun compose_printer _ Var = "Int.toString"
+ | compose_printer ctxt (Con (s, types)) =
+ combine (printer_of ctxt s) (map (compose_printer ctxt) types)
+ | compose_printer ctxt (Tuple t) =
+ let
+ fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+ fun tuple_body t = space_implode " ^ \", \" ^ "
+ (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
+ (t ~~ (1 upto (length t))))
+ in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
+
+(*produce compilable string*)
+fun build_check ctxt name (ty, spec) =
+ "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+ ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
+ ^ name ^ "\", Property.pred (" ^ spec ^ "));";
+
+(*produce compilable string - non-eqtype functions*)
+(*
+fun safe_check name (ty, spec) =
+ let
+ val default =
+ (case AList.lookup (op =) (!gen_table) "->" of
+ NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+ | SOME entry => entry)
+ in
+ (gen_table :=
+ AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
+ build_check name (ty, spec) before
+ gen_table := AList.update (op =) ("->", default) (!gen_table))
+ end;
+*)
+
+end;
+--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generator.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,235 @@
+(* Title: Tools/Spec_Check/generator.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Random generators for Isabelle/ML's types.
+*)
+
+signature GENERATOR = sig
+ include BASE_GENERATOR
+ (* text generators *)
+ val char : char gen
+ val charRange : char * char -> char gen
+ val charFrom : string -> char gen
+ val charByType : (char -> bool) -> char gen
+ val string : (int gen * char gen) -> string gen
+ val substring : string gen -> substring gen
+ val cochar : (char, 'b) co
+ val costring : (string, 'b) co
+ val cosubstring : (substring, 'b) co
+ (* integer generators *)
+ val int : int gen
+ val int_pos : int gen
+ val int_neg : int gen
+ val int_nonpos : int gen
+ val int_nonneg : int gen
+ val coint : (int, 'b) co
+ (* real generators *)
+ val real : real gen
+ val real_frac : real gen
+ val real_pos : real gen
+ val real_neg : real gen
+ val real_nonpos : real gen
+ val real_nonneg : real gen
+ val real_finite : real gen
+ (* function generators *)
+ val function_const : 'c * 'b gen -> ('a -> 'b) gen
+ val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
+ val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
+ val unit : unit gen
+ val ref' : 'a gen -> 'a Unsynchronized.ref gen
+ (* more generators *)
+ val term : int -> term gen
+ val typ : int -> typ gen
+
+ val stream : stream
+end
+
+structure Generator : GENERATOR =
+struct
+
+open Base_Generator
+
+val stream = start (new())
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+(* text *)
+
+type char = Char.char
+type string = String.string
+type substring = Substring.substring
+
+
+val char = map Char.chr (range (0, Char.maxOrd))
+fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
+
+fun charFrom s =
+ choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
+
+fun charByType p = filter p char
+
+val string = vector CharVector.tabulate
+
+fun substring gen r =
+ let
+ val (s, r') = gen r
+ val (i, r'') = range (0, String.size s) r'
+ val (j, r''') = range (0, String.size s - i) r''
+ in
+ (Substring.substring (s, i, j), r''')
+ end
+
+fun cochar c =
+ if Char.ord c = 0 then variant 0
+ else variant 1 o cochar (Char.chr (Char.ord c div 2))
+
+fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
+
+fun costring s = cosubstring (Substring.full s)
+
+(* integers *)
+val digit = charRange (#"0", #"9")
+val nonzero = string (lift 1, charRange (#"1", #"9"))
+fun digits' n = string (range (0, n-1), digit)
+fun digits n = map2 op^ (nonzero, digits' n)
+
+val maxDigits = 64
+val ratio = 49
+
+fun pos_or_neg f r =
+ let
+ val (s, r') = digits maxDigits r
+ in (f (the (Int.fromString s)), r') end
+
+val int_pos = pos_or_neg I
+val int_neg = pos_or_neg Int.~
+val zero = lift 0
+
+val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
+val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
+val int = chooseL [int_nonneg, int_nonpos]
+
+fun coint n =
+ if n = 0 then variant 0
+ else if n < 0 then variant 1 o coint (~ n)
+ else variant 2 o coint (n div 2)
+
+(* reals *)
+val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
+
+fun real_frac r =
+ let val (s, r') = digits r
+ in (the (Real.fromString s), r') end
+
+val {exp=minExp,...} = Real.toManExp Real.minPos
+val {exp=maxExp,...} = Real.toManExp Real.posInf
+
+val ratio = 99
+
+fun mk r =
+ let
+ val (a, r') = digits r
+ val (b, r'') = digits r'
+ val (e, r''') = range (minExp div 4, maxExp div 4) r''
+ val x = String.concat [a, ".", b, "E", Int.toString e]
+ in
+ (the (Real.fromString x), r''')
+ end
+
+val real_pos = chooseL' (List.map ((pair 1) o lift)
+ [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
+
+val real_neg = map Real.~ real_pos
+
+val real_zero = Real.fromInt 0
+val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
+val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
+
+val real = chooseL [real_nonneg, real_nonpos]
+
+val real_finite = filter Real.isFinite real
+
+(*alternate list generator - uses an integer generator to determine list length*)
+fun list' int gen = vector List.tabulate (int, gen);
+
+(* more function generators *)
+
+fun function_const (_, gen2) r =
+ let
+ val (v, r') = gen2 r
+ in (fn _ => v, r') end;
+
+fun function_strict size (gen1, gen2) r =
+ let
+ val (def, r') = gen2 r
+ val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
+ in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
+
+fun function_lazy (gen1, gen2) r =
+ let
+ val (initial1, r') = gen1 r
+ val (initial2, internal) = gen2 r'
+ val seed = Unsynchronized.ref internal
+ val table = Unsynchronized.ref [(initial1, initial2)]
+ fun new_entry k =
+ let
+ val (new_val, new_seed) = gen2 (!seed)
+ val _ = seed := new_seed
+ val _ = table := AList.update (op =) (k, new_val) (!table)
+ in new_val end
+ in
+ (fn v1 =>
+ case AList.lookup (op =) (!table) v1 of
+ NONE => new_entry v1
+ | SOME v2 => v2, r')
+ end;
+
+(* unit *)
+
+fun unit r = ((), r);
+
+(* references *)
+
+fun ref' gen r =
+ let val (value, r') = gen r
+ in (Unsynchronized.ref value, r') end;
+
+(* types and terms *)
+
+val sort_string = selectL ["sort1", "sort2", "sort3"];
+val type_string = selectL ["TCon1", "TCon2", "TCon3"];
+val tvar_string = selectL ["a", "b", "c"];
+
+val const_string = selectL ["c1", "c2", "c3"];
+val var_string = selectL ["x", "y", "z"];
+val index = selectL [0, 1, 2, 3];
+val bound_index = selectL [0, 1, 2, 3];
+
+val sort = list (flip' (1, 2)) sort_string;
+
+fun typ n =
+ let
+ fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
+ val tfree = map TFree (zip (tvar_string, sort))
+ val tvar = map TVar (zip (zip (tvar_string, index), sort))
+ in
+ if n = 0 then chooseL [tfree, tvar]
+ else chooseL [type' (n div 2), tfree, tvar]
+ end;
+
+fun term n =
+ let
+ val const = map Const (zip (const_string, typ 10))
+ val free = map Free (zip (var_string, typ 10))
+ val var = map Var (zip (zip (var_string, index), typ 10))
+ val bound = map Bound bound_index
+ fun abs m = map Abs (zip3 (var_string, typ 10, term m))
+ fun app m = map (op $) (zip (term m, term m))
+ in
+ if n = 0 then chooseL [const, free, var, bound]
+ else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
+ end;
+
+end--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_style.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,113 @@
+(* Title: Tools/Spec_Check/output_style.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Output styles for presenting Spec_Check's results.
+*)
+
+structure Output_Style : sig end =
+struct
+
+(* perl style *)
+
+val perl_style =
+ Spec_Check.register_style "Perl"
+ (fn ctxt => fn tag =>
+ let
+ val target = Config.get ctxt Spec_Check.gen_target
+ val namew = Config.get ctxt Spec_Check.column_width
+ val sort_examples = Config.get ctxt Spec_Check.sort_examples
+ val show_stats = Config.get ctxt Spec_Check.show_stats
+ val limit = Config.get ctxt Spec_Check.examples
+
+ val resultw = 8
+ val countw = 20
+ val allw = namew + resultw + countw + 2
+
+ val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
+
+ fun result ({count = 0, ...}, _) _ = "dubious"
+ | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
+ | result ({count, tags}, badobjs) true =
+ if not (null badobjs) then "FAILED"
+ else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
+ else "ok"
+
+ fun ratio (0, _) = "(0/0 passed)"
+ | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
+ | ratio (count, n) =
+ "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)"
+
+ fun update (stats, badobjs) donep =
+ "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
+ StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
+ StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
+
+ fun status (_, result, (stats, badobjs)) =
+ if Property.failure result then warning (update (stats, badobjs) false) else ()
+
+ fun prtag count (tag, n) first =
+ if String.isPrefix "__" tag then ("", first)
+ else
+ let
+ val ratio = round ((real n / real count) * 100.0)
+ in
+ (((if first then "" else StringCvt.padRight #" " allw "\n") ^
+ StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
+ false)
+ end
+
+ fun prtags ({count, tags} : Property.stats) =
+ if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
+
+ fun err badobjs =
+ let
+ fun iter [] _ = ()
+ | iter (e :: es) k =
+ (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
+ StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
+ iter es (k + 1))
+ in
+ iter (maybe_sort (take limit (map_filter I badobjs))) 0
+ end
+
+ fun finish (stats, badobjs) =
+ if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
+ else (warning (update (stats, badobjs) true); err badobjs)
+ in
+ {status = status, finish = finish}
+ end)
+
+val _ = Theory.setup perl_style;
+
+
+(* CM style: meshes with CM output; highlighted in sml-mode *)
+
+val cm_style =
+ Spec_Check.register_style "CM"
+ (fn ctxt => fn tag =>
+ let
+ fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
+ val gen_target = Config.get ctxt Spec_Check.gen_target
+ val _ = writeln ("[testing " ^ tag ^ "... ")
+ fun finish ({count, ...} : Property.stats, badobjs) =
+ (case (count, badobjs) of
+ (0, []) => warning ("no valid cases generated]")
+ | (n, []) => writeln (
+ if n >= gen_target then "ok]"
+ else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
+ | (_, es) =>
+ let
+ val wd = size (string_of_int (length es))
+ fun each (NONE, _) = ()
+ | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+ in
+ (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+ end)
+ in
+ {status = K (), finish = finish}
+ end)
+
+val _ = Theory.setup cm_style;
+
+end--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/property.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,77 @@
+(* Title: Tools/Spec_Check/property.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Conditional properties that can track argument distribution.
+*)
+
+signature PROPERTY =
+sig
+
+type 'a pred = 'a -> bool
+type 'a prop
+val pred : 'a pred -> 'a prop
+val pred2 : ('a * 'b) pred -> 'b -> 'a prop
+val implies : 'a pred * 'a prop -> 'a prop
+val ==> : 'a pred * 'a pred -> 'a prop
+val trivial : 'a pred -> 'a prop -> 'a prop
+val classify : 'a pred -> string -> 'a prop -> 'a prop
+val classify' : ('a -> string option) -> 'a prop -> 'a prop
+
+(*Results*)
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+val test : 'a prop -> 'a * stats -> result * stats
+val stats : stats
+val success : result pred
+val failure : result pred
+
+end
+
+structure Property : PROPERTY =
+struct
+
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+type 'a pred = 'a -> bool
+type 'a prop = 'a * stats -> result * stats
+
+fun success (SOME true) = true
+ | success _ = false
+
+fun failure (SOME false) = true
+ | failure _ = false
+
+fun apply f x = (case try f x of NONE => SOME false | some => some)
+fun pred f (x,s) = (apply f x, s)
+fun pred2 f z = pred (fn x => f (x, z))
+
+fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
+
+fun ==> (p1, p2) = implies (p1, pred p2)
+
+fun wrap trans p (x,s) =
+ let val (result,s) = p (x,s)
+ in (result, trans (x, result, s)) end
+
+fun classify' f =
+ wrap (fn (x, result, {tags, count}) =>
+ { tags =
+ if is_some result then
+ (case f x of
+ NONE => tags
+ | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
+ else tags,
+ count = count })
+
+fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
+
+fun trivial cond = classify cond "trivial"
+
+fun test p =
+ wrap (fn (_, result, {tags, count}) =>
+ { tags = tags, count = if is_some result then count + 1 else count }) p
+
+val stats = { tags = [], count = 0 }
+
+end--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/random.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,46 @@
+(* Title: Tools/Spec_Check/random.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Random number engine.
+*)
+
+signature RANDOM =
+sig
+ type rand
+ val new : unit -> rand
+ val range : int * int -> rand -> int * rand
+ val split : rand -> rand * rand
+end
+
+structure Random : RANDOM =
+struct
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+ let
+ val t = a * seed
+ in
+ t - m * real(floor(t/m))
+ end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+ if min > max then raise Domain (* TODO: raise its own error *)
+ else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
+
+fun split r =
+ let
+ val r = r / a
+ val r0 = real(floor r)
+ val r1 = r - r0
+ in
+ (nextrand r0, nextrand r1)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/spec_check.ML Fri Aug 23 21:59:29 2013 +0200
@@ -0,0 +1,192 @@
+(* Title: Tools/Spec_Check/spec_check.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Specification-based testing of ML programs with random values.
+*)
+
+signature SPEC_CHECK =
+sig
+ val gen_target : int Config.T
+ val gen_max : int Config.T
+ val examples : int Config.T
+ val sort_examples : bool Config.T
+ val show_stats : bool Config.T
+ val column_width : int Config.T
+ val style : string Config.T
+
+ type output_style = Proof.context -> string ->
+ {status : string option * Property.result * (Property.stats * string option list) -> unit,
+ finish: Property.stats * string option list -> unit}
+
+ val register_style : string -> output_style -> theory -> theory
+
+ val checkGen : Proof.context ->
+ 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
+
+ val check_property : Proof.context -> string -> unit
+end;
+
+structure Spec_Check : SPEC_CHECK =
+struct
+
+(* configurations *)
+
+val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
+val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
+val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
+
+val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
+val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
+val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
+val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
+
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+type 'a rep = ('a -> string) option
+
+type output_style = Proof.context -> string ->
+ {status: string option * Property.result * (Property.stats * string option list) -> unit,
+ finish: Property.stats * string option list -> unit}
+
+fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
+
+structure Style = Theory_Data
+(
+ type T = output_style Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data : T = Symtab.merge (K true) data
+)
+
+fun get_style ctxt =
+ let val name = Config.get ctxt style in
+ (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
+ SOME style => style ctxt
+ | NONE => error ("No style called " ^ quote name ^ " found"))
+ end
+
+fun register_style name style = Style.map (Symtab.update (name, style))
+
+
+(* testing functions *)
+
+fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
+ let
+ val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
+
+ val {status, finish} = get_style ctxt tag
+ fun status' (obj, result, (stats, badobjs)) =
+ let
+ val badobjs' = if Property.failure result then obj :: badobjs else badobjs
+ val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
+ in badobjs' end
+
+ fun try_shrink (obj, result, stats') (stats, badobjs) =
+ let
+ fun is_failure s =
+ let val (result, stats') = Property.test prop (s, stats)
+ in if Property.failure result then SOME (s, result, stats') else NONE end
+ in
+ case get_first is_failure (shrink obj) of
+ SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
+ | NONE => status' (obj, result, (stats', badobjs))
+ end
+
+ fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
+ | iter (SOME (obj, stream), (stats, badobjs)) =
+ if #count stats >= Config.get ctxt gen_target then
+ finish (stats, map apply_show badobjs)
+ else
+ let
+ val (result, stats') = Property.test prop (obj, stats)
+ val badobjs' = if Property.failure result then
+ try_shrink (obj, result, stats') (stats, badobjs)
+ else
+ status' (obj, result, (stats', badobjs))
+ in iter (next stream, (stats', badobjs')) end
+ in
+ fn stream => iter (next stream, (s0, []))
+ end
+
+fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
+fun check ctxt = check' ctxt Property.stats
+fun checks ctxt = cpsCheck ctxt Property.stats
+
+fun checkGen ctxt (gen, show) (tag, prop) =
+ check' ctxt {count = 0, tags = [("__GEN", 0)]}
+ (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
+ cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
+ (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkOne ctxt show (tag, prop) obj =
+ check ctxt (List.getItem, show) (tag, prop) [obj]
+
+(*call the compiler and pass resulting type string to the parser*)
+fun determine_type ctxt s =
+ let
+ val return = Unsynchronized.ref "return"
+ val use_context : use_context =
+ {tune_source = #tune_source ML_Env.local_context,
+ name_space = #name_space ML_Env.local_context,
+ str_of_pos = #str_of_pos ML_Env.local_context,
+ print = fn r => return := r,
+ error = #error ML_Env.local_context}
+ val _ =
+ Context.setmp_thread_data (SOME (Context.Proof ctxt))
+ (fn () => Secure.use_text use_context (0, "generated code") true s) ()
+ in
+ Gen_Construction.parse_pred (! return)
+ end;
+
+(*call the compiler and run the test*)
+fun run_test ctxt s =
+ Context.setmp_thread_data (SOME (Context.Proof ctxt))
+ (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
+
+(*split input into tokens*)
+fun input_split s =
+ let
+ fun dot c = c = #"."
+ fun space c = c = #" "
+ val (head, code) = Substring.splitl (not o dot) (Substring.full s)
+ in
+ (String.tokens space (Substring.string head),
+ Substring.string (Substring.dropl dot code))
+ end;
+
+(*create the function from the input*)
+fun make_fun s =
+ let
+ val scan_param = Scan.one (fn s => s <> ";")
+ fun parameters s = Scan.repeat1 scan_param s
+ val p = $$ "ALL" |-- parameters
+ val (split, code) = input_split s
+ val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+ val (params, _) = Scan.finite stop p split
+ in "fn (" ^ commas params ^ ") => " ^ code end;
+
+(*read input and perform the test*)
+fun gen_check_property check ctxt s =
+ let
+ val func = make_fun s
+ val (_, ty) = determine_type ctxt func
+ in run_test ctxt (check ctxt "Check" (ty, func)) end;
+
+val check_property = gen_check_property Gen_Construction.build_check
+(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
+
+(*perform test for specification function*)
+fun gen_check_property_f check ctxt s =
+ let
+ val (name, ty) = determine_type ctxt s
+ in run_test ctxt (check ctxt name (ty, s)) end;
+
+val check_property_f = gen_check_property_f Gen_Construction.build_check
+(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
+
+end;
+
+fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
+--- a/src/Tools/WWW_Find/ROOT Fri Aug 23 16:51:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-session WWW_Find = Pure +
- theories [condition = ISABELLE_POLYML] WWW_Find
-
--- a/src/Tools/eqsubst.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/eqsubst.ML Fri Aug 23 21:59:29 2013 +0200
@@ -420,7 +420,7 @@
the goal) as well as the theorems to use *)
val setup =
Method.setup @{binding subst}
- (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
Attrib.thms >>
(fn ((asm, occs), inthms) => fn ctxt =>
SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))--- a/src/Tools/induct.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/induct.ML Fri Aug 23 21:59:29 2013 +0200
@@ -919,7 +919,7 @@
val cases_setup =
Method.setup @{binding cases}
- (Args.mode no_simpN --
+ (Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
(fn (no_simp, (insts, opt_rule)) => fn ctxt =>
METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
@@ -928,8 +928,9 @@
fun gen_induct_setup binding itac =
Method.setup binding
- (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
- (arbitrary -- taking -- Scan.option induct_rule)) >>
+ (Scan.lift (Args.mode no_simpN) --
+ (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (arbitrary -- taking -- Scan.option induct_rule)) >>
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
Seq.DETERM--- a/src/Tools/jEdit/etc/options Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/jEdit/etc/options Fri Aug 23 21:59:29 2013 +0200
@@ -3,6 +3,9 @@
public option jedit_logic : string = ""
-- "default logic session"
+public option jedit_reset_font_size : int = 18
+ -- "reset font size for main text area"
+
public option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
--- a/src/Tools/jEdit/src/actions.xml Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Fri Aug 23 21:59:29 2013 +0200
@@ -92,6 +92,11 @@
isabelle.jedit.Isabelle.toggle_node_required(view);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.reset-font-size">
+ <CODE>
+ isabelle.jedit.Isabelle.reset_font_size(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.increase-font-size">
<CODE>
isabelle.jedit.Isabelle.increase_font_size(view);
--- a/src/Tools/jEdit/src/isabelle.scala Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Aug 23 21:59:29 2013 +0200
@@ -107,6 +107,8 @@
view.getStatus.setMessageAndClear("Text font size: " + size)
}
+ def reset_font_size(view: View): Unit =
+ change_font_size(view, _ => PIDE.options.int("jedit_reset_font_size"))
def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
--- a/src/Tools/jEdit/src/jEdit.props Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Fri Aug 23 21:59:29 2013 +0200
@@ -207,6 +207,8 @@
isabelle.increase-font-size2.shortcut=C+EQUALS
#isabelle.increase-font-size2.shortcut2=C+ADD
isabelle.reset-continuous-checking.label=Reset continuous checking
+isabelle.reset-font-size.label=Reset font size
+isabelle.reset-font-size.shortcut=C+0
isabelle.reset-node-required.label=Reset node required
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
--- a/src/Tools/try.ML Fri Aug 23 16:51:53 2013 +0200
+++ b/src/Tools/try.ML Fri Aug 23 21:59:29 2013 +0200
@@ -142,7 +142,6 @@
(* hybrid tool setup *)
-fun tool_setup tool =
- (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
+fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
end;