1.1 --- a/TODO.md	Wed Oct 19 10:43:04 2022 +0200
     1.2 +++ b/TODO.md	Wed Oct 19 13:10:24 2022 +0200
     1.3 @@ -62,11 +62,11 @@
     1.4  
     1.5  ***** priority of WN items is top down, most urgent/simple on top
     1.6  
     1.7 -* WN: follow up 5d: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE
     1.8 -      follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
     1.9 +* WN: follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
    1.10                     Thus eliminate use of Thy_Info.get_theory
    1.11        follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__"
    1.12  
    1.13 +* WN: Sub_Problem.tac_from_prog: use ctxt from pt
    1.14  * WN: improve naming in refine.sml, m-match.sml
    1.15  * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
    1.16  * WN: review Prog_Tac:

     2.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Wed Oct 19 10:43:04 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Oct 19 13:10:24 2022 +0200
     2.3 @@ -73,13 +73,13 @@
     2.4    | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
     2.5      let
     2.6        val tid = HOLogic.dest_string thmID
     2.7 -      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
     2.8 +      val sub' = Subst.program_to_input sub
     2.9      in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
    2.10    | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
    2.11       (Tactic.Rewrite_Set (HOLogic.dest_string rls))
    2.12 -  | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
    2.13 +  | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
    2.14      let
    2.15 -      val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
    2.16 +      val sub' =  Subst.program_to_input sub
    2.17      in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
    2.18    | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
    2.19        (Tactic.Calculate (HOLogic.dest_string op_))

     3.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Oct 19 10:43:04 2022 +0200
     3.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Oct 19 13:10:24 2022 +0200
     3.3 @@ -222,7 +222,7 @@
     3.4          val thy = Proof_Context.theory_of ctxt
     3.5          val f = Calc.current_formula cs;
     3.6  		    val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
     3.7 -		    val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)
     3.8 +		    val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube
     3.9  		    val ro = get_rew_ord ctxt rew_ord'
    3.10  		  in
    3.11  		    if foldl and_ (true, map TermC.contains_Var subte)

     4.1 --- a/src/Tools/isac/Interpret/sub-problem.sml	Wed Oct 19 10:43:04 2022 +0200
     4.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml	Wed Oct 19 13:10:24 2022 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4      let
     4.5        val (dI, pI, mI) = Prog_Tac.dest_spec spec'
     4.6        val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);
     4.7 -      val ctxt = Proof_Context.init_global thy (*OR user_ctxt ?*)
     4.8 +      val ctxt = Proof_Context.init_global thy (*TODO: use ctxt from pt *)
     4.9  	    val ags = TermC.isalist2list ags';
    4.10  	    val (pI, pors, mI) = 
    4.11  	      if mI = ["no_met"]

     5.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Wed Oct 19 10:43:04 2022 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Wed Oct 19 13:10:24 2022 +0200
     5.3 @@ -64,9 +64,9 @@
     5.4    val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
     5.5    val is: term -> bool
     5.6  
     5.7 -  val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs
     5.8 -(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)
     5.9 -(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)
    5.10 +  val Take_adapt_to_type: Proof.context -> TermC.as_string -> term
    5.11 +  val Substitute_adapt_to_type: theory -> Subst.program -> Subst.as_string_eqs
    5.12 +  val Substitute_adapt_to_type': Proof.context -> Subst.input -> Subst.as_eqs
    5.13  end
    5.14  \<close> ML \<open>
    5.15  (**)
    5.16 @@ -214,29 +214,30 @@
    5.17  fun is t = TermC.contains_Const_typeless all_Consts t
    5.18  
    5.19  
    5.20 -(** adapt_to_type arguments of specific tactics **)
    5.21 +(** arguments of specific tactics \<open>adapt_to_type\<close> **)
    5.22  (*
    5.23    Programs are stored as terms typed by the theory they are defined in.
    5.24 -  Specific Prog_Tac take substitutions as arguments; these substitutions have
    5.25 -  the variables to be substituted typed with the program;
    5.26 -  these variables need to be adapt_to_type from the user-context in order to conform
    5.27 -  with the terms input by the user.
    5.28 +  Thus specific Prog_Tac require \<open>adapt_to_type\<close> for their arguments at the moment,
    5.29 +  where the formal arguments are substituted to actual arguments;
    5.30 +  i.e. formal arguments require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>.
    5.31 +
    5.32 +  Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>.
    5.33  *)
    5.34 -fun Substitute_adapt_to_type thy isasub = 
    5.35 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    5.36 +fun Take_adapt_to_type ctxt arg = arg
    5.37 +  |> TermC.parse ctxt
    5.38 +  |> Model_Pattern.adapt_term_to_type ctxt
    5.39 +
    5.40 +fun Substitute_adapt_to_type thy isasub =
    5.41    isasub
    5.42    |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
    5.43    |> TermC.isalist2list
    5.44    |> Subst.eqs_to_input;
    5.45  
    5.46 -fun Rewrite_Inst_adapt_to_type thy sub =
    5.47 -  sub 
    5.48 -(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)
    5.49 -  |> Subst.program_to_input
    5.50 -
    5.51 -(*eliminated ERROR: c_2 = (0 :: 'a)*)
    5.52 -fun Take_adapt_to_type ctxt arg = arg
    5.53 -  |> TermC.parse ctxt
    5.54 -  |> Model_Pattern.adapt_term_to_type ctxt
    5.55 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    5.56 +fun Substitute_adapt_to_type' ctxt strs = strs
    5.57 +  |> map (TermC.parse ctxt)
    5.58 +  |> map (Model_Pattern.adapt_term_to_type ctxt)
    5.59  
    5.60  (**)end(*struct*)
    5.61  \<close> ML \<open>