# HG changeset patch # User Peter Lammich # Date 1608140886 0 # Node ID 686c7ee213e9ee1fda327df44bb145e5fa22083b # Parent 1dc01c11aa86be45f2a3fde4ac5f5eec1cb4c9a3# Parent 12baa337aee290cf28c547d62c3865d459f6d26d merged diff -r 1dc01c11aa86 -r 686c7ee213e9 NEWS --- a/NEWS Wed Dec 16 17:47:50 2020 +0000 +++ b/NEWS Wed Dec 16 17:48:06 2020 +0000 @@ -16,6 +16,14 @@ *** Isabelle/jEdit Prover IDE *** +* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition +of the formal entity at the caret position. + +* The visual feedback on caret entity focus is normally restricted to +definitions within the visible text area. The keyboard modifier "CS" +overrides this: then all defining and referencing positions are shown. +See also option "jedit_focus_modifier". + * Auto nitpick is enabled by default: it is now reasonably fast due to Kodkod invocation within Isabelle/Scala. diff -r 1dc01c11aa86 -r 686c7ee213e9 etc/options --- a/etc/options Wed Dec 16 17:47:50 2020 +0000 +++ b/etc/options Wed Dec 16 17:48:06 2020 +0000 @@ -159,7 +159,7 @@ public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" -public option editor_input_delay : real = 0.3 +public option editor_input_delay : real = 0.2 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Doc/JEdit/JEdit.thy Wed Dec 16 17:48:06 2020 +0000 @@ -1287,8 +1287,9 @@ defining position with all its referencing positions. This correspondence is highlighted in the text according to the cursor position, see also \figref{fig:scope1}. Here the referencing positions are rendered with an - additional border, in reminiscence to a hyperlink: clicking there moves the - cursor to the original defining position. + additional border, in reminiscence to a hyperlink. A mouse click with \<^verbatim>\C\ + modifier, or the action @{action_def "isabelle.goto-entity"} (shortcut + \<^verbatim>\CS+d\) jumps to the original defining position. \begin{figure}[!htb] \begin{center} @@ -1300,8 +1301,9 @@ The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\CS+ENTER\) supports semantic selection of all occurrences of the formal entity at the - caret position. This facilitates systematic renaming, using regular jEdit - editing of a multi-selection, see also \figref{fig:scope2}. + caret position, with a defining position in the current editor buffer. This + facilitates systematic renaming, using regular jEdit editing of a + multi-selection, see also \figref{fig:scope2}. \begin{figure}[!htb] \begin{center} @@ -1310,6 +1312,12 @@ \caption{The result of semantic selection and systematic renaming} \label{fig:scope2} \end{figure} + + By default, the visual feedback on scopes is restricted to definitions + within the visible text area. The keyboard modifier \<^verbatim>\CS\ overrides this: + then all defining and referencing positions are shown. This modifier may be + configured via option @{system_option jedit_focus_modifier}; the default + coincides with the modifier for the above keyboard actions. \ diff -r 1dc01c11aa86 -r 686c7ee213e9 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Wed Dec 16 17:47:50 2020 +0000 +++ b/src/HOL/ATP.thy Wed Dec 16 17:48:06 2020 +0000 @@ -1,6 +1,7 @@ (* Title: HOL/ATP.thy Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen + Author: Martin Desharnais, UniBw Muenchen *) section \Automatic Theorem Provers (ATPs)\ diff -r 1dc01c11aa86 -r 686c7ee213e9 src/HOL/Data_Structures/Trie_Fun.thy --- a/src/HOL/Data_Structures/Trie_Fun.thy Wed Dec 16 17:47:50 2020 +0000 +++ b/src/HOL/Data_Structures/Trie_Fun.thy Wed Dec 16 17:48:06 2020 +0000 @@ -17,12 +17,12 @@ "isin (Nd b m) [] = b" | "isin (Nd b m) (k # xs) = (case m k of None \ False | Some t \ isin t xs)" -fun insert :: "('a::linorder) list \ 'a trie \ 'a trie" where +fun insert :: "'a list \ 'a trie \ 'a trie" where "insert [] (Nd b m) = Nd True m" | "insert (x#xs) (Nd b m) = Nd b (m(x := Some(insert xs (case m x of None \ empty | Some t \ t))))" -fun delete :: "('a::linorder) list \ 'a trie \ 'a trie" where +fun delete :: "'a list \ 'a trie \ 'a trie" where "delete [] (Nd b m) = Nd False m" | "delete (x#xs) (Nd b m) = Nd b (case m x of diff -r 1dc01c11aa86 -r 686c7ee213e9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 16 17:47:50 2020 +0000 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 16 17:48:06 2020 +0000 @@ -33,7 +33,7 @@ datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic - datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice + datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | @@ -97,6 +97,8 @@ val tptp_true : string val tptp_lambda : string val tptp_empty_list : string + val tptp_unary_builtins : string list + val tptp_binary_builtins : string list val dfg_individual_type : string val isabelle_info_prefix : string val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list @@ -191,7 +193,7 @@ datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic -datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice +datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | @@ -257,6 +259,10 @@ val tptp_lambda = "^" val tptp_empty_list = "[]" +val tptp_unary_builtins = [tptp_not] +val tptp_binary_builtins = + [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal] + val dfg_individual_type = "iii" (* cannot clash *) val isabelle_info_prefix = "isabelle_" @@ -455,7 +461,8 @@ else "") -fun tptp_string_of_term _ (ATerm ((s, []), [])) = s +fun tptp_string_of_term _ (ATerm ((s, []), [])) = + s |> member (op =) (tptp_unary_builtins @ tptp_binary_builtins) s ? parens | tptp_string_of_term format (ATerm ((s, tys), ts)) = let val of_type = string_of_type format @@ -473,8 +480,8 @@ else if s = tptp_ho_forall orelse s = tptp_ho_exists then (case ts of [AAbs (((s', ty), tm), [])] => - (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever - possible, to work around LEO-II 1.2.8 parser limitation. *) + (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work + around LEO-II, Leo-III, and Satallax parser limitation. *) tptp_string_of_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) @@ -482,19 +489,18 @@ else if s = tptp_choice then (case ts of [AAbs (((s', ty), tm), args)] => - (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is - always applied to an abstraction. *) + (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an + abstraction. *) tptp_string_of_app format (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^ "]: " ^ of_term tm ^ "" |> parens) (map of_term args) | _ => app ()) - else if s = tptp_not then - (* agsyHOL doesn't like negations applied like this: "~ @ t". *) - (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens | _ => s) - else if member (op =) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, - tptp_not_iff, tptp_equal] s then - (* agsyHOL doesn't like connectives applied like this: "& @ t1 @ t2". *) + else if member (op =) tptp_unary_builtins s then + (* generate e.g. "~ t" instead of "~ @ t". *) + (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens) + else if member (op =) tptp_binary_builtins s then + (* generate e.g. "t1 & t2" instead of "& @ t1 @ t2". *) (case ts of [t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens | _ => app ()) diff -r 1dc01c11aa86 -r 686c7ee213e9 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 16 17:47:50 2020 +0000 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 16 17:48:06 2020 +0000 @@ -2,6 +2,7 @@ Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen + Author: Martin Desharnais, UniBw Muenchen Translation of HOL to FOL for Metis and Sledgehammer. *) @@ -99,7 +100,7 @@ val is_type_enc_sound : type_enc -> bool val type_enc_of_string : strictness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc - val is_lambda_free : term -> bool + val is_first_order_lambda_free : term -> bool val do_cheaply_conceal_lambdas : typ list -> term -> term val mk_aconns : atp_connective -> ('a, 'b, 'c, 'd) atp_formula list @@ -162,7 +163,7 @@ fun is_type_enc_native (Native _) = true | is_type_enc_native _ = false -fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Bool_Free, _, _, _)) = false +fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true | is_type_enc_full_higher_order _ = false fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true @@ -654,11 +655,11 @@ | (_, Undercover_Types) => raise Same.SAME | (Mangled_Monomorphic, _) => if is_type_level_uniform level then - Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level) + Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level) else raise Same.SAME | (poly as Raw_Polymorphic _, All_Types) => - Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types) + Native (Higher_Order THF_With_Choice, fool, poly, All_Types) | _ => raise Same.SAME)) end @@ -695,8 +696,8 @@ end handle Same.SAME => error ("Unknown type encoding: " ^ quote s) -fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free - | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free +fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free + | min_hologic _ THF_Lambda_Free = THF_Lambda_Free | min_hologic THF_Without_Choice _ = THF_Without_Choice | min_hologic _ THF_Without_Choice = THF_Without_Choice | min_hologic _ _ = THF_With_Choice @@ -728,42 +729,62 @@ (if is_type_enc_sound type_enc then Tags else Guards) stuff | adjust_type_enc _ type_enc = type_enc -fun is_lambda_free t = +fun is_first_order_lambda_free t = (case t of - \<^const>\Not\ $ t1 => is_lambda_free t1 - | Const (\<^const_name>\All\, _) $ Abs (_, _, t') => is_lambda_free t' - | Const (\<^const_name>\All\, _) $ t1 => is_lambda_free t1 - | Const (\<^const_name>\Ex\, _) $ Abs (_, _, t') => is_lambda_free t' - | Const (\<^const_name>\Ex\, _) $ t1 => is_lambda_free t1 - | \<^const>\HOL.conj\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 - | \<^const>\HOL.disj\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 - | \<^const>\HOL.implies\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 + \<^const>\Not\ $ t1 => is_first_order_lambda_free t1 + | Const (\<^const_name>\All\, _) $ Abs (_, _, t') => is_first_order_lambda_free t' + | Const (\<^const_name>\All\, _) $ t1 => is_first_order_lambda_free t1 + | Const (\<^const_name>\Ex\, _) $ Abs (_, _, t') => is_first_order_lambda_free t' + | Const (\<^const_name>\Ex\, _) $ t1 => is_first_order_lambda_free t1 + | \<^const>\HOL.conj\ $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2 + | \<^const>\HOL.disj\ $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2 + | \<^const>\HOL.implies\ $ t1 $ t2 => + is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2 | Const (\<^const_name>\HOL.eq\, Type (_, [\<^typ>\bool\, _])) $ t1 $ t2 => - is_lambda_free t1 andalso is_lambda_free t2 + is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)) -fun simple_translate_lambdas do_lambdas ctxt t = - if is_lambda_free t then +fun simple_translate_lambdas do_lambdas ctxt type_enc t = + if is_first_order_lambda_free t then t else let - fun trans Ts t = + fun trans_first_order Ts t = (case t of - \<^const>\Not\ $ t1 => \<^const>\Not\ $ trans Ts t1 + \<^const>\Not\ $ t1 => \<^const>\Not\ $ trans_first_order Ts t1 | (t0 as Const (\<^const_name>\All\, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, trans (T :: Ts) t') - | (t0 as Const (\<^const_name>\All\, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1) + t0 $ Abs (s, T, trans_first_order (T :: Ts) t') + | (t0 as Const (\<^const_name>\All\, _)) $ t1 => + trans_first_order Ts (t0 $ eta_expand Ts t1 1) | (t0 as Const (\<^const_name>\Ex\, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, trans (T :: Ts) t') - | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1) - | (t0 as \<^const>\HOL.conj\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 - | (t0 as \<^const>\HOL.disj\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 - | (t0 as \<^const>\HOL.implies\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 + t0 $ Abs (s, T, trans_first_order (T :: Ts) t') + | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => + trans_first_order Ts (t0 $ eta_expand Ts t1 1) + | (t0 as \<^const>\HOL.conj\) $ t1 $ t2 => + t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2 + | (t0 as \<^const>\HOL.disj\) $ t1 $ t2 => + t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2 + | (t0 as \<^const>\HOL.implies\) $ t1 $ t2 => + t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2 | (t0 as Const (\<^const_name>\HOL.eq\, Type (_, [\<^typ>\bool\, _]))) $ t1 $ t2 => - t0 $ trans Ts t1 $ trans Ts t2 + t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then t else t |> Envir.eta_contract |> do_lambdas ctxt Ts) + + fun trans_fool Ts t = + (case t of + (t0 as Const (\<^const_name>\All\, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, trans_fool (T :: Ts) t') + | (t0 as Const (\<^const_name>\All\, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1) + | (t0 as Const (\<^const_name>\Ex\, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, trans_fool (T :: Ts) t') + | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1) + | t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2 + | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts + | _ => t) + + val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end @@ -809,18 +830,18 @@ Lambda_Lifting.is_quantifier #> fst -fun lift_lams_part_2 ctxt (facts, lifted) = +fun lift_lams_part_2 ctxt type_enc (facts, lifted) = (facts, lifted) (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid of them *) - |> apply2 (map (introduce_combinators ctxt)) + |> apply2 (map (introduce_combinators ctxt type_enc)) |> apply2 (map constify_lifted) (* Requires bound variables not to clash with any schematic variables (as should be the case right after lambda-lifting). *) |>> map (hol_open_form (unprefix hol_close_form_prefix)) ||> map (hol_open_form I) -fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt +fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc fun intentionalize_def (Const (\<^const_name>\All\, _) $ Abs (_, _, t)) = intentionalize_def t @@ -1103,67 +1124,121 @@ val unmangled_invert_const = invert_const o hd o unmangled_const_name +fun vars_of_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars + | vars_of_iterm vars (IVar ((s, _), _)) = insert (op =) s vars + | vars_of_iterm vars (IApp (tm1, tm2)) = union (op =) (vars_of_iterm vars tm1) (vars_of_iterm vars tm2) + | vars_of_iterm vars (IAbs (_, tm)) = vars_of_iterm vars tm + +fun generate_unique_name gen unique n = + let val x = gen n in + if unique x then x else generate_unique_name gen unique (n + 1) + end + +fun eta_expand_quantifier_body (tm as IAbs _) = tm + | eta_expand_quantifier_body tm = + let + (* We accumulate all variables because E 2.5 does not support variable shadowing. *) + val vars = vars_of_iterm [] tm + val x = generate_unique_name + (fn n => "X" ^ (if n = 0 then "" else string_of_int n)) + (fn name => not (exists (equal name) vars)) 0 + val T = domain_type (ityp_of tm) + in + IAbs ((`I x, T), IApp (tm, IConst (`I x, T, []))) + end + fun introduce_proxies_in_iterm type_enc = let - fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, []) - | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ = - (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser - limitation. This works in conjuction with special code in - "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever - possible. *) + fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] = + (* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser + limitations. This works in conjunction with special code in "ATP_Problem" that uses the + syntactic sugar "!" and "?" whenever possible. *) IAbs ((`I "P", p_T), IApp (IConst (`I ho_quant, T, []), IAbs ((`I "X", x_T), IApp (IConst (`I "P", p_T, []), IConst (`I "X", x_T, []))))) - | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier" + | tweak_ho_quant ho_quant T _ = IConst (`I ho_quant, T, []) + fun tweak_ho_equal T argc = + if argc = 2 then + IConst (`I tptp_equal, T, []) + else + (* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers + complain about not being able to infer the type of "=". *) + let val i_T = domain_type T in + IAbs ((`I "Y", i_T), + IAbs ((`I "Z", i_T), + IApp (IApp (IConst (`I tptp_equal, T, []), + IConst (`I "Y", i_T, [])), + IConst (`I "Z", i_T, [])))) + end fun intro top_level args (IApp (tm1, tm2)) = - IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2) + let + val tm1' = intro top_level (tm2 :: args) tm1 + val tm2' = intro false [] tm2 + val tm2'' = + (case tm1' of + IConst ((s, _), _, _) => + if s = tptp_ho_forall orelse s = tptp_ho_exists then + eta_expand_quantifier_body tm2' + else + tm2' + | _ => tm2') + in + IApp (tm1', tm2'') + end | intro top_level args (IConst (name as (s, _), T, T_args)) = (case proxify_const s of SOME proxy_base => let val argc = length args - val plain_const = IConst (name, T, []) + fun plain_const () = IConst (name, T, []) fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) - val is_fool = is_type_enc_fool type_enc - fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const + fun handle_fool card x = if card = argc then x else proxy_const () in - if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then - (case (top_level, s) of - (_, "c_False") => IConst (`I tptp_false, T, []) - | (_, "c_True") => IConst (`I tptp_true, T, []) - | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, [])) - | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, [])) - | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, [])) - | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, [])) - | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args) - | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args) - | (false, s) => + if top_level then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | _ => plain_const ()) + else if is_type_enc_full_higher_order type_enc then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "c_Not" => IConst (`I tptp_not, T, []) + | "c_conj" => IConst (`I tptp_and, T, []) + | "c_disj" => IConst (`I tptp_or, T, []) + | "c_implies" => IConst (`I tptp_implies, T, []) + | "c_All" => tweak_ho_quant tptp_ho_forall T args + | "c_Ex" => tweak_ho_quant tptp_ho_exists T args + | s => if is_tptp_equal s then - if argc = 2 then - IConst (`I tptp_equal, T, []) - else if is_fool then - proxy_const () - else - (* Eta-expand partially applied THF equality, because the - LEO-II and Satallax parsers complain about not being able to - infer the type of "=". *) - let val i_T = domain_type T in - IAbs ((`I "Y", i_T), - IAbs ((`I "Z", i_T), - IApp (IApp (IConst (`I tptp_equal, T, []), - IConst (`I "Y", i_T, [])), - IConst (`I "Z", i_T, [])))) - end + tweak_ho_equal T argc else - plain_const - | _ => plain_const) + plain_const ()) + else if is_type_enc_fool type_enc then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, [])) + | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, [])) + | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, [])) + | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, [])) + | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args) + | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args) + | s => + if is_tptp_equal s then + handle_fool 2 (IConst (`I tptp_equal, T, [])) + else + plain_const ()) else - IConst (proxy_base |>> prefix const_prefix, T, T_args) + proxy_const () end - | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args - else IConst (name, T, T_args)) + | NONE => + if s = tptp_choice then + tweak_ho_quant tptp_choice T args + else + IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end @@ -1423,20 +1498,20 @@ (** predicators and application operators **) -type sym_info = - {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, - in_conj : bool} +type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool} fun default_sym_tab_entries type_enc = - (make_fixed_const NONE \<^const_name>\undefined\, - {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) :: - ([tptp_false, tptp_true] - |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @ - ([tptp_equal, tptp_old_equal] - |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false})) - |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc) - ? cons (prefixed_predicator_name, - {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) + let + fun mk_sym_info pred n = + {pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false} + in + (make_fixed_const NONE \<^const_name>\undefined\, mk_sym_info false 0) :: + (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @ + (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @ + (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins)) + |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc) + ? cons (prefixed_predicator_name, mk_sym_info true 1) + end datatype app_op_level = Min_App_Op | @@ -1833,17 +1908,17 @@ else if lam_trans = liftingN orelse lam_trans = lam_liftingN then lift_lams ctxt type_enc else if lam_trans = combsN then - map (introduce_combinators ctxt) #> rpair [] + map (introduce_combinators ctxt type_enc) #> rpair [] else if lam_trans = combs_and_liftingN then lift_lams_part_1 ctxt type_enc - ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) - #> lift_lams_part_2 ctxt + ##> maps (fn t => [t, introduce_combinators ctxt type_enc (intentionalize_def t)]) + #> lift_lams_part_2 ctxt type_enc else if lam_trans = combs_or_liftingN then lift_lams_part_1 ctxt type_enc ##> map (fn t => (case head_of (strip_qnt_body \<^const_name>\All\ t) of \<^term>\(=) ::bool => bool => bool\ => t - | _ => introduce_combinators ctxt (intentionalize_def t))) - #> lift_lams_part_2 ctxt + | _ => introduce_combinators ctxt type_enc (intentionalize_def t))) + #> lift_lams_part_2 ctxt type_enc else if lam_trans = keep_lamsN then map (Envir.eta_contract) #> rpair [] else diff -r 1dc01c11aa86 -r 686c7ee213e9 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Dec 16 17:47:50 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Dec 16 17:48:06 2020 +0000 @@ -296,7 +296,7 @@ val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS val (format, enc) = if modern then - (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher") + (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher_fool") else (TFF (Without_FOOL, Monomorphic), "mono_native") in diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Pure/PIDE/markup.scala Wed Dec 16 17:48:06 2020 +0000 @@ -119,7 +119,7 @@ def unapply(markup: Markup): Option[Long] = if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None } - object Id + object Occ { def unapply(markup: Markup): Option[Long] = Def.unapply(markup) orElse Ref.unapply(markup) diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Pure/PIDE/rendering.scala Wed Dec 16 17:48:06 2020 +0000 @@ -178,6 +178,13 @@ val empty: Focus = apply(Set.empty) def make(args: List[Text.Info[Focus]]): Focus = (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }) + + val full: Focus = + new Focus(Set.empty) + { + override def apply(id: Long): Boolean = true + override def toString: String = "Focus.full" + } } sealed class Focus private[Rendering](protected val rep: Set[Long]) @@ -439,14 +446,14 @@ range, (List(Markup.Empty), None), elements, command_states => { - case (((markups, color), Text.Info(_, XML.Elem(markup, _)))) + case ((markups, color), Text.Info(_, XML.Elem(markup, _))) if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) => Some((markup :: markups, color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => Some((Nil, Some(Rendering.Color.bad))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(Rendering.Color.intensify))) - case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => + case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => val color = @@ -472,7 +479,7 @@ else None }) color <- - (result match { + result match { case (markups, opt_color) if markups.nonEmpty => val status = Document_Status.Command_Status.make(markups.iterator) if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) @@ -480,7 +487,7 @@ else if (status.is_canceled) Some(Rendering.Color.canceled) else opt_color case (_, opt_color) => opt_color - }) + } } yield Text.Info(r, color) } @@ -504,33 +511,38 @@ case _ => None })) - def entity_focus(range: Text.Range, visible_defs: Rendering.Focus): Rendering.Focus = + def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus = Rendering.Focus.make( snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => { case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _))) - if visible_defs(i) => Some(focus + i) + if defs_focus(i) => Some(focus + i) case _ => None })) /* caret focus */ - def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus = + def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus = { val focus = entity_focus_defs(caret_range) if (focus.defined) focus - else entity_focus(caret_range, entity_focus_defs(visible_range)) + else if (defs_range == Text.Range.offside) Rendering.Focus.empty + else { + val defs_focus = + if (defs_range == Text.Range.full) Rendering.Focus.full + else entity_focus_defs(defs_range) + entity_focus(caret_range, defs_focus) + } } - def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = + def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] = { - val focus_defs = caret_focus(caret_range, visible_range) - if (focus_defs.defined) { - snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ => + val focus = caret_focus(caret_range, defs_range) + if (focus.defined) { + snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ => { - case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) - if focus_defs(i) => Some(true) + case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true) case _ => None }).flatMap(info => if (info.info) Some(info.range) else None) } diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/etc/options Wed Dec 16 17:48:06 2020 +0000 @@ -39,6 +39,9 @@ public option jedit_text_overview : bool = true -- "paint text overview column" +public option jedit_focus_modifier : string = "CS" + -- "keyboard modifier to enable entity focus regardless of def visibility" + public option isabelle_fonts_hinted : bool = true -- "use hinted Isabelle DejaVu fonts (change requires restart)" diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/actions.xml Wed Dec 16 17:48:06 2020 +0000 @@ -67,6 +67,11 @@ isabelle.jedit.Isabelle.newline(textArea); + + + isabelle.jedit.Isabelle.goto_entity(view); + + isabelle.jedit.Isabelle.select_entity(textArea); diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/isabelle.scala Wed Dec 16 17:48:06 2020 +0000 @@ -352,7 +352,18 @@ } - /* selection */ + /* formal entities */ + + def goto_entity(view: View) + { + val text_area = view.getTextArea + for { + doc_view <- Document_View.get(text_area) + rendering = doc_view.get_rendering() + caret_range = JEdit_Lib.caret_range(text_area) + link <- rendering.hyperlink_entity(caret_range) + } link.info.follow(view) + } def select_entity(text_area: JEditTextArea) { diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/jEdit.props Wed Dec 16 17:48:06 2020 +0000 @@ -225,6 +225,8 @@ isabelle.exclude-word.label=Exclude word isabelle.first-error.label=Go to first error isabelle.first-error.shortcut=CS+a +isabelle.goto-entity.label=Go to definition of formal entity at caret +isabelle.goto-entity.shortcut=CS+d isabelle.include-word-permanently.label=Include word permanently isabelle.include-word.label=Include word isabelle.increase-font-size.label=Increase font size diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 16 17:48:06 2020 +0000 @@ -17,8 +17,8 @@ import scala.util.parsing.input.CharSequenceReader import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} -import org.gjt.sp.jedit.gui.KeyEventWorkaround +import org.gjt.sp.jedit.io.{FileVFS, VFSManager} +import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator} import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} @@ -400,4 +400,10 @@ def shift_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0 + + def modifier_string(evt: InputEvent): String = + KeyEventTranslator.getModifierString(evt) match { + case null => "" + case s => s + } } diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 16 17:48:06 2020 +0000 @@ -285,6 +285,18 @@ }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } + def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = + { + snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( + range, Vector.empty, Rendering.entity_elements, _ => + { + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => + val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) + opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) + case _ => None + }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } + } + /* active elements */ diff -r 1dc01c11aa86 -r 686c7ee213e9 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Dec 16 17:47:50 2020 +0000 +++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Dec 16 17:48:06 2020 +0000 @@ -10,9 +10,9 @@ import isabelle._ -import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo} +import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, - FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} + FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent} import java.awt.font.TextAttribute import javax.swing.SwingUtilities import java.text.AttributedString @@ -71,6 +71,32 @@ pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") + /* caret focus modifier */ + + @volatile private var caret_focus_modifier = false + + def caret_focus_range: Text.Range = + if (caret_focus_modifier) Text.Range.full + else JEdit_Lib.visible_range(text_area) getOrElse Text.Range.offside + + private val key_listener = + JEdit_Lib.key_listener( + key_pressed = (evt: KeyEvent) => + { + val mod = PIDE.options.string("jedit_focus_modifier") + val old = caret_focus_modifier + caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt)) + if (caret_focus_modifier != old) caret_update() + }, + key_released = _ => + { + if (caret_focus_modifier) { + caret_focus_modifier = false + caret_update() + } + }) + + /* common painter state */ @volatile private var painter_rendering: JEdit_Rendering = null @@ -86,11 +112,10 @@ painter_rendering = get_rendering() painter_clip = gfx.getClip caret_focus = - JEdit_Lib.visible_range(text_area) match { - case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated => - painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range) - case _ => Rendering.Focus.empty + if (caret_enabled && !painter_rendering.snapshot.is_outdated) { + painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range) } + else Rendering.Focus.empty } } @@ -674,6 +699,7 @@ painter.removeExtension(orig_text_painter) painter.addMouseListener(mouse_listener) painter.addMouseMotionListener(mouse_motion_listener) + text_area.addKeyListener(key_listener) text_area.addFocusListener(focus_listener) view.addWindowListener(window_listener) } @@ -684,6 +710,7 @@ val painter = text_area.getPainter view.removeWindowListener(window_listener) text_area.removeFocusListener(focus_listener) + text_area.removeKeyListener(key_listener) painter.removeMouseMotionListener(mouse_motion_listener) painter.removeMouseListener(mouse_listener) painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)