1.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Sat May 02 15:41:27 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Sat May 02 16:34:42 2020 +0200
1.3 @@ -67,6 +67,7 @@
1.4 handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, [])
1.5
1.6 fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
1.7 +(*TODO: input requires parse _: _ -> _ option*)
1.8 fun T_from_input thy input = (input
1.9 |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
1.10 |> map TermC.isapair2pair
1.11 @@ -74,8 +75,9 @@
1.12 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
1.13 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
1.14
1.15 +val eqs_to_input = map UnparseC.term;
1.16 +(*TODO: input requires parse _: _ -> _ option*)
1.17 val input_to_terms = map TermC.str2term;
1.18 -val eqs_to_input = map UnparseC.term;
1.19
1.20 fun program_to_input sub = (sub
1.21 |> HOLogic.dest_list
2.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 15:41:27 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 16:34:42 2020 +0200
2.3 @@ -34,7 +34,7 @@
2.4 case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
2.5 SOME (f', (id, thm))
2.6 => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
2.7 - | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
2.8 + | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")
2.9 else Applicable.No msg
2.10 end
2.11 | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
2.12 @@ -46,47 +46,40 @@
2.13 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
2.14 end
2.15 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
2.16 - | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
2.17 - | check Tactic.Or_to_List (pt, (p, p_)) =
2.18 + | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
2.19 + | check Tactic.Or_to_List cs =
2.20 let
2.21 - val f = case p_ of
2.22 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
2.23 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.24 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.25 - in (let val ls = Prog_Expr.or2list f
2.26 - in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
2.27 - handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
2.28 + val f = Calc.current_formula cs;
2.29 + val ls = Prog_Expr.or2list f;
2.30 + in
2.31 + Applicable.Yes (Tactic.Or_to_List' (f, ls))
2.32 end
2.33 - | check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) =
2.34 + | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
2.35 let
2.36 - val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
2.37 + val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;
2.38 val thy = ThyC.get_theory thy';
2.39 val f = Calc.current_formula cs;
2.40 in
2.41 if msg = "OK"
2.42 then
2.43 - case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
2.44 - SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
2.45 - | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
2.46 + case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
2.47 + SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
2.48 + | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
2.49 else Applicable.No msg
2.50 end
2.51 - | check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) =
2.52 + | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =
2.53 let
2.54 val pp = Ctree.par_pblobj pt p;
2.55 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.56 val thy = ThyC.get_theory thy';
2.57 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
2.58 val f = Calc.current_formula cs;
2.59 + val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
2.60 in
2.61 - let
2.62 - val subst = Subst.T_from_input thy subs;
2.63 - in
2.64 - case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
2.65 - SOME (f',asm) =>
2.66 - Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
2.67 - | NONE => Applicable.No ((fst thm'')^" not applicable")
2.68 - end
2.69 - handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
2.70 + case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
2.71 + SOME (f', asm) =>
2.72 + Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
2.73 + | NONE => Applicable.No (fst thm ^ " not applicable")
2.74 end
2.75 | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
2.76 let
2.77 @@ -99,37 +92,29 @@
2.78 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
2.79 | NONE => Applicable.No (rls ^ " not applicable")
2.80 end
2.81 - | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =
2.82 - if member op = [Pos.Pbl, Pos.Met] p_
2.83 - then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
2.84 - else
2.85 + | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
2.86 let
2.87 val pp = Ctree.par_pblobj pt p;
2.88 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.89 val thy = ThyC.get_theory thy';
2.90 val f = Calc.current_formula cs;
2.91 - val subst = Subst.T_from_input thy subs;
2.92 + val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
2.93 in
2.94 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
2.95 SOME (f', asm)
2.96 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
2.97 | NONE => Applicable.No (rls ^ " not applicable")
2.98 - handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
2.99 end
2.100 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
2.101 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
2.102 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
2.103 -
2.104 - (*Substitute combines two different kind of "substitution":
2.105 - (1) subst_atomic: for ?a..?z
2.106 - (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
2.107 - | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
2.108 + | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
2.109 let
2.110 val pp = Ctree.par_pblobj pt p
2.111 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
2.112 val f = Calc.current_formula cs;
2.113 val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
2.114 - val subte = Subst.input_to_terms sube
2.115 + val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
2.116 val subst = Subst.T_from_string_eqs thy sube
2.117 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
2.118 in
2.119 @@ -146,37 +131,30 @@
2.120 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
2.121 end
2.122 | check (Tactic.Tac id) (cs as (pt, (p, _))) =
2.123 - let
2.124 - val pp = Ctree.par_pblobj pt p;
2.125 - val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.126 - val thy = ThyC.get_theory thy';
2.127 - val f = Calc.current_formula cs;
2.128 - in case id of
2.129 - "subproblem_equation_dummy" =>
2.130 - if TermC.is_expliceq f
2.131 - then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
2.132 - else Applicable.No "applicable only to equations made explicit"
2.133 - | "solve_equation_dummy" =>
2.134 - let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
2.135 - in
2.136 - if id' <> "subproblem_equation_dummy"
2.137 - then Applicable.No "no subproblem"
2.138 - else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
2.139 - then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
2.140 - else error ("Solve_Step.check: f= " ^ f')
2.141 + let
2.142 + val pp = Ctree.par_pblobj pt p;
2.143 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
2.144 + val thy = ThyC.get_theory thy';
2.145 + val f = Calc.current_formula cs;
2.146 + in case id of
2.147 + "subproblem_equation_dummy" =>
2.148 + if TermC.is_expliceq f
2.149 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
2.150 + else Applicable.No "applicable only to equations made explicit"
2.151 + | "solve_equation_dummy" =>
2.152 + let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
2.153 + in
2.154 + if id' <> "subproblem_equation_dummy"
2.155 + then Applicable.No "no subproblem"
2.156 + else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
2.157 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
2.158 + else error ("Solve_Step.check: f= " ^ f')
2.159 + end
2.160 + | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
2.161 end
2.162 - | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
2.163 - end
2.164 | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
2.165 - | check (Tactic.Begin_Trans) (pt, (p, p_)) =
2.166 - let
2.167 - val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
2.168 - Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
2.169 - | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
2.170 - | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
2.171 - in (Applicable.Yes (Tactic.Begin_Trans' f))
2.172 - handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
2.173 - end
2.174 + | check (Tactic.Begin_Trans) cs =
2.175 + Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
2.176 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
2.177 if p_ = Pos.Res
2.178 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))