(*  Title:      Pure/Tools/invoke.ML

     ID:         $Id$

     Author:     Makarius

 Schematic invocation of locale expression in proof context.

 *)

 signature INVOKE =

 sig

   val invoke: string * Attrib.src list -> Locale.expr -> string option list ->

     (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state

   val invoke_i: string * attribute list -> Locale.expr -> term option list ->

     (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state

 end;

 structure Invoke: INVOKE =

 struct

 (* invoke *)

 local

 fun gen_invoke prep_att prep_expr parse_term add_fixes

     (prfx, raw_atts) raw_expr raw_insts fixes int state =

   let

     val thy = Proof.theory_of state;

     val _ = Proof.assert_forward_or_chain state;

     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];

     val more_atts = map (prep_att thy) raw_atts;

     val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);

     val prems = maps Element.prems_of elems;

     val params = maps Element.params_of elems;

     val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));

     val prems' = map Logic.varify prems;

     val params' = map (Logic.varify o Free) params;

     val types' = map (Logic.varifyT o TFree) types;

     val state' = state

       |> Proof.enter_forward

       |> Proof.begin_block

       |> Proof.map_context (snd o add_fixes fixes);

     val ctxt' = Proof.context_of state';

     val raw_insts' = zip_options params' raw_insts

       handle Library.UnequalLengths => error "Too many instantiations";

     fun prep_inst (t, u) =

       TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);

     val insts = map #1 raw_insts' ~~

       Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));

     val inst_rules =

       replicate (length types') Drule.termI @

       map (fn t =>

         (case AList.lookup (op =) insts t of

           SOME u => Drule.mk_term (Thm.cterm_of thy u)

         | NONE => Drule.termI)) params';

     val propp =

       [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),

        (("", []), map (rpair [] o Logic.mk_term) params'),

        (("", []), map (rpair [] o Element.mark_witness) prems')];

     fun after_qed results =

       Proof.end_block #>

       Proof.map_context (fn ctxt =>

         let

           val ([res_types, res_params, res_prems], ctxt'') =

             fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';

           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;

           val params'' = map (Thm.term_of o Drule.dest_term) res_params;

           val inst = Element.morph_ctxt (Element.inst_morphism thy

             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));

           val elems' = map inst elems;

           val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;

           val notes =

             maps (Element.facts_of thy) elems'

             |> Element.satisfy_facts prems''

             |> Element.generalize_facts ctxt'' ctxt

             |> Attrib.map_facts (Attrib.attribute_i thy)

             |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));

         in

           ctxt

           |> ProofContext.sticky_prefix prfx

           |> ProofContext.qualified_names

           |> (snd o ProofContext.note_thmss_i "" notes)

           |> ProofContext.restore_naming ctxt

         end) #>

       Proof.put_facts NONE #> Seq.single;

   in

     state'

     |> Proof.chain_facts chain_facts

     |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i

       "invoke" NONE after_qed propp

     |> Element.refine_witness

     |> Seq.hd

     |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),

       Position.none))

     |> Seq.hd

   end;

 in

 fun invoke x =

   gen_invoke Attrib.attribute Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;

 fun invoke_i x = gen_invoke (K I) Locale.cert_expr (K I) ProofContext.add_fixes_i x;

 end;

 (* concrete syntax *)

 local structure P = OuterParse and K = OuterKeyword in

 val _ =

   OuterSyntax.command "invoke"

     "schematic invocation of locale expression in proof context"

     (K.tag_proof K.prf_goal)

     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes

       >> (fn (((name, expr), (insts, _)), fixes) =>

           Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));

 end;

 end;