# HG changeset patch # User wneuper # Date 1666177824 -7200 # Node ID dd387c9fa89a6b73cc8e79e0c7c54dab29f27faa # Parent bb3140a02f3d593119b152b61a9925822a4a062e cleanup 1: clarify adapt_to_type for Prog_Tac diff -r bb3140a02f3d -r dd387c9fa89a TODO.md --- a/TODO.md Wed Oct 19 10:43:04 2022 +0200 +++ b/TODO.md Wed Oct 19 13:10:24 2022 +0200 @@ -62,11 +62,11 @@ ***** priority of WN items is top down, most urgent/simple on top -* WN: follow up 5d: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE - follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context} +* WN: follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context} Thus eliminate use of Thy_Info.get_theory follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" +* WN: Sub_Problem.tac_from_prog: use ctxt from pt * WN: improve naming in refine.sml, m-match.sml * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› * WN: review Prog_Tac: diff -r bb3140a02f3d -r dd387c9fa89a src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Wed Oct 19 10:43:04 2022 +0200 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Oct 19 13:10:24 2022 +0200 @@ -73,13 +73,13 @@ | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Inst\, _) $ sub $ thmID $ _) = let val tid = HOLogic.dest_string thmID - val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + val sub' = Subst.program_to_input sub in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Rewrite_Set\,_) $ rls $ _) = (Tactic.Rewrite_Set (HOLogic.dest_string rls)) - | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Set_Inst\, _) $ sub $ rls $ _) = + | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Rewrite_Set_Inst\, _) $ sub $ rls $ _) = let - val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + val sub' = Subst.program_to_input sub in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Calculate\, _) $ op_ $ _) = (Tactic.Calculate (HOLogic.dest_string op_)) diff -r bb3140a02f3d -r dd387c9fa89a src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Wed Oct 19 10:43:04 2022 +0200 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Oct 19 13:10:24 2022 +0200 @@ -222,7 +222,7 @@ val thy = Proof_Context.theory_of ctxt val f = Calc.current_formula cs; val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) - val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*) + val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube val ro = get_rew_ord ctxt rew_ord' in if foldl and_ (true, map TermC.contains_Var subte) diff -r bb3140a02f3d -r dd387c9fa89a src/Tools/isac/Interpret/sub-problem.sml --- a/src/Tools/isac/Interpret/sub-problem.sml Wed Oct 19 10:43:04 2022 +0200 +++ b/src/Tools/isac/Interpret/sub-problem.sml Wed Oct 19 13:10:24 2022 +0200 @@ -12,7 +12,7 @@ let val (dI, pI, mI) = Prog_Tac.dest_spec spec' val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt); - val ctxt = Proof_Context.init_global thy (*OR user_ctxt ?*) + val ctxt = Proof_Context.init_global thy (*TODO: use ctxt from pt *) val ags = TermC.isalist2list ags'; val (pI, pors, mI) = if mI = ["no_met"] diff -r bb3140a02f3d -r dd387c9fa89a src/Tools/isac/ProgLang/Prog_Tac.thy --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 19 10:43:04 2022 +0200 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 19 13:10:24 2022 +0200 @@ -64,9 +64,9 @@ val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option val is: term -> bool - val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs -(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**) -(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**) + val Take_adapt_to_type: Proof.context -> TermC.as_string -> term + val Substitute_adapt_to_type: theory -> Subst.program -> Subst.as_string_eqs + val Substitute_adapt_to_type': Proof.context -> Subst.input -> Subst.as_eqs end \ ML \ (**) @@ -214,29 +214,30 @@ fun is t = TermC.contains_Const_typeless all_Consts t -(** adapt_to_type arguments of specific tactics **) +(** arguments of specific tactics \adapt_to_type\ **) (* Programs are stored as terms typed by the theory they are defined in. - Specific Prog_Tac take substitutions as arguments; these substitutions have - the variables to be substituted typed with the program; - these variables need to be adapt_to_type from the user-context in order to conform - with the terms input by the user. + Thus specific Prog_Tac require \adapt_to_type\ for their arguments at the moment, + where the formal arguments are substituted to actual arguments; + i.e. formal arguments require \adapt_to_type\ for \Calc.T\. + + Remarkably this appears not necessary for \Rewrite_Inst\ and \Rewrite_Set_Inst\. *) -fun Substitute_adapt_to_type thy isasub = +(* TermC.parse ctxt fails with "c_2 = 0" \ \c_2 = (0 :: 'a)\ and thus requires adapt_to_type *) +fun Take_adapt_to_type ctxt arg = arg + |> TermC.parse ctxt + |> Model_Pattern.adapt_term_to_type ctxt + +fun Substitute_adapt_to_type thy isasub = isasub |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) |> TermC.isalist2list |> Subst.eqs_to_input; -fun Rewrite_Inst_adapt_to_type thy sub = - sub -(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*) - |> Subst.program_to_input - -(*eliminated ERROR: c_2 = (0 :: 'a)*) -fun Take_adapt_to_type ctxt arg = arg - |> TermC.parse ctxt - |> Model_Pattern.adapt_term_to_type ctxt +(* TermC.parse ctxt fails with "c_2 = 0" \ \c_2 = (0 :: 'a)\ and thus requires adapt_to_type *) +fun Substitute_adapt_to_type' ctxt strs = strs + |> map (TermC.parse ctxt) + |> map (Model_Pattern.adapt_term_to_type ctxt) (**)end(*struct*) \ ML \