--- 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.).
--- 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
--- 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;
--- 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 ..
--- 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, " ^
--- 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
--- 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
--- 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
--- 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
--- 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 ())
--- 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
--- 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
--- 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"
--- 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 *)
--- 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 *)
--- 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 *)
--- 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 *)
--- 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 *)
--- 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 *)
--- 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 *)
--- 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
--- 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;
--- 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
--- 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
--- 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))
--- 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
--- 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
--- 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)
--- 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;
*}
--- 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;
--- 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 *)
--- 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),
--- 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;
--- 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;
+
--- 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 \
--- 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;
--- 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;
--- 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 **)
--- 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 =
--- 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;
--- 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
--- 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"
--- 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
--- 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,
--- 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";
--- 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 ()))
--- 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,
--- 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;
--- 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;
--- 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;
--- 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;
--- 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 "" ::
--- 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 "" ::
--- 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)));
--- 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);
--- 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