1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 12:13:20 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 15:41:27 2020 +0200
1.3 @@ -619,7 +619,7 @@
1.4 *)
1.5 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
1.6 let
1.7 - val fo = Calc.get_current_formula ptp
1.8 + val fo = Calc.current_formula ptp
1.9 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.10 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
1.11 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
2.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 12:13:20 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 15:41:27 2020 +0200
2.3 @@ -24,18 +24,10 @@
2.4 check tactics (input by the user, mostly) for applicability
2.5 and determine as much of the result of the tactic as possible initially.
2.6 *)
2.7 -fun check (Tactic.CAScmd ct') _ =
2.8 - error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
2.9 - | check (m as Tactic.Calculate op_) (pt, (p, p_)) =
2.10 - if member op = [Pos.Pbl, Pos.Met] p_
2.11 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
2.12 - else
2.13 +fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
2.14 let
2.15 - val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
2.16 - val f = case p_ of
2.17 - Frm => Ctree.get_obj Ctree.g_form pt p
2.18 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.19 - | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.20 + val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
2.21 + val f = Calc.current_formula cs;
2.22 in
2.23 if msg = "OK"
2.24 then
2.25 @@ -45,35 +37,18 @@
2.26 | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
2.27 else Applicable.No msg
2.28 end
2.29 - | check (Tactic.Check_Postcond pI) (_, (p, p_)) =
2.30 - if member op = [Pos.Pbl, Pos.Met] p_
2.31 - then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.32 - else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
2.33 - | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =
2.34 - if member op = [Pos.Pbl, Pos.Met] p_
2.35 - then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.36 - else
2.37 + | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
2.38 + Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
2.39 + | check (Tactic.Check_elementwise pred) cs =
2.40 let
2.41 - val pp = Ctree.par_pblobj pt p;
2.42 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.43 - val thy = ThyC.get_theory thy'
2.44 - val metID = (Ctree.get_obj Ctree.g_metID pt pp)
2.45 - val {crls, ...} = Specify.get_met metID
2.46 - val (f, asm) = case p_ of
2.47 - Frm => (Ctree.get_obj Ctree.g_form pt p , [])
2.48 - | Pos.Res => Ctree.get_obj Ctree.g_result pt p
2.49 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.50 - val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;
2.51 + val f = Calc.current_formula cs;
2.52 in
2.53 - Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
2.54 + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
2.55 end
2.56 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
2.57 | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
2.58 | check Tactic.Or_to_List (pt, (p, p_)) =
2.59 - if member op = [Pos.Pbl, Pos.Met] p_
2.60 - then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
2.61 - else
2.62 - let
2.63 + let
2.64 val f = case p_ of
2.65 Pos.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 @@ -82,17 +57,11 @@
2.68 in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
2.69 handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
2.70 end
2.71 - | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) =
2.72 - if member op = [Pos.Pbl, Pos.Met] p_
2.73 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
2.74 - else
2.75 + | check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) =
2.76 let
2.77 val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
2.78 val thy = ThyC.get_theory thy';
2.79 - val f = case p_ of
2.80 - Frm => Ctree.get_obj Ctree.g_form pt p
2.81 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.82 - | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));
2.83 + val f = Calc.current_formula cs;
2.84 in
2.85 if msg = "OK"
2.86 then
2.87 @@ -101,19 +70,13 @@
2.88 | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
2.89 else Applicable.No msg
2.90 end
2.91 - | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) =
2.92 - if member op = [Pos.Pbl, Pos.Met] p_
2.93 - then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
2.94 - else
2.95 + | check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) =
2.96 let
2.97 val pp = Ctree.par_pblobj pt p;
2.98 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.99 val thy = ThyC.get_theory thy';
2.100 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
2.101 - val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
2.102 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
2.103 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
2.104 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.105 + val f = Calc.current_formula cs;
2.106 in
2.107 let
2.108 val subst = Subst.T_from_input thy subs;
2.109 @@ -123,26 +86,20 @@
2.110 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
2.111 | NONE => Applicable.No ((fst thm'')^" not applicable")
2.112 end
2.113 - handle _ => Applicable.No ("syntax error in "^(subs2str subs))
2.114 + handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
2.115 end
2.116 - | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =
2.117 - if member op = [Pos.Pbl, Pos.Met] p_
2.118 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.119 - else
2.120 + | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
2.121 let
2.122 val pp = Ctree.par_pblobj pt p;
2.123 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.124 - val (f, _) = case p_ of
2.125 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
2.126 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
2.127 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.128 + val f = Calc.current_formula cs;
2.129 in
2.130 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
2.131 SOME (f', asm)
2.132 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
2.133 | NONE => Applicable.No (rls ^ " not applicable")
2.134 end
2.135 - | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) =
2.136 + | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =
2.137 if member op = [Pos.Pbl, Pos.Met] p_
2.138 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
2.139 else
2.140 @@ -150,66 +107,50 @@
2.141 val pp = Ctree.par_pblobj pt p;
2.142 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.143 val thy = ThyC.get_theory thy';
2.144 - val (f, _) = case p_ of
2.145 - Frm => (Ctree.get_obj Ctree.g_form pt p, p)
2.146 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
2.147 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.148 + val f = Calc.current_formula cs;
2.149 val subst = Subst.T_from_input thy subs;
2.150 in
2.151 - case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
2.152 - SOME (f',asm)
2.153 + case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
2.154 + SOME (f', asm)
2.155 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
2.156 | NONE => Applicable.No (rls ^ " not applicable")
2.157 handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
2.158 end
2.159 - | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =
2.160 - if Pos.on_specification p_
2.161 - then
2.162 - Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.163 - else (*some fields filled later in LI*)
2.164 - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
2.165 - TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
2.166 - (*Substitute combines two different kind of "substitution":
2.167 + | check (Tactic.Subproblem (domID, pblID)) (_, _) =
2.168 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
2.169 + TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
2.170 +
2.171 + (*Substitute combines two different kind of "substitution":
2.172 (1) subst_atomic: for ?a..?z
2.173 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
2.174 - | check (m as Tactic.Substitute sube) (pt, (p, p_)) =
2.175 - if member op = [Pos.Pbl, Pos.Met] p_
2.176 - then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
2.177 - else
2.178 - let
2.179 - val pp = Ctree.par_pblobj pt p
2.180 - val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
2.181 - val f = case p_ of
2.182 - Frm => Ctree.get_obj Ctree.g_form pt p
2.183 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.184 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.185 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
2.186 - val subte = Subst.input_to_terms sube
2.187 - val subst = Subst.T_from_string_eqs thy sube
2.188 - val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
2.189 - in
2.190 - if foldl and_ (true, map TermC.contains_Var subte)
2.191 - then (*1*)
2.192 - let val f' = subst_atomic subst f
2.193 - in if f = f'
2.194 - then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
2.195 - else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
2.196 - end
2.197 - else (*2*)
2.198 - case Rewrite.rewrite_terms_ thy ro erls subte f of
2.199 - SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
2.200 - | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
2.201 - end
2.202 - | check (Tactic.Tac id) (pt, (p, p_)) =
2.203 + | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
2.204 + let
2.205 + val pp = Ctree.par_pblobj pt p
2.206 + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
2.207 + val f = Calc.current_formula cs;
2.208 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
2.209 + val subte = Subst.input_to_terms sube
2.210 + val subst = Subst.T_from_string_eqs thy sube
2.211 + val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
2.212 + in
2.213 + if foldl and_ (true, map TermC.contains_Var subte)
2.214 + then (*1*)
2.215 + let val f' = subst_atomic subst f
2.216 + in if f = f'
2.217 + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
2.218 + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
2.219 + end
2.220 + else (*2*)
2.221 + case Rewrite.rewrite_terms_ thy ro erls subte f of
2.222 + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
2.223 + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
2.224 + end
2.225 + | check (Tactic.Tac id) (cs as (pt, (p, _))) =
2.226 let
2.227 val pp = Ctree.par_pblobj pt p;
2.228 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.229 val thy = ThyC.get_theory thy';
2.230 - val f = case p_ of
2.231 - Frm => Ctree.get_obj Ctree.g_form pt p
2.232 - | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"
2.233 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.234 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.235 + val f = Calc.current_formula cs;
2.236 in case id of
2.237 "subproblem_equation_dummy" =>
2.238 if TermC.is_expliceq f
3.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml Sat May 02 12:13:20 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Sat May 02 15:41:27 2020 +0200
3.3 @@ -6,7 +6,7 @@
3.4 signature CALCULATION =
3.5 sig
3.6 type T
3.7 - val get_current_formula: T -> term
3.8 + val current_formula: T -> term
3.9
3.10 end
3.11
3.12 @@ -16,11 +16,11 @@
3.13 (**)
3.14 type T = Ctree.state
3.15
3.16 -fun get_current_formula (pt, (p, p_)) =
3.17 +fun current_formula (pt, (p, p_)) =
3.18 case p_ of
3.19 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
3.20 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
3.21 - | _ => TermC.empty (*on PblObj is fo <> ifo*);
3.22 + | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
3.23
3.24 (**)end(**)
3.25
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 12:13:20 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 15:41:27 2020 +0200
4.3 @@ -4,7 +4,7 @@
4.4
4.5 regular expression for search:
4.6
4.7 -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
4.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|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
4.9
4.10 *)
4.11 signature TACTIC =
4.12 @@ -21,7 +21,6 @@
4.13 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
4.14 | Specify_Theory' of ThyC.id
4.15 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.16 - | CAScmd' of term
4.17 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
4.18 | Check_Postcond' of Problem.id * term
4.19 | Check_elementwise' of term * TermC.as_string * Selem.result
4.20 @@ -55,7 +54,6 @@
4.21 | Specify_Problem of Problem.id
4.22 | Specify_Theory of ThyC.id
4.23 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.24 - | CAScmd of TermC.as_string
4.25 | Calculate of string
4.26 | Check_Postcond of Problem.id
4.27 | Check_elementwise of TermC.as_string
4.28 @@ -121,7 +119,6 @@
4.29 | Specify_Problem of Problem.id
4.30 | Specify_Theory of ThyC.id
4.31 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.32 - | CAScmd of TermC.as_string
4.33 | Calculate of string
4.34 | Check_Postcond of Problem.id
4.35 | Check_elementwise of TermC.as_string
4.36 @@ -172,7 +169,6 @@
4.37
4.38 | Take cterm' => "Take " ^ quote cterm'
4.39 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
4.40 - | CAScmd cterm' => "CAScmd " ^ quote cterm'
4.41
4.42 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
4.43 | Or_to_List => "Or_to_List "
4.44 @@ -210,7 +206,6 @@
4.45
4.46 | Take _ => "Take"
4.47 | Subproblem _ => "Subproblem"
4.48 - | CAScmd _ => "CAScmd"
4.49
4.50 | Check_elementwise _ => "Check_elementwise"
4.51 | Or_to_List => "Or_to_List "
4.52 @@ -324,7 +319,6 @@
4.53 (bool * term) list)) (* individual preconditions marked true/false *)
4.54 | Specify_Theory' of ThyC.id
4.55 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
4.56 - | CAScmd' of term
4.57 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
4.58 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
4.59 Problem.id * (* id of the Problem to be checked *)
4.60 @@ -399,7 +393,6 @@
4.61 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
4.62 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
4.63 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
4.64 - | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
4.65
4.66 | Empty_Tac_ => "Empty_Tac_"
4.67 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"