src/Pure/Tools/invoke.ML
author wenzelm
Tue Nov 21 18:07:37 2006 +0100 (2006-11-21)
changeset 21440 807a39221a58
parent 20893 c99f79910ae8
child 21483 e4be91feca50
permissions -rw-r--r--
notes: proper kind;
     1 (*  Title:      Pure/Tools/invoke.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Schematic invocation of locale expression in proof context.
     6 *)
     7 
     8 signature INVOKE =
     9 sig
    10   val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
    11     (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    12   val invoke_i: string * attribute list -> Locale.expr -> term option list ->
    13     (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    14 end;
    15 
    16 structure Invoke: INVOKE =
    17 struct
    18 
    19 
    20 (* invoke *)
    21 
    22 local
    23 
    24 fun gen_invoke prep_att prep_expr prep_terms add_fixes
    25     (prfx, raw_atts) raw_expr raw_insts fixes int state =
    26   let
    27     val _ = Proof.assert_forward_or_chain state;
    28     val thy = Proof.theory_of state;
    29 
    30     val more_atts = map (prep_att thy) raw_atts;
    31     val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
    32 
    33     val prems = maps Element.prems_of elems;
    34     val params = maps Element.params_of elems;
    35     val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
    36 
    37     val prems' = map Logic.varify prems;
    38     val params' = map (Logic.varify o Free) params;
    39     val types' = map (Logic.varifyT o TFree) types;
    40 
    41     val state' = state
    42       |> Proof.begin_block
    43       |> Proof.map_context (snd o add_fixes fixes);
    44     val ctxt' = Proof.context_of state';
    45 
    46     val raw_insts' = zip_options params' raw_insts
    47       handle Library.UnequalLengths => error "Too many instantiations";
    48     val insts = map #1 raw_insts' ~~
    49       prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts');
    50     val inst_rules =
    51       replicate (length types') Drule.termI @
    52       map (fn t =>
    53         (case AList.lookup (op =) insts t of
    54           SOME u => Drule.mk_term (Thm.cterm_of thy u)
    55         | NONE => Drule.termI)) params';
    56 
    57     val propp =
    58       [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
    59        (("", []), map (rpair [] o Logic.mk_term) params'),
    60        (("", []), map (rpair [] o Element.mark_witness) prems')];
    61     fun after_qed results =
    62       Proof.end_block #>
    63       Proof.map_context (fn ctxt =>
    64         let
    65           val ([res_types, res_params, res_prems], ctxt'') =
    66             fold_burrow (apfst snd oo Variable.import false) results ctxt';
    67 
    68           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
    69           val params'' = map (Thm.term_of o Drule.dest_term) res_params;
    70           val elems' = elems |> map (Element.inst_ctxt thy
    71             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
    72           val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
    73           val notes =
    74             maps (Element.facts_of thy) elems'
    75             |> Element.satisfy_facts prems''
    76             |> Element.export_facts ctxt'' ctxt
    77             |> Attrib.map_facts (Attrib.attribute_i thy)
    78             |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
    79         in
    80           ctxt
    81           |> ProofContext.sticky_prefix prfx
    82           |> ProofContext.qualified_names
    83           |> (snd o ProofContext.note_thmss_i "" notes)
    84           |> ProofContext.restore_naming ctxt
    85         end) #>
    86       Proof.put_facts NONE #> Seq.single;
    87   in
    88     state'
    89     |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
    90       "invoke" NONE after_qed propp
    91     |> Element.refine_witness
    92     |> Seq.hd
    93     |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules)))))))
    94     |> Seq.hd
    95   end;
    96 
    97 (* FIXME *)
    98 fun read_terms ctxt args =
    99   #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args)
   100   |> Variable.polymorphic ctxt;
   101 
   102 (* FIXME *)
   103 fun cert_terms ctxt args = map fst args;
   104 
   105 in
   106 
   107 fun invoke x = gen_invoke Attrib.attribute Locale.read_expr read_terms ProofContext.add_fixes x;
   108 fun invoke_i x = gen_invoke (K I) Locale.cert_expr cert_terms ProofContext.add_fixes_i x;
   109 
   110 end;
   111 
   112 
   113 (* concrete syntax *)
   114 
   115 local structure P = OuterParse and K = OuterKeyword in
   116 
   117 val invokeP =
   118   OuterSyntax.command "invoke"
   119     "schematic invocation of locale expression in proof context"
   120     (K.tag_proof K.prf_goal)
   121     (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes
   122       >> (fn (((name, expr), insts), fixes) =>
   123           Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
   124 
   125 val _ = OuterSyntax.add_parsers [invokeP];
   126 
   127 end;
   128 
   129 end;