1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sat May 02 09:15:39 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sat May 02 10:57:04 2020 +0200
1.3 @@ -152,13 +152,6 @@
1.4 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
1.5 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.6 else Not_Associated
1.7 - | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.8 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.9 - if Rule_Set.id rls = HOLogic.dest_string rls_ then
1.10 - if f = f_ then
1.11 - Associated (m, f', ContextC.insert_assumptions asms' ctxt)
1.12 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.13 - else Not_Associated
1.14 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
1.15 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.16 if Rule_Set.id rls = HOLogic.dest_string rls_ then
1.17 @@ -166,13 +159,6 @@
1.18 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
1.19 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.20 else Not_Associated
1.21 - | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
1.22 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.23 - if Rule_Set.id rls = HOLogic.dest_string rls_ then
1.24 - if f = f_ then
1.25 - Associated (m, f', ContextC.insert_assumptions asms' ctxt)
1.26 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.27 - else Not_Associated
1.28 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
1.29 (case stac of
1.30 (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
2.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 09:15:39 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 10:57:04 2020 +0200
2.3 @@ -231,10 +231,6 @@
2.4 | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
2.5 end
2.6 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
2.7 -(*RM*)| check (Tactic.Take_Inst ct') _ =
2.8 - raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
2.9 -(*RM*)| check (Tactic.Begin_Sequ) _ =
2.10 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
2.11 | check (Tactic.Begin_Trans) (pt, (p, p_)) =
2.12 let
2.13 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
2.14 @@ -244,65 +240,10 @@
2.15 in (Applicable.Yes (Tactic.Begin_Trans' f))
2.16 handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
2.17 end
2.18 - | check (Tactic.Split_And) _ =
2.19 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
2.20 - | check (Tactic.Split_Or) _ =
2.21 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
2.22 - | check (Tactic.Split_Intersect) _ =
2.23 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
2.24 - | check (Tactic.Conclude_And) _ =
2.25 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
2.26 - | check (Tactic.Conclude_Or) _ =
2.27 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
2.28 - | check Tactic.Collect_Trues _ =
2.29 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
2.30 - | check (Tactic.End_Sequ) _ =
2.31 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
2.32 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
2.33 if p_ = Pos.Res
2.34 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
2.35 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
2.36 - | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
2.37 - | check (Tactic.End_Subproblem) _ =
2.38 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
2.39 - | check (Tactic.End_Intersect) _ =
2.40 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
2.41 - | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =
2.42 - if member op = [Pos.Pbl, Pos.Met] p_
2.43 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.44 - else
2.45 - let
2.46 - val pp = Ctree.par_pblobj pt p
2.47 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
2.48 - val f = case p_ of
2.49 - Frm => Ctree.get_obj Ctree.g_form pt p
2.50 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.51 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.52 - in
2.53 - case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
2.54 - SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
2.55 - | NONE => Applicable.No (rls^" not applicable")
2.56 - end
2.57 - | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =
2.58 - if member op = [Pos.Pbl, Pos.Met] p_
2.59 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
2.60 - else
2.61 - let
2.62 - val pp = Ctree.par_pblobj pt p;
2.63 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.64 - val thy = ThyC.get_theory thy';
2.65 - val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
2.66 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.67 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.68 - val subst = Subst.T_from_input thy subs
2.69 - in
2.70 - case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
2.71 - SOME (f', asm)
2.72 - => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
2.73 - | NONE => Applicable.No (rls ^ " not applicable")
2.74 - handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
2.75 - end
2.76 -(*RM* )| End_Detail( *RM*)
2.77 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
2.78 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
2.79
3.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 09:15:39 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 10:57:04 2020 +0200
3.3 @@ -39,15 +39,9 @@
3.4 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
3.5 (*RM*)| Tac_ of theory * string * string * string
3.6 | Take' of term
3.7 -(*RM* )| Take_Inst of TermC.as_string( *RM*)
3.8 -(*RM*)| Begin_Sequ' | Begin_Trans' of term
3.9 -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
3.10 -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
3.11 -(*RM*)| End_Sequ' | End_Trans' of Selem.result
3.12 -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
3.13 -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
3.14 -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
3.15 -(*RM*)| End_Detail' of Selem.result;
3.16 + | End_Detail' of Selem.result
3.17 + | Begin_Trans' of term | End_Trans' of Selem.result
3.18 + | End_Proof''
3.19
3.20 val string_of: T -> string
3.21
3.22 @@ -81,15 +75,8 @@
3.23 | Substitute of Subst.input
3.24 (*RM*)| Tac of string
3.25 | Take of TermC.as_string
3.26 -(*RM*)| Take_Inst of TermC.as_string
3.27 -(*RM*)| Begin_Sequ | Begin_Trans
3.28 -(*RM*)| Split_And | Split_Or | Split_Intersect
3.29 -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
3.30 -(*RM*)| End_Sequ | End_Trans
3.31 -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
3.32 -(*RM*)| Detail_Set of Rule_Set.id
3.33 -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
3.34 -(*RM*)| End_Detail
3.35 + | End_Detail
3.36 + | Begin_Trans | End_Trans
3.37 | End_Proof';
3.38
3.39 val input_to_string : input -> string
3.40 @@ -156,15 +143,8 @@
3.41 | Substitute of Subst.input
3.42 (*RM*)| Tac of string
3.43 | Take of TermC.as_string
3.44 -(*RM*)| Take_Inst of TermC.as_string
3.45 -(*RM*)| Begin_Sequ | Begin_Trans
3.46 -(*RM*)| Split_And | Split_Or | Split_Intersect
3.47 -(*RM*)| Conclude_And | Conclude_Or | Collect_Trues
3.48 -(*RM*)| End_Sequ | End_Trans
3.49 -(*RM*)| End_Ruleset | End_Subproblem | End_Intersect
3.50 -(*RM*)| Detail_Set of Rule_Set.id
3.51 -(*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
3.52 -(*RM*)| End_Detail
3.53 + | End_Detail
3.54 + | Begin_Trans | End_Trans
3.55 | End_Proof';
3.56
3.57 fun input_to_string ma = case ma of
3.58 @@ -193,8 +173,6 @@
3.59 | Rewrite_Set_Inst (subs, rls) =>
3.60 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
3.61 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
3.62 - | Detail_Set rls => "Detail_Set " ^ quote rls
3.63 - | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
3.64 | End_Detail => "End_Detail"
3.65 | Derive rls' => "Derive " ^ rls'
3.66 | Calculate op_ => "Calculate " ^ op_
3.67 @@ -202,7 +180,6 @@
3.68 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
3.69
3.70 | Take cterm' => "Take " ^ quote cterm'
3.71 - | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
3.72 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
3.73 | End_Subproblem => "End_Subproblem"
3.74 | CAScmd cterm' => "CAScmd " ^ quote cterm'
3.75 @@ -238,15 +215,12 @@
3.76 | Rewrite _ => "Rewrite"
3.77 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
3.78 | Rewrite_Set _ => "Rewrite_Set"
3.79 - | Detail_Set _ => "Detail_Set"
3.80 - | Detail_Set_Inst _ => "Detail_Set_Inst"
3.81 | Derive _ => "Derive "
3.82 | Calculate _ => "Calculate "
3.83 | Substitute _ => "Substitute"
3.84 | Apply_Assumption _ => "Apply_Assumption"
3.85
3.86 | Take _ => "Take"
3.87 - | Take_Inst _ => "Take_Inst"
3.88 | Subproblem _ => "Subproblem"
3.89 | End_Subproblem => "End_Subproblem"
3.90 | CAScmd _ => "CAScmd"
3.91 @@ -377,7 +351,6 @@
3.92 (*RM*)| Derive' of Rule_Set.T
3.93 | Empty_Tac_
3.94 | Free_Solve'
3.95 -(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
3.96 | Or_to_List' of term * term
3.97 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
3.98 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
3.99 @@ -398,14 +371,9 @@
3.100 term (* resulting from the substitution *)
3.101 (*RM*)| Tac_ of theory * string * string * string
3.102 | Take' of term
3.103 -(*RM*)| Begin_Sequ' | Begin_Trans' of term
3.104 -(*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
3.105 -(*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
3.106 -(*RM*)| End_Sequ' | End_Trans' of Selem.result
3.107 -(*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
3.108 -(*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
3.109 -(*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
3.110 -(*RM*)| End_Detail' of Selem.result;
3.111 + | End_Detail' of Selem.result
3.112 + | Begin_Trans' of term | End_Trans' of Selem.result
3.113 + | End_Proof''
3.114
3.115 fun string_of ma = case ma of
3.116 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
3.117 @@ -438,8 +406,6 @@
3.118 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
3.119 "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
3.120 | End_Detail' _ => "End_Detail' xxx"
3.121 - | Detail_Set' _ => "Detail_Set' xxx"
3.122 - | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
3.123
3.124 | Derive' rls => "Derive' " ^ Rule_Set.id rls
3.125 | Calculate' _ => "Calculate' "
3.126 @@ -452,6 +418,10 @@
3.127
3.128 | Empty_Tac_ => "Empty_Tac_"
3.129 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
3.130 +
3.131 + | Begin_Trans' _ => "Begin_Trans' xxx"
3.132 + | End_Trans' _ => "End_Trans' xxx"
3.133 + | End_Proof'' => "End_Trans' xxx"
3.134 | _ => "string_of not impl. for arg";
3.135
3.136 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
3.137 @@ -468,12 +438,8 @@
3.138 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
3.139
3.140 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
3.141 - | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
3.142 -
3.143 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
3.144 Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
3.145 - | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
3.146 - Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
3.147
3.148 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
3.149 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
4.1 --- a/src/Tools/isac/Specify/generate.sml Sat May 02 09:15:39 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/generate.sml Sat May 02 10:57:04 2020 +0200
4.3 @@ -245,16 +245,6 @@
4.4 in
4.5 ((p, Res), c, FormKF (UnparseC.term f'), pt)
4.6 end
4.7 - | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) =
4.8 - let
4.9 - val (pt, _) = cappend_form pt p (is, ctxt) f
4.10 - val pt = update_branch pt p TransitiveB
4.11 - val is = init_istate (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs, Rule_Set.id rls)) f
4.12 - val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
4.13 - val pos' = ((lev_on o lev_dn) p, Frm)
4.14 - in
4.15 - generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
4.16 - end
4.17 | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
4.18 let
4.19 val (pt, c) = cappend_atomic pt p (is, ctxt) f
4.20 @@ -263,16 +253,6 @@
4.21 in
4.22 ((p, Res), c, FormKF (UnparseC.term f'), pt)
4.23 end
4.24 - | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) =
4.25 - let
4.26 - val (pt, _) = cappend_form pt p (is, ctxt) f
4.27 - val pt = update_branch pt p TransitiveB
4.28 - val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f
4.29 - val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
4.30 - val pos' = ((lev_on o lev_dn) p, Frm)
4.31 - in
4.32 - generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
4.33 - end
4.34 | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
4.35 let
4.36 val (pt, c) = append_result pt p l (scval, []) Complete