# HG changeset patch # User wenzelm # Date 1466512967 -7200 # Node ID ae9330fdbc16fe443840244c0a5f0f467551fb31 # Parent 054a92af0f2b487204edacdf9e64d81acfff4d4a position information for literal facts; Markup.entry may have empty kind/name; diff -r 054a92af0f2b -r ae9330fdbc16 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue Jun 21 11:03:24 2016 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue Jun 21 14:42:47 2016 +0200 @@ -16,7 +16,7 @@ val names = map Thm.get_name_hint thms val add_info = if null names then I else suffix (":\n" ^ commas names) - val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) + val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))) fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt diff -r 054a92af0f2b -r ae9330fdbc16 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jun 21 11:03:24 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jun 21 14:42:47 2016 +0200 @@ -468,6 +468,7 @@ val named_locals = Facts.dest_static true [global_facts] local_facts val unnamed_locals = Facts.props local_facts + |> map #1 |> filter (is_useful_unnamed_local_fact ctxt) |> map (pair "" o single) diff -r 054a92af0f2b -r ae9330fdbc16 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Jun 21 11:03:24 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Jun 21 14:42:47 2016 +0200 @@ -945,15 +945,18 @@ in -fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; - fun potential_facts ctxt prop = let val body = Term.strip_all_body prop; - val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts; + val vacuous = + filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts + |> map (rpair Position.none); in Facts.could_unify (facts_of ctxt) body @ vacuous end; -fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i); +fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; + +fun some_fact_tac ctxt = + SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i); end; @@ -993,18 +996,23 @@ val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s |> singleton (Variable.polymorphic ctxt); - fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop); + fun err ps msg = + error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop); val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); - fun prove_fact th = - Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); - val results = map_filter (try prove_fact) (potential_facts ctxt prop'); - val thm = - (case distinct Thm.eq_thm_prop results of - [thm] => thm - | [] => err "Failed to retrieve literal fact" - | _ => err "Ambiguous specification of literal fact"); - in pick true ("", Position.none) [thm] end + fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); + val results = map_filter (try (apfst prove)) (potential_facts ctxt prop'); + val (thm, thm_pos) = + (case distinct (eq_fst Thm.eq_thm_prop) results of + [res] => res + | [] => err [] "Failed to retrieve literal fact" + | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact"); + + val markup = + (Markup.entity Markup.literal_factN "") + |> Markup.properties (Position.def_properties_of thm_pos); + val _ = Context_Position.report_generic context pos markup; + in pick true ("", thm_pos) [thm] end | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; @@ -1450,7 +1458,7 @@ fun pretty_local_facts verbose ctxt = let val facts = facts_of ctxt; - val props = Facts.props facts; + val props = map #1 (Facts.props facts); val local_facts = (if null props then [] else [("", props)]) @ Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts; diff -r 054a92af0f2b -r ae9330fdbc16 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Jun 21 11:03:24 2016 +0200 +++ b/src/Pure/PIDE/markup.ML Tue Jun 21 14:42:47 2016 +0200 @@ -86,6 +86,7 @@ val fixedN: string val fixed: string -> T val caseN: string val case_: string -> T val dynamic_factN: string val dynamic_fact: string -> T + val literal_factN: string val literal_fact: string -> T val method_modifierN: string val tfreeN: string val tfree: T val tvarN: string val tvar: T @@ -343,7 +344,9 @@ val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; -fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]); +fun entity kind name = + (entityN, + (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); fun get_entity_kind (name, props) = if name = entityN then AList.lookup (op =) props kindN @@ -441,6 +444,7 @@ val (fixedN, fixed) = markup_string "fixed" nameN; val (caseN, case_) = markup_string "case" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; +val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; val method_modifierN = "method_modifier"; diff -r 054a92af0f2b -r ae9330fdbc16 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Jun 21 11:03:24 2016 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Jun 21 14:42:47 2016 +0200 @@ -95,10 +95,9 @@ def unapply(markup: Markup): Option[(String, String)] = markup match { case Markup(ENTITY, props) => - (props, props) match { - case (Kind(kind), Name(name)) => Some((kind, name)) - case _ => None - } + val kind = Kind.unapply(props).getOrElse("") + val name = Name.unapply(props).getOrElse("") + Some((kind, name)) case _ => None } } diff -r 054a92af0f2b -r ae9330fdbc16 src/Pure/facts.ML --- a/src/Pure/facts.ML Tue Jun 21 11:03:24 2016 +0200 +++ b/src/Pure/facts.ML Tue Jun 21 14:42:47 2016 +0200 @@ -36,8 +36,8 @@ val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: bool -> T list -> T -> (string * thm list) list val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list - val props: T -> thm list - val could_unify: T -> term -> thm list + val props: T -> (thm * Position.T) list + val could_unify: T -> term -> (thm * Position.T) list val merge: T * T -> T val add_static: Context.generic -> {strict: bool, index: bool} -> binding * thm list -> T -> string * T @@ -134,7 +134,7 @@ datatype T = Facts of {facts: fact Name_Space.table, - props: thm Net.net}; + props: (thm * Position.T) Net.net}; fun make_facts facts props = Facts {facts = facts, props = props}; @@ -227,7 +227,7 @@ (* indexed props *) -val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of; +val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst); fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); fun could_unify (Facts {props, ...}) = Net.unify_term props; @@ -250,11 +250,13 @@ fun add_static context {strict, index} (b, ths) (Facts {facts, props}) = let val ths' = map Thm.trim_context ths; + val pos = #2 (Position.default (Binding.pos_of b)); + val (name, facts') = if Binding.is_empty b then ("", facts) else Name_Space.define context strict (b, Static ths') facts; val props' = props - |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths'; + |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths'; in (name, make_facts facts' props') end; diff -r 054a92af0f2b -r ae9330fdbc16 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Jun 21 11:03:24 2016 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Tue Jun 21 14:42:47 2016 +0200 @@ -604,6 +604,7 @@ val kind1 = Word.implode(Word.explode('_', kind)) val txt1 = if (name == "") kind1 + else if (kind1 == "") quote(name) else kind1 + " " + quote(name) val t = prev.info._1 val txt2 =