# HG changeset patch # User bulwahn # Date 1300692556 -3600 # Node ID 143f3719491102573f678ae3e5a2b05d58883694 # Parent 2de57cda5b24187b10aaa0aa8eada96358940e4c# Parent 878f33040280b91677181bc8b6b738e49a839d39 merged diff -r 2de57cda5b24 -r 143f37194911 NEWS --- a/NEWS Fri Mar 18 18:19:42 2011 +0100 +++ b/NEWS Mon Mar 21 08:29:16 2011 +0100 @@ -50,6 +50,9 @@ - sledgehammer available_provers ~> sledgehammer supported_provers INCOMPATIBILITY. +* "try": + - Added "simp:", "intro:", and "elim:" options. + * Function package: discontinued option "tailrec". INCOMPATIBILITY. Use partial_function instead. @@ -62,6 +65,9 @@ *** ML *** +* Structure Timing provides various operations for timing; supersedes +former start_timing/end_timing etc. + * Path.print is the official way to show file-system paths to users (including quotes etc.). diff -r 2de57cda5b24 -r 143f37194911 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/doc-src/System/Thy/Presentation.thy Mon Mar 21 08:29:16 2011 +0100 @@ -448,7 +448,7 @@ -P PATH set path for remote theory browsing information -Q INT set threshold for sub-proof parallelization (default 50) -T LEVEL multithreading: trace level (default 0) - -V VERSION declare alternative document VERSION + -V VARIANT declare alternative document VARIANT -b build mode (output heap image, using current dir) -d FORMAT build document as FORMAT (default false) -f NAME use ML file NAME (default ROOT.ML) @@ -523,16 +523,16 @@ \secref{sec:tool-latex} for more details. \medskip The @{verbatim "-V"} option declares alternative document - versions, consisting of name/tags pairs (cf.\ options @{verbatim + variants, consisting of name/tags pairs (cf.\ options @{verbatim "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The standard document is equivalent to ``@{verbatim "document=theory,proof,ML"}'', which means that all theory begin/end commands, proof body texts, and ML code will be presented - faithfully. An alternative version ``@{verbatim + faithfully. An alternative variant ``@{verbatim "outline=/proof/ML"}'' would fold proof and ML parts, replacing the original text by a short place-holder. The form ``@{text name}@{verbatim "=-"},'' means to remove document @{text name} from - the list of versions to be processed. Any number of @{verbatim + the list of variants to be processed. Any number of @{verbatim "-V"} options may be given; later declarations have precedence over earlier ones. @@ -682,15 +682,15 @@ corresponding output files named after @{verbatim root} as well, e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}. - \medskip When running the session, Isabelle copies the original - @{verbatim document} directory into its proper place within - @{setting ISABELLE_BROWSER_INFO} according to the session path. - Then, for any processed theory @{text A} some {\LaTeX} source is - generated and put there as @{text A}@{verbatim ".tex"}. - Furthermore, a list of all generated theory files is put into - @{verbatim session.tex}. Typically, the root {\LaTeX} file provided - by the user would include @{verbatim session.tex} to get a document - containing all the theories. + \medskip When running the session, Isabelle copies the content of + the original @{verbatim document} directory into its proper place + within @{setting ISABELLE_BROWSER_INFO}, according to the session + path and document variant. Then, for any processed theory @{text A} + some {\LaTeX} source is generated and put there as @{text + A}@{verbatim ".tex"}. Furthermore, a list of all generated theory + files is put into @{verbatim session.tex}. Typically, the root + {\LaTeX} file provided by the user would include @{verbatim + session.tex} to get a document containing all the theories. The {\LaTeX} versions of the theories require some macros defined in @{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim diff -r 2de57cda5b24 -r 143f37194911 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 18 18:19:42 2011 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Mar 21 08:29:16 2011 +0100 @@ -474,7 +474,7 @@ -P PATH set path for remote theory browsing information -Q INT set threshold for sub-proof parallelization (default 50) -T LEVEL multithreading: trace level (default 0) - -V VERSION declare alternative document VERSION + -V VARIANT declare alternative document VARIANT -b build mode (output heap image, using current dir) -d FORMAT build document as FORMAT (default false) -f NAME use ML file NAME (default ROOT.ML) @@ -550,12 +550,12 @@ \secref{sec:tool-latex} for more details. \medskip The \verb|-V| option declares alternative document - versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The + variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end commands, proof body texts, and ML code will be presented - faithfully. An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the + faithfully. An alternative variant ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the original text by a short place-holder. The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from - the list of versions to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over + the list of variants to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over earlier ones. \medskip The \verb|-g| option produces images of the theory @@ -693,15 +693,13 @@ corresponding output files named after \verb|root| as well, e.g.\ \verb|root.dvi| for target format \verb|dvi|. - \medskip When running the session, Isabelle copies the original - \verb|document| directory into its proper place within - \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} according to the session path. - Then, for any processed theory \isa{A} some {\LaTeX} source is - generated and put there as \isa{A}\verb|.tex|. - Furthermore, a list of all generated theory files is put into - \verb|session.tex|. Typically, the root {\LaTeX} file provided - by the user would include \verb|session.tex| to get a document - containing all the theories. + \medskip When running the session, Isabelle copies the content of + the original \verb|document| directory into its proper place + within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session + path and document variant. Then, for any processed theory \isa{A} + some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|. Furthermore, a list of all generated theory + files is put into \verb|session.tex|. Typically, the root + {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories. The {\LaTeX} versions of the theories require some macros defined in \verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine; diff -r 2de57cda5b24 -r 143f37194911 lib/Tools/usedir --- a/lib/Tools/usedir Fri Mar 18 18:19:42 2011 +0100 +++ b/lib/Tools/usedir Mon Mar 21 08:29:16 2011 +0100 @@ -21,7 +21,7 @@ echo " -P PATH set path for remote theory browsing information" echo " -Q INT set threshold for sub-proof parallelization (default 100)" echo " -T LEVEL multithreading: trace level (default 0)" - echo " -V VERSION declare alternative document VERSION" + echo " -V VARIANT declare alternative document VARIANT" echo " -b build mode (output heap image, using current dir)" echo " -d FORMAT build document as FORMAT (default false)" echo " -f NAME use ML file NAME (default ROOT.ML)" @@ -74,7 +74,7 @@ MAXTHREADS="1" RPATH="" TRACETHREADS="0" -DOCUMENT_VERSIONS="" +DOCUMENT_VARIANTS="" BUILD="" DOCUMENT=false ROOT_FILE="ROOT.ML" @@ -122,10 +122,10 @@ TRACETHREADS="$OPTARG" ;; V) - if [ -z "$DOCUMENT_VERSIONS" ]; then - DOCUMENT_VERSIONS="\"$OPTARG\"" + if [ -z "$DOCUMENT_VARIANTS" ]; then + DOCUMENT_VARIANTS="\"$OPTARG\"" else - DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\"" + DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\"" fi ;; b) @@ -241,7 +241,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \ -q -w $LOGIC $NAME > "$LOG" RC="$?" else @@ -250,7 +250,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \ -r -q "$LOGIC" > "$LOG" RC="$?" cd .. diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 21 08:29:16 2011 +0100 @@ -22,8 +22,7 @@ "expected file ending " ^ quote ext) val base_path = Path.explode base_name |> tap check_ext - val (full_path, _) = - Thy_Load.check_file (Thy_Load.master_directory thy) base_path + val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path val _ = Boogie_VCs.is_closed thy orelse error ("Found the beginning of a new Boogie environment, " ^ diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Matrix/Compute_Oracle/report.ML --- a/src/HOL/Matrix/Compute_Oracle/report.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/report.ML Mon Mar 21 08:29:16 2011 +0100 @@ -11,9 +11,9 @@ fun timeit f = let - val t1 = start_timing () + val t1 = Timing.start () val x = f () - val t2 = #message (end_timing t1) + val t2 = Timing.message (Timing.result t1) val _ = writeln ((report_space ()) ^ "--> "^t2) in x diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Mar 21 08:29:16 2011 +0100 @@ -210,10 +210,7 @@ | NONE => default) fun cpu_time f x = - let - val start = start_timing () - val result = Exn.capture (fn () => f x) () - val time = Time.toMilliseconds (#cpu (end_timing start)) - in (Exn.release result, time) end + let val ({cpu, ...}, y) = Timing.timing f x + in (y, Time.toMilliseconds cpu) end end diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 21 08:29:16 2011 +0100 @@ -558,7 +558,7 @@ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK - val trivial = Try.invoke_try (SOME try_timeout) pre + val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre handle TimeLimit.TimeOut => false fun apply_reconstructor m1 m2 = if metis_ft diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Mar 21 08:29:16 2011 +0100 @@ -150,7 +150,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) in - case Try.invoke_try (SOME (seconds 5.0)) state of + case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of true => (Solved, ([], NONE)) | false => (Unsolved, ([], NONE)) end @@ -332,12 +332,9 @@ fun count x = (length oo filter o equal) x -fun cpu_time description f = - let - val start = start_timing () - val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) - in (Exn.release result, (description, time)) end +fun cpu_time description e = + let val ({cpu, ...}, result) = Timing.timing e () + in (result, (description, Time.toMilliseconds cpu)) end (* fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t = let diff -r 2de57cda5b24 -r 143f37194911 src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Mar 21 08:29:16 2011 +0100 @@ -15,8 +15,7 @@ fun spark_open vc_name thy = let - val (vc_path, _) = Thy_Load.check_file - (Thy_Load.master_directory thy) (Path.explode vc_name); + val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name); val (base, header) = (case Path.split_ext vc_path of (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Action.thy Mon Mar 21 08:29:16 2011 +0100 @@ -12,9 +12,8 @@ (** abstract syntax **) -types - 'a trfun = "(state * state) => 'a" - action = "bool trfun" +type_synonym 'a trfun = "(state * state) => 'a" +type_synonym action = "bool trfun" arities prod :: (world, world) world diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Init.thy --- a/src/HOL/TLA/Init.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Init.thy Mon Mar 21 08:29:16 2011 +0100 @@ -14,8 +14,7 @@ typedecl behavior arities behavior :: world -types - temporal = "behavior form" +type_synonym temporal = "behavior form" consts diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Intensional.thy Mon Mar 21 08:29:16 2011 +0100 @@ -15,9 +15,8 @@ (** abstract syntax **) -types - ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) - 'w form = "('w, bool) expr" +type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) +type_synonym 'w form = "('w, bool) expr" consts Valid :: "('w::world) form => bool" diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/MemClerk.thy --- a/src/HOL/TLA/Memory/MemClerk.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/MemClerk.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,11 +8,10 @@ imports Memory RPC MemClerkParameters begin -types - (* The clerk takes the same arguments as the memory and sends requests to the RPC *) - mClkSndChType = "memChType" - mClkRcvChType = "rpcSndChType" - mClkStType = "(PrIds => mClkState) stfun" +(* The clerk takes the same arguments as the memory and sends requests to the RPC *) +type_synonym mClkSndChType = "memChType" +type_synonym mClkRcvChType = "rpcSndChType" +type_synonym mClkStType = "(PrIds => mClkState) stfun" definition (* state predicates *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/MemClerkParameters.thy --- a/src/HOL/TLA/Memory/MemClerkParameters.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Mon Mar 21 08:29:16 2011 +0100 @@ -10,11 +10,10 @@ datatype mClkState = clkA | clkB -types - (* types sent on the clerk's send and receive channels are argument types - of the memory and the RPC, respectively *) - mClkSndArgType = "memOp" - mClkRcvArgType = "rpcOp" +(* types sent on the clerk's send and receive channels are argument types + of the memory and the RPC, respectively *) +type_synonym mClkSndArgType = "memOp" +type_synonym mClkRcvArgType = "rpcOp" definition (* translate a memory call to an RPC call *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/Memory.thy --- a/src/HOL/TLA/Memory/Memory.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/Memory.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,10 +8,9 @@ imports MemoryParameters ProcedureInterface begin -types - memChType = "(memOp, Vals) channel" - memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) - resType = "(PrIds => Vals) stfun" +type_synonym memChType = "(memOp, Vals) channel" +type_synonym memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *) +type_synonym resType = "(PrIds => Vals) stfun" consts (* state predicates *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Mar 21 08:29:16 2011 +0100 @@ -10,8 +10,7 @@ datatype histState = histA | histB -types - histType = "(PrIds => histState) stfun" (* the type of the history variable *) +type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *) consts (* the specification *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/ProcedureInterface.thy --- a/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,15 +8,13 @@ imports "../TLA" RPCMemoryParams begin -typedecl +typedecl ('a,'r) chan (* type of channels with argument type 'a and return type 'r. we model a channel as an array of variables (of type chan) rather than a single array-valued variable because the notation gets a little simpler. *) - ('a,'r) chan -types - ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun" +type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun" consts (* data-level functions *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/RPC.thy --- a/src/HOL/TLA/Memory/RPC.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/RPC.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,10 +8,9 @@ imports RPCParameters ProcedureInterface Memory begin -types - rpcSndChType = "(rpcOp,Vals) channel" - rpcRcvChType = "memChType" - rpcStType = "(PrIds => rpcState) stfun" +type_synonym rpcSndChType = "(rpcOp,Vals) channel" +type_synonym rpcRcvChType = "memChType" +type_synonym rpcStType = "(PrIds => rpcState) stfun" consts (* state predicates *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Memory/RPCMemoryParams.thy --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,10 +8,10 @@ imports Main begin -types - bit = "bool" (* Signal wires for the procedure interface. - Defined as bool for simplicity. All I should really need is - the existence of two distinct values. *) +type_synonym bit = "bool" + (* Signal wires for the procedure interface. + Defined as bool for simplicity. All I should really need is + the existence of two distinct values. *) (* all of these are simple (HOL) types *) typedecl Locs (* "syntactic" value type *) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/TLA/Stfun.thy --- a/src/HOL/TLA/Stfun.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/TLA/Stfun.thy Mon Mar 21 08:29:16 2011 +0100 @@ -13,9 +13,8 @@ arities state :: world -types - 'a stfun = "state => 'a" - stpred = "bool stfun" +type_synonym 'a stfun = "state => 'a" +type_synonym stpred = "bool stfun" consts diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 21 08:29:16 2011 +0100 @@ -300,6 +300,24 @@ | bound_for_plain_rel _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) +fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) = + case constrs of + [_, _] => + (case constrs |> map (snd o #const) |> List.partition is_fun_type of + ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1) + | _ => false) + | _ => false + +fun needed_values need_vals T = + AList.lookup (op =) need_vals T |> the_default NONE |> these + +fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) = + length (needed_values need_vals typ) = card + +fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) = + exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us + | is_sel_of_constr _ _ = false + fun bound_for_sel_rel ctxt debug need_vals dtypes (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]), R as Func (Atom (_, j0), R2), nick)) = @@ -308,46 +326,80 @@ val {delta, epsilon, exclusive, explicit_max, ...} = constr_spec dtypes (constr_s, T1) val dtype as {card, ...} = datatype_spec dtypes T1 |> the - val need_vals = - AList.lookup (op =) need_vals T1 |> the_default NONE |> these + val T1_need_vals = needed_values need_vals T1 in ([(x, bound_comment ctxt debug nick T R)], let - val complete_need_vals = (length need_vals = card) + val discr = (R2 = Formula Neut) + val complete_need_vals = (length T1_need_vals = card) val (my_need_vals, other_need_vals) = - need_vals - |> List.partition - (fn (Construct (sel_us, _, _, _), _) => - exists (fn FreeRel (x', _, _, _) => x = x' - | _ => false) sel_us - | _ => false) - fun upper_bound_ts () = - if complete_need_vals then - my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet - else if not (null other_need_vals) then - index_seq (delta + j0) (epsilon - delta) - |> filter_out (member (op = o apsnd snd) other_need_vals) - |> map (KK.Tuple o single) |> KK.TupleSet + T1_need_vals |> List.partition (is_sel_of_constr x) + fun atom_seq_for_self_rec j = + if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0) + fun exact_bound_for_perhaps_needy_atom j = + case AList.find (op =) my_need_vals j of + [constr_u] => + let + val n = sel_no_from_name nick + val arg_u = + case constr_u of + Construct (_, _, _, arg_us) => nth arg_us n + | _ => raise Fail "expected \"Construct\"" + val T2_need_vals = needed_values need_vals T2 + in + case AList.lookup (op =) T2_need_vals arg_u of + SOME arg_j => SOME (KK.TupleAtomSeq (1, arg_j)) + | _ => NONE + end + | _ => NONE + fun n_fold_tuple_union [] = KK.TupleSet [] + | n_fold_tuple_union (ts :: tss) = + fold (curry (KK.TupleUnion o swap)) tss ts + fun tuple_perhaps_needy_atom upper j = + single_atom j + |> not discr + ? (fn ts => KK.TupleProduct (ts, + case exact_bound_for_perhaps_needy_atom j of + SOME ts => ts + | NONE => if upper then upper_bound_for_rep R2 + else KK.TupleSet [])) + fun bound_tuples upper = + if null T1_need_vals then + if upper then + KK.TupleAtomSeq (epsilon - delta, delta + j0) + |> not discr + ? (fn ts => KK.TupleProduct (ts, upper_bound_for_rep R2)) + else + KK.TupleSet [] else - KK.TupleAtomSeq (epsilon - delta, delta + j0) + (if complete_need_vals then + my_need_vals |> map snd + else + index_seq (delta + j0) (epsilon - delta) + |> filter_out (member (op = o apsnd snd) other_need_vals)) + |> map (tuple_perhaps_needy_atom upper) + |> n_fold_tuple_union in if explicit_max = 0 orelse - (complete_need_vals andalso null my_need_vals) (* ### needed? *) then + (complete_need_vals andalso null my_need_vals) then [KK.TupleSet []] else - if R2 = Formula Neut then - [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet []) + if discr then + [bound_tuples true] + |> not (exclusive orelse all_values_are_needed need_vals dtype) + ? cons (KK.TupleSet []) else - [KK.TupleSet [], + [bound_tuples false, if T1 = T2 andalso epsilon > delta andalso is_datatype_acyclic dtype then index_seq delta (epsilon - delta) |> map (fn j => KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]], - KK.TupleAtomSeq (j, j0))) - |> foldl1 KK.TupleUnion + KK.TupleAtomSeq (atom_seq_for_self_rec j))) + |> n_fold_tuple_union else - KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)] + bound_tuples true] + |> distinct (op =) end) end | bound_for_sel_rel _ _ _ _ u = @@ -1499,14 +1551,14 @@ let val dummy_u = RelReg (0, type_of u, rep_of u) in case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u) |> kodkod_formula_from_nut ofs kk of - KK.RelEq (KK.RelReg _, r) => KK.RelEq (KK.Atom j, r) + KK.RelEq (KK.RelReg _, r) => SOME (KK.RelEq (KK.Atom j, r)) | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut", "malformed Kodkod formula") end fun needed_values_for_datatype [] _ _ = SOME [] | needed_values_for_datatype need_us ofs - ({typ, card, constrs, ...} : datatype_spec) = + ({typ, card, constrs, ...} : datatype_spec) = let fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) = fold aux us @@ -1537,9 +1589,10 @@ SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd) end -fun needed_value_axioms_for_datatype _ _ NONE = [KK.False] - | needed_value_axioms_for_datatype ofs kk (SOME fixed) = - fixed |> map (atom_equation_for_nut ofs kk) +fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False] + | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) = + if is_datatype_nat_like (the (datatype_spec dtypes T)) then [] + else fixed |> map_filter (atom_equation_for_nut ofs kk) fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) @@ -1707,27 +1760,35 @@ |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes) -fun sel_axiom_for_sel hol_ctxt binarize j0 +fun sel_axioms_for_sel hol_ctxt binarize j0 (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...}) - rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec) - n = + need_vals rel_table dom_r (dtype as {typ, ...}) + ({const, delta, epsilon, exclusive, ...} : constr_spec) n = let val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n val (r, R, _) = const_triple rel_table x + val rel_x = + case r of + KK.Rel x => x + | _ => raise BAD ("Nitpick_Kodkod.sel_axioms_for_sel", "non-Rel") val R2 = dest_Func R |> snd val z = (epsilon - delta, delta + j0) in if exclusive then - kk_n_ary_function kk (Func (Atom z, R2)) r + [kk_n_ary_function kk (Func (Atom z, R2)) r] + else if all_values_are_needed need_vals dtype then + typ |> needed_values need_vals + |> filter (is_sel_of_constr rel_x) + |> map (fn (_, j) => kk_n_ary_function kk R2 (kk_join (KK.Atom j) r)) else let val r' = kk_join (KK.Var (1, 0)) r in - kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] - (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) - (kk_n_ary_function kk R2 r') (kk_no r')) + [kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] + (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) + (kk_n_ary_function kk R2 r') (kk_no r'))] end end -fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table - (constr as {const, delta, epsilon, explicit_max, ...}) = +fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table + dtype (constr as {const, delta, epsilon, explicit_max, ...}) = let val honors_explicit_max = explicit_max < 0 orelse epsilon - delta <= explicit_max @@ -1749,17 +1810,20 @@ " too small for \"max\"") in max_axiom :: - map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr) - (index_seq 0 (num_sels_for_constr_type (snd const))) + maps (sel_axioms_for_sel hol_ctxt binarize j0 kk need_vals rel_table + dom_r dtype constr) + (index_seq 0 (num_sels_for_constr_type (snd const))) end end -fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table - ({constrs, ...} : datatype_spec) = - maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs +fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals + (dtype as {constrs, ...}) = + maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals + dtype) constrs -fun uniqueness_axiom_for_constr hol_ctxt binarize +fun uniqueness_axioms_for_constr hol_ctxt binarize ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} - : kodkod_constrs) rel_table ({const, ...} : constr_spec) = + : kodkod_constrs) need_vals rel_table dtype + ({const, ...} : constr_spec) = let fun conjunct_for_sel r = kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) @@ -1771,36 +1835,42 @@ val set_r = triples |> hd |> #1 in if num_sels = 0 then - kk_lone set_r + [kk_lone set_r] + else if all_values_are_needed need_vals dtype then + [] else - kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) - (kk_implies - (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) - (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) + [kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) + (kk_implies + (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) + (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))] end -fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table - ({constrs, ...} : datatype_spec) = - map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs +fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table + (dtype as {constrs, ...}) = + maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table + dtype) constrs fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) - rel_table - ({card, constrs, ...} : datatype_spec) = + need_vals rel_table (dtype as {card, constrs, ...}) = if forall #exclusive constrs then [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool] + else if all_values_are_needed need_vals dtype then + [] else let val rs = map (discr_rel_expr rel_table o #const) constrs in [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), kk_disjoint_sets kk rs] end -fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = [] - | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table +fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = [] + | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table (dtype as {typ, ...}) = let val j0 = offset_of_type ofs typ in - sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @ - uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @ - partition_axioms_for_datatype j0 kk rel_table dtype + sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table + dtype @ + uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table + dtype @ + partition_axioms_for_datatype j0 kk need_vals rel_table dtype end fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals @@ -1812,11 +1882,11 @@ |> strongly_connected_sub_nfas in acyclicity_axioms_for_datatypes kk nfas @ - maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @ + maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @ sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break kk rel_table nfas dtypes @ - maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) - dtypes + maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk + rel_table) dtypes end end; diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Mon Mar 21 08:29:16 2011 +0100 @@ -527,10 +527,10 @@ val rs = these (AList.lookup (op =) clauses p) fun check_mode m = let - val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => + val res = cond_timeit false "work part of check_mode for one mode" (fn _ => map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs) in - Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => + cond_timeit false "aux part of check_mode for one mode" (fn _ => case find_indices is_none res of [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res) | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is))) @@ -538,7 +538,7 @@ val _ = if show_mode_inference options then tracing ("checking " ^ string_of_int (length ms) ^ " modes ...") else () - val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms) + val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms) val (ms', errors) = split res in ((p, (ms' : ((bool * mode) * bool) list)), errors) @@ -622,7 +622,7 @@ (check_modes_pred' mode_analysis_options options ctxt param_vs clauses (modes @ extra_modes)) modes val ((modes : (string * ((bool * mode) * bool) list) list), errors) = - Output.cond_timeit false "Fixpount computation of mode analysis" (fn () => + cond_timeit false "Fixpount computation of mode analysis" (fn () => if show_invalid_clauses options then fixp_with_state (fn (modes, errors) => let diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Mar 21 08:29:16 2011 +0100 @@ -130,12 +130,12 @@ fun preprocess options t thy = let val _ = print_step options "Fetching definitions from theory..." - val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" + val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph" (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t |> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr)) val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else () in - Output.cond_timeit (!Quickcheck.timing) "preprocess-process" + cond_timeit (!Quickcheck.timing) "preprocess-process" (fn () => (fold_rev (preprocess_strong_conn_constnames options gr) (Term_Graph.strong_conn gr) thy)) end diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 21 08:29:16 2011 +0100 @@ -1363,7 +1363,7 @@ val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt, modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt) val ((moded_clauses, needs_random), errors) = - Output.cond_timeit (!Quickcheck.timing) "Infering modes" + cond_timeit (!Quickcheck.timing) "Infering modes" (fn _ => infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses) val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy @@ -1373,19 +1373,19 @@ val _ = print_modes options modes val _ = print_step options "Defining executable functions..." val thy'' = - Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..." + cond_timeit (!Quickcheck.timing) "Defining executable functions..." (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' |> Theory.checkpoint) val ctxt'' = ProofContext.init_global thy'' val _ = print_step options "Compiling equations..." val compiled_terms = - Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ => compile_preds options (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses) val _ = print_compiled_terms options ctxt'' compiled_terms val _ = print_step options "Proving equations..." val result_thms = - Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds (maps_modes result_thms) @@ -1393,7 +1393,7 @@ val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy''' = - Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => + cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib thy ])] thy)) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Mar 21 08:29:16 2011 +0100 @@ -211,12 +211,9 @@ val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple -fun cpu_time description f = - let - val start = start_timing () - val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) - in (Exn.release result, (description, time)) end +fun cpu_time description e = + let val ({cpu, ...}, result) = Timing.timing e () + in (result, (description, Time.toMilliseconds cpu)) end fun compile_term compilation options ctxt (t, eval_terms) = let diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Mar 21 08:29:16 2011 +0100 @@ -115,8 +115,8 @@ let val ths = Attrib.eval_thms ctxt [xthm] val bracket = - implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg) - ^ "]") args) + map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args + |> implode fun nth_name j = case xref of Facts.Fact s => backquote s ^ bracket diff -r 2de57cda5b24 -r 143f37194911 src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/try.ML Mon Mar 21 08:29:16 2011 +0100 @@ -7,7 +7,9 @@ signature TRY = sig val auto : bool Unsynchronized.ref - val invoke_try : Time.time option -> Proof.state -> bool + val invoke_try : + Time.time option -> string list * string list * string list -> Proof.state + -> bool val setup : theory -> theory end; @@ -40,59 +42,85 @@ NONE end -fun named_method thy name = - Method.method thy (Args.src ((name, []), Position.none)) +val parse_method = + enclose "(" ")" + #> Outer_Syntax.scan Position.start + #> filter Token.is_proper + #> Scan.read Token.stopper Method.parse + #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source") -fun apply_named_method_on_first_goal name ctxt = - let val thy = ProofContext.theory_of ctxt in - Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name))) - end +fun apply_named_method_on_first_goal method thy = + method |> parse_method + |> Method.method thy + |> Method.Basic + |> curry Method.SelectGoals 1 + |> Proof.refine handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *) -fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st = +fun add_attr_text (NONE, _) s = s + | add_attr_text (_, []) s = s + | add_attr_text (SOME x, fs) s = + s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs +fun attrs_text (sx, ix, ex) (ss, is, es) = + "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)] + +fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt + triple st = if not auto orelse run_if_auto then - do_generic timeout_opt - (name ^ (if all_goals andalso - nprems_of (#goal (Proof.goal st)) > 1 then - "[1]" - else - "")) I (#goal o Proof.goal) - (apply_named_method_on_first_goal name (Proof.context_of st)) st + let val attrs = attrs_text attrs triple in + do_generic timeout_opt + (name ^ (if all_goals andalso + nprems_of (#goal (Proof.goal st)) > 1 then + "[1]" + else + "") ^ + attrs) I (#goal o Proof.goal) + (apply_named_method_on_first_goal (name ^ attrs) + (Proof.theory_of st)) st + end else NONE -(* name * (all_goals, run_if_auto) *) +val full_attrs = (SOME "simp", SOME "intro", SOME "elim") +val clas_attrs = (NONE, SOME "intro", SOME "elim") +val simp_attrs = (SOME "add", NONE, NONE) +val metis_attrs = (SOME "", SOME "", SOME "") +val no_attrs = (NONE, NONE, NONE) + +(* name * ((all_goals, run_if_auto), (simp, intro, elim) *) val named_methods = - [("simp", (false, true)), - ("auto", (true, true)), - ("fast", (false, false)), - ("fastsimp", (false, false)), - ("force", (false, false)), - ("blast", (false, true)), - ("metis", (false, true)), - ("linarith", (false, true)), - ("presburger", (false, true))] + [("simp", ((false, true), simp_attrs)), + ("auto", ((true, true), full_attrs)), + ("fast", ((false, false), clas_attrs)), + ("fastsimp", ((false, false), full_attrs)), + ("force", ((false, false), full_attrs)), + ("blast", ((false, true), clas_attrs)), + ("metis", ((false, true), metis_attrs)), + ("linarith", ((false, true), no_attrs)), + ("presburger", ((false, true), no_attrs))] val do_methods = map do_named_method named_methods fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" -fun do_try auto timeout_opt st = +fun do_try auto timeout_opt triple st = let val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) in - case do_methods |> Par_List.map (fn f => f auto timeout_opt st) + case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st) |> map_filter I |> sort (int_ord o pairself snd) of [] => (if auto then () else writeln "No proof found."; (false, st)) | xs as (s, _) :: _ => let - val xs = xs |> map swap |> AList.coalesce (op =) + val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s))) + |> AList.coalesce (op =) |> map (swap o apsnd commas) + val need_parens = exists_string (curry (op =) " ") s val message = (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^ Markup.markup Markup.sendback ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" - else "apply") ^ " " ^ s) ^ + else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" in (true, st |> (if auto then @@ -105,17 +133,43 @@ end end -val invoke_try = fst oo do_try false +fun invoke_try timeout_opt = fst oo do_try false timeout_opt val tryN = "try" +fun try_trans triple = + Toplevel.keep (K () o do_try false (SOME default_timeout) triple + o Toplevel.proof_of) + +fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2) + +fun string_of_xthm (xref, args) = + Facts.string_of_ref xref ^ + implode (map (enclose "[" "]" o Pretty.str_of + o Args.pretty_src @{context}) args) + +val parse_fact_refs = + Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) + (Parse_Spec.xthm >> string_of_xthm)) +val parse_attr = + Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs + >> (fn ss => (ss, [], [])) + || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs + >> (fn is => ([], is, [])) + || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs + >> (fn es => ([], [], es)) +fun parse_attrs x = + (Args.parens parse_attrs + || Scan.repeat parse_attr + >> (fn triple => fold merge_attrs triple ([], [], []))) x + +val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans + val _ = Outer_Syntax.improper_command tryN - "try a combination of proof methods" Keyword.diag - (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout) - o Toplevel.proof_of))) + "try a combination of proof methods" Keyword.diag parse_try_command -val auto_try = do_try true NONE +val auto_try = do_try true NONE ([], [], []) val setup = Auto_Tools.register_tool (auto, auto_try) diff -r 2de57cda5b24 -r 143f37194911 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Mon Mar 21 08:29:16 2011 +0100 @@ -536,13 +536,12 @@ fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) | and_to_list fm acc = rev (fm :: acc) val clauses = and_to_list prop_fm [] - val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) - clauses - val cterms = map (Thm.cterm_of @{theory}) terms - val timer = start_timing () - val thm = sat.rawsat_thm @{context} cterms + val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses + val cterms = map (Thm.cterm_of @{theory}) terms + val start = Timing.start () + val thm = sat.rawsat_thm @{context} cterms in - (end_timing timer, !sat.counter) + (Timing.result start, ! sat.counter) end; *} diff -r 2de57cda5b24 -r 143f37194911 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Provers/blast.ML Mon Mar 21 08:29:16 2011 +0100 @@ -914,7 +914,7 @@ fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = if b then - writeln (#message (end_timing start) ^ " for search. Closed: " + writeln (Timing.message (Timing.result start) ^ " for search. Closed: " ^ string_of_int (!nclosed) ^ " tried: " ^ string_of_int (!ntried) ^ " tactics: " ^ string_of_int (length tacs)) @@ -1256,7 +1256,7 @@ val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem fun cont (tacs,_,choices) = - let val start = start_timing () + let val start = Timing.start () in case Seq.pull(EVERY' (rev tacs) i st) of NONE => (writeln ("PROOF FAILED for depth " ^ @@ -1265,7 +1265,7 @@ else (); backtrack choices) | cell => (if (!trace orelse !stats) - then writeln (#message (end_timing start) ^ " for reconstruction") + then writeln (Timing.message (Timing.result start) ^ " for reconstruction") else (); Seq.make(fn()=> cell)) end @@ -1273,13 +1273,13 @@ handle PROVE => Seq.empty (*Public version with fixed depth*) -fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st; +fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st; val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20); fun blast_tac cs i st = ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit) - (timing_depth_tac (start_timing ()) cs) 0) i + (timing_depth_tac (Timing.start ()) cs) 0) i THEN flexflex_tac) st handle TRANS s => ((if !trace then warning ("blast: " ^ s) else ()); @@ -1299,7 +1299,7 @@ let val state as State {fullTrace = ft, ...} = initialize thy; val res = timeap prove - (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I); + (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I); val _ = fullTrace := !ft; in res end; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/General/file.ML Mon Mar 21 08:29:16 2011 +0100 @@ -11,12 +11,13 @@ val shell_path: Path.T -> string val cd: Path.T -> unit val pwd: unit -> Path.T - val full_path: Path.T -> Path.T + val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool - val check: Path.T -> unit val rm: Path.T -> unit val is_dir: Path.T -> bool + val check_dir: Path.T -> Path.T + val check_file: Path.T -> Path.T val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a @@ -51,9 +52,18 @@ val cd = cd o platform_path; val pwd = Path.explode o pwd; -fun full_path path = - if Path.is_absolute path then path - else Path.append (pwd ()) path; + +(* full_path *) + +fun full_path dir path = + let + val path' = Path.expand path; + val _ = Path.is_current path' andalso error "Bad file specification"; + val path'' = Path.append dir path'; + in + if Path.is_absolute path'' then path'' + else Path.append (pwd ()) path'' + end; (* tmp_path *) @@ -66,15 +76,19 @@ val exists = can OS.FileSys.modTime o platform_path; -fun check path = - if exists path then () - else error ("No such file or directory: " ^ Path.print path); - val rm = OS.FileSys.remove o platform_path; fun is_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); +fun check_dir path = + if exists path andalso is_dir path then path + else error ("No such directory: " ^ Path.print path); + +fun check_file path = + if exists path andalso not (is_dir path) then path + else error ("No such file: " ^ Path.print path); + (* open files *) diff -r 2de57cda5b24 -r 143f37194911 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/General/markup.ML Mon Mar 21 08:29:16 2011 +0100 @@ -100,7 +100,7 @@ val elapsedN: string val cpuN: string val gcN: string - val timingN: string val timing: timing -> T + val timingN: string val timing: Timing.timing -> T val subgoalsN: string val proof_stateN: string val proof_state: int -> T val stateN: string val state: T @@ -312,7 +312,7 @@ val cpuN = "cpu"; val gcN = "gc"; -fun timing ({elapsed, cpu, gc, ...}: timing) = +fun timing {elapsed, cpu, gc} = (timingN, [(elapsedN, Time.toString elapsed), (cpuN, Time.toString cpu), diff -r 2de57cda5b24 -r 143f37194911 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/General/output.ML Mon Mar 21 08:29:16 2011 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/output.ML Author: Makarius, Hagia Maria Sion Abbey (Jerusalem) -Output channels and timing messages. +Isabelle output channels. *) signature BASIC_OUTPUT = @@ -10,11 +10,6 @@ val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit - val cond_timeit: bool -> string -> (unit -> 'a) -> 'a - val timeit: (unit -> 'a) -> 'a - val timeap: ('a -> 'b) -> 'a -> 'b - val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b - val timing: bool Unsynchronized.ref end; signature OUTPUT = @@ -111,31 +106,6 @@ fun legacy_feature s = warning ("Legacy feature! " ^ s); - - -(** timing **) - -(*conditional timing with message*) -fun cond_timeit flag msg e = - if flag then - let - val start = start_timing (); - val result = Exn.capture e (); - val end_msg = #message (end_timing start); - val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg); - in Exn.release result end - else e (); - -(*unconditional timing*) -fun timeit e = cond_timeit true "" e; - -(*timed application function*) -fun timeap f x = timeit (fn () => f x); -fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); - -(*global timing mode*) -val timing = Unsynchronized.ref false; - end; structure Basic_Output: BASIC_OUTPUT = Output; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/General/timing.ML Mon Mar 21 08:29:16 2011 +0100 @@ -4,19 +4,46 @@ Basic support for time measurement. *) -val seconds = Time.fromReal; +signature BASIC_TIMING = +sig + val cond_timeit: bool -> string -> (unit -> 'a) -> 'a + val timeit: (unit -> 'a) -> 'a + val timeap: ('a -> 'b) -> 'a -> 'b + val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b +end -fun start_timing () = +signature TIMING = +sig + include BASIC_TIMING + type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time} + type start + val start: unit -> start + val result: start -> timing + val timing: ('a -> 'b) -> 'a -> timing * 'b + val message: timing -> string +end + +structure Timing: TIMING = +struct + +(* timer control *) + +type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}; + +abstype start = Start of + Timer.real_timer * Time.time * Timer.cpu_timer * + {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}} +with + +fun start () = let val real_timer = Timer.startRealTimer (); val real_time = Timer.checkRealTimer real_timer; val cpu_timer = Timer.startCPUTimer (); val cpu_times = Timer.checkCPUTimes cpu_timer; - in (real_timer, real_time, cpu_timer, cpu_times) end; + in Start (real_timer, real_time, cpu_timer, cpu_times) end; -type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time}; - -fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing = +fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = let val real_time2 = Timer.checkRealTimer real_timer; val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; @@ -27,10 +54,41 @@ val elapsed = real_time2 - real_time; val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; val cpu = usr2 - usr + sys2 - sys + gc; + in {elapsed = elapsed, cpu = cpu, gc = gc} end; - val message = - (toString elapsed ^ "s elapsed time, " ^ - toString cpu ^ "s cpu time, " ^ - toString gc ^ "s GC time") handle Time.Time => ""; - in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; +end; + +fun timing f x = + let + val start = start (); + val y = f x; + in (result start, y) end; + + +(* timing messages *) + +fun message {elapsed, cpu, gc} = + Time.toString elapsed ^ "s elapsed time, " ^ + Time.toString cpu ^ "s cpu time, " ^ + Time.toString gc ^ "s GC time" handle Time.Time => ""; +fun cond_timeit enabled msg e = + if enabled then + let + val (timing, result) = timing (Exn.capture e) (); + val end_msg = message timing; + val _ = + if Exn.is_interrupt_exn result then () + else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg); + in Exn.release result end + else e (); + +fun timeit e = cond_timeit true "" e; +fun timeap f x = timeit (fn () => f x); +fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); + +end; + +structure Basic_Timing: BASIC_TIMING = Timing; +open Basic_Timing; + diff -r 2de57cda5b24 -r 143f37194911 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/IsaMakefile Mon Mar 21 08:29:16 2011 +0100 @@ -21,7 +21,6 @@ BOOTSTRAP_FILES = \ General/exn.ML \ - General/timing.ML \ ML-Systems/compiler_polyml-5.2.ML \ ML-Systems/compiler_polyml-5.3.ML \ ML-Systems/ml_name_space.ML \ @@ -101,6 +100,7 @@ General/symbol.ML \ General/symbol_pos.ML \ General/table.ML \ + General/timing.ML \ General/url.ML \ General/xml.ML \ General/xml_data.ML \ diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Mon Mar 21 08:29:16 2011 +0100 @@ -271,7 +271,7 @@ fun load_thy name init pos text = let val (lexs, commands) = get_syntax (); - val time = ! Output.timing; + val time = ! Toplevel.timing; val _ = Present.init_theory name; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Mon Mar 21 08:29:16 2011 +0100 @@ -218,7 +218,7 @@ val quiet = Unsynchronized.ref false; val debug = Runtime.debug; val interact = Unsynchronized.ref false; -val timing = Output.timing; +val timing = Unsynchronized.ref false; val profiling = Unsynchronized.ref 0; val skip_proofs = Unsynchronized.ref false; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Mon Mar 21 08:29:16 2011 +0100 @@ -14,10 +14,12 @@ else use "ML-Systems/single_assignment_polyml.ML"; use "ML-Systems/multithreading.ML"; -use "General/timing.ML"; use "ML-Systems/ml_pretty.ML"; use "ML-Systems/use_context.ML"; +val seconds = Time.fromReal; + + (** ML system and platform related **) diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ML-Systems/proper_int.ML --- a/src/Pure/ML-Systems/proper_int.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ML-Systems/proper_int.ML Mon Mar 21 08:29:16 2011 +0100 @@ -13,8 +13,6 @@ (* Int *) -structure OrigInt = Int; -structure OrigIntInf = IntInf; type int = IntInf.int; structure IntInf = diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Mar 21 08:29:16 2011 +0100 @@ -13,7 +13,6 @@ use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; -use "General/timing.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/ml_pretty.ML"; structure PolyML = struct end; @@ -21,8 +20,9 @@ use "ML-Systems/use_context.ML"; +val seconds = Time.fromReal; + (*low-level pointer equality*) - CM.autoload "$smlnj/init/init.cmi"; val pointer_eq = InlineT.ptreql; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/PIDE/document.ML Mon Mar 21 08:29:16 2011 +0100 @@ -241,9 +241,9 @@ val is_proof = Keyword.is_proof (Toplevel.name_of tr); val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); - val start = start_timing (); + val start = Timing.start (); val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; - val _ = timing tr (end_timing start); + val _ = timing tr (Timing.result start); val _ = List.app (Toplevel.error_msg tr) errs; val res = (case result of diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Mon Mar 21 08:29:16 2011 +0100 @@ -364,7 +364,9 @@ fun string_of_pgipurl p = Path.implode p -fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl))) +fun attrval_of_pgipurl purl = + "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl)) + fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)] val pgipurl_of_attrs = pgipurl_of_string o get_attr "url" diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Mon Mar 21 08:29:16 2011 +0100 @@ -156,7 +156,7 @@ bool_pref Pattern.trace_unify_fail "trace-unification" "Output error diagnostics during unification", - bool_pref Output.timing + bool_pref Toplevel.timing "global-timing" "Whether to enable timing in Isabelle.", bool_pref Toplevel.debug diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Mar 21 08:29:16 2011 +0100 @@ -588,14 +588,14 @@ fun filerefs f = let val thy = thy_name f - val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy) + val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy)) in issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, name=NONE, idtables=[], fileurls=filerefs}) end fun thyrefs thy = - let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy) + let val thyrefs = #imports (Thy_Load.check_thy Path.current thy) in issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, diff -r 2de57cda5b24 -r 143f37194911 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/ROOT.ML Mon Mar 21 08:29:16 2011 +0100 @@ -21,6 +21,7 @@ use "General/alist.ML"; use "General/table.ML"; use "General/output.ML"; +use "General/timing.ML"; use "General/properties.ML"; use "General/markup.ML"; use "General/scan.ML"; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/System/session.ML Mon Mar 21 08:29:16 2011 +0100 @@ -92,22 +92,21 @@ fun dumping (_, "") = NONE | dumping (cp, path) = SOME (cp, Path.explode path); -fun use_dir item root build modes reset info doc doc_graph doc_versions parent +fun use_dir item root build modes reset info doc doc_graph doc_variants parent name dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = ((fn () => (init reset parent name; - Present.init build info doc doc_graph doc_versions (path ()) name + Present.init build info doc doc_graph doc_variants (path ()) name (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())); if timing then let - val start = start_timing (); + val start = Timing.start (); val _ = use root; - val stop = end_timing start; val _ = Output.raw_stderr ("Timing " ^ item ^ " (" ^ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ - #message stop ^ ")\n"); + Timing.message (Timing.result start) ^ ")\n"); in () end else use root; finish ())) diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Thy/present.ML Mon Mar 21 08:29:16 2011 +0100 @@ -6,7 +6,7 @@ signature BASIC_PRESENT = sig - val no_document: ('a -> 'b) -> 'a -> 'b + val no_document: ('a -> 'b) -> 'a -> 'b (*not thread-safe!*) end; signature PRESENT = @@ -18,8 +18,9 @@ val display_graph: {name: string, ID: string, dir: string, unfold: bool, path: string, parents: string list} list -> unit val init: bool -> bool -> string -> bool -> string list -> string list -> - string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit - val finish: unit -> unit + string -> (bool * Path.T) option -> Url.T option * bool -> bool -> + theory list -> unit (*not thread-safe!*) + val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit val theory_source: string -> (unit -> HTML.text) -> unit val theory_output: string -> string -> unit @@ -64,7 +65,7 @@ (** additional theory data **) -structure BrowserInfoData = Theory_Data +structure Browser_Info = Theory_Data ( type T = {name: string, session: string list, is_local: bool}; val empty = {name = "", session = [], is_local = false}: T; @@ -72,8 +73,8 @@ fun merge _ = empty; ); -val put_info = BrowserInfoData.put; -val get_info = BrowserInfoData.get; +val put_info = Browser_Info.put; +val get_info = Browser_Info.get; val session_name = #name o get_info; @@ -107,7 +108,6 @@ let val name = Context.theory_name thy; val {name = sess_name, session, is_local} = get_info thy; - val path' = Path.append (Path.make session) (html_path name); val entry = {name = name, ID = ID_of session name, dir = sess_name, path = @@ -165,14 +165,14 @@ CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f)); val suppress_tex_source = Unsynchronized.ref false; -fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; (* FIXME unreliable *) +fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; fun init_theory_info name info = change_browser_info (fn (theories, files, tex_index, html_index, graph) => (Symtab.update (name, info) theories, files, tex_index, html_index, graph)); fun change_theory_info name f = - change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) => + change_browser_info (fn (theories, files, tex_index, html_index, graph) => (case Symtab.lookup theories name of NONE => error ("Browser info: cannot access theory document " ^ quote name) | SOME info => (Symtab.update (name, map_theory_info f info) theories, files, @@ -203,9 +203,6 @@ fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => (tex_source, Buffer.add txt html_source, html)); -fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) => - (tex_source, html_source, Buffer.add txt html)); - (** global session state **) @@ -215,16 +212,16 @@ type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, - doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option, - remote_path: Url.T option, verbose: bool, readme: Path.T option}; + dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool, + readme: Path.T option}; fun make_session_info (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, - doc_prefix1, doc_prefix2, remote_path, verbose, readme) = + dump_prefix, remote_path, verbose, readme) = {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, - doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path, - verbose = verbose, readme = readme}: session_info; + dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose, + readme = readme}: session_info; (* state *) @@ -232,7 +229,6 @@ val session_info = Unsynchronized.ref (NONE: session_info option); fun with_session x f = (case ! session_info of NONE => x | SOME info => f info); -fun with_context f = f (Context.theory_name (ML_Context.the_global_context ())); @@ -256,22 +252,22 @@ session_entries (get_entries dir) ^ HTML.end_document |> File.write (Path.append dir index_path); -fun update_index dir name = CRITICAL (fn () => +fun update_index dir name = (case try get_entries dir of NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir) - | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir))); + | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); -(* document versions *) +(* document variants *) -fun read_version str = +fun read_variant str = (case space_explode "=" str of [name] => (name, "") | [name, tags] => (name, tags) - | _ => error ("Malformed document version specification: " ^ quote str)); + | _ => error ("Malformed document variant specification: " ^ quote str)); -fun read_versions strs = - rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs))) +fun read_variants strs = + rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs))) |> filter_out (fn (_, s) => s = "-"); @@ -279,9 +275,9 @@ fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); -fun init build info doc doc_graph doc_versions path name doc_prefix2 - (remote_path, first_time) verbose thys = CRITICAL (fn () => - if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then +fun init build info doc doc_graph doc_variants path name dump_prefix + (remote_path, first_time) verbose thys = + if not build andalso not info andalso doc = "" andalso is_none dump_prefix then (browser_info := empty_browser_info; session_info := NONE) else let @@ -290,16 +286,15 @@ val sess_prefix = Path.make path; val html_prefix = Path.append (Path.expand output_path) sess_prefix; - val (doc_prefix1, documents) = - if doc = "" then (NONE, []) - else if not (File.exists document_path) then - (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); - (NONE, [])) - else (SOME (Path.append html_prefix document_path, html_prefix), - read_versions doc_versions); + val documents = + if doc = "" then [] + else if not (can File.check_dir document_path) then + (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); []) + else read_variants doc_variants; val parent_index_path = Path.append Path.parent index_path; - val index_up_lnk = if first_time then + val index_up_lnk = + if first_time then Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path)) else Url.File parent_index_path; val readme = @@ -309,15 +304,16 @@ val docs = (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ - map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; + map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; val index_text = HTML.begin_index (index_up_lnk, parent_name) (Url.File index_path, session_name) docs (Url.explode "medium.html"); in - session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, - info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); + session_info := + SOME (make_session_info (name, parent_name, session_name, path, html_prefix, + info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme)); browser_info := init_browser_info remote_path path thys; add_html_index (0, index_text) - end); + end; (* isabelle tool wrappers *) @@ -365,9 +361,9 @@ write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; -fun finish () = CRITICAL (fn () => - with_session () (fn {name, info, html_prefix, doc_format, doc_graph, - documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} => +fun finish () = + with_session () (fn {name, info, html_prefix, doc_format, + doc_graph, documents, dump_prefix, path, verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -379,7 +375,7 @@ val sorted_graph = sorted_index graph; val opt_graphs = - if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then + if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then SOME (isabelle_browser sorted_graph) else NONE; @@ -393,41 +389,46 @@ File.write (Path.append path graph_eps_path) eps)); write_tex_index tex_index path; List.app (finish_tex path) thys); + val _ = + if info then + (Isabelle_System.mkdirs (Path.append html_prefix session_path); + File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); + File.write (Path.append html_prefix session_entries_path) ""; + create_index html_prefix; + if length path > 1 then update_index parent_html_prefix name else (); + (case readme of NONE => () | SOME path => File.copy path html_prefix); + write_graph sorted_graph (Path.append html_prefix graph_path); + Isabelle_System.isabelle_tool "browser" "-b"; + File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; + List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) + (HTML.applet_pages name (Url.File index_path, name)); + File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; + List.app finish_html thys; + List.app (uncurry File.write) files; + if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") + else ()) + else (); + + val _ = + (case dump_prefix of NONE => () | SOME (cp, path) => + (prepare_sources cp path; + if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") + else ())); + + val doc_paths = + documents |> Par_List.map (fn (name, tags) => + let + val path = Path.append html_prefix (Path.basic name); + val _ = prepare_sources true path; + in isabelle_document true doc_format name tags path html_prefix end); + val _ = + if verbose then + doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n")) + else (); in - if info then - (Isabelle_System.mkdirs (Path.append html_prefix session_path); - File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); - File.write (Path.append html_prefix session_entries_path) ""; - create_index html_prefix; - if length path > 1 then update_index parent_html_prefix name else (); - (case readme of NONE => () | SOME path => File.copy path html_prefix); - write_graph sorted_graph (Path.append html_prefix graph_path); - Isabelle_System.isabelle_tool "browser" "-b"; - File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; - List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) - (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; - List.app finish_html thys; - List.app (uncurry File.write) files; - if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ()) - else (); - - (case doc_prefix2 of NONE => () | SOME (cp, path) => - (prepare_sources cp path; - if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ())); - - (case doc_prefix1 of NONE => () | SOME (path, result_path) => - documents |> List.app (fn (name, tags) => - let - val _ = prepare_sources true path; - val doc_path = isabelle_document true doc_format name tags path result_path; - in - if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else () - end)); - browser_info := empty_browser_info; session_info := NONE - end)); + end); (* theory elements *) @@ -462,7 +463,7 @@ val files_html = files |> map (fn (raw_path, loadit) => let - val path = #1 (Thy_Load.check_file dir raw_path); + val path = Thy_Load.check_file dir raw_path; val base = Path.base path; val base_html = html_ext base; val _ = add_file (Path.append html_prefix base_html, diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Thy/term_style.ML Mon Mar 21 08:29:16 2011 +0100 @@ -19,7 +19,7 @@ fun err_dup_style name = error ("Duplicate declaration of antiquote style: " ^ quote name); -structure StyleData = Theory_Data +structure Styles = Theory_Data ( type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; val empty = Symtab.empty; @@ -32,12 +32,12 @@ (* accessors *) fun the_style thy name = - (case Symtab.lookup (StyleData.get thy) name of + (case Symtab.lookup (Styles.get thy) name of NONE => error ("Unknown antiquote style: " ^ quote name) | SOME (style, _) => style); fun setup name style thy = - StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy + Styles.map (Symtab.update_new (name, (style, stamp ()))) thy handle Symtab.DUP _ => err_dup_style name; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Thy/thy_header.ML Mon Mar 21 08:29:16 2011 +0100 @@ -7,7 +7,7 @@ signature THY_HEADER = sig val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list - val read: Position.T -> string -> string * string list * (string * bool) list + val read: Position.T -> string -> string * string list * (Path.T * bool) list val thy_path: string -> Path.T val split_thy_path: Path.T -> Path.T * string val consistent_name: string -> string -> unit @@ -63,7 +63,8 @@ |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |> Source.get_single; in - (case res of SOME (x, _) => x + (case res of + SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses) | NONE => error ("Unexpected end of input" ^ Position.str_of pos)) end; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Thy/thy_info.ML Mon Mar 21 08:29:16 2011 +0100 @@ -232,7 +232,7 @@ val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val pos = Path.position thy_path; - val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text)); + val (_, _, uses) = Thy_Header.read pos text; fun init _ = Thy_Load.begin_theory dir name imports parent_thys uses |> Present.begin_theory update_time dir uses; @@ -251,24 +251,20 @@ fun check_deps dir name = (case lookup_deps name of - SOME NONE => (true, NONE, get_parents name, NONE) + SOME NONE => (true, NONE, get_parents name) | NONE => - let val {master, text, imports, ...} = Thy_Load.deps_thy dir name - in (false, SOME (make_deps master imports), imports, SOME text) end + let val {master, text, imports, ...} = Thy_Load.check_thy dir name + in (false, SOME (make_deps master imports, text), imports) end | SOME (SOME {master, imports}) => - let val master' = Thy_Load.check_thy dir name in - if #2 master <> #2 master' then - let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name; - in (false, SOME (make_deps master' imports'), imports', SOME text') end - else - let - val current = - (case lookup_theory name of - NONE => false - | SOME theory => Thy_Load.all_current theory); - val deps' = SOME (make_deps master' imports); - in (current, deps', imports, NONE) end - end); + let + val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name; + val deps' = SOME (make_deps master' imports', text'); + val current = + #2 master = #2 master' andalso + (case lookup_theory name of + NONE => false + | SOME theory => Thy_Load.all_current theory); + in (current, deps', imports') end); in @@ -285,14 +281,15 @@ SOME task => (task_finished task, tasks) | NONE => let - val (current, deps, imports, opt_text) = check_deps dir' name + val (current, deps, imports) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ required_by "\n" initiators); val parents = map base_name imports; val (parents_current, tasks') = - require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks; + require_thys (name :: initiators) + (Path.append dir (master_dir (Option.map #1 deps))) imports tasks; val all_current = current andalso parents_current; val task = @@ -300,10 +297,8 @@ else (case deps of NONE => raise Fail "Malformed deps" - | SOME (dep as {master = (thy_path, _), ...}) => - let - val text = (case opt_text of SOME text => text | NONE => File.read thy_path); - val update_time = serial (); + | SOME (dep, text) => + let val update_time = serial () in Task (parents, load_thy initiators update_time dep text name) end); in (all_current, new_entry name parents task tasks') end) end; @@ -336,7 +331,7 @@ fun register_thy theory = let val name = Context.theory_name theory; - val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name; + val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; val parents = map Context.theory_name (Theory.parents_of theory); val imports = Thy_Load.imports_of theory; val deps = make_deps master imports; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Thy/thy_load.ML Mon Mar 21 08:29:16 2011 +0100 @@ -1,27 +1,25 @@ (* Title: Pure/Thy/thy_load.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Loading files that contribute to a theory, including global load path -management. +Loading files that contribute to a theory. Global master path. *) signature THY_LOAD = sig - val set_master_path: Path.T -> unit - val get_master_path: unit -> Path.T val master_directory: theory -> Path.T val imports_of: theory -> string list val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory - val check_file: Path.T -> Path.T -> Path.T * SHA1.digest - val check_thy: Path.T -> string -> Path.T * SHA1.digest - val deps_thy: Path.T -> string -> - {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list} + val check_file: Path.T -> Path.T -> Path.T + val check_thy: Path.T -> string -> + {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list} val loaded_files: theory -> Path.T list val all_current: theory -> bool val provide_file: Path.T -> theory -> theory val use_ml: Path.T -> unit val exec_ml: Path.T -> generic_theory -> generic_theory val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory + val set_master_path: Path.T -> unit + val get_master_path: unit -> Path.T end; structure Thy_Load: THY_LOAD = @@ -69,51 +67,25 @@ else (master_dir, imports, required, (src_path, path_id) :: provided)); -(* stateful master path *) - -local - val master_path = Unsynchronized.ref Path.current; -in - -fun set_master_path path = master_path := path; -fun get_master_path () = ! master_path; - -end; - - (* check files *) -fun get_file dir src_path = +fun check_file dir file = File.check_file (File.full_path dir file); + +fun digest_file dir file = let - val path = Path.expand src_path; - val _ = Path.is_current path andalso error "Bad file specification"; - val full_path = File.full_path (Path.append dir path); - in - if File.exists full_path - then SOME (full_path, SHA1.digest (File.read full_path)) - else NONE - end; - -fun check_file dir file = - (case get_file dir file of - SOME path_id => path_id - | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir)); + val full_path = check_file dir file; + val id = SHA1.digest (File.read full_path); + in (full_path, id) end; fun check_thy dir name = - check_file dir (Thy_Header.thy_path name); - - -(* theory deps *) - -fun deps_thy master_dir name = let - val master as (thy_path, _) = check_thy master_dir name; - val text = File.read thy_path; - val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text; + val master_file = check_file dir (Thy_Header.thy_path name); + val text = File.read master_file; + val (name', imports, uses) = + if name = Context.PureN then (Context.PureN, [], []) + else Thy_Header.read (Path.position master_file) text; val _ = Thy_Header.consistent_name name name'; - val uses = map (Path.explode o #1) uses; - in {master = master, text = text, imports = imports, uses = uses} end; - + in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end; (* loaded files *) @@ -138,7 +110,7 @@ let val {master_dir, provided, ...} = Files.get thy; fun current (src_path, (_, id)) = - (case get_file master_dir src_path of + (case try (digest_file master_dir) src_path of NONE => false | SOME (_, id') => id = id'); in can check_loaded thy andalso forall current provided end; @@ -149,15 +121,15 @@ (* provide files *) fun provide_file src_path thy = - provide (src_path, check_file (master_directory thy) src_path) thy; + provide (src_path, digest_file (master_directory thy) src_path) thy; fun use_ml src_path = if is_none (Context.thread_data ()) then - ML_Context.eval_file (#1 (check_file Path.current src_path)) + ML_Context.eval_file (check_file Path.current src_path) else let val thy = ML_Context.the_global_context (); - val (path, id) = check_file (master_directory thy) src_path; + val (path, id) = digest_file (master_directory thy) src_path; val _ = ML_Context.eval_file path; val _ = Context.>> Local_Theory.propagate_ml_env; @@ -178,5 +150,16 @@ |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |> Theory.checkpoint; + +(* global master path *) + +local + val master_path = Unsynchronized.ref Path.current; +in + +fun set_master_path path = master_path := path; +fun get_master_path () = ! master_path; + end; +end; diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Tools/find_consts.ML Mon Mar 21 08:29:16 2011 +0100 @@ -69,7 +69,7 @@ fun find_consts ctxt raw_criteria = let - val start = start_timing (); + val start = Timing.start (); val thy = ProofContext.theory_of ctxt; val low_ranking = 10000; @@ -114,7 +114,7 @@ |> sort (rev_order o int_ord o pairself snd) |> map (apsnd fst o fst); - val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; + val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; in Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: Pretty.str "" :: diff -r 2de57cda5b24 -r 143f37194911 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/Tools/find_theorems.ML Mon Mar 21 08:29:16 2011 +0100 @@ -464,7 +464,7 @@ fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let - val start = start_timing (); + val start = Timing.start (); val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt)) @@ -480,7 +480,7 @@ then " (" ^ string_of_int returned ^ " displayed)" else "")); - val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; + val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; in Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" :: diff -r 2de57cda5b24 -r 143f37194911 src/Pure/theory.ML --- a/src/Pure/theory.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Pure/theory.ML Mon Mar 21 08:29:16 2011 +0100 @@ -84,7 +84,7 @@ fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers}; -structure ThyData = Theory_Data_PP +structure Thy = Theory_Data_PP ( type T = thy; val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; @@ -104,9 +104,9 @@ in make_thy (axioms', defs', (bgs', ens')) end; ); -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args); +fun rep_theory thy = Thy.get thy |> (fn Thy args => args); -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) => +fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) => make_thy (f (axioms, defs, wrappers))); diff -r 2de57cda5b24 -r 143f37194911 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Tools/Code/code_haskell.ML Mon Mar 21 08:29:16 2011 +0100 @@ -350,7 +350,7 @@ (*serialization*) fun write_module width (SOME destination) (module_name, content) = let - val _ = File.check destination; + val _ = File.check_dir destination; val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode o separate "/" o Long_Name.explode) module_name; val _ = Isabelle_System.mkdirs (Path.dir filepath); diff -r 2de57cda5b24 -r 143f37194911 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Tools/quickcheck.ML Mon Mar 21 08:29:16 2011 +0100 @@ -166,12 +166,9 @@ error "Term to be tested contains schematic variables"; in () end -fun cpu_time description f = - let - val start = start_timing () - val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) - in (Exn.release result, (description, time)) end +fun cpu_time description e = + let val ({cpu, ...}, result) = Timing.timing e () + in (result, (description, Time.toMilliseconds cpu)) end fun limit ctxt (limit_time, is_interactive) f exc () = if limit_time then