theory Thm_inst
imports Term_pat
begin

section {* Monad for theorem instantiation based on bindings in proof contexts *}

subsection {* Implementation *}

ML {*
local
fun read_termTs ctxt schematic ts Ts =
  let
    val ts' =
      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
      |> Variable.polymorphic ctxt;
    val Ts' = map Term.fastype_of ts';
    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;

fun make_inst f v =
  let
    val t = Var v;
    val t' = f t;
  in if t aconv t' then NONE else SOME (t, t') end;


fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));

fun the_type vars (xi: indexname) =
  (case AList.lookup (op =) vars xi of
    SOME T => T
  | NONE => error_var "No such variable in theorem: " xi);

fun instantiate inst =
  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
  Envir.beta_norm;

fun make_instT f v =
  let
    val T = TVar v;
    val T' = f T;
  in if T = T' then NONE else SOME (T, T') end;

fun read_insts ctxt term_insts (tvars, vars) =
  let
    val thy = Proof_Context.theory_of ctxt;
    val cert = Thm.cterm_of thy;
    val certT = Thm.ctyp_of thy;


    (* type instantiations *)

    val instT1 = Term_Subst.instantiateT [];
    val vars1 = map (apsnd instT1) vars;


    (* term instantiations *)

    val (xs, ts) = split_list term_insts;
    val Ts = map (the_type vars1) xs;
    val (ts, inferred) = read_termTs ctxt false ts Ts;

    val instT2 = Term.typ_subst_TVars inferred;
    val vars2 = map (apsnd instT2) vars1;
    val inst2 = instantiate (xs ~~ ts);


    (* result *)

    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
    val inst_vars = map_filter (make_inst inst2) vars2;
  in
    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
  end

  val add_used =
  (Thm.fold_terms o fold_types o fold_atyps)
    (fn TFree (a, _) => insert (op =) a
      | TVar ((a, _), _) => insert (op =) a
      | _ => I)

fun term_instantiate ctxt term_insts thm =
  let
    val ctxt' = ctxt
      |> Variable.declare_thm thm
      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); 
                 (* FIXME !? *)
    val tvars = Thm.fold_terms Term.add_tvars thm [];
    val vars = Thm.fold_terms Term.add_vars thm [];
    val insts = read_insts ctxt' term_insts (tvars, vars);
  in
    Drule.instantiate_normalize insts thm
    |> Rule_Cases.save thm
  end

in
  fun ctxt_instantiate ctxt thm = let
     val binds = Variable.binds_of ctxt
     val vars = Thm.fold_terms Term.add_vars thm [] |> map fst
     val inst = map_filter ( Vartab.lookup_key binds) vars |> map (apsnd snd)
     val thm' = term_instantiate ctxt inst thm 
  in thm' end

  fun thm_instM thm = 
   liftM (lift (m0M (fn ctxt =>
    returnM (ctxt_instantiate ctxt thm)
   )) |> exnM err_trans)

end
*}

subsection {* Examples *}

lemma h: "x = x \<and> y = y"
  by simp

ML {*
  val ctxt = @{context}
  val t = ctxt_instantiate ctxt @{thm h} |> prop_of
*}

ML {*
  val t =   [((), @{context})] |> @{match "?x"} @{term "[]::nat list"} |--
                                  @{match "?y"} @{term "1::nat"} |--
                                  thm_instM @{thm h}
*}
 
end