walther@59920: (* Title: Specify/solve-step.sml walther@59920: Author: Walther Neuper walther@59920: (c) due to copyright terms walther@59920: walther@59920: Code for the solve-phase in analogy to structure Specify_Step for the specify-phase. walther@59920: *) walther@59920: walther@59920: signature SOLVE_STEP = walther@59920: sig walther@59921: val check: Tactic.input -> Calc.T -> Applicable.T walther@59959: val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T walther@59935: walther@59959: val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T walther@59932: val s_add_general: State_Steps.T -> walther@59932: Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' walther@59933: val add_hard: walther@59959: theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T walther@59932: walther@59935: val get_ruleset: 'a -> Pos.pos -> Ctree.ctree -> Walther@60509: string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool walther@59935: val get_eval: string -> Pos.pos ->Ctree.ctree -> walther@59935: string * ThyC.id * (string * Rule_Def.eval_fn) wenzelm@60223: \<^isac_test>\ walther@59935: val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list wenzelm@60223: \ walther@59920: end walther@59920: walther@59920: (**) walther@59996: structure Solve_Step(**): SOLVE_STEP(**) = walther@59920: struct walther@59920: (**) walther@59920: walther@59935: (** get data from Calc.T **) walther@59935: walther@59935: (* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *) walther@59935: fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = walther@59935: (rew_ord', erls, ca) walther@59935: | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = walther@59935: (rew_ord', erls, ca) walther@59935: | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = walther@59935: (rew_ord', erls, ca) walther@59962: | rew_info rls = raise ERROR ("rew_info called with '" ^ Rule_Set.id rls ^ "'"); walther@59935: walther@59935: fun get_ruleset _ p pt = walther@59935: let walther@59935: val (pbl, p', rls') = Ctree.parent_node pt p walther@59935: in walther@59935: if pbl walther@59935: then walther@59935: let walther@59935: val thy' = Ctree.get_obj Ctree.g_domID pt p' walther@60154: val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p') walther@59935: in ("OK", thy', rew_ord', erls, false) end walther@59935: else walther@59935: let walther@59935: val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p) walther@59935: val (rew_ord', erls, _) = rew_info rls' walther@59935: in ("OK", thy', rew_ord', erls, false) end walther@59935: end; walther@59935: walther@59935: fun get_eval scrop p pt = walther@59935: let walther@59935: val (pbl, p', rls') = Ctree.parent_node pt p walther@59935: in walther@59935: if pbl walther@59935: then walther@59935: let walther@59935: val thy' = Ctree.get_obj Ctree.g_domID pt p' walther@60154: val {calc = scr_isa_fns, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p') walther@59935: val opt = assoc (scr_isa_fns, scrop) walther@59935: in walther@59935: case opt of walther@59935: SOME isa_fn => ("OK", thy', isa_fn) walther@59935: | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn)) walther@59935: end walther@59935: else walther@59935: let walther@59935: val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p); walther@59935: val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) walther@59935: in walther@59935: case assoc (scr_isa_fns, scrop) of walther@59935: SOME isa_fn => ("OK",thy',isa_fn) walther@59935: | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn)) walther@59935: end walther@59935: end; walther@59935: walther@59935: (** Solve_Step.check **) walther@59935: walther@59922: (* walther@59922: check tactics (input by the user, mostly) for applicability walther@59922: and determine as much of the result of the tactic as possible initially. walther@59922: *) walther@59932: fun check (Tactic.Apply_Method mI) (pt, (p, _)) = walther@59932: let walther@59932: val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of walther@59932: Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) walther@59932: | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj" walther@59970: val {where_, ...} = Problem.from_store pI Walther@60477: val pres = map (I_Model.environment probl |> subst_atomic) where_ walther@59932: val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) walther@59932: then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres walther@59932: else ctxt walther@59932: in walther@59932: Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt)) walther@59932: end walther@59932: | check (Tactic.Calculate op_) (cs as (pt, (p, _))) = walther@59923: let walther@59935: val (msg, thy', isa_fn) = get_eval op_ p pt; walther@59928: val f = Calc.current_formula cs; walther@59923: in walther@59923: if msg = "OK" walther@59923: then Walther@60500: case Rewrite.calculate_ (ThyC.id_to_ctxt thy') isa_fn f of walther@59923: SOME (f', (id, thm)) walther@59923: => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm)))) walther@59929: | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable") walther@59923: else Applicable.No msg walther@59923: end walther@59928: | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*) walther@59928: Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty)) walther@59928: | check (Tactic.Check_elementwise pred) cs = walther@59923: let walther@59928: val f = Calc.current_formula cs; walther@59923: in walther@59928: Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, []))) walther@59923: end walther@59923: | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" walther@59929: | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve') walther@59929: | check Tactic.Or_to_List cs = walther@59928: let walther@59929: val f = Calc.current_formula cs; walther@59929: val ls = Prog_Expr.or2list f; walther@59929: in walther@59929: Applicable.Yes (Tactic.Or_to_List' (f, ls)) walther@59923: end walther@59929: | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = walther@59923: let walther@59935: val (msg, thy', ro, rls', _) = get_ruleset thm p pt; Walther@60506: val thy = ThyC.get_theory thy'; Walther@60506: val ctxt = Proof_Context.init_global thy; walther@59928: val f = Calc.current_formula cs; walther@59923: in walther@59923: if msg = "OK" walther@59923: then Walther@60506: case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of walther@59929: SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm))) walther@59929: | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") walther@59923: else Applicable.No msg walther@59923: end walther@59929: | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = walther@59921: let walther@59921: val pp = Ctree.par_pblobj pt p; walther@59921: val thy' = Ctree.get_obj Ctree.g_domID pt pp; walther@59921: val thy = ThyC.get_theory thy'; Walther@60500: val ctxt = Proof_Context.init_global thy; walther@60154: val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp); walther@59928: val f = Calc.current_formula cs; Walther@60500: val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) walther@59921: in Walther@60506: case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of walther@59929: SOME (f', asm) => walther@59929: Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm))) walther@59929: | NONE => Applicable.No (fst thm ^ " not applicable") walther@59921: end walther@59928: | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) = walther@59921: let walther@59923: val pp = Ctree.par_pblobj pt p; walther@59921: val thy' = Ctree.get_obj Ctree.g_domID pt pp; walther@59928: val f = Calc.current_formula cs; walther@59923: in Walther@60500: case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of walther@59921: SOME (f', asm) walther@59923: => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) walther@59923: | NONE => Applicable.No (rls ^ " not applicable") walther@59921: end walther@59929: | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) = walther@59921: let walther@59921: val pp = Ctree.par_pblobj pt p; walther@59921: val thy' = Ctree.get_obj Ctree.g_domID pt pp; walther@59921: val thy = ThyC.get_theory thy'; Walther@60500: val ctxt = Proof_Context.init_global thy; walther@59928: val f = Calc.current_formula cs; Walther@60500: val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*) walther@59921: in Walther@60500: case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of walther@59928: SOME (f', asm) walther@59921: => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) walther@59921: | NONE => Applicable.No (rls ^ " not applicable") walther@59921: end walther@59928: | check (Tactic.Subproblem (domID, pblID)) (_, _) = walther@60154: Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [], walther@59928: TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) walther@59936: | check (Tactic.Substitute sube) (cs as (pt, (p, _))) = walther@59928: let walther@59928: val pp = Ctree.par_pblobj pt p walther@59928: val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) Walther@60500: val ctxt = Proof_Context.init_global thy; walther@59928: val f = Calc.current_formula cs; walther@60154: val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) walther@59929: val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*) walther@59928: val subst = Subst.T_from_string_eqs thy sube Walther@60506: val ro = assoc_rew_ord thy rew_ord' walther@59928: in walther@59928: if foldl and_ (true, map TermC.contains_Var subte) walther@59928: then (*1*) walther@59928: let val f' = subst_atomic subst f walther@59928: in if f = f' walther@59928: then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") walther@59928: else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) walther@59928: end walther@59928: else (*2*) Walther@60500: case Rewrite.rewrite_terms_ ctxt ro erls subte f of walther@59928: SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) walther@59928: | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") walther@59928: end walther@59928: | check (Tactic.Tac id) (cs as (pt, (p, _))) = walther@59929: let walther@59929: val pp = Ctree.par_pblobj pt p; walther@59929: val thy' = Ctree.get_obj Ctree.g_domID pt pp; walther@59929: val thy = ThyC.get_theory thy'; walther@59929: val f = Calc.current_formula cs; walther@59936: in walther@59936: Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) walther@59921: end walther@59923: | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) walther@59929: | check (Tactic.Begin_Trans) cs = walther@59929: Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs)) walther@59923: | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) walther@59923: if p_ = Pos.Res walther@59923: then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) walther@59923: else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" walther@59921: | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof'' walther@59921: | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m); walther@59920: walther@59935: walther@59935: (** Solve_Step.add **) walther@59935: walther@59932: fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) = walther@59932: (case topt of walther@59932: SOME t => walther@59932: let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t walther@59959: in (pos, c, Test_Out.EmptyMout, pt) end walther@59959: | NONE => (pos, [], Test_Out.EmptyMout, pt)) walther@59932: | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *) walther@59931: let walther@59931: val p = walther@59931: let val (ps, p') = split_last p (* no connex to prev.ppobj *) walther@59931: in if p' = 0 then ps @ [1] else p end walther@59931: val (pt, c) = Ctree.cappend_form pt p l t walther@59931: in walther@59959: ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt) walther@59931: end walther@59931: | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_form pt p l t walther@59931: val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*) walther@59931: (* replace the old PrfOjb ~~~~~ *) walther@59931: val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p walther@59931: val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*) walther@59931: in walther@59959: ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt) walther@59931: end walther@59931: | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) = walther@59931: (*append after existing PrfObj vvvvvvvvvvvvv*) walther@59931: add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm)) walther@59931: | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = walther@59931: let walther@59931: val p' = Pos.lev_up p walther@59931: val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete walther@59931: in walther@59959: ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt) walther@59931: end walther@59931: | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f walther@59931: (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete; walther@59931: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete walther@59931: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f walther@59931: (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete walther@59931: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f walther@59931: (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete walther@59931: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt) walther@59931: end walther@59931: | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) walther@59931: end walther@59931: | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete walther@59931: in walther@59959: ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt) walther@59931: end walther@59931: | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt,c) = walther@59931: Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete walther@59959: in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) walther@59931: end walther@59931: | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) = walther@59931: let walther@59931: val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete walther@59931: in walther@59959: ((p,Pos.Res), c, Test_Out.FormKF f', pt) walther@59931: end walther@59931: | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)) walther@59931: (l as (_, ctxt)) (pt, (p, _)) = walther@59932: let walther@59932: val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID)) walther@59932: (oris, (domID, pblID, metID), hdl, ctxt_specify) walther@60360: val f = Syntax.string_of_term ctxt f walther@59932: in walther@59959: ((p, Pos.Pbl), c, Test_Out.FormKF f, pt) walther@59932: end walther@59932: | add m' _ (_, pos) = walther@59932: raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos) walther@59932: walther@59932: (* LI switches between solve-phase and specify-phase *) walther@59932: fun add_general tac ic cs = walther@59932: if Tactic.for_specify' tac walther@59933: then Specify_Step.add tac ic cs walther@59932: else add tac ic cs walther@59932: walther@59933: (* the order of State_Steps is reversed: insert last element first *) walther@59932: fun s_add_general [] ptp = ptp walther@59932: | s_add_general tacis (pt, c, _) = walther@59931: let walther@59932: val (tacis', (_, tac_, (p, is))) = split_last tacis walther@59933: val (p', c', _, pt') = add_general tac_ is (pt, p) walther@59931: in walther@59932: s_add_general tacis' (pt', c@c', p') walther@59931: end walther@59932: walther@59933: (* a still undeveloped concept: do a calculation without LI *) walther@59933: fun add_hard _(*thy*) m' (p, p_) pt = walther@59933: let walther@59933: val p = case p_ of walther@59933: Pos.Frm => p | Pos.Res => Pos.lev_on p walther@59962: | _ => raise ERROR ("generate_hard: call by " ^ Pos.pos'2str (p,p_)) walther@59933: in walther@59933: add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_)) walther@59933: end walther@59931: walther@59920: (**)end(**);