# HG changeset patch # User Walther Neuper # Date 1588409824 -7200 # Node ID caf3839e53c5579c755e2fd5d8de76d328e782e9 # Parent eb40bce6d6f1ff0b4e26f2f6ac8ffd43b3f2b1dd remove unused tactics, part 1 diff -r eb40bce6d6f1 -r caf3839e53c5 src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Sat May 02 09:15:39 2020 +0200 +++ b/src/Tools/isac/Interpret/li-tool.sml Sat May 02 10:57:04 2020 +0200 @@ -152,13 +152,6 @@ Associated (m, f', ContextC.insert_assumptions asms' ctxt) else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) else Not_Associated - | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = - if Rule_Set.id rls = HOLogic.dest_string rls_ then - if f = f_ then - Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')), (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = if Rule_Set.id rls = HOLogic.dest_string rls_ then @@ -166,13 +159,6 @@ Associated (m, f', ContextC.insert_assumptions asms' ctxt) else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) else Not_Associated - | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = - if Rule_Set.id rls = HOLogic.dest_string rls_ then - if f = f_ then - Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) = (case stac of (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) => diff -r eb40bce6d6f1 -r caf3839e53c5 src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 09:15:39 2020 +0200 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 10:57:04 2020 +0200 @@ -231,10 +231,6 @@ | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) end | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) -(*RM*)| check (Tactic.Take_Inst ct') _ = - raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct')) -(*RM*)| check (Tactic.Begin_Sequ) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ)) | check (Tactic.Begin_Trans) (pt, (p, p_)) = let val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*) @@ -244,65 +240,10 @@ in (Applicable.Yes (Tactic.Begin_Trans' f)) handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'") end - | check (Tactic.Split_And) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And) - | check (Tactic.Split_Or) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or) - | check (Tactic.Split_Intersect) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect)) - | check (Tactic.Conclude_And) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And) - | check (Tactic.Conclude_Or) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or) - | check Tactic.Collect_Trues _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues) - | check (Tactic.End_Sequ) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ)) | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) if p_ = Pos.Res then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" - | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset) - | check (Tactic.End_Subproblem) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem) - | check (Tactic.End_Intersect) _ = - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect)) - | check (m as Tactic.Detail_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 - 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 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); - in - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of - SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm))) - | NONE => Applicable.No (rls^" not applicable") - end - | check (m as Tactic.Detail_Set_Inst (subs, 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 - 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.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_)); - val subst = Subst.T_from_input thy subs - in - case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of - SOME (f', asm) - => Applicable.Yes (Tactic.Detail_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 -(*RM* )| End_Detail( *RM*) | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof'' | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m); diff -r eb40bce6d6f1 -r caf3839e53c5 src/Tools/isac/MathEngBasic/tactic.sml --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 09:15:39 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 10:57:04 2020 +0200 @@ -39,15 +39,9 @@ | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term (*RM*)| Tac_ of theory * string * string * string | Take' of term -(*RM* )| Take_Inst of TermC.as_string( *RM*) -(*RM*)| Begin_Sequ' | Begin_Trans' of term -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term -(*RM*)| End_Sequ' | End_Trans' of Selem.result -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof'' -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result -(*RM*)| End_Detail' of Selem.result; + | End_Detail' of Selem.result + | Begin_Trans' of term | End_Trans' of Selem.result + | End_Proof'' val string_of: T -> string @@ -81,15 +75,8 @@ | Substitute of Subst.input (*RM*)| Tac of string | Take of TermC.as_string -(*RM*)| Take_Inst of TermC.as_string -(*RM*)| Begin_Sequ | Begin_Trans -(*RM*)| Split_And | Split_Or | Split_Intersect -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues -(*RM*)| End_Sequ | End_Trans -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect -(*RM*)| Detail_Set of Rule_Set.id -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id -(*RM*)| End_Detail + | End_Detail + | Begin_Trans | End_Trans | End_Proof'; val input_to_string : input -> string @@ -156,15 +143,8 @@ | Substitute of Subst.input (*RM*)| Tac of string | Take of TermC.as_string -(*RM*)| Take_Inst of TermC.as_string -(*RM*)| Begin_Sequ | Begin_Trans -(*RM*)| Split_And | Split_Or | Split_Intersect -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues -(*RM*)| End_Sequ | End_Trans -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect -(*RM*)| Detail_Set of Rule_Set.id -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id -(*RM*)| End_Detail + | End_Detail + | Begin_Trans | End_Trans | End_Proof'; fun input_to_string ma = case ma of @@ -193,8 +173,6 @@ | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls) | Rewrite_Set rls => "Rewrite_Set " ^ quote rls - | Detail_Set rls => "Detail_Set " ^ quote rls - | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls) | End_Detail => "End_Detail" | Derive rls' => "Derive " ^ rls' | Calculate op_ => "Calculate " ^ op_ @@ -202,7 +180,6 @@ | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's | Take cterm' => "Take " ^ quote cterm' - | Take_Inst cterm' => "Take_Inst " ^ quote cterm' | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID) | End_Subproblem => "End_Subproblem" | CAScmd cterm' => "CAScmd " ^ quote cterm' @@ -238,15 +215,12 @@ | Rewrite _ => "Rewrite" | Rewrite_Set_Inst _ => "Rewrite_Set_Inst" | Rewrite_Set _ => "Rewrite_Set" - | Detail_Set _ => "Detail_Set" - | Detail_Set_Inst _ => "Detail_Set_Inst" | Derive _ => "Derive " | Calculate _ => "Calculate " | Substitute _ => "Substitute" | Apply_Assumption _ => "Apply_Assumption" | Take _ => "Take" - | Take_Inst _ => "Take_Inst" | Subproblem _ => "Subproblem" | End_Subproblem => "End_Subproblem" | CAScmd _ => "CAScmd" @@ -377,7 +351,6 @@ (*RM*)| Derive' of Rule_Set.T | Empty_Tac_ | Free_Solve' -(*RM* )| Apply_Assumption of TermC.as_string list( *RM*) | Or_to_List' of term * term | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result @@ -398,14 +371,9 @@ term (* resulting from the substitution *) (*RM*)| Tac_ of theory * string * string * string | Take' of term -(*RM*)| Begin_Sequ' | Begin_Trans' of term -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term -(*RM*)| End_Sequ' | End_Trans' of Selem.result -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof'' -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result -(*RM*)| End_Detail' of Selem.result; + | End_Detail' of Selem.result + | Begin_Trans' of term | End_Trans' of Selem.result + | End_Proof'' fun string_of ma = case ma of Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec) @@ -438,8 +406,6 @@ | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))" | End_Detail' _ => "End_Detail' xxx" - | Detail_Set' _ => "Detail_Set' xxx" - | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx" | Derive' rls => "Derive' " ^ Rule_Set.id rls | Calculate' _ => "Calculate' " @@ -452,6 +418,10 @@ | Empty_Tac_ => "Empty_Tac_" | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")" + + | Begin_Trans' _ => "Begin_Trans' xxx" + | End_Trans' _ => "End_Trans' xxx" + | End_Proof'' => "End_Trans' xxx" | _ => "string_of not impl. for arg"; fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI @@ -468,12 +438,8 @@ | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm) | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls) - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls) - | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls) - | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) = - Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls) | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_) | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred diff -r eb40bce6d6f1 -r caf3839e53c5 src/Tools/isac/Specify/generate.sml --- a/src/Tools/isac/Specify/generate.sml Sat May 02 09:15:39 2020 +0200 +++ b/src/Tools/isac/Specify/generate.sml Sat May 02 10:57:04 2020 +0200 @@ -245,16 +245,6 @@ in ((p, Res), c, FormKF (UnparseC.term f'), pt) end - | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) = - let - val (pt, _) = cappend_form pt p (is, ctxt) f - val pt = update_branch pt p TransitiveB - val is = init_istate (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs, Rule_Set.id rls)) f - val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt) - val pos' = ((lev_on o lev_dn) p, Frm) - in - generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*) - end | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = let val (pt, c) = cappend_atomic pt p (is, ctxt) f @@ -263,16 +253,6 @@ in ((p, Res), c, FormKF (UnparseC.term f'), pt) end - | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) = - let - val (pt, _) = cappend_form pt p (is, ctxt) f - val pt = update_branch pt p TransitiveB - val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f - val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt) - val pos' = ((lev_on o lev_dn) p, Frm) - in - generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*) - end | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = let val (pt, c) = append_result pt p l (scval, []) Complete