1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 17:39:04 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 09:25:51 2020 +0200
     1.3 @@ -9,6 +9,10 @@
     1.4  sig
     1.5    val check: Tactic.input -> Calc.T -> Applicable.T
     1.6    val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
     1.7 +  val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
     1.8 +  val s_add_general: State_Steps.T ->
     1.9 +    Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
    1.10 +
    1.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.12    (*NONE*)                                                     
    1.13  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.14 @@ -25,7 +29,20 @@
    1.15    check tactics (input by the user, mostly) for applicability
    1.16    and determine as much of the result of the tactic as possible initially.
    1.17  *)
    1.18 -fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
    1.19 +fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
    1.20 +      let
    1.21 +        val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
    1.22 +          Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
    1.23 +        | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
    1.24 +        val {where_, ...} = Specify.get_pbt pI
    1.25 +        val pres = map (Model.mk_env probl |> subst_atomic) where_
    1.26 +        val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
    1.27 +          then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
    1.28 +          else ctxt
    1.29 +      in
    1.30 +        Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
    1.31 +      end
    1.32 +  | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
    1.33        let 
    1.34          val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
    1.35          val f = Calc.current_formula cs;
    1.36 @@ -163,7 +180,13 @@
    1.37    | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
    1.38    | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
    1.39  
    1.40 -fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
    1.41 +fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) = 
    1.42 +    (case topt of 
    1.43 +      SOME t => 
    1.44 +        let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
    1.45 +        in (pos, c, Generate.EmptyMout, pt) end
    1.46 +    | NONE => (pos, [], Generate.EmptyMout, pt))
    1.47 +  | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
    1.48      let
    1.49        val p =
    1.50          let val (ps, p') = split_last p (* no connex to prev.ppobj *)
    1.51 @@ -261,13 +284,31 @@
    1.52        end
    1.53    | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
    1.54        (l as (_, ctxt)) (pt, (p, _)) =
    1.55 +      let
    1.56 +  	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
    1.57 +  	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
    1.58 +  	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
    1.59 +      in
    1.60 +        ((p, Pos.Pbl), c, Generate.FormKF f, pt)
    1.61 +      end
    1.62 +  | add m' _ (_, pos) =
    1.63 +      raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
    1.64 +
    1.65 +(* LI switches between solve-phase and specify-phase *)
    1.66 +fun add_general tac ic cs =
    1.67 +  if Tactic.for_specify' tac
    1.68 +  then Generate.generate1 tac ic cs
    1.69 +  else add tac ic cs
    1.70 +
    1.71 +(* tacis are in reverse order from do_next/specify_: last = fst to insert *)
    1.72 +fun s_add_general [] ptp = ptp
    1.73 +  | s_add_general tacis (pt, c, _) = 
    1.74      let
    1.75 -	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
    1.76 -	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
    1.77 -	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
    1.78 +      val (tacis', (_, tac_, (p, is))) = split_last tacis
    1.79 +	    val (p',c',_,pt') = add_general tac_ is (pt, p)
    1.80      in
    1.81 -      ((p, Pos.Pbl), c, Generate.FormKF f, pt)
    1.82 +      s_add_general tacis' (pt', c@c', p')
    1.83      end
    1.84 -  | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m')
    1.85 +
    1.86  
    1.87  (**)end(**);