position information for literal facts;
authorwenzelm
Tue Jun 21 14:42:47 2016 +0200 (2016-06-21)
changeset 63337ae9330fdbc16
parent 63336 054a92af0f2b
child 63338 94c6e3ed0afb
position information for literal facts;
Markup.entry may have empty kind/name;
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/Pure/Isar/proof_context.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/facts.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Tue Jun 21 11:03:24 2016 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Tue Jun 21 14:42:47 2016 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4      val names = map Thm.get_name_hint thms
     1.5      val add_info = if null names then I else suffix (":\n" ^ commas names)
     1.6  
     1.7 -    val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
     1.8 +    val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre)))
     1.9  
    1.10      fun metis ctxt =
    1.11        Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Jun 21 11:03:24 2016 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Jun 21 14:42:47 2016 +0200
     2.3 @@ -468,6 +468,7 @@
     2.4      val named_locals = Facts.dest_static true [global_facts] local_facts
     2.5      val unnamed_locals =
     2.6        Facts.props local_facts
     2.7 +      |> map #1
     2.8        |> filter (is_useful_unnamed_local_fact ctxt)
     2.9        |> map (pair "" o single)
    2.10  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jun 21 11:03:24 2016 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jun 21 14:42:47 2016 +0200
     3.3 @@ -945,15 +945,18 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
     3.8 -
     3.9  fun potential_facts ctxt prop =
    3.10    let
    3.11      val body = Term.strip_all_body prop;
    3.12 -    val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts;
    3.13 +    val vacuous =
    3.14 +      filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts
    3.15 +      |> map (rpair Position.none);
    3.16    in Facts.could_unify (facts_of ctxt) body @ vacuous end;
    3.17  
    3.18 -fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
    3.19 +fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
    3.20 +
    3.21 +fun some_fact_tac ctxt =
    3.22 +  SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i);
    3.23  
    3.24  end;
    3.25  
    3.26 @@ -993,18 +996,23 @@
    3.27          val prop =
    3.28            Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
    3.29            |> singleton (Variable.polymorphic ctxt);
    3.30 -        fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
    3.31 +        fun err ps msg =
    3.32 +          error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop);
    3.33  
    3.34          val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
    3.35 -        fun prove_fact th =
    3.36 -          Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
    3.37 -        val results = map_filter (try prove_fact) (potential_facts ctxt prop');
    3.38 -        val thm =
    3.39 -          (case distinct Thm.eq_thm_prop results of
    3.40 -            [thm] => thm
    3.41 -          | [] => err "Failed to retrieve literal fact"
    3.42 -          | _ => err "Ambiguous specification of literal fact");
    3.43 -      in pick true ("", Position.none) [thm] end
    3.44 +        fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
    3.45 +        val results = map_filter (try (apfst prove)) (potential_facts ctxt prop');
    3.46 +        val (thm, thm_pos) =
    3.47 +          (case distinct (eq_fst Thm.eq_thm_prop) results of
    3.48 +            [res] => res
    3.49 +          | [] => err [] "Failed to retrieve literal fact"
    3.50 +          | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
    3.51 +
    3.52 +        val markup =
    3.53 +          (Markup.entity Markup.literal_factN "")
    3.54 +          |> Markup.properties (Position.def_properties_of thm_pos);
    3.55 +        val _ = Context_Position.report_generic context pos markup;
    3.56 +      in pick true ("", thm_pos) [thm] end
    3.57    | retrieve pick context (Facts.Named ((xname, pos), sel)) =
    3.58        let
    3.59          val thy = Context.theory_of context;
    3.60 @@ -1450,7 +1458,7 @@
    3.61  fun pretty_local_facts verbose ctxt =
    3.62    let
    3.63      val facts = facts_of ctxt;
    3.64 -    val props = Facts.props facts;
    3.65 +    val props = map #1 (Facts.props facts);
    3.66      val local_facts =
    3.67        (if null props then [] else [("<unnamed>", props)]) @
    3.68        Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
     4.1 --- a/src/Pure/PIDE/markup.ML	Tue Jun 21 11:03:24 2016 +0200
     4.2 +++ b/src/Pure/PIDE/markup.ML	Tue Jun 21 14:42:47 2016 +0200
     4.3 @@ -86,6 +86,7 @@
     4.4    val fixedN: string val fixed: string -> T
     4.5    val caseN: string val case_: string -> T
     4.6    val dynamic_factN: string val dynamic_fact: string -> T
     4.7 +  val literal_factN: string val literal_fact: string -> T
     4.8    val method_modifierN: string
     4.9    val tfreeN: string val tfree: T
    4.10    val tvarN: string val tvar: T
    4.11 @@ -343,7 +344,9 @@
    4.12  val (bindingN, binding) = markup_elem "binding";
    4.13  
    4.14  val entityN = "entity";
    4.15 -fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
    4.16 +fun entity kind name =
    4.17 +  (entityN,
    4.18 +    (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
    4.19  
    4.20  fun get_entity_kind (name, props) =
    4.21    if name = entityN then AList.lookup (op =) props kindN
    4.22 @@ -441,6 +444,7 @@
    4.23  val (fixedN, fixed) = markup_string "fixed" nameN;
    4.24  val (caseN, case_) = markup_string "case" nameN;
    4.25  val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    4.26 +val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
    4.27  
    4.28  val method_modifierN = "method_modifier";
    4.29  
     5.1 --- a/src/Pure/PIDE/markup.scala	Tue Jun 21 11:03:24 2016 +0200
     5.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jun 21 14:42:47 2016 +0200
     5.3 @@ -95,10 +95,9 @@
     5.4      def unapply(markup: Markup): Option[(String, String)] =
     5.5        markup match {
     5.6          case Markup(ENTITY, props) =>
     5.7 -          (props, props) match {
     5.8 -            case (Kind(kind), Name(name)) => Some((kind, name))
     5.9 -            case _ => None
    5.10 -          }
    5.11 +          val kind = Kind.unapply(props).getOrElse("")
    5.12 +          val name = Name.unapply(props).getOrElse("")
    5.13 +          Some((kind, name))
    5.14          case _ => None
    5.15        }
    5.16    }
     6.1 --- a/src/Pure/facts.ML	Tue Jun 21 11:03:24 2016 +0200
     6.2 +++ b/src/Pure/facts.ML	Tue Jun 21 14:42:47 2016 +0200
     6.3 @@ -36,8 +36,8 @@
     6.4    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
     6.5    val dest_static: bool -> T list -> T -> (string * thm list) list
     6.6    val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
     6.7 -  val props: T -> thm list
     6.8 -  val could_unify: T -> term -> thm list
     6.9 +  val props: T -> (thm * Position.T) list
    6.10 +  val could_unify: T -> term -> (thm * Position.T) list
    6.11    val merge: T * T -> T
    6.12    val add_static: Context.generic -> {strict: bool, index: bool} ->
    6.13      binding * thm list -> T -> string * T
    6.14 @@ -134,7 +134,7 @@
    6.15  
    6.16  datatype T = Facts of
    6.17   {facts: fact Name_Space.table,
    6.18 -  props: thm Net.net};
    6.19 +  props: (thm * Position.T) Net.net};
    6.20  
    6.21  fun make_facts facts props = Facts {facts = facts, props = props};
    6.22  
    6.23 @@ -227,7 +227,7 @@
    6.24  
    6.25  (* indexed props *)
    6.26  
    6.27 -val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
    6.28 +val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
    6.29  
    6.30  fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
    6.31  fun could_unify (Facts {props, ...}) = Net.unify_term props;
    6.32 @@ -250,11 +250,13 @@
    6.33  fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
    6.34    let
    6.35      val ths' = map Thm.trim_context ths;
    6.36 +    val pos = #2 (Position.default (Binding.pos_of b));
    6.37 +
    6.38      val (name, facts') =
    6.39        if Binding.is_empty b then ("", facts)
    6.40        else Name_Space.define context strict (b, Static ths') facts;
    6.41      val props' = props
    6.42 -      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths';
    6.43 +      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
    6.44    in (name, make_facts facts' props') end;
    6.45  
    6.46  
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 11:03:24 2016 +0200
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 14:42:47 2016 +0200
     7.3 @@ -604,6 +604,7 @@
     7.4              val kind1 = Word.implode(Word.explode('_', kind))
     7.5              val txt1 =
     7.6                if (name == "") kind1
     7.7 +              else if (kind1 == "") quote(name)
     7.8                else kind1 + " " + quote(name)
     7.9              val t = prev.info._1
    7.10              val txt2 =