signature SUB_PROBLEM =

sig

  val tac_from_prog: Ctree.ctree -> term -> Tactic.input * Tactic.T

end

(**)

structure Sub_Problem(**): SUB_PROBLEM(**) =

struct

(**)

fun tac_from_prog pt (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =

    let

      val (dI, pI, mI) = Prog_Tac.dest_spec spec'

      val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);

      val ctxt = Proof_Context.init_global thy (*TODO: use ctxt from pt *)

	    val ags = TermC.isalist2list ags';

	    val (pI, pors, mI) = 

	      if mI = ["no_met"]

	      then

          let

            val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T

		          handle ERROR "actual args do not match formal args"

			          => (M_Match.arguments_msg ctxt pI stac ags (*raise exn*);[]);

		        val pI' = Refine.refine_ori' ctxt pors pI;

		      in (pI', pors (* refinement over models with diff.prec only *), 

		          (hd o #met o Problem.from_store ctxt) pI') end

	      else (pI, (M_Match.arguments thy ((#ppc o Problem.from_store ctxt) pI) ags)

		      handle ERROR "actual args do not match formal args"

		      => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI);

      val (fmz_, vals) = O_Model.values' pors;

	    val {cas, ppc, thy, ...} = Problem.from_store ctxt pI

	    val dI = Context.theory_name thy (*take dI from _refined_ pbl*)

	    val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))

	    val ctxt = ContextC.initialise dI vals

	    val hdl =

        case cas of

		      NONE => Auto_Prog.pblterm dI pI

		    | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ vals) t

      val f = Auto_Prog.subpbl (strip_thy dI) pI

    in

      (Tactic.Subproblem (dI, pI),	Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))

    end

  | tac_from_prog _ t = raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term t)

(**)end(**)