# HG changeset patch # User Walther Neuper # Date 1588426887 -7200 # Node ID 7601a1fa20b9604f09b891a8faf542fd70009b08 # Parent 877d6bc38715c2c7df1df347f18282682c2100ce simplify Solve_Step.check, remove CAScmd (is not a tactic) diff -r 877d6bc38715 -r 7601a1fa20b9 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 12:13:20 2020 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 15:41:27 2020 +0200 @@ -619,7 +619,7 @@ *) fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo = let - val fo = Calc.get_current_formula ptp + val fo = Calc.current_formula ptp val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*) diff -r 877d6bc38715 -r 7601a1fa20b9 src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 12:13:20 2020 +0200 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 15:41:27 2020 +0200 @@ -24,18 +24,10 @@ check tactics (input by the user, mostly) for applicability and determine as much of the result of the tactic as possible initially. *) -fun check (Tactic.CAScmd ct') _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct')) - | check (m as Tactic.Calculate op_) (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) - else +fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) = let - val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt; - val f = case p_ of - Frm => Ctree.get_obj Ctree.g_form pt p - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt; + val f = Calc.current_formula cs; in if msg = "OK" then @@ -45,35 +37,18 @@ | NONE => Applicable.No ("'calculate "^op_^"' not applicable") else Applicable.No msg end - | check (Tactic.Check_Postcond pI) (_, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) - else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty)) - | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_)) - else + | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*) + Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty)) + | check (Tactic.Check_elementwise pred) cs = let - val pp = Ctree.par_pblobj pt p; - val thy' = Ctree.get_obj Ctree.g_domID pt pp; - val thy = ThyC.get_theory thy' - val metID = (Ctree.get_obj Ctree.g_metID pt pp) - val {crls, ...} = Specify.get_met metID - val (f, asm) = case p_ of - Frm => (Ctree.get_obj Ctree.g_form pt p , []) - | Pos.Res => Ctree.get_obj Ctree.g_result pt p - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); - val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f; + val f = Calc.current_formula cs; in - Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm))) + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, []))) end | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *) | check Tactic.Or_to_List (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_))) - else - let + let val f = case p_ of Pos.Frm => Ctree.get_obj Ctree.g_form pt p | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p @@ -82,17 +57,11 @@ in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end) handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f) end - | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_))) - else + | check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) = let val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt; val thy = ThyC.get_theory thy'; - val f = case p_ of - Frm => Ctree.get_obj Ctree.g_form pt p - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_)); + val f = Calc.current_formula cs; in if msg = "OK" then @@ -101,19 +70,13 @@ | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable") else Applicable.No msg end - | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_)) - else + | check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) = let val pp = Ctree.par_pblobj pt p; val thy' = Ctree.get_obj Ctree.g_domID pt pp; val thy = ThyC.get_theory thy'; val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp); - val (f, _) = case p_ of (*p 12.4.00 unnecessary*) - Frm => (Ctree.get_obj Ctree.g_form pt p, p) - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val f = Calc.current_formula cs; in let val subst = Subst.T_from_input thy subs; @@ -123,26 +86,20 @@ Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) | NONE => Applicable.No ((fst thm'')^" not applicable") end - handle _ => Applicable.No ("syntax error in "^(subs2str subs)) + handle _ => Applicable.No ("syntax error in " ^ subs2str subs) end - | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) - else + | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) = let val pp = Ctree.par_pblobj pt p; val thy' = Ctree.get_obj Ctree.g_domID pt pp; - val (f, _) = case p_ of - Frm => (Ctree.get_obj Ctree.g_form pt p, p) - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val f = Calc.current_formula cs; in case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of SOME (f', asm) => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) | NONE => Applicable.No (rls ^ " not applicable") end - | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) = + | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) = if member op = [Pos.Pbl, Pos.Met] p_ then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) else @@ -150,66 +107,50 @@ val pp = Ctree.par_pblobj pt p; val thy' = Ctree.get_obj Ctree.g_domID pt pp; val thy = ThyC.get_theory thy'; - val (f, _) = case p_ of - Frm => (Ctree.get_obj Ctree.g_form pt p, p) - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val f = Calc.current_formula cs; val subst = Subst.T_from_input thy subs; in - case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of - SOME (f',asm) + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of + SOME (f', asm) => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) | NONE => Applicable.No (rls ^ " not applicable") handle _ => Applicable.No ("syntax error in " ^(subs2str subs)) end - | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) = - if Pos.on_specification p_ - then - Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) - else (*some fields filled later in LI*) - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], - TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) - (*Substitute combines two different kind of "substitution": + | check (Tactic.Subproblem (domID, pblID)) (_, _) = + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) + + (*Substitute combines two different kind of "substitution": (1) subst_atomic: for ?a..?z (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*) - | check (m as Tactic.Substitute sube) (pt, (p, p_)) = - if member op = [Pos.Pbl, Pos.Met] p_ - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) - else - let - val pp = Ctree.par_pblobj pt p - val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) - val f = case p_ of - Frm => Ctree.get_obj Ctree.g_form pt p - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) - val subte = Subst.input_to_terms sube - val subst = Subst.T_from_string_eqs thy sube - val ro = Rewrite_Ord.assoc_rew_ord rew_ord' - in - if foldl and_ (true, map TermC.contains_Var subte) - then (*1*) - let val f' = subst_atomic subst f - in if f = f' - then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") - else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) - end - else (*2*) - case Rewrite.rewrite_terms_ thy ro erls subte f of - SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) - | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") - end - | check (Tactic.Tac id) (pt, (p, p_)) = + | check (Tactic.Substitute sube) (cs as (pt, (p, _))) = + let + val pp = Ctree.par_pblobj pt p + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) + val f = Calc.current_formula cs; + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) + val subte = Subst.input_to_terms sube + val subst = Subst.T_from_string_eqs thy sube + val ro = Rewrite_Ord.assoc_rew_ord rew_ord' + in + if foldl and_ (true, map TermC.contains_Var subte) + then (*1*) + let val f' = subst_atomic subst f + in if f = f' + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) + end + else (*2*) + case Rewrite.rewrite_terms_ thy ro erls subte f of + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") + end + | check (Tactic.Tac id) (cs as (pt, (p, _))) = let val pp = Ctree.par_pblobj pt p; val thy' = Ctree.get_obj Ctree.g_domID pt pp; val thy = ThyC.get_theory thy'; - val f = case p_ of - Frm => Ctree.get_obj Ctree.g_form pt p - | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl" - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); + val f = Calc.current_formula cs; in case id of "subproblem_equation_dummy" => if TermC.is_expliceq f diff -r 877d6bc38715 -r 7601a1fa20b9 src/Tools/isac/MathEngBasic/calculation.sml --- a/src/Tools/isac/MathEngBasic/calculation.sml Sat May 02 12:13:20 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Sat May 02 15:41:27 2020 +0200 @@ -6,7 +6,7 @@ signature CALCULATION = sig type T - val get_current_formula: T -> term + val current_formula: T -> term end @@ -16,11 +16,11 @@ (**) type T = Ctree.state -fun get_current_formula (pt, (p, p_)) = +fun current_formula (pt, (p, p_)) = case p_ of Pos.Frm => Ctree.get_obj Ctree.g_form pt p | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => TermC.empty (*on PblObj is fo <> ifo*); + | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); (**)end(**) diff -r 877d6bc38715 -r 7601a1fa20b9 src/Tools/isac/MathEngBasic/tactic.sml --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 12:13:20 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 15:41:27 2020 +0200 @@ -4,7 +4,7 @@ regular expression for search: -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|CAScmd|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 +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 *) signature TACTIC = @@ -21,7 +21,6 @@ | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list)) | Specify_Theory' of ThyC.id (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) - | CAScmd' of term | Calculate' of ThyC.id * string * term * (term * ThmC.T) | Check_Postcond' of Problem.id * term | Check_elementwise' of term * TermC.as_string * Selem.result @@ -55,7 +54,6 @@ | Specify_Problem of Problem.id | Specify_Theory of ThyC.id (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) - | CAScmd of TermC.as_string | Calculate of string | Check_Postcond of Problem.id | Check_elementwise of TermC.as_string @@ -121,7 +119,6 @@ | Specify_Problem of Problem.id | Specify_Theory of ThyC.id (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) - | CAScmd of TermC.as_string | Calculate of string | Check_Postcond of Problem.id | Check_elementwise of TermC.as_string @@ -172,7 +169,6 @@ | Take cterm' => "Take " ^ quote cterm' | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID) - | CAScmd cterm' => "CAScmd " ^ quote cterm' | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm' | Or_to_List => "Or_to_List " @@ -210,7 +206,6 @@ | Take _ => "Take" | Subproblem _ => "Subproblem" - | CAScmd _ => "CAScmd" | Check_elementwise _ => "Check_elementwise" | Or_to_List => "Or_to_List " @@ -324,7 +319,6 @@ (bool * term) list)) (* individual preconditions marked true/false *) | Specify_Theory' of ThyC.id (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*) - | CAScmd' of term | Calculate' of ThyC.id * string * term * (term * ThmC.T) | Check_Postcond' of (* last step in solving a (sub-)Problem *) Problem.id * (* id of the Problem to be checked *) @@ -399,7 +393,6 @@ | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*) | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => "Subproblem' "(*^(pair2str (domID, strs2str ,))*) - | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*) | Empty_Tac_ => "Empty_Tac_" | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"