# HG changeset patch # User wenzelm # Date 1377287969 -7200 # Node ID b881bee69d3acd6047b55d17f3c23c3a21b37002 # Parent a5805fe4e91c32e0377548e72299afe76e7f5469# Parent 31e24d6ff1eaf8930eb55c5e9c236d699eb0be62 merged diff -r a5805fe4e91c -r b881bee69d3a Admin/isatest/isatest-stats --- 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 diff -r a5805fe4e91c -r b881bee69d3a CONTRIBUTORS --- 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 diff -r a5805fe4e91c -r b881bee69d3a NEWS --- 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 diff -r a5805fe4e91c -r b881bee69d3a ROOTS --- 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 + diff -r a5805fe4e91c -r b881bee69d3a lib/texinputs/isabelle.sty --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/Doc/IsarImplementation/ML.thy --- 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 '}' | '\' | '\' + @{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 \}"} or @{text "@{note - \}"} augment the compilation context without generating code. The - non-ASCII braces @{text "\"} and @{text "\"} 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 \ b\<^sub>n}"} recalls existing facts @{text - "b\<^sub>1, \, 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 {* - \ - @{let ?t = my_term} - @{note my_refl = reflexive [of ?t]} - fun foo th = Thm.transitive th @{thm my_refl} - \ -*} - -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. *} diff -r a5805fe4e91c -r b881bee69d3a src/Doc/IsarImplementation/document/style.sty --- 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} diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Decision_Procs/Cooper.thy --- 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" diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Decision_Procs/Ferrack.thy --- 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" diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Decision_Procs/MIR.thy --- 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" diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Import/import_data.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Nominal/nominal_induct.ML --- 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))); diff -r a5805fe4e91c -r b881bee69d3a src/HOL/ROOT --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/Examples.thy --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/README --- 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. - diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/Spec_Check.thy --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/base_generator.ML --- 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 - diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/gen_construction.ML --- 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; - diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/generator.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/output_style.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/property.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/random.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Spec_Check/spec_check.ML --- 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; - diff -r a5805fe4e91c -r b881bee69d3a src/HOL/Tools/reflection.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/Pure/General/antiquote.ML --- 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 <> "\\" andalso s <> "\\" - 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 --| $$$ "\\"; -val scan_close = Symbol_Pos.scan_pos --| $$$ "\\"; - 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/args.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/attrib.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/calculation.ML --- 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); diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/class.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/code.ML --- 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*) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/context_rules.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/isar_cmd.ML --- 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 *) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/locale.ML --- 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 ***) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/method.ML --- 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!*) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/object_logic.ML --- 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 *) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Isar/rule_insts.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/ML/ml_antiquote.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/ML/ml_context.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/ML/ml_lex.ML --- 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); diff -r a5805fe4e91c -r b881bee69d3a src/Pure/ML/ml_thms.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Proof/extraction.ML --- 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 ****) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Proof/proof_rewrite_rules.ML --- 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 ****) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Syntax/syntax_phases.ML --- 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')]); diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/latex.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/present.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/rail.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/term_style.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/thy_load.ML --- 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 *) diff -r a5805fe4e91c -r b881bee69d3a src/Pure/Thy/thy_output.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/axclass.ML --- 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, diff -r a5805fe4e91c -r b881bee69d3a src/Pure/pure_thy.ML --- 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; diff -r a5805fe4e91c -r b881bee69d3a src/Pure/simplifier.ML --- 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"); diff -r a5805fe4e91c -r b881bee69d3a src/Pure/theory.ML --- 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 **) diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Code/code_runtime.ML --- 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."; diff -r a5805fe4e91c -r b881bee69d3a src/Tools/ROOT --- /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 + diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/Examples.thy --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/README --- /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. + diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/Spec_Check.thy --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/base_generator.ML --- /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 + diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/gen_construction.ML --- /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; + diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/generator.ML --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/output_style.ML --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/property.ML --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/random.ML --- /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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/Spec_Check/spec_check.ML --- /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; + diff -r a5805fe4e91c -r b881bee69d3a src/Tools/WWW_Find/ROOT --- 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 - diff -r a5805fe4e91c -r b881bee69d3a src/Tools/eqsubst.ML --- 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))) diff -r a5805fe4e91c -r b881bee69d3a src/Tools/induct.ML --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/jEdit/etc/options --- 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" diff -r a5805fe4e91c -r b881bee69d3a src/Tools/jEdit/src/actions.xml --- 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); + + + isabelle.jedit.Isabelle.reset_font_size(view); + + isabelle.jedit.Isabelle.increase_font_size(view); diff -r a5805fe4e91c -r b881bee69d3a src/Tools/jEdit/src/isabelle.scala --- 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)) diff -r a5805fe4e91c -r b881bee69d3a src/Tools/jEdit/src/jEdit.props --- 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 diff -r a5805fe4e91c -r b881bee69d3a src/Tools/try.ML --- 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;