Walther@60610: signature SUB_PROBLEM =
Walther@60610: sig
Walther@60610:   val tac_from_prog: Ctree.state -> term -> Tactic.input * Tactic.T
Walther@60610:   val common_sub_thy: theory * theory -> theory
Walther@60610: end
Walther@60610: 
Walther@60610: (**)
Walther@60610: structure Sub_Problem(**): SUB_PROBLEM(**) =
Walther@60610: struct
Walther@60610: (**)
Walther@60610: 
Walther@60610: fun common_sub_thy (thy1, thy2) =
Walther@60610:   if Context.subthy (thy1, thy2) then thy2
Walther@60610:   else if Context.subthy (thy2, thy1) then thy1
Walther@60610:     else Know_Store.get_ref_last_thy ()
Walther@60610: 
Walther@60742: fun tac_from_prog (pt, _) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
Walther@60610:     let
Walther@60610:       val (dI, pI, mI) = Prog_Tac.dest_spec spec'
Walther@60610:       val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
Walther@60610:       val init_ctxt = Proof_Context.init_global thy
Walther@60610: 	    val ags = TermC.isalist2list ags';
Walther@60610: 	    val (pI, pors, mI) = 
Walther@60610: 	      if mI = ["no_met"]
Walther@60610: 	      then
Walther@60610:           let
Walther@60610:             val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
Walther@60610: 		          handle ERROR "actual args do not match formal args"
Walther@60610: 			          => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
Walther@60742: 		        val pI' = Refine.by_o_model' init_ctxt pors pI;
Walther@60640: 		      in (pI', pors (* refinement over models with diff.precond only *), 
Walther@60610: 		          (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
Walther@60610: 	      else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
Walther@60610: 		      handle ERROR "actual args do not match formal args"
Walther@60610: 		      => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
Walther@60610:       val (fmz_, vals) = O_Model.values' init_ctxt pors;
Walther@60610: 	    val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
Walther@60610: 	    val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
Walther@60610: 	    val dI = Context.theory_name
Walther@60610:         (common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
Walther@60654: 	    val ctxt = ContextC.init_for_prog init_ctxt vals
Walther@60610: 	    val hdl =
Walther@60610:         case cas of
Walther@60610: 		      NONE => Auto_Prog.pblterm dI pI
Walther@60610: 		    | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
Walther@60682:       val f = Auto_Prog.subpbl (ThmC.cut_longid dI) pI
Walther@60610:     in
Walther@60610:       (Tactic.Subproblem (dI, pI),	Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
Walther@60610:     end
Walther@60673:   | tac_from_prog _ t =
Walther@60678:     raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term (ContextC.for_ERROR ()) t)
Walther@60610: 
Walther@60610: (**)end(**)