--- 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.
--- 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
--- 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>\<open>C\<close>
+ modifier, or the action @{action_def "isabelle.goto-entity"} (shortcut
+ \<^verbatim>\<open>CS+d\<close>) jumps to the original defining position.
\begin{figure}[!htb]
\begin{center}
@@ -1300,8 +1301,9 @@
The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
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>\<open>CS\<close> 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.
\<close>
--- 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 \<open>Automatic Theorem Provers (ATPs)\<close>
--- 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 \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
-fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun insert :: "'a list \<Rightarrow> 'a trie \<Rightarrow> '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 \<Rightarrow> empty | Some t \<Rightarrow> t))))"
-fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun delete :: "'a list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
"delete [] (Nd b m) = Nd False m" |
"delete (x#xs) (Nd b m) = Nd b
(case m x of
--- 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 ())
--- 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>\<open>Not\<close> $ t1 => is_lambda_free t1
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
- | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_lambda_free t1
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
- | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_lambda_free t1
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
+ \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
+ | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+ | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
+ | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
+ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ 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>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans Ts t1
+ \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, trans (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
+ t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+ trans_first_order Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, trans (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
- | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
- | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
+ t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+ trans_first_order Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+ | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+ | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ 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>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ 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>\<open>All\<close>, _) $ 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>\<open>undefined\<close>,
- {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>\<open>undefined\<close>, 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>\<open>All\<close> t) of
\<^term>\<open>(=) ::bool => bool => bool\<close> => 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
--- 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
--- 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)
--- 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)
}
--- 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)"
--- 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);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.goto-entity">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_entity(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.select-entity">
<CODE>
isabelle.jedit.Isabelle.select_entity(textArea);
--- 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)
{
--- 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
--- 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
+ }
}
--- 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 */
--- 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)