1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 11:36:13 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 12:13:20 2020 +0200
1.3 @@ -67,19 +67,15 @@
1.4 in
1.5 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
1.6 end
1.7 -(*RM* )| Derive of Rule_Set.id( *RM*)
1.8 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.9 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
1.10 - | check (Tactic.Apply_Assumption cts') _ =
1.11 - raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
1.12 - (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
1.13 | check Tactic.Or_to_List (pt, (p, p_)) =
1.14 if member op = [Pos.Pbl, Pos.Met] p_
1.15 then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
1.16 else
1.17 let
1.18 val f = case p_ of
1.19 - Frm => Ctree.get_obj Ctree.g_form pt p
1.20 + Pos.Frm => Ctree.get_obj Ctree.g_form pt p
1.21 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.22 | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
1.23 in (let val ls = Prog_Expr.or2list f
2.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 11:36:13 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 12:13:20 2020 +0200
2.3 @@ -4,7 +4,7 @@
2.4
2.5 regular expression for search:
2.6
2.7 -Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|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
2.8 +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
2.9
2.10 *)
2.11 signature TACTIC =
2.12 @@ -25,10 +25,9 @@
2.13 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
2.14 | Check_Postcond' of Problem.id * term
2.15 | Check_elementwise' of term * TermC.as_string * Selem.result
2.16 -(*RM*)| Derive' of Rule_Set.T
2.17 + | Derive' of Rule_Set.T
2.18 | Empty_Tac_
2.19 | Free_Solve'
2.20 -(*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
2.21 | Or_to_List' of term * term
2.22 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
2.23 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
2.24 @@ -60,10 +59,9 @@
2.25 | Calculate of string
2.26 | Check_Postcond of Problem.id
2.27 | Check_elementwise of TermC.as_string
2.28 -(*RM*)| Derive of Rule_Set.id(*RM*)
2.29 + | Derive of Rule_Set.id
2.30 | Empty_Tac
2.31 -(*RM*)| Free_Solve
2.32 -(*RM*)| Apply_Assumption of TermC.as_string list
2.33 + | Free_Solve
2.34 | Or_to_List
2.35 | Rewrite of ThmC.T
2.36 | Rewrite_Inst of Subst.input * ThmC.T
2.37 @@ -127,10 +125,9 @@
2.38 | Calculate of string
2.39 | Check_Postcond of Problem.id
2.40 | Check_elementwise of TermC.as_string
2.41 -(*RM*)| Derive of Rule_Set.id
2.42 + | Derive of Rule_Set.id
2.43 | Empty_Tac
2.44 -(*RM*)| Free_Solve
2.45 -(*RM*)| Apply_Assumption of TermC.as_string list
2.46 + | Free_Solve
2.47 | Or_to_List
2.48 | Rewrite of ThmC.T
2.49 | Rewrite_Inst of Subst.input * ThmC.T
2.50 @@ -169,22 +166,19 @@
2.51 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
2.52 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
2.53 | End_Detail => "End_Detail"
2.54 - | Derive rls' => "Derive " ^ rls'
2.55 + | Derive rls' => "Derive " ^ rls'
2.56 | Calculate op_ => "Calculate " ^ op_
2.57 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
2.58 - | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
2.59
2.60 | Take cterm' => "Take " ^ quote cterm'
2.61 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
2.62 - | End_Subproblem => "End_Subproblem"
2.63 | CAScmd cterm' => "CAScmd " ^ quote cterm'
2.64
2.65 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
2.66 | Or_to_List => "Or_to_List "
2.67 - | Collect_Trues => "Collect_Trues"
2.68
2.69 | Empty_Tac => "Empty_Tac"
2.70 - | Tac string => "Tac " ^ string
2.71 +(*RM*)| Tac string => "Tac " ^ string(*RM*)
2.72 | End_Proof' => "input End_Proof'"
2.73 | _ => "input_to_string not impl. for ?!";
2.74
2.75 @@ -213,16 +207,13 @@
2.76 | Derive _ => "Derive "
2.77 | Calculate _ => "Calculate "
2.78 | Substitute _ => "Substitute"
2.79 - | Apply_Assumption _ => "Apply_Assumption"
2.80
2.81 | Take _ => "Take"
2.82 | Subproblem _ => "Subproblem"
2.83 - | End_Subproblem => "End_Subproblem"
2.84 | CAScmd _ => "CAScmd"
2.85
2.86 | Check_elementwise _ => "Check_elementwise"
2.87 | Or_to_List => "Or_to_List "
2.88 - | Collect_Trues => "Collect_Trues"
2.89
2.90 | Empty_Tac => "Empty_Tac"
2.91 | Tac _ => "Tac "
2.92 @@ -342,7 +333,7 @@
2.93 term * (* the current formula: [x=1,x=...] *)
2.94 string * (* the pred from Check_elementwise *)
2.95 Selem.result (* composed from (1) and (2): {x. pred} *)
2.96 -(*RM*)| Derive' of Rule_Set.T
2.97 + | Derive' of Rule_Set.T(* for Generate.embed_deriv *)
2.98 | Empty_Tac_
2.99 | Free_Solve'
2.100 | Or_to_List' of term * term
2.101 @@ -365,8 +356,9 @@
2.102 term (* resulting from the substitution *)
2.103 (*RM*)| Tac_ of theory * string * string * string
2.104 | Take' of term
2.105 - | End_Detail' of Selem.result
2.106 - | Begin_Trans' of term | End_Trans' of Selem.result
2.107 + | End_Detail' of Selem.result (* for intermediate steps into Rewrite_Set *)
2.108 + | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
2.109 + | End_Trans' of Selem.result (* for intermediate steps into Rewrite_Set *)
2.110 | End_Proof''
2.111
2.112 fun string_of ma = case ma of
3.1 --- a/src/Tools/isac/TODO.thy Sat May 02 11:36:13 2020 +0200
3.2 +++ b/src/Tools/isac/TODO.thy Sat May 02 12:13:20 2020 +0200
3.3 @@ -26,8 +26,8 @@
3.4 (*/------- to -------\*)
3.5 (*\------- to -------/*)
3.6 \begin{itemize}
3.7 - \item ML_file "rule-set.sml" Know_Store -> MathEngBasic (=ThmC, Rewrite)
3.8 - probably first review calcelems.sml
3.9 + \item xxx
3.10 + \item rm warnings from solve-step.sml
3.11 \item xxx
3.12 \item rename/relocate: Selem.result -> Calc.result ?OR? (NEW..)Formula.result
3.13 \item xxx