# HG changeset patch # User Fabian Huch # Date 1739033044 -3600 # Node ID bb6a3b379f6a23875cb85f48bc4a7cc4339f86ac # Parent 1126ee407227beda2d91bc884a7f107794759e20# Parent eebb8270b3cc1ca36d71b54dac7813e711d9d98c merged diff -r 1126ee407227 -r bb6a3b379f6a NEWS --- 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. diff -r 1126ee407227 -r bb6a3b379f6a src/Doc/Isar_Ref/HOL_Specific.thy --- 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}? diff -r 1126ee407227 -r bb6a3b379f6a src/Doc/Sugar/Sugar.thy --- 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 @@ \ lemma True proof - - \ \pretty trivial\ - show True by force + show True by (rule TrueI) qed text_raw \ \end{minipage}\end{center} @@ -498,21 +497,20 @@ \begin{quote} \small -\verb!text_raw {!\verb!*!\\ +\verb!text_raw \!\verb!!\\ \verb! \begin{figure}!\\ \verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ \verb! \isastyleminor\isamarkuptrue!\\ -\verb!*!\verb!}!\\ +\verb!\!\verb!!\\ \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!!\\ \verb! \end{minipage}\end{center}!\\ \verb! \caption{Example proof in a figure.}\label{fig:proof}!\\ \verb! \end{figure}!\\ -\verb!*!\verb!}! +\verb!\!\verb!! \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!\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!!\\ \emph{theory text}\\ -\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}! +\verb!\text_raw\!\verb!%endsnip\!\verb!! \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. diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Data_Structures/Define_Time_Function.ML --- 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 (_ \ ... \ _ to _ \ ... \ 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 \ nat \ nat \ 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 \ nat \ 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 \ 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 \ 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 (_ \ ... \ _ to _ \ ... \ 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 \ (nat \ nat option) \ 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 \ 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 \ 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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Data_Structures/Define_Time_Function.thy --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Data_Structures/Time_Examples.thy --- /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 \ bool" + and odd :: "nat \ 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 \ 'b" + and T_f :: "'a \ nat" +begin + +fun simple where + "simple a = f a" +time_fun simple + +fun even :: "'a list \ 'b list" and odd :: "'a list \ '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 \ nat" where + "locSum [] = 0" +| "locSum (x#xs) = x + locSum xs" +time_fun locSum + +fun map :: "'a list \ 'b list" where + "map [] = []" +| "map (x#xs) = f x # map xs" +time_fun map + +end + +definition "let_lambda a b c \ let lam = (\a b. a + b) in lam a (lam b c)" +time_fun let_lambda + +partial_function (tailrec) collatz :: "nat \ bool" where + "collatz n = (if n \ 1 then True + else if n mod 2 = 0 then collatz (n div 2) + else collatz (3 * n + 1))" + +text \This is the expected time function:\ +partial_function (option) T_collatz' :: "nat \ nat option" where + "T_collatz' n = (if n \ 1 then Some 0 + else if n mod 2 = 0 then Option.bind (T_collatz' (n div 2)) (\k. Some (Suc k)) + else Option.bind (T_collatz' (3 * n + 1)) (\k. Some (Suc k)))" +time_fun_0 "(mod)" +time_partial_function collatz + +text \Proof that they are the same up to 20:\ +lemma setIt: "P i \ \n \ {Suc i..j}. P n \ \n \ {i..j}. P n" + by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) +lemma "\n \ {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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Groups_List.thy --- 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 \ set xs \ 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 \ 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 \ n \ sum_list [m.. {m..x. x \ set xs \ 0 \ x) \ 0 \ sum_list xs" -by (induction xs) auto + by (induction xs) auto lemma sum_list_nonpos: "(\x. x \ set xs \ x \ 0) \ sum_list xs \ 0" -by (induction xs) (auto simp: add_nonpos_nonpos) + by (induction xs) (auto simp: add_nonpos_nonpos) lemma sum_list_nonneg_eq_0_iff: "(\x. x \ set xs \ 0 \ x) \ sum_list xs = 0 \ (\x\ 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 \ (\n \ 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 \ set xs \ x \ 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 \ ns ! k \ 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 \ 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: "(\x\xs. r) = of_nat (length xs) * r" @@ -276,8 +287,7 @@ lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list" shows "\ length xs = length ys; \i. i < length xs \ xs!i \ ys!i \ \ sum_list xs \ 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 \ 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 \ set xs" "\x. x \ set xs \ x \ 0" + shows "x \ sum_list xs" + using assms +proof (induction xs) + case (Cons y xs) + show ?case + proof (cases "y = x") + case True + have "x + 0 \ 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 \ 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 \Horner sums\ diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Nat.thy --- 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 \ n \ 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 \ m < n" for m n :: nat @@ -1755,6 +1755,9 @@ by simp qed +lemma of_nat_diff_if: \of_nat (m - n) = (if n\m then of_nat m - of_nat n else 0)\ + by (simp add: not_le less_imp_le) + end text \Class for unital semirings with characteristic zero. diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Number_Theory/Cong.thy --- 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 \Thanks to Manuel Eberl\ +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) \ 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 \ 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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/ROOT --- 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 + diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Real_Vector_Spaces.thy --- 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) = (\x\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 \ 0 \ of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)" by (simp add: of_real_def nonzero_inverse_scaleR_distrib) diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/TPTP/TPTP_Interpret_Test.thy --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Tools/SMT/smt_config.ML --- 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>\=\ |-- 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>\smt_solver\ +val _ = + Theory.setup (Attrib.setup \<^binding>\smt_solver\ (Scan.lift (\<^keyword>\=\ |-- Args.name) >> (Thm.declaration_attribute o K o select_solver)) - "SMT solver configuration" + "SMT solver configuration"); (* options *) -val oracle = Attrib.setup_config_bool \<^binding>\smt_oracle\ (K true) -val timeout = Attrib.setup_config_real \<^binding>\smt_timeout\ (K 0.0) -val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\smt_reconstruction_step_timeout\ (K 10.0) -val random_seed = Attrib.setup_config_int \<^binding>\smt_random_seed\ (K 1) -val read_only_certificates = Attrib.setup_config_bool \<^binding>\smt_read_only_certificates\ (K false) -val verbose = Attrib.setup_config_bool \<^binding>\smt_verbose\ (K true) -val trace = Attrib.setup_config_bool \<^binding>\smt_trace\ (K false) -val trace_verit = Attrib.setup_config_bool \<^binding>\smt_debug_verit\ (K false) -val spy_verit_attr = Attrib.setup_config_bool \<^binding>\smt_spy_verit\ (K false) -val spy_z3 = Attrib.setup_config_bool \<^binding>\smt_spy_z3\ (K false) -val trace_arith_verit = Attrib.setup_config_bool \<^binding>\smt_debug_arith_verit\ (K false) -val trace_verit_compression = Attrib.setup_config_bool \<^binding>\verit_compress_proofs\ (K true) -val statistics = Attrib.setup_config_bool \<^binding>\smt_statistics\ (K false) -val monomorph_limit = Attrib.setup_config_int \<^binding>\smt_monomorph_limit\ (K 10) -val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (K 500) -val explicit_application = Attrib.setup_config_int \<^binding>\smt_explicit_application\ (K 1) -val higher_order = Attrib.setup_config_bool \<^binding>\smt_higher_order\ (K false) -val native_bv = Attrib.setup_config_bool \<^binding>\native_bv\ (K true) -val nat_as_int = Attrib.setup_config_bool \<^binding>\smt_nat_as_int\ (K false) -val infer_triggers = Attrib.setup_config_bool \<^binding>\smt_infer_triggers\ (K false) -val debug_files = Attrib.setup_config_string \<^binding>\smt_debug_files\ (K "") -val sat_solver = Attrib.setup_config_string \<^binding>\smt_sat_solver\ (K "cdclite") -val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\smt_cvc_lethe\ (K false) +val oracle = Attrib.setup_config_bool \<^binding>\smt_oracle\ (K true); +val timeout = Attrib.setup_config_real \<^binding>\smt_timeout\ (K 0.0); +val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\smt_reconstruction_step_timeout\ (K 10.0); +val random_seed = Attrib.setup_config_int \<^binding>\smt_random_seed\ (K 1); +val read_only_certificates = Attrib.setup_config_bool \<^binding>\smt_read_only_certificates\ (K false); +val verbose = Attrib.setup_config_bool \<^binding>\smt_verbose\ (K true); +val trace = Attrib.setup_config_bool \<^binding>\smt_trace\ (K false); +val trace_verit = Attrib.setup_config_bool \<^binding>\smt_debug_verit\ (K false); +val spy_verit_attr = Attrib.setup_config_bool \<^binding>\smt_spy_verit\ (K false); +val spy_z3 = Attrib.setup_config_bool \<^binding>\smt_spy_z3\ (K false); +val trace_arith_verit = Attrib.setup_config_bool \<^binding>\smt_debug_arith_verit\ (K false); +val trace_verit_compression = Attrib.setup_config_bool \<^binding>\verit_compress_proofs\ (K true); +val statistics = Attrib.setup_config_bool \<^binding>\smt_statistics\ (K false); +val monomorph_limit = Attrib.setup_config_int \<^binding>\smt_monomorph_limit\ (K 10); +val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (K 500); +val explicit_application = Attrib.setup_config_int \<^binding>\smt_explicit_application\ (K 1); +val higher_order = Attrib.setup_config_bool \<^binding>\smt_higher_order\ (K false); +val native_bv = Attrib.setup_config_bool \<^binding>\native_bv\ (K true); +val nat_as_int = Attrib.setup_config_bool \<^binding>\smt_nat_as_int\ (K false); +val infer_triggers = Attrib.setup_config_bool \<^binding>\smt_infer_triggers\ (K false); +val debug_files = Attrib.setup_config_string \<^binding>\smt_debug_files\ (K ""); +val sat_solver = Attrib.setup_config_string \<^binding>\smt_sat_solver\ (K "cdclite"); +val cvc_experimental_lethe = Attrib.setup_config_bool \<^binding>\smt_cvc_lethe\ (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>\smt_certificates\ +val _ = + Theory.setup (Attrib.setup \<^binding>\smt_certificates\ (Scan.lift (\<^keyword>\=\ |-- 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>\smt_status\ @@ -284,4 +275,4 @@ \and the values of SMT configuration options" (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) -end; +end diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/HOL/Tools/SMT/smt_systems.ML --- 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 = diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/Concurrent/timeout.ML --- 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; diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/General/bytes.ML --- 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 *) diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/General/time.ML --- 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; diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/General/timing.ML --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/General/value.ML --- 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; diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/Isar/runtime.ML --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/PIDE/markup.ML --- 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); diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/ROOT.ML --- 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"; diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/System/bash.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) => diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/System/isabelle_system.ML --- 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>\bash_process_address\; val password = Options.default_string \<^system_option>\bash_process_password\; @@ -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; diff -r 1126ee407227 -r bb6a3b379f6a src/Pure/System/process_result.ML --- 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 diff -r 1126ee407227 -r bb6a3b379f6a src/Tools/cache_io.ML --- 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