1.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -63,7 +63,11 @@
     1.4    val get_first_argument : term -> term option (*TODO rename get_first_argument*)
     1.5    val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
     1.6    val is: term -> bool
     1.7 -end 
     1.8 +
     1.9 +  val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs
    1.10 +(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)
    1.11 +(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)
    1.12 +end
    1.13  \<close> ML \<open>
    1.14  (**)
    1.15  structure Prog_Tac(**): PROGAM_TACTIC(**) =
    1.16 @@ -208,9 +212,36 @@
    1.17    SubProblem, Substitute, Take, Check_elementwise, Assumptions]
    1.18  
    1.19  fun is t = TermC.contains_Const_typeless all_Consts t
    1.20 -(**)end(**)
    1.21 +
    1.22 +
    1.23 +(** adapt_to_type arguments of specific tactics **)
    1.24 +(*
    1.25 +  Programs are stored as terms typed by the theory they are defined in.
    1.26 +  Specific Prog_Tac take substitutions as arguments; these substitutions have
    1.27 +  the variables to be substituted typed with the program;
    1.28 +  these variables need to be adapt_to_type from the user-context in order to conform
    1.29 +  with the terms input by the user.
    1.30 +*)
    1.31 +fun Substitute_adapt_to_type thy isasub = 
    1.32 +  isasub
    1.33 +  |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
    1.34 +  |> TermC.isalist2list
    1.35 +  |> Subst.eqs_to_input;
    1.36 +
    1.37 +fun Rewrite_Inst_adapt_to_type thy sub =
    1.38 +  sub 
    1.39 +(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)
    1.40 +  |> Subst.program_to_input
    1.41 +
    1.42 +(*eliminated ERROR: c_2 = (0 :: 'a)*)
    1.43 +fun Take_adapt_to_type ctxt arg = arg
    1.44 +  |> TermC.parse ctxt
    1.45 +  |> Model_Pattern.adapt_term_to_type ctxt
    1.46 +
    1.47 +(**)end(*struct*)
    1.48  \<close> ML \<open>
    1.49  \<close> 
    1.50 +
    1.51  subsection \<open>TODO\<close>
    1.52  ML \<open>
    1.53  \<close> ML \<open>