walther@59747: (* Title: Specify/step-specify.sml walther@59747: Author: Walther Neuper 2019 walther@59747: (c) due to copyright terms walther@59747: *) walther@59747: walther@59747: signature STEP_SPECIFY = walther@59747: sig walther@59791: (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*) walther@60020: val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post walther@59981: val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post walther@59975: Walther@60652: val initialise: theory -> Formalise.T -> walther@60114: term * term * References.T * O_Model.T * Proof.context Walther@60652: val initialise': theory -> Formalise.T -> Calc.T * State_Steps.T walther@59747: end walther@59747: walther@59747: (**) walther@59747: structure Step_Specify(**): STEP_SPECIFY(**) = walther@59747: struct walther@59747: (**) walther@59763: open Pos walther@59763: open Ctree walther@59977: open Specification walther@59747: walther@59806: fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) = walther@59763: let Walther@60752: val (oris, ospec, probl, spec, ctxt, meth) = case get_obj I pt p of Walther@60752: PblObj {origin = (oris, ospec, _), probl, spec, ctxt, meth, ...} => (oris, ospec, probl, spec, ctxt, meth) walther@59962: | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj" Walther@60494: val (_, pI, mI) = References.select_input ospec spec Walther@60585: val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI Walther@60771: val pbl = I_Model.init_POS ctxt oris model (* fill in descriptions *) walther@59763: val (pbl, met) = case cas of walther@59763: NONE => (pbl, []) Walther@60771: | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI) Walther@60752: val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met) walther@59933: val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos) walther@60020: in walther@60020: ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) walther@60020: end walther@60021: | by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_Add_ "#Given" ct ptp walther@60021: | by_tactic_input (Tactic.Add_Find ct) ptp = Specify.by_Add_ "#Find" ct ptp walther@60021: | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp walther@60021: walther@60154: (* called with MethodC.id_empty *) walther@59810: | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) = walther@59763: let walther@59763: val (oris, dI, ctxt) = case get_obj I pt p of walther@59763: (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt) walther@59962: | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj" Walther@60742: val opt = Refine.by_o_model ctxt oris pI walther@59763: in walther@59763: case opt of walther@59763: SOME pI' => Walther@60556: let Walther@60585: val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' walther@59763: (*val pt = update_pbl pt p pbl ..done by Model_Problem*) Walther@60585: val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets walther@59763: val (pos, c, _, pt) = walther@59933: Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos) walther@59763: in walther@60020: ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]), walther@60020: (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) walther@59763: end walther@60021: | NONE => ("failure", ([], [], ptp)) walther@59763: end walther@59806: | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) = walther@59763: let walther@59763: val (dI, dI', probl, ctxt) = case get_obj I pt p of walther@59763: PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} => walther@59763: (dI, dI', probl, ctxt) walther@59962: | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj" walther@59879: val thy = if dI' = ThyC.id_empty then dI else dI' walther@59763: in Walther@60676: case Refine.problem (ThyC.get_theory ctxt thy) pI probl of walther@60021: NONE => ("failure", ([], [], ptp)) walther@59763: | SOME rfd => walther@59763: let walther@59933: val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos) walther@59763: in walther@60020: ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, walther@60020: (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) walther@59763: end walther@59763: end walther@60020: | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) = walther@59763: let Walther@60760: val (oris, pI', probl, meth, ctxt) = case get_obj I pt p of Walther@60760: PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, meth, ctxt, ...} => Walther@60760: (oris, pI', probl, meth, ctxt) walther@59962: | _ => raise ERROR "" Walther@60585: val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI Walther@60760: val (check, (i_model, preconds)) = walther@59903: if pI' = Problem.id_empty andalso pI = Problem.id_empty Walther@60771: then (false, (I_Model.OLD_to_POS (I_Model.init model), [])) Walther@60769: else M_Match.by_i_models ctxt oris Walther@60771: (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls) walther@59810: val (c, pt) = Walther@60760: case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of walther@59810: ((_, Pbl), c, _, pt) => (c, pt) walther@59962: | _ => raise ERROR "" walther@59763: in Walther@60760: ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds))), walther@60020: (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))) walther@59763: end walther@60014: | by_tactic_input (Tactic.Specify_Method id) (pt, pos) = walther@59763: let walther@60014: val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos) Walther@60760: val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model)) walther@60014: (Istate_Def.Uistate, ctxt) (pt, pos) walther@60011: in Walther@60760: ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model), walther@60020: (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos))) walther@59763: end walther@59806: | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) = walther@59763: let walther@59763: val ctxt = get_ctxt pt pos walther@60014: val (pos, c, _, pt) = walther@59933: Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos) walther@59763: in (*FIXXXME: check if pbl can still be parsed*) walther@60020: ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, walther@60020: (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))) walther@59763: end walther@59806: | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) = walther@59763: let walther@59763: val ctxt = get_ctxt pt pos walther@59933: val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos) walther@59763: in (*FIXXXME: check if met can still be parsed*) walther@60020: ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, walther@60020: (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))) walther@59763: end Walther@60628: | by_tactic_input m' (ctree, pos) = Walther@60628: let Walther@60628: val ctxt = Ctree.get_ctxt ctree pos Walther@60628: in Walther@60628: raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string ctxt m') Walther@60628: end walther@60020: (**) walther@60020: walther@59806: walther@60015: fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos) = walther@59806: let walther@60015: val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met)) walther@60015: (Istate_Def.Uistate, ContextC.empty) (pt, pos) walther@60015: (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) walther@59806: in walther@59806: ("ok", ([], [], (pt, (p, Pbl)))) walther@59806: end walther@59806: (* called only if no_met is specified *) walther@59806: | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) = walther@59806: let Walther@60585: val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre Walther@60585: val (domID, metID) = (Context.theory_name thy, Walther@60585: if length solve_mets = 0 then MethodC.id_empty Walther@60585: else hd solve_mets) walther@59806: val ((p,_), _, _, pt) = walther@59933: Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) walther@59846: (Istate_Def.Uistate, ContextC.empty) (pt, pos) walther@59806: (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) walther@59806: in walther@59806: ("ok", ([], [], (pt,(p, Pbl)))) walther@59806: end walther@60021: | by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos) = walther@59806: let walther@59806: val ctxt = get_ctxt pt pos walther@59806: val (pos, _, _, pt) = walther@59933: Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos) walther@59806: in walther@60021: ("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd, walther@60021: (pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos))) walther@59806: end Walther@60586: | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (pt, pos as (p, _)) = walther@59806: let walther@59995: val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of walther@59806: PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} => walther@59806: (oris, dI', pI', mI', dI, mI, ctxt, met) walther@59962: | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj" walther@59806: val (p, pt) = Walther@60586: case Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (Istate_Def.Uistate, ctxt) (pt, pos) of walther@59806: ((p, Pbl), _, _, pt) => (p, pt) walther@59962: | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)" walther@59806: in walther@59806: ("ok", ([], [], (pt, (p, Pbl)))) walther@59806: end walther@60014: | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) = walther@59806: let walther@60014: val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos) Walther@60760: val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model)) walther@60014: (Istate_Def.Uistate, ctxt) (pt, pos) walther@60011: in walther@59806: ("ok", ([], [], (pt, pos))) walther@60014: end walther@60016: | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_Add_ "#Given" ct (pt, p) walther@60016: | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p) walther@60016: | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p) walther@60020: (*strange old code, redes*) walther@60015: | by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) = walther@59806: let walther@59806: val p_ = case p_ of Met => Met | _ => Pbl walther@60015: val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_)) walther@59806: in walther@60015: if domID = dI then walther@60015: ("ok", ([], [], (pt, (p, p_)))) Walther@60586: else (*FIXME: check model wrt. (new!) domID ..? still parsable?*) walther@59806: let walther@60015: val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID) walther@60015: (Istate_Def.Uistate, ctxt) (pt, (p, p_)) walther@59806: in walther@59806: ("ok", ([], [], (pt, (p, p_)))) walther@59990: end walther@59806: end walther@59806: | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def" walther@59806: Walther@60556: (* create a calc-tree with oris via a cas.refined pbl *) Walther@60652: (* initialise <-?-> initialise' *) Walther@60652: fun initialise thy (fmz, (_, pI, mI)) = walther@60150: let Walther@60576: val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) walther@60150: val (pI, (pors, pctxt), mI) = walther@60150: if mI = ["no_met"] walther@60150: then walther@60150: let Walther@60653: val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; Walther@60742: val pI' = Refine.by_o_model' pctxt pors pI; Walther@60651: in (pI', (pors (*refinement over models with diff.precond only*), pctxt), Walther@60651: (hd o #solve_mets o Problem.from_store ctxt) pI') Walther@60651: end Walther@60651: else Walther@60651: let Walther@60653: val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; Walther@60651: in (pI, (pors, pctxt), mI) end; Walther@60651: val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) Walther@60651: val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy')) Walther@60651: val hdl = case cas of Walther@60651: NONE => Auto_Prog.pblterm dI pI Walther@60651: | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t Walther@60651: val hdlPIDE = case cas of Walther@60651: NONE => Auto_Prog.pblterm dI pI Walther@60651: | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t Walther@60651: in Walther@60651: (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) Walther@60651: end; Walther@60652: (*TODO: HOW RELATES initialise' \ initialise *) Walther@60652: fun initialise' thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) Walther@60651: if pI <> [] Walther@60651: then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) Walther@60651: let Walther@60651: val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI Walther@60651: val dI = if dI = "" then Context.theory_name thy else dI Walther@60651: val mI = if mI = [] then hd solve_mets else mI Walther@60651: val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t Walther@60651: val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI)) Walther@60651: ([], (dI,pI,mI), hdl, ContextC.empty) Walther@60651: val pt = update_spec pt [] (dI, pI, mI) Walther@60691: val pits = I_Model.init (*Proof_Context.init_global thy*) model Walther@60651: val pt = update_pbl pt [] pits Walther@60651: in ((pt, ([] , Pbl)), []) end Walther@60651: else Walther@60651: if mI <> [] Walther@60651: then (* from met-browser *) Walther@60651: let Walther@60651: val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI Walther@60651: val dI = if dI = "" then "Isac_Knowledge" else dI Walther@60651: val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) Walther@60651: ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty) Walther@60651: val pt = update_spec pt [] (dI, pI, mI) Walther@60691: val mits = I_Model.init (*Proof_Context.init_global thy*) model Walther@60651: val pt = update_met pt [] mits Walther@60651: in ((pt, ([], Met)), []) end Walther@60651: else (* new example, pepare for interactive modeling *) Walther@60651: let Walther@60651: val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) Walther@60651: ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty) Walther@60651: in ((pt, ([], Pbl)), []) end Walther@60652: | initialise' thy (model, refs) = Walther@60651: let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *) Walther@60652: val (_, hdl, refs, pors, pctxt) = initialise thy (model, refs) Walther@60651: val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) Walther@60651: (model, refs) (pors, refs, hdl, pctxt) Walther@60651: in Walther@60651: ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) Walther@60651: end Walther@60651: walther@59763: (**)end(**)