1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
     1.5  
     1.6  \<^isac_test>\<open>
     1.7 +  val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context
     1.8    val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
     1.9  \<close>
    1.10  end
    1.11 @@ -84,6 +85,31 @@
    1.12  		  end
    1.13    end;
    1.14  
    1.15 +(** get context reliably at switch_specify_solve **)
    1.16 +
    1.17 +fun at_begin_program (is, Pos.Res) = last_elem is = 0
    1.18 +  | at_begin_program _ = false;
    1.19 +
    1.20 +(* strange special case at Apply_Method *)
    1.21 +fun get_ctxt_from_PblObj pt (p_, Pos.Res) =
    1.22 +    let
    1.23 +      val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
    1.24 +      val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
    1.25 +    in ctxt end
    1.26 +  | get_ctxt_from_PblObj _ _ = raise ERROR "get_ctxt_from_PblObj called by PrfObj or EmptyPtree";
    1.27 +
    1.28 +fun get_ctxt pt (p_, Pos.Pbl) =
    1.29 +    let
    1.30 +      val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
    1.31 +      val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
    1.32 +    in ctxt end
    1.33 +  | get_ctxt pt pos =
    1.34 +    if at_begin_program pos
    1.35 +    then get_ctxt_from_PblObj pt pos
    1.36 +    else Ctree.get_ctxt pt pos
    1.37 +
    1.38 +
    1.39 +
    1.40  (** Solve_Step.check **)
    1.41  
    1.42  (*
    1.43 @@ -94,7 +120,7 @@
    1.44        let
    1.45          val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
    1.46            Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
    1.47 -        | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
    1.48 +        | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
    1.49          val {where_, ...} = Problem.from_store ctxt pI
    1.50          val pres = map (I_Model.environment probl |> subst_atomic) where_
    1.51          val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
    1.52 @@ -196,7 +222,7 @@
    1.53          val thy = Proof_Context.theory_of ctxt
    1.54          val f = Calc.current_formula cs;
    1.55  		    val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
    1.56 -		    val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
    1.57 +		    val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)
    1.58  		    val ro = get_rew_ord ctxt rew_ord'
    1.59  		  in
    1.60  		    if foldl and_ (true, map TermC.contains_Var subte)
    1.61 @@ -218,7 +244,17 @@
    1.62        in
    1.63          Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
    1.64        end
    1.65 -  | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
    1.66 +(*/----------------- updated----------------------------------* )
    1.67 +  | check (Tactic.Take str) (pt, pos) =
    1.68 +      Applicable.Yes (Tactic.Take'
    1.69 +        (TermC.parse ((*Solve_Step.*)get_ctxt pt pos) str)) (*always applicable*)
    1.70 +( *------------------- updated----------------------------------*)
    1.71 +  | check (Tactic.Take str) (pt, pos) =
    1.72 +    let
    1.73 +      val ctxt = (*Solve_Step.*)get_ctxt pt pos
    1.74 +      val t = Prog_Tac.Take_adapt_to_type ctxt str
    1.75 +    in Applicable.Yes (Tactic.Take' t) end
    1.76 +(*\----------------- updated----------------------------------*)
    1.77    | check (Tactic.Begin_Trans) cs =
    1.78        Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
    1.79    | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
    1.80 @@ -327,9 +363,11 @@
    1.81            Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
    1.82          in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) 
    1.83          end
    1.84 -  | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
    1.85 +  | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
    1.86        let
    1.87 -        val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
    1.88 +        val ctxt = Ctree.get_ctxt pt pos
    1.89 +        val (pt, c) = Ctree.cappend_atomic pt p l
    1.90 +          (TermC.parse ctxt f) (Tactic.Tac id) (TermC.parse ctxt f', []) Ctree.Complete
    1.91        in
    1.92          ((p,Pos.Res), c, Test_Out.FormKF f', pt)
    1.93        end