1.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Thu Oct 20 12:12:18 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Fri Oct 21 15:19:00 2022 +0200
1.3 @@ -14,18 +14,17 @@
1.4 type T = LibraryC.subst;
1.5 val to_string: T -> string
1.6
1.7 - type as_eqs = term list (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)
1.8 + type as_eqs = term list (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)
1.9 type program = term (* in programs: @{term "[(''bdv_1'', x::real), ..]} *)
1.10 - type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
1.11 + type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
1.12 val input_empty: input
1.13
1.14 - type as_string_eqs (* for Tactic.Substitute ["bdv_1 = x", ...] *)
1.15 + type as_string_eqs (* for Tactic.Substitute ["bdv_1 = x", ...] *)
1.16 val string_eqs_to_string: as_string_eqs -> string
1.17
1.18 val T_to_string_eqs: T -> as_string_eqs
1.19 val T_to_input: T -> input
1.20 val T_from_string_eqs: theory -> as_string_eqs -> T
1.21 - val T_from_input: Proof.context -> input -> T
1.22
1.23 val eqs_to_input: as_eqs -> as_string_eqs
1.24 val program_to_input: program -> input
1.25 @@ -68,14 +67,6 @@
1.26 handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, [])
1.27
1.28 fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
1.29 -(*TODO: input requires parse _: _ -> _ option*)
1.30 -fun T_from_input ctxt input = (input
1.31 - |> map (TermC.parse_patt (Proof_Context.theory_of ctxt))
1.32 - |> map TermC.isapair2pair
1.33 - |> map (apfst HOLogic.dest_string)
1.34 - |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
1.35 - handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
1.36 -
1.37 val eqs_to_input = map UnparseC.term;
1.38
1.39 fun program_to_input sub = (sub
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Thu Oct 20 12:12:18 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Fri Oct 21 15:19:00 2022 +0200
2.3 @@ -75,9 +75,7 @@
2.4 val parseNEW: Proof.context -> string -> term option(*old version to be eliminated*)
2.5 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*)
2.6 val parseNEW'': theory -> string -> term (*old version to be eliminated*)
2.7 - val parse_strict: theory -> string -> term (*to be 1.replaced by parse_patt*)
2.8 (*goal*)val parse: Proof.context -> string -> term
2.9 - val parse_patt_PIDE: theory -> string -> term (*rename to parse_patt*)
2.10 (*goal*)val parse_patt: theory -> string -> term (*with typ_a2real still for tests *)
2.11 (*for test/* *)
2.12 (*goal*)val parse_test: Proof.context -> string -> term
2.13 @@ -562,17 +560,12 @@
2.14 (*\----- old versions to be eliminated -------------------------------------------------------/*)
2.15
2.16 (* to be replaced by parse..*)
2.17 -fun parse_strict thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
2.18 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
2.19 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
2.20 (*rename to parse_patt..*)
2.21 -fun parse_patt_PIDE thy str = (thy, str)
2.22 - |>> Proof_Context.init_global
2.23 - |-> Proof_Context.read_term_pattern
2.24 fun parse_patt thy str = (thy, str)
2.25 |>> Proof_Context.init_global
2.26 |-> Proof_Context.read_term_pattern
2.27 -(**)|> typ_a2real; (** )TODO drop*)
2.28
2.29 (** parse in test/* **)
2.30 (*
3.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Oct 20 12:12:18 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Oct 21 15:19:00 2022 +0200
3.3 @@ -174,7 +174,7 @@
3.4 XML.Elem (("VALUE", []), [xml_of_term value])])
3.5 fun xml_of_subs (subs : Subst.input) =
3.6 XML.Elem (("SUBSTITUTION", []),
3.7 - map xml_of_sub (Subst.T_from_input (ThyC.id_to_ctxt "Isac_Knowledge") subs))
3.8 + map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs))
3.9 fun xml_of_sube sube =
3.10 XML.Elem (("SUBSTITUTION", []),
3.11 map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
4.1 --- a/src/Tools/isac/Interpret/istate.sml Thu Oct 20 12:12:18 2022 +0200
4.2 +++ b/src/Tools/isac/Interpret/istate.sml Fri Oct 21 15:19:00 2022 +0200
4.3 @@ -179,7 +179,7 @@
4.4 val thy = ThyC.get_theory "Isac_Knowledge"
4.5 val ctxt = Proof_Context.init_global thy
4.6 val rls' = get_rls ctxt rls
4.7 - val v = case Subst.T_from_input ctxt subs of
4.8 + val v = case Tactic.subst_adapt_to_type ctxt subs of
4.9 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
4.10 | _ => raise ERROR "init_detail: uncovered case"
4.11 val prog = Auto_Prog.gen thy t rls'
5.1 --- a/src/Tools/isac/Interpret/solve-step.sml Thu Oct 20 12:12:18 2022 +0200
5.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri Oct 21 15:19:00 2022 +0200
5.3 @@ -180,7 +180,7 @@
5.4 val thy = Proof_Context.theory_of ctxt
5.5 val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp);
5.6 val f = Calc.current_formula cs;
5.7 - val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
5.8 + val subst = Tactic.subst_adapt_to_type ctxt subs;
5.9 in
5.10 case Rewrite.rewrite_inst_ ctxt (get_rew_ord ctxt ro') erls false subst (snd thm) f of
5.11 SOME (f', asm) =>
5.12 @@ -204,7 +204,7 @@
5.13 val ctxt = Ctree.get_loc pt pos |> snd
5.14 val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
5.15 val f = Calc.current_formula cs;
5.16 - val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
5.17 + val subst = Tactic.subst_adapt_to_type ctxt subs;
5.18 in
5.19 case Rewrite.rewrite_set_inst_ ctxt false subst (get_rls ctxt rls) f of
5.20 SOME (f', asm)
6.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Oct 20 12:12:18 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Oct 21 15:19:00 2022 +0200
6.3 @@ -139,11 +139,11 @@
6.4 setup \<open>KEStore_Elems.add_mets @{context}
6.5 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Diff} ["diff", "differentiate_on_R"]
6.6 [("chain-rule-diff-both",
6.7 - [TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
6.8 - TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
6.9 - TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
6.10 - TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
6.11 - TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
6.12 + [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
6.13 + TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
6.14 + TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
6.15 + TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
6.16 + TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
6.17 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
6.18 @{thm diff_exp_chain}])]]
6.19 \<close>
6.20 @@ -169,11 +169,11 @@
6.21 setup \<open>KEStore_Elems.add_mets @{context}
6.22 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Rational} ["simplification", "of_rationals"]
6.23 [("addition-of-fractions",
6.24 - [TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
6.25 - TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
6.26 - TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
6.27 - TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
6.28 - TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
6.29 + [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
6.30 + TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
6.31 + TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
6.32 + TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
6.33 + TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
6.34 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
6.35 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
6.36 \<close>
7.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Oct 20 12:12:18 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Oct 21 15:19:00 2022 +0200
7.3 @@ -11,7 +11,7 @@
7.4
7.5 consts
7.6
7.7 - d_d :: "[real, real]=> real"
7.8 + d_d :: "[real, real] => real"
7.9
7.10 (*descriptions in the related problems*)
7.11 derivativeEq :: "bool => una"
8.1 --- a/src/Tools/isac/MathEngBasic/method.sml Thu Oct 20 12:12:18 2022 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Fri Oct 21 15:19:00 2022 +0200
8.3 @@ -90,7 +90,7 @@
8.4 val wh = (case wh of
8.5 [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
8.6 | ((_, wh') :: []) =>
8.7 - (*(case \<^try>\<open> *)map (TermC.parse_patt_PIDE thy) wh'(*\<close> of
8.8 + (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
8.9 SOME x => x
8.10 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))*)
8.11 | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
9.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Thu Oct 20 12:12:18 2022 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Fri Oct 21 15:19:00 2022 +0200
9.3 @@ -127,7 +127,7 @@
9.4 val wh = (case wh of
9.5 [] => []
9.6 | ((_, wh') :: []) => (*special case in parsing*)
9.7 - (*(case \<^try>\<open> *)map (TermC.parse_patt_PIDE thy) wh'(*\<close> of
9.8 + (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
9.9 SOME x => x
9.10 | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
9.11 | _ => raise ERROR ("prep_input: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
10.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Oct 20 12:12:18 2022 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Fri Oct 21 15:19:00 2022 +0200
10.3 @@ -38,7 +38,13 @@
10.4 \<close>
10.5 end
10.6
10.7 -(* must be global for re-use in other structs *)
10.8 +(*
10.9 + Must be global for re-use in other structs.
10.10 +
10.11 + DOES NOT WORK IN me, etc: in Test_Code.init_calc @{context} --
10.12 + @{context} is overwritten by ctxt derived from Formalisation.
10.13 + THUS USE WITH DIRECT rewrite_, etc.
10.14 +*)
10.15 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
10.16 (* no of rewrites exceeding this int -> NO_REWRITE *)
10.17 val rewrite_limit = Attrib.setup_config_int \<^binding>\<open>rewrite_limit\<close> (K 100);
11.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Oct 20 12:12:18 2022 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Oct 21 15:19:00 2022 +0200
11.3 @@ -1,9 +1,10 @@
11.4 -(* Title: Tactics; tac_ for interaction with frontend, input for internal use.
11.5 +(* Title: "MathEngBasic/tactic.sml"
11.6 Author: Walther Neuper 170121
11.7 (c) due to copyright terms
11.8
11.9 -regular expression for search:
11.10 +Tactics; tac_ for interaction with frontend, input for internal use.
11.11
11.12 +Regular expression for search:
11.13 Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
11.14
11.15 *)
11.16 @@ -73,6 +74,9 @@
11.17 | Begin_Trans | End_Trans
11.18 | End_Proof';
11.19
11.20 + type subst_input
11.21 + val subst_adapt_to_type: Proof.context -> subst_input -> Subst.T
11.22 +
11.23 val input_to_string : input -> string
11.24 val tac2IDstr : input -> string
11.25 val is_empty : input -> bool
11.26 @@ -97,6 +101,24 @@
11.27 struct
11.28 (**)
11.29
11.30 +(** conversion from input-terms to terms in \<open>Calc.T\<close> **)
11.31 +(*
11.32 + A Tactic are input with string-arguments;
11.33 + while parsing these require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>.
11.34 +*)
11.35 +type subst_input = string list
11.36 +val dummyT = TFree ("'a", ["HOL.type"]);
11.37 +
11.38 +fun subst_adapt_to_type ctxt subst = (subst
11.39 + |> map (TermC.parse ctxt)
11.40 + |> map TermC.isapair2pair (*replace by HOLogic.strip_tuple etc*)
11.41 + |> map (apfst HOLogic.dest_string)
11.42 + |> map (apfst (fn str => (TermC.mk_Free (str, dummyT))))
11.43 + |> map (fn (t1, t2) =>
11.44 + (Model_Pattern.adapt_term_to_type ctxt t1, Model_Pattern.adapt_term_to_type ctxt t2)))
11.45 + handle TERM _ => raise TERM ("Tactic.subst_adapt_to_type: wrong argument " ^ strs2str' subst, [])
11.46 +
11.47 +
11.48 (** tactics for user at front-end **)
11.49
11.50 datatype input =
11.51 @@ -275,12 +297,12 @@
11.52 try_rew ctxt (ro, get_rew_ord ctxt ro) erls [] f (Rule.Thm thm'')
11.53 | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
11.54 try_rew ctxt (ro, get_rew_ord ctxt ro) erls
11.55 - (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
11.56 + (subst_adapt_to_type ctxt subs) f (Rule.Thm thm'')
11.57
11.58 | applicable ctxt _ _ f (Rewrite_Set rls') =
11.59 filter_appl_rews ctxt [] f (get_rls ctxt rls')
11.60 | applicable ctxt _ _ f (Rewrite_Set_Inst (subs, rls')) =
11.61 - filter_appl_rews ctxt (Subst.T_from_input ctxt subs) f (get_rls ctxt rls')
11.62 + filter_appl_rews ctxt (subst_adapt_to_type ctxt subs) f (get_rls ctxt rls')
11.63 | applicable _ _ _ _ tac =
11.64 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
11.65
12.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Oct 20 12:12:18 2022 +0200
12.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Oct 21 15:19:00 2022 +0200
12.3 @@ -21,7 +21,7 @@
12.4 Vars :: "'a => real list" (*get the variables of a term *)
12.5 matches :: "['a, 'a] => bool"
12.6 matchsub :: "['a, 'a] => bool"
12.7 - some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
12.8 + some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
12.9 occurs_in :: "[real , 'a] => bool" ("_ occurs'_in _")
12.10
12.11 abs :: "real => real" ("(|| _ ||)")
13.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Oct 20 12:12:18 2022 +0200
13.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Fri Oct 21 15:19:00 2022 +0200
13.3 @@ -214,14 +214,15 @@
13.4 fun is t = TermC.contains_Const_typeless all_Consts t
13.5
13.6
13.7 -(** arguments of specific tactics \<open>adapt_to_type\<close> **)
13.8 +(** conversion from program-terms to terms in \<open>Calc.T\<close> **)
13.9 (*
13.10 Programs are stored as terms typed by the theory they are defined in.
13.11 - Thus specific Prog_Tac require \<open>adapt_to_type\<close> for their arguments at the moment,
13.12 + Thus some Prog_Tac require \<open>adapt_to_type\<close> for their arguments at the moment,
13.13 where the formal arguments are substituted to actual arguments;
13.14 i.e. formal arguments require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>.
13.15
13.16 - Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>.
13.17 + Remarkably this appears not necessary for \<open>Rewrite_Inst\<close> and \<open>Rewrite_Set_Inst\<close>;
13.18 + for these, hoewever, \<open>adapt_to_type\<close> is required for conversion from \<open>Tac.subst_input\<close>.
13.19 *)
13.20 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
13.21 fun Take_adapt_to_type ctxt arg = arg
14.1 --- a/src/Tools/isac/Specify/cas-command.sml Thu Oct 20 12:12:18 2022 +0200
14.2 +++ b/src/Tools/isac/Specify/cas-command.sml Fri Oct 21 15:19:00 2022 +0200
14.3 @@ -102,7 +102,7 @@
14.4 Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
14.5 >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
14.6 let
14.7 - val t = TermC.parse_strict thy term;
14.8 + val t = TermC.parse (Proof_Context.init_global thy) term;
14.9 val pblID = References_Def.explode_id pbl;
14.10 val metID = References_Def.explode_id met;
14.11 val set_data =
15.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Thu Oct 20 12:12:18 2022 +0200
15.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Fri Oct 21 15:19:00 2022 +0200
15.3 @@ -28,7 +28,7 @@
15.4 "-------- fun T_from_input -----------------------------------------------------";
15.5 "-------- fun T_from_input -----------------------------------------------------";
15.6 "-------- fun T_from_input -----------------------------------------------------";
15.7 -case Subst.T_from_input ctxt ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
15.8 +case Tactic.subst_adapt_to_type ctxt ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
15.9 [(Free ("bdv_1", _), Free ("x", _)),
15.10 (Free ("bdv_2", _), Free ("y", _)),
15.11 (Free ("bdv_3", _), Free ("z", _))] => ()
16.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml Thu Oct 20 12:12:18 2022 +0200
16.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml Fri Oct 21 15:19:00 2022 +0200
16.3 @@ -7,7 +7,8 @@
16.4 "table of contents -----------------------------------------------------------------------------";
16.5 "-----------------------------------------------------------------------------------------------";
16.6 "-----------------------------------------------------------------------------------------------";
16.7 -"----------- fun result, fun creates_assms ---------------------------------------------------";
16.8 +"----------- fun result, fun creates_assms -----------------------------------------------------";
16.9 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
16.10 "-----------------------------------------------------------------------------------------------";
16.11 "-----------------------------------------------------------------------------------------------";
16.12 "-----------------------------------------------------------------------------------------------";
16.13 @@ -23,3 +24,14 @@
16.14 ;
16.15 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
16.16 if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
16.17 +
16.18 +
16.19 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
16.20 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
16.21 +"----------- fun subst_adapt_to_type -----------------------------------------------------------";
16.22 +val subs = ["(''bdv'', x)"];
16.23 +
16.24 +val [((Free ("bdv", T1)), Free ("x", T2))] = subst_adapt_to_type ctxt subs;
16.25 +if T1 = HOLogic.realT andalso T2 = HOLogic.realT
16.26 +then () else error "subst_adapt_to_type CHANGED";
16.27 +
17.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Thu Oct 20 12:12:18 2022 +0200
17.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Fri Oct 21 15:19:00 2022 +0200
17.3 @@ -54,7 +54,7 @@
17.4 Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv");
17.5 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
17.6 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv");
17.7 - val v = case Subst.T_from_input ctxt subs of
17.8 + val v = case Tactic.subst_adapt_to_type ctxt subs of
17.9 (_, v) :: _ => v;
17.10 (*case*) get_rls ctxt rls (*of*);
17.11