--- a/NEWS Sat Feb 08 17:24:19 2025 +0100
+++ b/NEWS Sat Feb 08 17:44:04 2025 +0100
@@ -343,6 +343,8 @@
* Theory "HOL-Library.Suc_Notation" provides compact notation for
iterated Suc terms.
+* Theory "HOL.Nat": of_nat_diff is now a simprule, minor INCOMPATIBILITY.
+
* Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
INCOMPATIBILITY: need to adjust theory imports.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Feb 08 17:44:04 2025 +0100
@@ -1653,7 +1653,6 @@
;
@@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
- @{syntax nat}?
;
@@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
--- a/src/Doc/Sugar/Sugar.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Doc/Sugar/Sugar.thy Sat Feb 08 17:44:04 2025 +0100
@@ -486,8 +486,7 @@
\<close>
lemma True
proof -
- \<comment> \<open>pretty trivial\<close>
- show True by force
+ show True by (rule TrueI)
qed
text_raw \<open>
\end{minipage}\end{center}
@@ -498,21 +497,20 @@
\begin{quote}
\small
-\verb!text_raw {!\verb!*!\\
+\verb!text_raw \!\verb!<open>!\\
\verb! \begin{figure}!\\
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
\verb! \isastyleminor\isamarkuptrue!\\
-\verb!*!\verb!}!\\
+\verb!\!\verb!<close>!\\
\verb!lemma True!\\
\verb!proof -!\\
-\verb! -- "pretty trivial"!\\
-\verb! show True by force!\\
+\verb! show True by (rule TrueI)!\\
\verb!qed!\\
-\verb!text_raw {!\verb!*!\\
+\verb!text_raw \!\verb!<open>!\\
\verb! \end{minipage}\end{center}!\\
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
\verb! \end{figure}!\\
-\verb!*!\verb!}!
+\verb!\!\verb!<close>!
\end{quote}
Other theory text, e.g.\ definitions, can be put in figures, too.
@@ -535,9 +533,9 @@
You have to place the following lines before and after the snippet, where snippets must always be
consecutive lines of theory text:
\begin{quote}
-\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
+\verb!\text_raw\!\verb!<open>\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!<close>!\\
\emph{theory text}\\
-\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
+\verb!\text_raw\!\verb!<open>%endsnip\!\verb!<close>!
\end{quote}
where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
and \texttt{2} are explained in a moment.
--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sat Feb 08 17:44:04 2025 +0100
@@ -26,13 +26,21 @@
val print_timing': Proof.context -> pfunc -> pfunc -> unit
val print_timing: Proof.context -> Function.info -> Function.info -> unit
+type time_config = {
+ print: bool,
+ simp: bool,
+ partial: bool
+}
+datatype result = Function of Function.info | PartialFunction of thm
val reg_and_proove_time_func: local_theory -> term list -> term list
- -> bool -> bool -> Function.info * local_theory
+ -> time_config -> result * local_theory
val reg_time_func: local_theory -> term list -> term list
- -> bool -> bool -> Function.info * local_theory
+ -> time_config -> result * local_theory
+
val time_dom_tac: Proof.context -> thm -> thm list -> int -> tactic
+
end
structure Timing_Functions : TIMING_FUNCTIONS =
@@ -43,9 +51,6 @@
(* Configure config variable to adjust the suffix *)
val bsuffix = Attrib.setup_config_string @{binding "time_suffix"} (K "")
-(* some default values to build terms easier *)
-val zero = Const (@{const_name "Groups.zero"}, HOLogic.natT)
-val one = Const (@{const_name "Groups.one"}, HOLogic.natT)
(* Extracts terms from function info *)
fun terms_of_info (info: Function.info) =
map Thm.prop_of (case #simps info of SOME s => s
@@ -132,15 +137,6 @@
(* returns true if it's a let term *)
fun is_let (Const (@{const_name "HOL.Let"},_)) = true
| is_let _ = false
-(* change type of original function to new type (_ \<Rightarrow> ... \<Rightarrow> _ to _ \<Rightarrow> ... \<Rightarrow> nat)
- and replace all function arguments f with (t*T_f) if used *)
-fun change_typ' used (Type ("fun", [T1, T2])) =
- Type ("fun", [check_for_fun' (used 0) T1, change_typ' (fn i => used (i+1)) T2])
- | change_typ' _ _ = HOLogic.natT
-and check_for_fun' true (f as Type ("fun", [_,_])) = HOLogic.mk_prodT (f, change_typ' (K false) f)
- | check_for_fun' false (f as Type ("fun", [_,_])) = change_typ' (K true) f
- | check_for_fun' _ t = t
-val change_typ = change_typ' (K true)
(* Convert string name of function to its timing equivalent *)
fun fun_name_to_time' ctxt s second name =
let
@@ -186,28 +182,6 @@
fun const_comp (Const (nm,T)) (Const (nm',T')) = nm = nm' andalso typ_comp T T'
| const_comp _ _ = false
-fun time_term ctxt s (Const (nm,T)) =
-let
- val T_nm = fun_name_to_time ctxt s nm
- val T_T = change_typ T
-in
-(SOME (Syntax.check_term ctxt (Const (T_nm,T_T))))
- handle (ERROR _) =>
- case Syntax.read_term ctxt (Long_Name.base_name T_nm)
- of (Const (T_nm,T_T)) =>
- let
- fun col_Used i (Type ("fun", [Type ("fun", _), Ts])) (Type ("fun", [T', Ts'])) =
- (if is_Used T' then [i] else []) @ col_Used (i+1) Ts Ts'
- | col_Used i (Type ("fun", [_, Ts])) (Type ("fun", [_, Ts'])) = col_Used (i+1) Ts Ts'
- | col_Used _ _ _ = []
- in
- SOME (Const (T_nm,change_typ' (contains (col_Used 0 T T_T)) T))
- end
- | _ => error ("Timing function of " ^ nm ^ " is not defined")
-end
- | time_term _ _ _ = error "Internal error: No valid function given"
-
-
type 'a wctxt = {
ctxt: local_theory,
origins: term list,
@@ -262,6 +236,23 @@
| freeTerms t = t
fun freeTypes (TVar ((t, _), T)) = TFree (t, T)
| freeTypes t = t
+fun fix_definition (Const ("Pure.eq", _) $ l $ r) = HOLogic.mk_Trueprop (HOLogic.mk_eq (l,r))
+ | fix_definition t = t
+fun check_definition [t] = [t]
+ | check_definition _ = error "Only a single definition is allowed"
+fun get_terms theory (term: term) =
+let
+ val equations = Spec_Rules.retrieve theory term
+ |> map #rules
+ |> map (map Thm.prop_of)
+ handle Empty => error "Function or terms of function not found"
+in
+ equations
+ |> map (map fix_definition)
+ |> filter (List.exists
+ (fn t => typ_comp (t |> get_l |> strip_comb |> fst |> dest_Const |> snd) (term |> strip_comb |> fst |> dest_Const |> snd)))
+ |> hd
+end
fun fixCasecCases _ [t] = [t]
| fixCasecCases wctxt (t::ts) =
@@ -348,193 +339,6 @@
}) o get_r
fun is_rec ctxt (term: term list) = List.foldr (or (find_rec ctxt term)) false
-(* 3. Convert equations *)
-(* Some Helper *)
-val plusTyp = @{typ "nat => nat => nat"}
-fun plus (SOME a) (SOME b) = SOME (Const (@{const_name "Groups.plus"}, plusTyp) $ a $ b)
- | plus (SOME a) NONE = SOME a
- | plus NONE (SOME b) = SOME b
- | plus NONE NONE = NONE
-fun opt_term NONE = HOLogic.zero
- | opt_term (SOME t) = t
-fun use_origin (Free (nm, T as Type ("fun",_))) = HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
- | use_origin t = t
-
-(* Conversion of function term *)
-fun fun_to_time' ctxt (origin: term list) second (func as Const (nm,T)) =
-let
- val origin' = map (fst o strip_comb) origin
-in
- if contains' const_comp origin' func then SOME (Free (func |> Term.term_name |> fun_name_to_time' ctxt true second, change_typ T)) else
- if Zero_Funcs.is_zero (Proof_Context.theory_of ctxt) (nm,T) then NONE else
- time_term ctxt false func
-end
- | fun_to_time' _ _ _ (Free (nm,T)) =
- SOME (HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ T))))
- | fun_to_time' _ _ _ _ = error "Internal error: invalid function to convert"
-fun fun_to_time context origin func = fun_to_time' context origin false func
-
-(* Convert arguments of left side of a term *)
-fun conv_arg _ (Free (nm,T as Type("fun",_))) =
- Free (nm, HOLogic.mk_prodT (T, change_typ' (K false) T))
- | conv_arg _ x = x
-fun conv_args ctxt = map (conv_arg ctxt)
-
-(* Handle function calls *)
-fun build_zero (Type ("fun", [T, R])) = Abs ("uu", T, build_zero R)
- | build_zero _ = zero
-fun funcc_use_origin (Free (nm, T as Type ("fun",_))) =
- HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
- | funcc_use_origin t = t
-fun funcc_conv_arg _ _ (t as (_ $ _)) = map_aterms funcc_use_origin t
- | funcc_conv_arg _ u (Free (nm, T as Type ("fun",_))) =
- if u then Free (nm, HOLogic.mk_prodT (T, change_typ T))
- else HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ T)))
- | funcc_conv_arg wctxt true (f as Const (_,Type ("fun",_))) =
- HOLogic.mk_prod (f, funcc_conv_arg wctxt false f)
- | funcc_conv_arg wctxt false (f as Const (_,T as Type ("fun",_))) =
- Option.getOpt (fun_to_time (#ctxt wctxt) (#origins wctxt) f, build_zero T)
- | funcc_conv_arg wctxt false (f as Abs _) =
- f
- |> Term.strip_abs_eta ((length o fst o strip_type o type_of) f)
- ||> #f wctxt ||> opt_term
- |> list_abs
- | funcc_conv_arg wctxt true (f as Abs _) =
- let
- val f' = f
- |> Term.strip_abs_eta ((length o fst o strip_type o type_of) f)
- ||> map_aterms funcc_use_origin
- |> list_abs
- in
- HOLogic.mk_prod (f', funcc_conv_arg wctxt false f)
- end
- | funcc_conv_arg _ _ t = t
-
-fun funcc_conv_args _ _ [] = []
- | funcc_conv_args wctxt (Type ("fun", [t, ts])) (a::args) =
- funcc_conv_arg wctxt (is_Used t) a :: funcc_conv_args wctxt ts args
- | funcc_conv_args _ _ _ = error "Internal error: Non matching type"
-fun funcc wctxt func args =
-let
- fun get_T (Free (_,T)) = T
- | get_T (Const (_,T)) = T
- | get_T (_ $ (Free (_,Type (_, [_, T])))) = T (* Case of snd was constructed *)
- | get_T _ = error "Internal error: Forgotten type"
-in
- List.foldr (I #-> plus)
- (case fun_to_time (#ctxt wctxt) (#origins wctxt) func (* add case for abs *)
- of SOME t => SOME (list_comb (t, funcc_conv_args wctxt (get_T t) args))
- | NONE => NONE)
- (map (#f wctxt) args)
-end
-
-(* Handle case terms *)
-fun casecIsCase (Type (n1, [_,Type (n2, _)])) = (n1 = "fun" andalso n2 = "fun")
- | casecIsCase _ = false
-fun casecLastTyp (Type (n, [T1,T2])) = Type (n, [T1, change_typ T2])
- | casecLastTyp _ = error "Internal error: Invalid case type"
-fun casecTyp (Type (n, [T1, T2])) =
- Type (n, [change_typ T1, (if casecIsCase T2 then casecTyp else casecLastTyp) T2])
- | casecTyp _ = error "Internal error: Invalid case type"
-fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f (subst_bound (Free (v,Ta), t))
- of (nconst,t) => (nconst,absfree (v,Ta) t))
- | casecAbs f t = (case f t of NONE => (false,HOLogic.zero) | SOME t => (true,t))
-fun casecArgs _ [t] = (false, [map_aterms use_origin t])
- | casecArgs f (t::ar) =
- (case casecAbs f t of (nconst, tt) =>
- casecArgs f ar ||> (fn ar => tt :: ar) |>> (if nconst then K true else I))
- | casecArgs _ _ = error "Internal error: Invalid case term"
-fun casec wctxt (Const (t,T)) args =
- if not (casecIsCase T) then error "Internal error: Invalid case type" else
- let val (nconst, args') = casecArgs (#f wctxt) args in
- plus
- ((#f wctxt) (List.last args))
- (if nconst then
- SOME (list_comb (Const (t,casecTyp T), args'))
- else NONE)
- end
- | casec _ _ _ = error "Internal error: Invalid case term"
-
-(* Handle if terms -> drop the term if true and false terms are zero *)
-fun ifc wctxt _ cond tt ft =
- let
- val f = #f wctxt
- val rcond = map_aterms use_origin cond
- val tt = f tt
- val ft = f ft
- in
- plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
- if tt = ft then tt else
- (SOME ((Const (@{const_name "HOL.If"}, @{typ "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"})) $ rcond $ (opt_term tt) $ (opt_term ft))))
- end
-
-fun letc_lambda wctxt T (t as Abs _) =
- HOLogic.mk_prod (map_aterms use_origin t,
- Term.strip_abs_eta (strip_type T |> fst |> length) t ||> #f wctxt ||> opt_term |> list_abs)
- | letc_lambda _ _ t = map_aterms use_origin t
-fun letc wctxt expT exp ([(nm,_)]) t =
- plus (#f wctxt exp)
- (case #f wctxt t of SOME t' =>
- (if Term.used_free nm t'
- then
- let
- val exp' = letc_lambda wctxt expT exp
- val t' = list_abs ([(nm,fastype_of exp')], t')
- in
- Const (@{const_name "HOL.Let"}, [fastype_of exp', fastype_of t'] ---> HOLogic.natT) $ exp' $ t'
- end
- else t') |> SOME
- | NONE => NONE)
- | letc _ _ _ _ _ = error "Unknown let state"
-
-fun constc _ (Const ("HOL.undefined", _)) = SOME (Const ("HOL.undefined", @{typ "nat"}))
- | constc _ _ = NONE
-
-(* The converter for timing functions given to the walker *)
-val converter : term option converter = {
- constc = constc,
- funcc = funcc,
- ifc = ifc,
- casec = casec,
- letc = letc
- }
-fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
-
-(* Use converter to convert right side of a term *)
-fun to_time ctxt origin is_rec term =
- top_converter is_rec ctxt origin (walk ctxt origin converter term)
-
-(* Converts a term to its running time version *)
-fun convert_term ctxt (origin: term list) is_rec (pT $ (Const (eqN, _) $ l $ r)) =
-let
- val (l_const, l_params) = strip_comb l
-in
- pT
- $ (Const (eqN, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
- $ (list_comb (l_const |> fun_to_time ctxt origin |> Option.valOf, l_params |> conv_args ctxt))
- $ (to_time ctxt origin is_rec r))
-end
- | convert_term _ _ _ _ = error "Internal error: invalid term to convert"
-
-(* 3.5 Support for locales *)
-fun replaceFstSndFree ctxt (origin: term list) (rfst: term -> term) (rsnd: term -> term) =
- (walk ctxt origin {
- funcc = fn wctxt => fn t => fn args =>
- case args of
- (f as Free _)::args =>
- (case t of
- Const ("Product_Type.prod.fst", _) =>
- list_comb (rfst (t $ f), map (#f wctxt) args)
- | Const ("Product_Type.prod.snd", _) =>
- list_comb (rsnd (t $ f), map (#f wctxt) args)
- | t => list_comb (t, map (#f wctxt) (f :: args)))
- | args => list_comb (t, map (#f wctxt) args),
- constc = Iconst,
- ifc = Iif,
- casec = Icase,
- letc = Ilet
- })
-
(* 4. Tactic to prove "f_dom n" *)
fun time_dom_tac ctxt induct_rule domintros =
(Induction.induction_tac ctxt true [] [[]] [] (SOME [induct_rule]) []
@@ -542,211 +346,445 @@
(if i <= length domintros then [Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [List.nth (domintros, i-1)]] else []) @
[Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt domintros]) i)))
-
-fun fix_definition (Const ("Pure.eq", _) $ l $ r) = HOLogic.mk_Trueprop (HOLogic.mk_eq (l,r))
- | fix_definition t = t
-fun check_definition [t] = [t]
- | check_definition _ = error "Only a single definition is allowed"
-fun get_terms theory (term: term) =
-let
- val equations = Spec_Rules.retrieve theory term
- |> map #rules
- |> map (map Thm.prop_of)
- handle Empty => error "Function or terms of function not found"
-in
- equations
- |> map (map fix_definition)
- |> filter (List.exists
- (fn t => typ_comp (t |> get_l |> strip_comb |> fst |> dest_Const |> snd) (term |> strip_comb |> fst |> dest_Const |> snd)))
- |> hd
-end
-
-(* 5. Check for higher-order function if original function is used \<rightarrow> find simplifications *)
-fun find_used' T_t =
-let
- val (T_ident, T_args) = strip_comb (get_l T_t)
+(* Register timing function of a given function *)
+type time_config = {
+ print: bool,
+ simp: bool,
+ partial: bool
+}
+datatype result = Function of Function.info | PartialFunction of thm
+fun reg_time_func (lthy: local_theory) (term: term list) (terms: term list) (config: time_config) =
+ let
+ (* some default values to build terms easier *)
+ (* Const (@{const_name "Groups.zero"}, HOLogic.natT) *)
+ val zero = if #partial config then @{term "Some (0::nat)"} else HOLogic.zero
+ val one = Const (@{const_name "Groups.one"}, HOLogic.natT)
+ val natOptT = @{typ "nat option"}
+ val finT = if #partial config then natOptT else HOLogic.natT
+ val some = @{term "Some::nat \<Rightarrow> nat option"}
- fun filter_passed [] = []
- | filter_passed ((f as Free (_, Type ("Product_Type.prod",[Type ("fun",_), Type ("fun", _)])))::args) =
- f :: filter_passed args
- | filter_passed (_::args) = filter_passed args
- val frees = (walk @{context} [] {
- funcc = (fn wctxt => fn t => fn args =>
- (case t of (Const ("Product_Type.prod.snd", _)) => []
- | _ => (if t = T_ident then [] else filter_passed args)
- @ List.foldr (fn (l,r) => (#f wctxt) l @ r) [] args)),
- constc = (K o K) [],
- ifc = (fn wctxt => fn _ => fn cond => fn tt => fn tf => (#f wctxt) cond @ (#f wctxt) tt @ (#f wctxt) tf),
- casec = (fn wctxt => fn _ => fn cs => List.foldr (fn (l,r) => (#f wctxt) l @ r) [] cs),
- letc = (fn wctxt => fn _ => fn exp => fn _ => fn t => (#f wctxt) exp @ (#f wctxt) t)
- }) (get_r T_t)
- fun build _ [] = []
- | build i (a::args) =
- (if contains frees a then [(T_ident,i)] else []) @ build (i+1) args
-in
- build 0 T_args
-end
-fun find_simplifyble ctxt term terms =
-let
- val used =
- terms
- |> List.map find_used'
- |> List.foldr (op @) []
- val change =
- Option.valOf o fun_to_time ctxt term
- fun detect t i (Type ("fun",_)::args) =
- (if contains used (change t,i) then [] else [i]) @ detect t (i+1) args
- | detect t i (_::args) = detect t (i+1) args
- | detect _ _ [] = []
-in
- map (fn t => t |> type_of |> strip_type |> fst |> detect t 0) term
-end
+ (* change type of original function to new type (_ \<Rightarrow> ... \<Rightarrow> _ to _ \<Rightarrow> ... \<Rightarrow> nat)
+ and replace all function arguments f with (t*T_f) if used *)
+ fun change_typ' used (Type ("fun", [T1, T2])) =
+ Type ("fun", [check_for_fun' (used 0) T1, change_typ' (fn i => used (i+1)) T2])
+ | change_typ' _ _ = finT
+ and check_for_fun' true (f as Type ("fun", [_,_])) = HOLogic.mk_prodT (f, change_typ' (K false) f)
+ | check_for_fun' false (f as Type ("fun", [_,_])) = change_typ' (K true) f
+ | check_for_fun' _ t = t
+ val change_typ = change_typ' (K true)
+ fun time_term ctxt s (Const (nm,T)) =
+ let
+ val T_nm = fun_name_to_time ctxt s nm
+ val T_T = change_typ T
+ in
+ (SOME (Syntax.check_term ctxt (Const (T_nm,T_T))))
+ handle (ERROR _) =>
+ case Syntax.read_term ctxt (Long_Name.base_name T_nm)
+ of (Const (T_nm,T_T)) =>
+ let
+ fun col_Used i (Type ("fun", [Type ("fun", _), Ts])) (Type ("fun", [T', Ts'])) =
+ (if is_Used T' then [i] else []) @ col_Used (i+1) Ts Ts'
+ | col_Used i (Type ("fun", [_, Ts])) (Type ("fun", [_, Ts'])) = col_Used (i+1) Ts Ts'
+ | col_Used _ _ _ = []
+ val binderT = change_typ' (contains (col_Used 0 T T_T)) T |> Term.binder_types
+ val finT = Term.body_type T_T
+ in
+ SOME (Const (T_nm, binderT ---> finT))
+ end
+ | _ => error ("Timing function of " ^ nm ^ " is not defined")
+ end
+ | time_term _ _ _ = error "Internal error: No valid function given"
-fun define_simp' term simplifyable ctxt =
-let
- val base_name = case Named_Target.locale_of ctxt of
- NONE => ctxt |> Proof_Context.theory_of |> Context.theory_base_name
- | SOME nm => nm
-
- val orig_name = term |> dest_Const_name |> split_name |> List.last
- val red_name = fun_name_to_time ctxt false orig_name
- val name = fun_name_to_time' ctxt true true orig_name
- val full_name = base_name ^ "." ^ name
- val def_name = red_name ^ "_def"
- val def = Binding.name def_name
-
- val canon = Syntax.read_term (Local_Theory.exit ctxt) name |> strip_comb
- val canonFrees = canon |> snd
- val canonType = canon |> fst |> dest_Const_type |> strip_type |> fst |> take (length canonFrees)
+ fun opt_term NONE = zero
+ | opt_term (SOME t) = t
+ fun use_origin (Free (nm, T as Type ("fun",_))) = HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
+ | use_origin t = t
+
+ (* Conversion of function term *)
+ fun fun_to_time' ctxt (origin: term list) second (func as Const (nm,T)) =
+ let
+ val origin' = map (fst o strip_comb) origin
+ in
+ if contains' const_comp origin' func then SOME (Free (func |> Term.term_name |> fun_name_to_time' ctxt true second, change_typ T)) else
+ if Zero_Funcs.is_zero (Proof_Context.theory_of ctxt) (nm,T) then NONE else
+ time_term ctxt false func
+ end
+ | fun_to_time' _ _ _ (Free (nm,T)) =
+ SOME (HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ' (K true) T))))
+ | fun_to_time' _ _ _ _ = error "Internal error: invalid function to convert"
+ fun fun_to_time context origin func = fun_to_time' context origin false func
+
+ (* Convert arguments of left side of a term *)
+ fun conv_arg _ (Free (nm,T as Type("fun",_))) =
+ Free (nm, HOLogic.mk_prodT (T, change_typ' (K false) T))
+ | conv_arg _ x = x
+ fun conv_args ctxt = map (conv_arg ctxt)
+
+ (* 3. Convert equations *)
+ (* Some Helper *)
+ val plusTyp = @{typ "nat => nat => nat"}
+ fun plus (SOME a) (SOME b) = SOME ((if #partial config then @{term part_add} else Const (@{const_name "Groups.plus"}, plusTyp)) $ a $ b)
+ | plus (SOME a) NONE = SOME a
+ | plus NONE (SOME b) = SOME b
+ | plus NONE NONE = NONE
+ (* Partial helper *)
+ val OPTION_BIND = @{term "Option.bind::nat option \<Rightarrow> (nat \<Rightarrow> nat option) \<Rightarrow> nat option"}
+ fun OPTION_ABS_SUC args = Term.absfree ("_uu", @{typ nat})
+ (List.foldr (uncurry plus)
+ (SOME (some $ HOLogic.mk_Suc (Free ("_uu", @{typ nat})))) args |> Option.valOf)
+ fun build_option_bind term args =
+ OPTION_BIND $ term $ OPTION_ABS_SUC args
+ fun WRAP_FUNCTION t =
+ if (Term.head_of t |> Term.fastype_of |> Term.body_type) = finT
+ then t
+ else if #partial config
+ then some $ t
+ else @{term "the::nat option \<Rightarrow> nat"} $ t
- val types = term |> dest_Const_type |> strip_type |> fst
- val vars = Variable.variant_fixes (map (K "") types) ctxt |> fst
- fun l_typs' i ((T as (Type ("fun",_)))::types) =
- (if contains simplifyable i
- then change_typ T
- else HOLogic.mk_prodT (T,change_typ T))
- :: l_typs' (i+1) types
- | l_typs' i (T::types) = T :: l_typs' (i+1) types
- | l_typs' _ [] = []
- val l_typs = l_typs' 0 types
- val lhs =
- List.foldl (fn ((v,T),t) => t $ Free (v,T)) (Free (red_name,l_typs ---> HOLogic.natT)) (ListPair.zip (vars,l_typs))
- fun fixType (TFree _) = HOLogic.natT
- | fixType T = T
- fun fixUnspecified T = T |> strip_type ||> fixType |> (op --->)
- fun r_terms' i (v::vars) ((T as (Type ("fun",_)))::types) =
- (if contains simplifyable i
- then HOLogic.mk_prod (Const ("HOL.undefined", fixUnspecified T), Free (v,change_typ T))
- else Free (v,HOLogic.mk_prodT (T,change_typ T)))
- :: r_terms' (i+1) vars types
- | r_terms' i (v::vars) (T::types) = Free (v,T) :: r_terms' (i+1) vars types
- | r_terms' _ _ _ = []
- val r_terms = r_terms' 0 vars types
- val full_type = (r_terms |> map (type_of) ---> HOLogic.natT)
- val full = list_comb (Const (full_name,canonType ---> full_type), canonFrees)
- val rhs = list_comb (full, r_terms)
- val eq = (lhs, rhs) |> HOLogic.mk_eq |> HOLogic.mk_Trueprop
- val _ = Pretty.writeln (Pretty.block [Pretty.str "Defining simplified version:\n",
- Syntax.pretty_term ctxt eq])
-
- val (_, ctxt') = Specification.definition NONE [] [] ((def, []), eq) ctxt
-
-in
- ((def_name, orig_name), ctxt')
-end
-fun define_simp simpables ctxt =
-let
- fun cond ((term,simplifyable),(defs,ctxt)) =
- define_simp' term simplifyable ctxt |>> (fn def => def :: defs)
-in
- List.foldr cond ([], ctxt) simpables
-end
-
-
-fun replace from to =
- map (map_aterms (fn t => if t = from then to else t))
-fun replaceAll [] = I
- | replaceAll ((from,to)::xs) = replaceAll xs o replace from to
-fun calculateSimplifications ctxt T_terms term simpables =
-let
- (* Show where a simplification can take place *)
- fun reportReductions (t,(i::is)) =
- (Pretty.writeln (Pretty.str
- ((Term.term_name t |> fun_name_to_time ctxt true)
- ^ " can be simplified because only the time-function component of parameter "
- ^ (Int.toString (i + 1)) ^ " is used. "));
- reportReductions (t,is))
- | reportReductions (_,[]) = ()
- val _ = simpables
- |> map reportReductions
-
- (* Register definitions for simplified function *)
- val (reds, ctxt) = define_simp simpables ctxt
+ (* Handle function calls *)
+ fun build_zero (Type ("fun", [T, R])) = Abs ("uu", T, build_zero R)
+ | build_zero _ = zero
+ fun funcc_use_origin (Free (nm, T as Type ("fun",_))) =
+ HOLogic.mk_fst (Free (nm,HOLogic.mk_prodT (T, change_typ T)))
+ | funcc_use_origin t = t
+ fun funcc_conv_arg _ _ (t as (_ $ _)) = map_aterms funcc_use_origin t
+ | funcc_conv_arg _ u (Free (nm, T as Type ("fun",_))) =
+ if u then Free (nm, HOLogic.mk_prodT (T, change_typ T))
+ else HOLogic.mk_snd (Free (nm,HOLogic.mk_prodT (T,change_typ T)))
+ | funcc_conv_arg wctxt true (f as Const (_,Type ("fun",_))) =
+ HOLogic.mk_prod (f, funcc_conv_arg wctxt false f)
+ | funcc_conv_arg wctxt false (f as Const (_,T as Type ("fun",_))) =
+ Option.getOpt (fun_to_time (#ctxt wctxt) (#origins wctxt) f, build_zero T)
+ | funcc_conv_arg wctxt false (f as Abs _) =
+ f
+ |> Term.strip_abs_eta ((length o fst o strip_type o type_of) f)
+ ||> #f wctxt ||> opt_term
+ |> list_abs
+ | funcc_conv_arg wctxt true (f as Abs _) =
+ let
+ val f' = f
+ |> Term.strip_abs_eta ((length o fst o strip_type o type_of) f)
+ ||> map_aterms funcc_use_origin
+ |> list_abs
+ in
+ HOLogic.mk_prod (f', funcc_conv_arg wctxt false f)
+ end
+ | funcc_conv_arg _ _ t = t
+
+ fun funcc_conv_args _ _ [] = []
+ | funcc_conv_args wctxt (Type ("fun", [t, ts])) (a::args) =
+ funcc_conv_arg wctxt (is_Used t) a :: funcc_conv_args wctxt ts args
+ | funcc_conv_args _ _ _ = error "Internal error: Non matching type"
+ fun funcc wctxt func args =
+ let
+ fun get_T (Free (_,T)) = T
+ | get_T (Const (_,T)) = T
+ | get_T (_ $ (Free (_,Type (_, [_, T])))) = T (* Case of snd was constructed *)
+ | get_T _ = error "Internal error: Forgotten type"
+ val func = (case fun_to_time (#ctxt wctxt) (#origins wctxt) func
+ of SOME t => SOME (WRAP_FUNCTION (list_comb (t, funcc_conv_args wctxt (get_T t) args)))
+ | NONE => NONE)
+ val args = (map (#f wctxt) args)
+ in
+ (if not (#partial config) orelse func = NONE
+ then List.foldr (uncurry plus) func args
+ else build_option_bind (Option.valOf func) args |> SOME)
+ end
+
+ (* Handle case terms *)
+ fun casecIsCase (Type (n1, [_,Type (n2, _)])) = (n1 = "fun" andalso n2 = "fun")
+ | casecIsCase _ = false
+ fun casecLastTyp (Type (n, [T1,T2])) = Type (n, [T1, change_typ T2])
+ | casecLastTyp _ = error "Internal error: Invalid case type"
+ fun casecTyp (Type (n, [T1, T2])) =
+ Type (n, [change_typ T1, (if casecIsCase T2 then casecTyp else casecLastTyp) T2])
+ | casecTyp _ = error "Internal error: Invalid case type"
+ fun casecAbs f (Abs (v,Ta,t)) = (case casecAbs f (subst_bound (Free (v,Ta), t))
+ of (nconst,t) => (nconst,absfree (v,Ta) t))
+ | casecAbs f t = (case f t of NONE => (false, opt_term NONE) | SOME t => (true,t))
+ fun casecArgs _ [t] = (false, [map_aterms use_origin t])
+ | casecArgs f (t::ar) =
+ (case casecAbs f t of (nconst, tt) =>
+ casecArgs f ar ||> (fn ar => tt :: ar) |>> (if nconst then K true else I))
+ | casecArgs _ _ = error "Internal error: Invalid case term"
+ fun casec wctxt (Const (t,T)) args =
+ if not (casecIsCase T) then error "Internal error: Invalid case type" else
+ let val (nconst, args') = casecArgs (#f wctxt) args in
+ plus
+ ((#f wctxt) (List.last args))
+ (if nconst then
+ SOME (list_comb (Const (t,casecTyp T), args'))
+ else NONE)
+ end
+ | casec _ _ _ = error "Internal error: Invalid case term"
+
+ (* Handle if terms -> drop the term if true and false terms are zero *)
+ fun ifc wctxt _ cond tt ft =
+ let
+ val f = #f wctxt
+ val rcond = map_aterms use_origin cond
+ val tt = f tt
+ val ft = f ft
+ in
+ plus (f cond) (case (tt,ft) of (NONE, NONE) => NONE | _ =>
+ if tt = ft then tt else
+ (SOME ((Const (@{const_name "HOL.If"}, @{typ "bool"} --> finT --> finT --> finT)) $ rcond
+ $ (opt_term tt) $ (opt_term ft))))
+ end
+
+ fun letc_lambda wctxt T (t as Abs _) =
+ HOLogic.mk_prod (map_aterms use_origin t,
+ Term.strip_abs_eta (strip_type T |> fst |> length) t ||> #f wctxt ||> opt_term ||> map_types change_typ |> list_abs)
+ | letc_lambda _ _ t = map_aterms use_origin t
+ fun letc wctxt expT exp ([(nm,_)]) t =
+ plus (#f wctxt exp)
+ (case #f wctxt t of SOME t' =>
+ (if Term.used_free nm t'
+ then
+ let
+ val exp' = letc_lambda wctxt expT exp
+ val t' = list_abs ([(nm,fastype_of exp')], t')
+ in
+ Const (@{const_name "HOL.Let"}, [fastype_of exp', fastype_of t'] ---> finT) $ exp' $ t'
+ end
+ else t') |> SOME
+ | NONE => NONE)
+ | letc _ _ _ _ _ = error "Unknown let state"
+
+ fun constc _ (Const ("HOL.undefined", _)) = SOME (Const ("HOL.undefined", finT))
+ | constc _ _ = NONE
+
+ (* The converter for timing functions given to the walker *)
+ val converter : term option converter = {
+ constc = constc,
+ funcc = funcc,
+ ifc = ifc,
+ casec = casec,
+ letc = letc
+ }
+ fun top_converter is_rec _ _ =
+ if #partial config
+ then (fn t => Option.getOpt (t, zero))
+ else (opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE)))
+
+ (* Use converter to convert right side of a term *)
+ fun to_time ctxt origin is_rec term =
+ top_converter is_rec ctxt origin (walk ctxt origin converter term)
+
+ (* Converts a term to its running time version *)
+ fun convert_term ctxt (origin: term list) is_rec (pT $ (Const (eqN, _) $ l $ r)) =
+ let
+ val (l_const, l_params) = strip_comb l
+ in
+ pT
+ $ (Const (eqN, finT --> finT --> @{typ "bool"})
+ $ (list_comb (l_const |> fun_to_time ctxt origin |> Option.valOf, l_params |> conv_args ctxt))
+ $ (to_time ctxt origin is_rec r))
+ end
+ | convert_term _ _ _ _ = error "Internal error: invalid term to convert"
+
+ (* 3.5 Support for locales *)
+ fun replaceFstSndFree ctxt (origin: term list) (rfst: term -> term) (rsnd: term -> term) =
+ (walk ctxt origin {
+ funcc = fn wctxt => fn t => fn args =>
+ case args of
+ (f as Free _)::args =>
+ (case t of
+ Const ("Product_Type.prod.fst", _) =>
+ list_comb (rfst (t $ f), map (#f wctxt) args)
+ | Const ("Product_Type.prod.snd", _) =>
+ list_comb (rsnd (t $ f), map (#f wctxt) args)
+ | t => list_comb (t, map (#f wctxt) (f :: args)))
+ | args => list_comb (t, map (#f wctxt) args),
+ constc = Iconst,
+ ifc = Iif,
+ casec = Icase,
+ letc = Ilet
+ })
+
+ (* 5. Check for higher-order function if original function is used \<rightarrow> find simplifications *)
+ fun find_used' T_t =
+ let
+ val (T_ident, T_args) = strip_comb (get_l T_t)
+
+ fun filter_passed [] = []
+ | filter_passed ((f as Free (_, Type ("Product_Type.prod",[Type ("fun",_), Type ("fun", _)])))::args) =
+ f :: filter_passed args
+ | filter_passed (_::args) = filter_passed args
+ val frees = (walk lthy [] {
+ funcc = (fn wctxt => fn t => fn args =>
+ (case t of (Const ("Product_Type.prod.snd", _)) => []
+ | _ => (if t = T_ident then [] else filter_passed args)
+ @ List.foldr (fn (l,r) => (#f wctxt) l @ r) [] args)),
+ constc = (K o K) [],
+ ifc = (fn wctxt => fn _ => fn cond => fn tt => fn tf => (#f wctxt) cond @ (#f wctxt) tt @ (#f wctxt) tf),
+ casec = (fn wctxt => fn _ => fn cs => List.foldr (fn (l,r) => (#f wctxt) l @ r) [] cs),
+ letc = (fn wctxt => fn _ => fn exp => fn _ => fn t => (#f wctxt) exp @ (#f wctxt) t)
+ }) (get_r T_t)
+ fun build _ [] = []
+ | build i (a::args) =
+ (if contains frees a then [(T_ident,i)] else []) @ build (i+1) args
+ in
+ build 0 T_args
+ end
+ fun find_simplifyble ctxt term terms =
+ let
+ val used =
+ terms
+ |> List.map find_used'
+ |> List.foldr (op @) []
+ val change =
+ Option.valOf o fun_to_time ctxt term
+ fun detect t i (Type ("fun",_)::args) =
+ (if contains used (change t,i) then [] else [i]) @ detect t (i+1) args
+ | detect t i (_::args) = detect t (i+1) args
+ | detect _ _ [] = []
+ in
+ map (fn t => t |> type_of |> strip_type |> fst |> detect t 0) term
+ end
+
+ fun define_simp' term simplifyable ctxt =
+ let
+ val base_name = case Named_Target.locale_of ctxt of
+ NONE => ctxt |> Proof_Context.theory_of |> Context.theory_base_name
+ | SOME nm => nm
+
+ val orig_name = term |> dest_Const_name |> split_name |> List.last
+ val red_name = fun_name_to_time ctxt false orig_name
+ val name = fun_name_to_time' ctxt true true orig_name
+ val full_name = base_name ^ "." ^ name
+ val def_name = red_name ^ "_def"
+ val def = Binding.name def_name
+
+ val canon = Syntax.read_term (Local_Theory.exit ctxt) name |> strip_comb
+ val canonFrees = canon |> snd
+ val canonType = canon |> fst |> dest_Const_type |> strip_type |> fst |> take (length canonFrees)
+
+ val types = term |> dest_Const_type |> strip_type |> fst
+ val vars = Variable.variant_fixes (map (K "") types) ctxt |> fst
+ fun l_typs' i ((T as (Type ("fun",_)))::types) =
+ (if contains simplifyable i
+ then change_typ T
+ else HOLogic.mk_prodT (T,change_typ T))
+ :: l_typs' (i+1) types
+ | l_typs' i (T::types) = T :: l_typs' (i+1) types
+ | l_typs' _ [] = []
+ val l_typs = l_typs' 0 types
+ val lhs =
+ List.foldl (fn ((v,T),t) => t $ Free (v,T)) (Free (red_name,l_typs ---> HOLogic.natT)) (ListPair.zip (vars,l_typs))
+ fun fixType (TFree _) = HOLogic.natT
+ | fixType T = T
+ fun fixUnspecified T = T |> strip_type ||> fixType |> (op --->)
+ fun r_terms' i (v::vars) ((T as (Type ("fun",_)))::types) =
+ (if contains simplifyable i
+ then HOLogic.mk_prod (Const ("HOL.undefined", fixUnspecified T), Free (v,change_typ T))
+ else Free (v,HOLogic.mk_prodT (T,change_typ T)))
+ :: r_terms' (i+1) vars types
+ | r_terms' i (v::vars) (T::types) = Free (v,T) :: r_terms' (i+1) vars types
+ | r_terms' _ _ _ = []
+ val r_terms = r_terms' 0 vars types
+ val full_type = (r_terms |> map (type_of) ---> HOLogic.natT)
+ val full = list_comb (Const (full_name,canonType ---> full_type), canonFrees)
+ val rhs = list_comb (full, r_terms)
+ val eq = (lhs, rhs) |> HOLogic.mk_eq |> HOLogic.mk_Trueprop
+ val _ = Pretty.writeln (Pretty.block [Pretty.str "Defining simplified version:\n",
+ Syntax.pretty_term ctxt eq])
+
+ val (_, ctxt') = Specification.definition NONE [] [] ((def, []), eq) ctxt
+
+ in
+ ((def_name, orig_name), ctxt')
+ end
+ fun define_simp simpables ctxt =
+ let
+ fun cond ((term,simplifyable),(defs,ctxt)) =
+ define_simp' term simplifyable ctxt |>> (fn def => def :: defs)
+ in
+ List.foldr cond ([], ctxt) simpables
+ end
+
+
+ fun replace from to =
+ map (map_aterms (fn t => if t = from then to else t))
+ fun replaceAll [] = I
+ | replaceAll ((from,to)::xs) = replaceAll xs o replace from to
+ fun calculateSimplifications ctxt T_terms term simpables =
+ let
+ (* Show where a simplification can take place *)
+ fun reportReductions (t,(i::is)) =
+ (Pretty.writeln (Pretty.str
+ ((Term.term_name t |> fun_name_to_time ctxt true)
+ ^ " can be simplified because only the time-function component of parameter "
+ ^ (Int.toString (i + 1)) ^ " is used. "));
+ reportReductions (t,is))
+ | reportReductions (_,[]) = ()
+ val _ = simpables
+ |> map reportReductions
+
+ (* Register definitions for simplified function *)
+ val (reds, ctxt) = define_simp simpables ctxt
+
+ fun genRetype (Const (nm,T),is) =
+ let
+ val T_name = fun_name_to_time ctxt true nm |> split_name |> List.last
+ val from = Free (T_name,change_typ T)
+ val to = Free (T_name,change_typ' (not o contains is) T)
+ in
+ (from,to)
+ end
+ | genRetype _ = error "Internal error: invalid term"
+ val retyping = map genRetype simpables
+
+ fun replaceArgs (pT $ (eq $ l $ r)) =
+ let
+ val (t,params) = strip_comb l
+ fun match (Const (f_nm,_),_) =
+ (fun_name_to_time ctxt true f_nm |> Long_Name.base_name) = (dest_Free t |> fst)
+ | match _ = false
+ val simps = List.find match simpables |> Option.valOf |> snd
+
+ fun dest_Prod_snd (Free (nm, Type (_, [_, T2]))) =
+ Free (fun_name_to_time ctxt false nm, T2)
+ | dest_Prod_snd _ = error "Internal error: Argument is not a pair"
+ fun rep _ [] = ([],[])
+ | rep i (x::xs) =
+ let
+ val (rs,args) = rep (i+1) xs
+ in
+ if contains simps i
+ then (x::rs,dest_Prod_snd x::args)
+ else (rs,x::args)
+ end
+ val (rs,params) = rep 0 params
+ fun fFst _ = error "Internal error: Invalid term to simplify"
+ fun fSnd (t as (Const _ $ f)) =
+ (if contains rs f
+ then dest_Prod_snd f
+ else t)
+ | fSnd t = t
+ in
+ (pT $ (eq
+ $ (list_comb (t,params))
+ $ (replaceFstSndFree ctxt term fFst fSnd r
+ |> (fn t => replaceAll (map (fn t => (t,dest_Prod_snd t)) rs) [t])
+ |> hd
+ )
+ ))
+ end
+ | replaceArgs _ = error "Internal error: Invalid term"
+
+ (* Calculate reduced terms *)
+ val T_terms_red = T_terms
+ |> replaceAll retyping
+ |> map replaceArgs
+
+ val _ = print_lemma ctxt reds T_terms_red
+ val _ =
+ Pretty.writeln (Pretty.str "If you do not want the simplified T function, use \"time_fun [no_simp]\"")
+ in
+ ctxt
+ end
- fun genRetype (Const (nm,T),is) =
- let
- val T_name = fun_name_to_time ctxt true nm |> split_name |> List.last
- val from = Free (T_name,change_typ T)
- val to = Free (T_name,change_typ' (not o contains is) T)
- in
- (from,to)
- end
- | genRetype _ = error "Internal error: invalid term"
- val retyping = map genRetype simpables
-
- fun replaceArgs (pT $ (eq $ l $ r)) =
- let
- val (t,params) = strip_comb l
- fun match (Const (f_nm,_),_) =
- (fun_name_to_time ctxt true f_nm |> Long_Name.base_name) = (dest_Free t |> fst)
- | match _ = false
- val simps = List.find match simpables |> Option.valOf |> snd
-
- fun dest_Prod_snd (Free (nm, Type (_, [_, T2]))) =
- Free (fun_name_to_time ctxt false nm, T2)
- | dest_Prod_snd _ = error "Internal error: Argument is not a pair"
- fun rep _ [] = ([],[])
- | rep i (x::xs) =
- let
- val (rs,args) = rep (i+1) xs
- in
- if contains simps i
- then (x::rs,dest_Prod_snd x::args)
- else (rs,x::args)
- end
- val (rs,params) = rep 0 params
- fun fFst _ = error "Internal error: Invalid term to simplify"
- fun fSnd (t as (Const _ $ f)) =
- (if contains rs f
- then dest_Prod_snd f
- else t)
- | fSnd t = t
- in
- (pT $ (eq
- $ (list_comb (t,params))
- $ (replaceFstSndFree ctxt term fFst fSnd r
- |> (fn t => replaceAll (map (fn t => (t,dest_Prod_snd t)) rs) [t])
- |> hd
- )
- ))
- end
- | replaceArgs _ = error "Internal error: Invalid term"
-
- (* Calculate reduced terms *)
- val T_terms_red = T_terms
- |> replaceAll retyping
- |> map replaceArgs
-
- val _ = print_lemma ctxt reds T_terms_red
- val _ =
- Pretty.writeln (Pretty.str "If you do not want the simplified T function, use \"time_fun [no_simp]\"")
-in
- ctxt
-end
-
-(* Register timing function of a given function *)
-fun reg_time_func (lthy: local_theory) (term: term list) (terms: term list) print simp =
- let
val _ =
case time_term lthy true (hd term)
handle (ERROR _) => NONE
@@ -758,6 +796,7 @@
|> strip_comb |> snd
|> length
+ (********************* BEGIN OF CONVERSION *********************)
(* 1. Fix all terms *)
(* Exchange Var in types and terms to Free and check constraints *)
val terms = map
@@ -799,7 +838,7 @@
val T_terms = map (convert_term lthy term is_rec) terms
|> map (map_r (replaceFstSndFree lthy term fFst fSnd))
- val simpables = (if simp
+ val simpables = (if #simp config
then find_simplifyble lthy term T_terms
else map (K []) term)
|> (fn s => ListPair.zip (term,s))
@@ -808,7 +847,7 @@
(* Rename to secondary if simpable *)
fun genRename (t,_) =
let
- val old = fun_to_time lthy term t |> Option.valOf
+ val old = fun_to_time' lthy term false t |> Option.valOf
val new = fun_to_time' lthy term true t |> Option.valOf
in
(old,new)
@@ -824,6 +863,7 @@
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
val specs = map (fn eq => (((Binding.empty, []), eq), [], [])) can_T_terms
+ val part_specs = (Binding.empty_atts, hd can_T_terms)
(* Context for printing without showing question marks *)
val print_ctxt = lthy
@@ -831,13 +871,13 @@
|> Config.put show_sorts false (* Change it for debugging *)
val print_ctxt = List.foldl (fn (term, ctxt) => Variable.add_fixes_implicit term ctxt) print_ctxt (term @ T_terms)
(* Print result if print *)
- val _ = if not print then () else
+ val _ = if not (#print config) then () else
let
val nms = map (dest_Const_name) term
val typs = map (dest_Const_type) term
in
print_timing' print_ctxt { names=nms, terms=terms, typs=typs }
- { names=timing_names, terms=can_T_terms, typs=map change_typ typs }
+ { names=timing_names, terms=can_T_terms, typs=map change_typ typs }
end
(* For partial functions sequential=true is needed in order to support them
@@ -849,7 +889,9 @@
val fun_config = Function_Common.FunctionConfig
{sequential=seq, default=NONE, domintros=true, partials=false}
in
- Function.add_function bindings specs fun_config pat_completeness_auto lthy
+ if #partial config
+ then Partial_Function.add_partial_function "option" bindings part_specs lthy |>> PartialFunction o snd
+ else Function.add_function bindings specs fun_config pat_completeness_auto lthy |>> Function
end
val (info,ctxt) =
@@ -861,7 +903,7 @@
val ctxt = if simpable then calculateSimplifications ctxt T_terms term simpables else ctxt
in
- (info,ctxt)
+ (info, ctxt)
end
fun proove_termination (term: term list) terms (T_info: Function.info, lthy: local_theory) =
let
@@ -904,11 +946,12 @@
(auto_tac simp_lthy) lthy
end
in
- (time_info, lthy')
+ (Function time_info, lthy')
end
-fun reg_and_proove_time_func (lthy: local_theory) (term: term list) (terms: term list) print simp =
- reg_time_func lthy term terms print simp
- |> proove_termination term terms
+fun reg_and_proove_time_func (lthy: local_theory) (term: term list) (terms: term list) (config: time_config) =
+ case reg_time_func lthy term terms config
+ of (Function info, lthy') => proove_termination term terms (info, lthy')
+ | r => r
fun isTypeClass' (Const (nm,_)) =
(case split_name nm |> rev
@@ -945,43 +988,60 @@
| check_opts ["no_simp"] = true
| check_opts (a::_) = error ("Option " ^ a ^ " is not defined")
-(* Convert function into its timing function (called by command) *)
+(* Converts a function into its timing function using fun *)
fun reg_time_fun_cmd ((opts, funcs), thms) (ctxt: local_theory) =
let
val no_simp = check_opts opts
val fterms = map (Syntax.read_term ctxt) funcs
val ctxt = set_suffix fterms ctxt
+ val config = { print = true, simp = not no_simp, partial = false }
val (_, ctxt') = reg_and_proove_time_func ctxt fterms
(case thms of NONE => get_terms ctxt (hd fterms)
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
- true (not no_simp)
+ config
in ctxt'
end
-(* Convert function into its timing function (called by command) with termination proof provided by user*)
+(* Converts a function into its timing function using function with termination proof provided by user*)
fun reg_time_function_cmd ((opts, funcs), thms) (ctxt: local_theory) =
let
val no_simp = check_opts opts
val fterms = map (Syntax.read_term ctxt) funcs
val ctxt = set_suffix fterms ctxt
+ val config = { print = true, simp = not no_simp, partial = false }
val ctxt' = reg_time_func ctxt fterms
(case thms of NONE => get_terms ctxt (hd fterms)
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
- true (not no_simp)
+ config
|> snd
in ctxt'
end
-(* Convert function into its timing function (called by command) *)
+(* Converts a function definition into its timing function using definition *)
fun reg_time_definition_cmd ((opts, funcs), thms) (ctxt: local_theory) =
let
val no_simp = check_opts opts
val fterms = map (Syntax.read_term ctxt) funcs
val ctxt = set_suffix fterms ctxt
+ val config = { print = true, simp = not no_simp, partial = false }
val (_, ctxt') = reg_and_proove_time_func ctxt fterms
(case thms of NONE => get_terms ctxt (hd fterms) |> check_definition
| SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
- true (not no_simp)
+ config
+in ctxt'
+end
+
+(* Converts a a partial function into its timing function using partial_function *)
+fun reg_time_partial_function_cmd ((opts, funcs), thms) (ctxt: local_theory) =
+let
+ val no_simp = check_opts opts
+ val fterms = map (Syntax.read_term ctxt) funcs
+ val ctxt = set_suffix fterms ctxt
+ val config = { print = true, simp = not no_simp, partial = true }
+ val (_, ctxt') = reg_and_proove_time_func ctxt fterms
+ (case thms of NONE => get_terms ctxt (hd fterms) |> check_definition
+ | SOME thms => thms |> Attrib.eval_thms ctxt |> List.map Thm.prop_of)
+ config
in ctxt'
end
@@ -1001,4 +1061,8 @@
"Defines runtime function of a definition"
(parser >> reg_time_definition_cmd)
+val _ = Outer_Syntax.local_theory @{command_keyword "time_partial_function"}
+ "Defines runtime function of a definition"
+ (parser >> reg_time_partial_function_cmd)
+
end
--- a/src/HOL/Data_Structures/Define_Time_Function.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy Sat Feb 08 17:44:04 2025 +0100
@@ -12,6 +12,7 @@
keywords "time_fun" :: thy_decl
and "time_function" :: thy_decl
and "time_definition" :: thy_decl
+ and "time_partial_function" :: thy_decl
and "equations"
and "time_fun_0" :: thy_decl
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Time_Examples.thy Sat Feb 08 17:44:04 2025 +0100
@@ -0,0 +1,70 @@
+(*
+Author: Jonas Stahl
+
+Nonstandard examples of the time function definition commands.
+*)
+
+theory Time_Examples
+imports Define_Time_Function
+begin
+
+fun even :: "nat \<Rightarrow> bool"
+ and odd :: "nat \<Rightarrow> bool" where
+ "even 0 = True"
+| "odd 0 = False"
+| "even (Suc n) = odd n"
+| "odd (Suc n) = even n"
+time_fun even odd
+
+locale locTests =
+ fixes f :: "'a \<Rightarrow> 'b"
+ and T_f :: "'a \<Rightarrow> nat"
+begin
+
+fun simple where
+ "simple a = f a"
+time_fun simple
+
+fun even :: "'a list \<Rightarrow> 'b list" and odd :: "'a list \<Rightarrow> 'b list" where
+ "even [] = []"
+| "odd [] = []"
+| "even (x#xs) = f x # odd xs"
+| "odd (x#xs) = even xs"
+time_fun even odd
+
+fun locSum :: "nat list \<Rightarrow> nat" where
+ "locSum [] = 0"
+| "locSum (x#xs) = x + locSum xs"
+time_fun locSum
+
+fun map :: "'a list \<Rightarrow> 'b list" where
+ "map [] = []"
+| "map (x#xs) = f x # map xs"
+time_fun map
+
+end
+
+definition "let_lambda a b c \<equiv> let lam = (\<lambda>a b. a + b) in lam a (lam b c)"
+time_fun let_lambda
+
+partial_function (tailrec) collatz :: "nat \<Rightarrow> bool" where
+ "collatz n = (if n \<le> 1 then True
+ else if n mod 2 = 0 then collatz (n div 2)
+ else collatz (3 * n + 1))"
+
+text \<open>This is the expected time function:\<close>
+partial_function (option) T_collatz' :: "nat \<Rightarrow> nat option" where
+ "T_collatz' n = (if n \<le> 1 then Some 0
+ else if n mod 2 = 0 then Option.bind (T_collatz' (n div 2)) (\<lambda>k. Some (Suc k))
+ else Option.bind (T_collatz' (3 * n + 1)) (\<lambda>k. Some (Suc k)))"
+time_fun_0 "(mod)"
+time_partial_function collatz
+
+text \<open>Proof that they are the same up to 20:\<close>
+lemma setIt: "P i \<Longrightarrow> \<forall>n \<in> {Suc i..j}. P n \<Longrightarrow> \<forall>n \<in> {i..j}. P n"
+ by (metis atLeastAtMost_iff le_antisym not_less_eq_eq)
+lemma "\<forall>n \<in> {2..20}. T_collatz n = T_collatz' n"
+ apply (rule setIt, simp add: T_collatz.simps T_collatz'.simps, simp)+
+ by (simp add: T_collatz.simps T_collatz'.simps)
+
+end
\ No newline at end of file
--- a/src/HOL/Groups_List.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Groups_List.thy Sat Feb 08 17:44:04 2025 +0100
@@ -141,6 +141,12 @@
.
qed
+lemma sum_list_of_nat: "sum_list (map of_nat xs) = of_nat (sum_list xs)"
+ by (induction xs) auto
+
+lemma sum_list_of_int: "sum_list (map of_int xs) = of_int (sum_list xs)"
+ by (induction xs) auto
+
lemma (in comm_monoid_add) sum_list_map_remove1:
"x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)
@@ -171,7 +177,7 @@
lemma (in comm_monoid_add) distinct_sum_list_conv_Sum:
"distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)"
- by (induct xs) simp_all
+ by (metis local.sum.set_conv_list local.sum_list_def map_ident remdups_id_iff_distinct)
lemma sum_list_upt[simp]:
"m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
@@ -181,14 +187,14 @@
begin
lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs"
-by (induction xs) auto
+ by (induction xs) auto
lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0"
-by (induction xs) (auto simp: add_nonpos_nonpos)
+ by (induction xs) (auto simp: add_nonpos_nonpos)
lemma sum_list_nonneg_eq_0_iff:
"(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)"
-by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
+ by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
end
@@ -197,24 +203,29 @@
lemma sum_list_eq_0_iff [simp]:
"sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-by (simp add: sum_list_nonneg_eq_0_iff)
+ by (simp add: sum_list_nonneg_eq_0_iff)
lemma member_le_sum_list:
"x \<in> set xs \<Longrightarrow> x \<le> sum_list xs"
-by (induction xs) (auto simp: add_increasing add_increasing2)
+ by (induction xs) (auto simp: add_increasing add_increasing2)
lemma elem_le_sum_list:
"k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)"
-by (rule member_le_sum_list) simp
+ by (simp add: member_le_sum_list)
end
lemma (in ordered_cancel_comm_monoid_diff) sum_list_update:
"k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k"
-apply(induction xs arbitrary:k)
- apply (auto simp: add_ac split: nat.split)
-apply(drule elem_le_sum_list)
-by (simp add: local.add_diff_assoc local.add_increasing)
+proof (induction xs arbitrary:k)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons a xs)
+ then show ?case
+ apply (simp add: add_ac split: nat.split)
+ using add_increasing diff_add_assoc elem_le_sum_list zero_le by force
+qed
lemma (in monoid_add) sum_list_triv:
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
@@ -276,8 +287,7 @@
lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list"
shows "\<lbrakk> length xs = length ys; \<And>i. i < length xs \<longrightarrow> xs!i \<le> ys!i \<rbrakk>
\<Longrightarrow> sum_list xs \<le> sum_list ys"
-apply(induction xs ys rule: list_induct2)
-by(auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
+ by (induction xs ys rule: list_induct2) (auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
lemma (in monoid_add) sum_list_distinct_conv_sum_set:
"distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
@@ -369,6 +379,29 @@
thus ?case by simp
qed
+(*Note that we also have this for class canonically_ordered_monoid_add*)
+lemma member_le_sum_list:
+ fixes x :: "'a :: ordered_comm_monoid_add"
+ assumes "x \<in> set xs" "\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0"
+ shows "x \<le> sum_list xs"
+ using assms
+proof (induction xs)
+ case (Cons y xs)
+ show ?case
+ proof (cases "y = x")
+ case True
+ have "x + 0 \<le> x + sum_list xs"
+ by (intro add_mono order.refl sum_list_nonneg) (use Cons in auto)
+ thus ?thesis
+ using True by auto
+ next
+ case False
+ have "0 + x \<le> y + sum_list xs"
+ by (intro add_mono Cons.IH Cons.prems) (use Cons.prems False in auto)
+ thus ?thesis
+ by auto
+ qed
+qed auto
subsection \<open>Horner sums\<close>
--- a/src/HOL/Nat.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Nat.thy Sat Feb 08 17:44:04 2025 +0100
@@ -1268,7 +1268,7 @@
lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0"
for m n :: nat
- by (rule iffD2, rule diff_is_0_eq)
+ by simp
lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n"
for m n :: nat
@@ -1755,6 +1755,9 @@
by simp
qed
+lemma of_nat_diff_if: \<open>of_nat (m - n) = (if n\<le>m then of_nat m - of_nat n else 0)\<close>
+ by (simp add: not_le less_imp_le)
+
end
text \<open>Class for unital semirings with characteristic zero.
--- a/src/HOL/Number_Theory/Cong.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Sat Feb 08 17:44:04 2025 +0100
@@ -774,4 +774,35 @@
finally show ?thesis .
qed
+text \<open>Thanks to Manuel Eberl\<close>
+lemma prime_cong_4_nat_cases [consumes 1, case_names 2 cong_1 cong_3]:
+ assumes "prime (p :: nat)"
+ obtains "p = 2" | "[p = 1] (mod 4)" | "[p = 3] (mod 4)"
+proof -
+ have "[p = 2] (mod 4) \<longleftrightarrow> p = 2"
+ proof
+ assume "[p = 2] (mod 4)"
+ hence "p mod 4 = 2"
+ by (auto simp: cong_def)
+ hence "even p"
+ by (simp add: even_even_mod_4_iff)
+ with assms show "p = 2"
+ unfolding prime_nat_iff by force
+ qed auto
+ moreover have "[p \<noteq> 0] (mod 4)"
+ proof
+ assume "[p = 0] (mod 4)"
+ hence "4 dvd p"
+ by (auto simp: cong_0_iff)
+ with assms have "p = 4"
+ by (subst (asm) prime_nat_iff) auto
+ thus False
+ using assms by simp
+ qed
+ ultimately consider "[p = 3] (mod 4)" | "[p = 1] (mod 4)" | "p = 2"
+ by (fastforce simp: cong_def)
+ thus ?thesis
+ using that by metis
+qed
+
end
--- a/src/HOL/ROOT Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/ROOT Sat Feb 08 17:44:04 2025 +0100
@@ -319,6 +319,7 @@
Leftist_Heap_List
Binomial_Heap
Selection
+ Time_Examples
document_files "root.tex" "root.bib"
session "HOL-Import" in Import = HOL +
--- a/src/HOL/Real_Vector_Spaces.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Feb 08 17:44:04 2025 +0100
@@ -287,6 +287,9 @@
lemma of_real_prod[simp]: "of_real (prod f s) = (\<Prod>x\<in>s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
+lemma sum_list_of_real: "sum_list (map of_real xs) = of_real (sum_list xs)"
+ by (induction xs) auto
+
lemma nonzero_of_real_inverse:
"x \<noteq> 0 \<Longrightarrow> of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)"
by (simp add: of_real_def nonzero_inverse_scaleR_distrib)
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Sat Feb 08 17:44:04 2025 +0100
@@ -133,7 +133,7 @@
else
(warning (" test: file " ^ Path.print file ^
" raised exception: " ^ Runtime.exn_message exn);
- {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
+ Timing.zero)
val to_real = Time.toReal
val diff_elapsed =
#elapsed t2 - #elapsed t1
--- a/src/HOL/Tools/SMT/smt_config.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Sat Feb 08 17:44:04 2025 +0100
@@ -63,7 +63,7 @@
(*setup*)
val print_setup: Proof.context -> unit
-end;
+end
structure SMT_Config: SMT_CONFIG =
struct
@@ -74,7 +74,7 @@
name: string,
class: Proof.context -> SMT_Util.class,
avail: unit -> bool,
- options: Proof.context -> string list}
+ options: Proof.context -> string list};
structure Data = Generic_Data
(
@@ -100,7 +100,7 @@
fun set_solver_options (name, options) =
let val opts = String.tokens (Symbol.is_ascii_blank o str) options
- in map_solvers (Symtab.map_entry name (apsnd (K opts))) end
+ in map_solvers (Symtab.map_entry name (apsnd (K opts))) end;
fun add_solver (info as {name, ...} : solver_info) context =
if defined_solvers context name then
@@ -111,7 +111,7 @@
|> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
(Thm.declaration_attribute o K o set_solver_options o pair name))
- ("additional command-line options for SMT solver " ^ quote name))
+ ("additional command-line options for SMT solver " ^ quote name));
val all_solvers_of' = Symtab.keys o get_solvers';
val all_solvers_of = all_solvers_of' o Context.Proof;
@@ -130,7 +130,7 @@
if Context_Position.is_visible ctxt then
warning ("The SMT solver " ^ quote name ^ " is not installed")
else ()
- | warn_solver _ _ = ()
+ | warn_solver _ _ = ();
fun select_solver name context =
if not (defined_solvers context name) then
@@ -139,79 +139,79 @@
(warn_solver context name; put_solver name context)
else put_solver name context;
-fun no_solver_err () = error "No SMT solver selected"
+fun no_solver_err () = error "No SMT solver selected";
fun solver_of ctxt =
(case get_solver ctxt of
SOME name => name
- | NONE => no_solver_err ())
+ | NONE => no_solver_err ());
fun solver_info_of default select ctxt =
(case get_solver ctxt of
NONE => default ()
- | SOME name => select (Symtab.lookup (get_solvers ctxt) name))
+ | SOME name => select (Symtab.lookup (get_solvers ctxt) name));
fun solver_class_of ctxt =
let fun class_of ({class, ...}: solver_info, _) = class ctxt
- in solver_info_of no_solver_err (class_of o the) ctxt end
+ in solver_info_of no_solver_err (class_of o the) ctxt end;
fun solver_options_of ctxt =
let
fun all_options NONE = []
| all_options (SOME ({options, ...} : solver_info, opts)) =
opts @ options ctxt
- in solver_info_of (K []) all_options ctxt end
+ in solver_info_of (K []) all_options ctxt end;
-val setup_solver =
- Attrib.setup \<^binding>\<open>smt_solver\<close>
+val _ =
+ Theory.setup (Attrib.setup \<^binding>\<open>smt_solver\<close>
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
(Thm.declaration_attribute o K o select_solver))
- "SMT solver configuration"
+ "SMT solver configuration");
(* options *)
-val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
-val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0)
-val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
-val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
-val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
-val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
-val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
-val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
-val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
-val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
-val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
-val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
-val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
-val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
-val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
-val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
-val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
-val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
-val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
-val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
-val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
-val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
-val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false)
+val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true);
+val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0);
+val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0);
+val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1);
+val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false);
+val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true);
+val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false);
+val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false);
+val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false);
+val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false);
+val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false);
+val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true);
+val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false);
+val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10);
+val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500);
+val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1);
+val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false);
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true);
+val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false);
+val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false);
+val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "");
+val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite");
+val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\<open>smt_cvc_lethe\<close> (K false);
(* diagnostics *)
-fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ();
-fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
-fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
-fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose);
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace);
+fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics);
-fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ()
-fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ()
+fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ();
+fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ();
-fun spy_verit ctxt = Config.get ctxt spy_verit_attr
-fun spy_Z3 ctxt = Config.get ctxt spy_z3
-fun compress_verit_proofs ctxt = Config.get ctxt trace_verit_compression
+fun spy_verit ctxt = Config.get ctxt spy_verit_attr;
+fun spy_Z3 ctxt = Config.get ctxt spy_z3;
+fun compress_verit_proofs ctxt = Config.get ctxt trace_verit_compression;
-fun use_lethe_proof_from_cvc ctxt = Config.get ctxt cvc_experimental_lethe
+fun use_lethe_proof_from_cvc ctxt = Config.get ctxt cvc_experimental_lethe;
(* tools *)
@@ -222,9 +222,9 @@
fun with_time_limit ctxt timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
- handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out;
-fun with_timeout ctxt = with_time_limit ctxt timeout
+fun with_timeout ctxt = with_time_limit ctxt timeout;
(* certificates *)
@@ -237,46 +237,37 @@
let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name
in SOME (Cache_IO.unsynchronized_init dir) end);
-val setup_certificates =
- Attrib.setup \<^binding>\<open>smt_certificates\<close>
+val _ =
+ Theory.setup (Attrib.setup \<^binding>\<open>smt_certificates\<close>
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
- "SMT certificates configuration"
+ "SMT certificates configuration");
-(* setup *)
-
-val _ = Theory.setup (
- setup_solver #>
- setup_certificates)
+(* print_setup *)
fun print_setup ctxt =
let
- fun string_of_bool b = if b then "true" else "false"
-
- val names = available_solvers_of ctxt
- val ns = if null names then ["(none)"] else sort_strings names
- val n = the_default "(none)" (get_solver ctxt)
- val opts = solver_options_of ctxt
-
- val t = string_of_real (Config.get ctxt timeout)
+ val names = available_solvers_of ctxt;
+ val ns = if null names then ["(none)"] else sort_strings names;
+ val n = the_default "(none)" (get_solver ctxt);
+ val opts = solver_options_of ctxt;
+ val t = seconds (Config.get ctxt timeout)
val certs_filename =
(case get_certificates_path ctxt of
SOME path => Path.print path
- | NONE => "(disabled)")
- in
- Pretty.writeln (Pretty.big_list "SMT setup:" [
- Pretty.str ("Current SMT solver: " ^ n),
+ | NONE => "(disabled)");
+
+ val items =
+ [Pretty.str ("Current SMT solver: " ^ n),
Pretty.str ("Current SMT solver options: " ^ implode_space opts),
Pretty.str_list "Available SMT solvers: " "" ns,
- Pretty.str ("Current timeout: " ^ t ^ " seconds"),
- Pretty.str ("With proofs: " ^
- string_of_bool (not (Config.get ctxt oracle))),
+ Pretty.str ("Current timeout: " ^ (if Timeout.ignored t then "(none)" else Time.message t)),
+ Pretty.str ("With proofs: " ^ Value.print_bool (not (Config.get ctxt oracle))),
Pretty.str ("Certificates cache: " ^ certs_filename),
- Pretty.str ("Fixed certificates: " ^
- string_of_bool (Config.get ctxt read_only_certificates))])
- end
+ Pretty.str ("Fixed certificates: " ^ Value.print_bool (Config.get ctxt read_only_certificates))];
+ in Pretty.writeln (Pretty.big_list "SMT setup:" (map (Pretty.item o single) items)) end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
@@ -284,4 +275,4 @@
\and the values of SMT configuration options"
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
-end;
+end
--- a/src/HOL/Tools/SMT/smt_solver.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Feb 08 17:44:04 2025 +0100
@@ -60,35 +60,33 @@
local
-fun make_command command options problem_path proof_path =
- Bash.strings (command () @ options) ^ " " ^
- File.bash_platform_path problem_path ^
- " > " ^ File.bash_path proof_path ^ " 2>&1"
-
fun with_trace ctxt msg f x =
let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
in f x end
-fun run ctxt name mk_cmd input =
+fun run ctxt name cmd input =
(case SMT_Config.certificates_of ctxt of
NONE =>
if not (SMT_Config.is_available ctxt name) then
error ("The SMT solver " ^ quote name ^ " is not installed")
else if Config.get ctxt SMT_Config.debug_files = "" then
- with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input
+ with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run cmd) input
else
let
val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
val in_path = Path.ext "smt_in" base_path
val out_path = Path.ext "smt_out" base_path
- in Cache_IO.raw_run mk_cmd input in_path out_path end
+ val _ = File.write in_path input
+ val result = Cache_IO.run cmd input
+ val _ = Bytes.write out_path (Bytes.terminate_lines (Process_Result.out_lines result))
+ in result end
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
if Config.get ctxt SMT_Config.read_only_certificates then
error ("Bad certificate cache: missing certificate")
else
- Cache_IO.run_and_cache certs key mk_cmd input
+ Cache_IO.run_and_cache certs key cmd input
| (SOME output, _) =>
with_trace ctxt ("Using cached certificate from " ^
Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
@@ -99,20 +97,23 @@
| normal_return_codes "verit" = [0, 14, 255]
| normal_return_codes _ = [0, 1]
-fun run_solver ctxt name mk_cmd input =
+fun run_solver ctxt name cmd input =
let
fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines))
val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
- val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) =
- Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
+ val ({elapsed, ...}, result) =
+ Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name cmd)) input
+ val res = Process_Result.out_lines result
+ val err = Process_Result.err_lines result
+ val return_code = Process_Result.rc result
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
val output = drop_suffix (equal "") res
val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
- val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
- val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
+ val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Time.message elapsed]
+ val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Time.message elapsed]
val _ = member (op =) (normal_return_codes name) return_code orelse
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
@@ -136,23 +137,24 @@
in
-fun invoke memoize_fun_call name command options smt_options ithms ctxt =
+fun invoke memoize_fun_call name command cmd_options smt_options ithms ctxt =
let
- val options = options @ SMT_Config.solver_options_of ctxt
+ val options = cmd_options @ SMT_Config.solver_options_of ctxt
val comments = [implode_space options]
- val (str, replay_data as {context = ctxt', ...}) =
+ val (input, replay_data as {context = ctxt', ...}) =
ithms
|> tap (trace_assms ctxt)
|> SMT_Translate.translate ctxt name smt_options comments
||> tap trace_replay_data
- val run_solver = run_solver ctxt' name (make_command command options)
+ val cmd = Bash.script (Bash.strings (command () @ options))
+ val run_cmd = run_solver ctxt' name cmd
val output_lines =
(case memoize_fun_call of
- NONE => run_solver str
- | SOME memoize => split_lines (memoize (cat_lines o run_solver) str))
+ NONE => run_cmd input
+ | SOME memoize => split_lines (memoize (cat_lines o run_cmd) input))
in (output_lines, replay_data) end
end
--- a/src/HOL/Tools/SMT/smt_systems.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Sat Feb 08 17:44:04 2025 +0100
@@ -229,7 +229,7 @@
name = "z3",
class = select_class,
avail = make_avail "Z3",
- command = make_command "Z3",
+ command = fn () => [getenv "Z3_SOLVER", "-in"],
options = z3_options,
smt_options = [(":produce-proofs", "true")],
good_slices =
--- a/src/Pure/Concurrent/timeout.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/Concurrent/timeout.ML Sat Feb 08 17:44:04 2025 +0100
@@ -15,7 +15,7 @@
val end_time: Time.time -> Time.time
val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
val apply_physical: Time.time -> ('a -> 'b) -> 'a -> 'b
- val print: Time.time -> string
+ val message: Time.time -> string
end;
structure Timeout: TIMEOUT =
@@ -59,6 +59,6 @@
fun apply timeout f x = apply' {physical = false, timeout = timeout} f x;
fun apply_physical timeout f x = apply' {physical = true, timeout = timeout} f x;
-fun print t = "Timeout after " ^ Value.print_time t ^ "s";
+fun message t = "Timeout after " ^ Time.message t;
end;
--- a/src/Pure/General/bytes.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/General/bytes.ML Sat Feb 08 17:44:04 2025 +0100
@@ -36,6 +36,7 @@
val split_lines: T -> string list
val trim_split_lines: T -> string list
val cat_lines: string list -> T
+ val terminate_lines: string list -> T
val read_block: int -> BinIO.instream -> string
val read_stream: int -> BinIO.instream -> T
val write_stream: BinIO.outstream -> T -> unit
@@ -190,6 +191,8 @@
fun cat_lines lines = build (fold add (separate "\n" lines));
+fun terminate_lines lines = build (fold (fn line => add line #> add "\n") lines);
+
(* IO *)
--- a/src/Pure/General/time.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/General/time.ML Sat Feb 08 17:44:04 2025 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/General/time.scala
Author: Makarius
-Time based on nanoseconds (idealized).
+Time based on nanoseconds (idealized), printed as milliseconds.
*)
signature TIME =
@@ -10,6 +10,9 @@
val min: time * time -> time
val max: time * time -> time
val scale: real -> time -> time
+ val parse: string -> time
+ val print: time -> string
+ val message: time -> string
end;
structure Time: TIME =
@@ -22,4 +25,15 @@
fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t)));
+fun parse s =
+ (case Time.fromString s of
+ SOME t => t
+ | NONE => raise Fail ("Bad time " ^ quote s));
+
+fun print t =
+ if t < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - t)
+ else Time.toString t;
+
+fun message t = print t ^ "s";
+
end;
--- a/src/Pure/General/timing.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/General/timing.ML Sat Feb 08 17:44:04 2025 +0100
@@ -16,6 +16,7 @@
sig
include BASIC_TIMING
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+ val zero: timing
type start
val start: unit -> start
val result: start -> timing
@@ -34,6 +35,8 @@
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
+val zero: timing = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
+
(* timer control *)
@@ -83,9 +86,9 @@
is_relevant_time gc;
fun message {elapsed, cpu, gc} =
- Value.print_time elapsed ^ "s elapsed time, " ^
- Value.print_time cpu ^ "s cpu time, " ^
- Value.print_time gc ^ "s GC time" handle Time.Time => "";
+ Time.message elapsed ^ " elapsed time, " ^
+ Time.message cpu ^ " cpu time, " ^
+ Time.message gc ^ " GC time" handle Time.Time => "";
fun cond_timeit enabled msg e =
if enabled then
--- a/src/Pure/General/value.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/General/value.ML Sat Feb 08 17:44:04 2025 +0100
@@ -13,8 +13,6 @@
val print_int: int -> string
val parse_real: string -> real
val print_real: real -> string
- val parse_time: string -> Time.time
- val print_time: Time.time -> string
end;
structure Value: VALUE =
@@ -82,16 +80,4 @@
| _ => s)
end;
-
-(* time *)
-
-fun parse_time s =
- (case Time.fromString s of
- SOME x => x
- | NONE => raise Fail ("Bad time " ^ quote s));
-
-fun print_time x =
- if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x)
- else Time.toString x;
-
end;
--- a/src/Pure/Isar/runtime.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/Isar/runtime.ML Sat Feb 08 17:44:04 2025 +0100
@@ -113,7 +113,7 @@
let
val msg =
(case exn of
- Timeout.TIMEOUT t => Timeout.print t
+ Timeout.TIMEOUT t => Timeout.message t
| TOPLEVEL_ERROR => "Error"
| ERROR "" => "Error"
| ERROR msg => msg
--- a/src/Pure/PIDE/markup.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Feb 08 17:44:04 2025 +0100
@@ -703,9 +703,9 @@
val gcN = "gc";
fun timing_properties {elapsed, cpu, gc} =
- [(elapsedN, Value.print_time elapsed),
- (cpuN, Value.print_time cpu),
- (gcN, Value.print_time gc)];
+ [(elapsedN, Time.print elapsed),
+ (cpuN, Time.print cpu),
+ (gcN, Time.print gc)];
val timingN = "timing";
fun timing t = (timingN, timing_properties t);
--- a/src/Pure/ROOT.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/ROOT.ML Sat Feb 08 17:44:04 2025 +0100
@@ -54,6 +54,7 @@
ML_file "General/value.ML";
ML_file "General/properties.ML";
ML_file "General/output.ML";
+ML_file "General/time.ML";
ML_file "PIDE/markup.ML";
ML_file "General/utf8.ML";
ML_file "General/scan.ML";
@@ -94,7 +95,6 @@
ML_file "General/long_name.ML";
ML_file "General/binding.ML";
ML_file "General/seq.ML";
-ML_file "General/time.ML";
ML_file "General/timing.ML";
ML_file "General/sha1.ML";
--- a/src/Pure/System/bash.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/System/bash.ML Sat Feb 08 17:44:04 2025 +0100
@@ -10,10 +10,10 @@
val strings: string list -> string
type params
val dest_params: params ->
- {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+ {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
redirect: bool, timeout: Time.time, description: string}
val script: string -> params
- val input: string -> params -> params
+ val input: Bytes.T -> params -> params
val cwd: Path.T -> params -> params
val putenv: (string * string) list -> params -> params
val redirect: params -> params
@@ -56,7 +56,7 @@
abstype params =
Params of
- {script: string, input: string, cwd: Path.T option, putenv: (string * string) list,
+ {script: string, input: Bytes.T, cwd: Path.T option, putenv: (string * string) list,
redirect: bool, timeout: Time.time, description: string}
with
@@ -69,7 +69,7 @@
fun map_params f (Params {script, input, cwd, putenv, redirect, timeout, description}) =
make_params (f (script, input, cwd, putenv, redirect, timeout, description));
-fun script script = make_params (script, "", NONE, [], false, Time.zeroTime, "");
+fun script script = make_params (script, Bytes.empty, NONE, [], false, Time.zeroTime, "");
fun input input =
map_params (fn (script, _, cwd, putenv, redirect, timeout, description) =>
--- a/src/Pure/System/isabelle_system.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/System/isabelle_system.ML Sat Feb 08 17:44:04 2025 +0100
@@ -41,13 +41,15 @@
val {script, input, cwd, putenv, redirect, timeout, description} =
Bash.dest_params params;
val server_run =
- [Bash.server_run, script, input,
- let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
- let open XML.Encode in YXML.string_of_body o list (pair string string) end
- (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
- Value.print_bool redirect,
- Value.print_real (Time.toReal timeout),
- description];
+ [Bytes.string Bash.server_run,
+ Bytes.string script,
+ input,
+ let open XML.Encode in YXML.bytes_of_body (option (string o absolute_path) cwd) end,
+ let open XML.Encode in YXML.bytes_of_body o list (pair string string) end
+ (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
+ Bytes.string (Value.print_bool redirect),
+ Bytes.string (Value.print_real (Time.toReal timeout)),
+ Bytes.string description];
val address = Options.default_string \<^system_option>\<open>bash_process_address\<close>;
val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>;
@@ -93,7 +95,7 @@
Exn.Res res => res
| Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
in
- with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
+ with_streams (fn s => (Byte_Message.write_message (#2 s) server_run; loop NONE s))
end)
end;
--- a/src/Pure/System/process_result.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Pure/System/process_result.ML Sat Feb 08 17:44:04 2025 +0100
@@ -6,6 +6,7 @@
signature PROCESS_RESULT =
sig
+ val startup_failure_rc: int
val interrupt_rc: int
val timeout_rc: int
type T
@@ -29,6 +30,7 @@
structure Process_Result: PROCESS_RESULT =
struct
+val startup_failure_rc = 127
val interrupt_rc = 130
val timeout_rc = 142
--- a/src/Tools/cache_io.ML Sat Feb 08 17:24:19 2025 +0100
+++ b/src/Tools/cache_io.ML Sat Feb 08 17:44:04 2025 +0100
@@ -6,58 +6,18 @@
signature CACHE_IO =
sig
- (*IO wrapper*)
- type result = {
- output: string list,
- redirected_output: string list,
- return_code: int}
- val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
- val run: (Path.T -> Path.T -> string) -> string -> result
-
- (*cache*)
type cache
val unsynchronized_init: Path.T -> cache
val cache_path_of: cache -> Path.T
- val lookup: cache -> string -> result option * string
- val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
- val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
+ val lookup: cache -> string -> Process_Result.T option * string
+ val run: Bash.params -> string -> Process_Result.T
+ val run_and_cache: cache -> string -> Bash.params -> string -> Process_Result.T
+ val run_cached: cache -> Bash.params -> string -> Process_Result.T
end
structure Cache_IO : CACHE_IO =
struct
-(* IO wrapper *)
-
-val cache_io_prefix = "cache-io-"
-
-type result = {
- output: string list,
- redirected_output: string list,
- return_code: int}
-
-fun try_read_lines path =
- let
- fun loop n =
- (case try File.read_lines path of
- SOME lines => lines
- | NONE => if n > 0 then (OS.Process.sleep (seconds 0.05); loop (n - 1)) else [])
- in if File.exists path then loop (if ML_System.platform_is_windows then 20 else 0) else [] end
-
-fun raw_run make_cmd str in_path out_path =
- let
- val _ = File.write in_path str
- val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
- val out1 = try_read_lines out_path
- in {output = split_lines out2, redirected_output = out1, return_code = rc} end
-
-fun run make_cmd str =
- Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
- Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
- raw_run make_cmd str in_path out_path))
-
-
-(* cache *)
-
abstype cache = Cache of {
path: Path.T,
table: (int * (int * int * int) Symtab.table) Synchronized.var }
@@ -107,26 +67,47 @@
else (i, xsp)
val (out, err) =
apply2 rev (snd (fold load (File.read_lines cache_path) (1, ([], []))))
- in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
+ val result =
+ Process_Result.make {rc = 0, out_lines = out, err_lines = err, timing = Timing.zero}
+ in ((SOME result, key), tab) end))
end
-fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
+fun run cmd input =
let
- val {output = err, redirected_output=out, return_code} = run make_cmd str
- val (l1, l2) = apply2 length (out, err)
+ val result = cmd
+ |> Bash.input (Bytes.string input)
+ |> Bash.redirect
+ |> Isabelle_System.bash_process
+ val rc = Process_Result.rc result
+ in
+ if rc = Process_Result.startup_failure_rc then
+ Process_Result.make
+ {rc = rc,
+ err_lines = Process_Result.out_lines result,
+ out_lines = [],
+ timing = Process_Result.timing result}
+ else result
+ end
+
+fun run_and_cache (Cache {path = cache_path, table}) key cmd input =
+ let
+ val result = run cmd input
+ val out_lines = Process_Result.out_lines result
+ val err_lines = Process_Result.err_lines result
+ val (l1, l2) = apply2 length (out_lines, err_lines)
val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
- val lines = map (suffix "\n") (header :: out @ err)
+ val lines = map (suffix "\n") (header :: out_lines @ err_lines)
val _ = Synchronized.change table (fn (p, tab) =>
if Symtab.defined tab key then (p, tab)
else
let val _ = File.append_list cache_path lines
in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in {output = err, redirected_output = out, return_code = return_code} end
+ in result end
-fun run_cached cache make_cmd str =
- (case lookup cache str of
- (NONE, key) => run_and_cache cache key make_cmd str
+fun run_cached cache cmd input =
+ (case lookup cache input of
+ (NONE, key) => run_and_cache cache key cmd input
| (SOME output, _) => output)
end