walther@59984: signature SPECIFY = walther@59763: sig walther@59775: val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input) walther@59990: val do_all: Calc.T -> Calc.T walther@59990: val finish_phase: Calc.T -> Calc.T walther@59990: walther@60002: val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> walther@60002: (Model_Def.m_field * TermC.as_string) option walther@60016: val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post Walther@60578: (*from isac_test for Minisubpbl*) Walther@60575: val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T -> walther@60019: string * (Pos.pos_ * Tactic.input) Walther@60575: val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T -> walther@60019: string * (Pos.pos_ * Tactic.input) Walther@60578: Walther@60578: \<^isac_test>\ Walther@60578: (**) wenzelm@60223: \ walther@59763: end walther@59763: walther@59763: (**) walther@59984: structure Specify(**): SPECIFY(**) = walther@59763: struct walther@59763: (**) walther@59763: walther@59990: (* walther@59990: select an item in oris, notyet input in itms walther@59990: (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc) walther@60011: args of item_to_add walther@59990: thy : for? walther@59990: oris: from formalization 'type fmz', structured for efficient access walther@59990: pbt : the problem-pattern to be matched with oris in order to get itms walther@59990: itms: already input items walther@59990: *) walther@60002: fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*) walther@60002: let Walther@60477: fun test_d d (i, _, _, _, itm_) = (d = (I_Model.descriptor itm_)) andalso i <> 0 walther@60002: fun is_elem itms (_, (d, _)) = walther@60002: case find_first (test_d d) itms of SOME _ => true | NONE => false walther@60002: in walther@60002: case filter_out (is_elem itms) pbt of walther@60002: (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, [])) walther@60002: | _ => NONE walther@60002: end walther@60004: (* m_field is in ------vvvv *) walther@60002: | item_to_add thy oris _ itms = walther@60002: let walther@60017: fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef" walther@60017: fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v walther@60017: fun test_id ids r = member op= ids (#1 (r : O_Model.single)) walther@60002: fun test_subset itm (_, _, _, d, ts) = Walther@60477: (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts) walther@60002: fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false walther@60002: | false_and_not_Sup (_, _, false, _, _) = true walther@60002: | false_and_not_Sup _ = false Walther@60705: val v = if itms = [] then 1 else Pre_Conds.max_variant itms walther@60011: val vors = if v = 0 then oris else filter (testr_vt v) oris walther@60002: val vits = walther@60002: if v = 0 walther@60002: then itms (* because of dsc without dat *) walther@60002: else filter (testi_vt v) itms; (* itms..vat *) walther@60002: val icl = filter false_and_not_Sup vits; (* incomplete *) walther@60002: in walther@60002: if icl = [] then walther@60002: case filter_out (test_id (map #1 vits)) vors of walther@60002: [] => NONE Walther@60469: | miss => SOME (O_Model.get_field_term thy (hd miss)) walther@60002: else walther@60002: case find_first (test_subset (hd icl)) vors of walther@60011: NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt" Walther@60477: | SOME ori => SOME (I_Model.get_field_term thy ori (hd icl)) walther@60002: end walther@60002: walther@60019: walther@60019: (** find a next step in the specify-phase **) walther@60021: (* Walther@60575: here should be mutual recursion between for_problem ctxt and for_method walther@60021: *) Walther@60575: fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = walther@59763: let walther@60019: val cpI = if pI = Problem.id_empty then pI' else pI; walther@60154: val cmI = if mI = MethodC.id_empty then mI' else mI; Walther@60585: val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; Walther@60586: val {model = mpc, ...} = MethodC.from_store ctxt cmI Walther@60741: val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); walther@60019: in walther@60021: if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then walther@60019: ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) walther@60019: else if pI' = Problem.id_empty andalso pI = Problem.id_empty then walther@60019: ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) walther@60019: else walther@60019: case find_first (I_Model.is_error o #5) pbl of walther@60019: SOME (_, _, _, fd, itm_) => Walther@60676: ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory ctxt walther@60019: (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) walther@60019: | NONE => Walther@60676: (case item_to_add (ThyC.get_theory ctxt Walther@60578: (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of walther@60019: SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct')) walther@60019: | NONE => (*pbl-items complete*) walther@60019: if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI')) Walther@60726: (*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*) walther@60019: else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) walther@60019: else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) walther@60154: else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI')) walther@60019: else walther@60019: case find_first (I_Model.is_error o #5) met of walther@60019: SOME (_, _, _, fd, itm_) => Walther@60676: ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_)) walther@60019: | NONE => Walther@60676: (case item_to_add (ThyC.get_theory ctxt dI) oris mpc met of walther@60019: SOME (fd, ct') => Walther@60586: ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*) walther@60021: | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))) walther@60019: end walther@60019: Walther@60706: fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (_, met) = walther@60019: let walther@60154: val cmI = if mI = MethodC.id_empty then mI' else mI; Walther@60586: val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; Walther@60741: val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met); walther@60019: in walther@60019: (case find_first (I_Model.is_error o #5) met of walther@60019: SOME (_,_,_, fd, itm_) => Walther@60676: ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt Walther@60578: (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) walther@60019: | NONE => Walther@60676: case item_to_add (ThyC.get_theory ctxt Walther@60578: (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of walther@60019: SOME (fd, ct') => walther@60019: ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*) walther@60019: | NONE => walther@60019: (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI')) walther@60019: else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI')) walther@60019: else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI)) walther@60019: else ("dummy", (Pos.Met, Tactic.Apply_Method mI)))) walther@60019: end walther@60019: walther@60019: (* walther@60019: on finding a next step switching from problem to method or vice versa is possible, walther@60019: because the user is free to switch and edit the respective models independently. walther@60019: TODO: this free switch is NOT yet implemented; e.g. Walther@60575: preok is relevant for problem + method, i.e. in for_problem ctxt + for_method walther@60019: *) walther@60019: fun find_next_step (pt, pos as (_, p_)) = walther@60019: let walther@60019: val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, walther@60019: spec = refs, ...} = Calc.specify_data (pt, pos); Walther@60556: val ctxt = Ctree.get_ctxt pt pos walther@60011: in walther@60019: if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then walther@60011: case mI' of walther@60011: ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI')) walther@60011: | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem)) walther@60019: else if p_ = Pos.Pbl then Walther@60575: for_problem ctxt oris (o_refs, refs) (pbl, met) walther@60011: else Walther@60575: for_method ctxt oris (o_refs, refs) (pbl, met) walther@60019: end walther@60019: walther@60019: walther@60021: (** tools **) walther@59763: Walther@60556: fun by_Add_ m_field ct (pt, pos as (_, p_)) = walther@60016: let walther@60097: val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos) walther@60016: val (i_model, m_patt) = walther@60016: if p_ = Pos.Met then walther@60016: (met, Walther@60586: (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model) walther@60016: else walther@60016: (pbl, Walther@60585: (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model) walther@60016: in walther@60016: case I_Model.check_single ctxt m_field oris i_model m_patt ct of walther@60016: I_Model.Add i_single => (*..union old input *) walther@60016: let walther@60016: val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model Walther@60477: val tac' = I_Model.make_tactic m_field (ct, i_model') walther@60016: val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos) walther@60016: in Walther@60611: ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))], walther@60021: [], (pt', pos))) walther@60016: end walther@60016: | I_Model.Err msg => (msg, ([], [], (pt, pos))) walther@60016: end walther@59990: walther@59990: (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris walther@59990: + met from fmz; assumes pos on PblObj, meth = [] *) walther@59990: fun finish_phase (pt, pos as (p, p_)) = walther@59990: let walther@59990: val _ = if p_ <> Pos.Pbl walther@59990: then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos) walther@59990: else () walther@59990: val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of walther@59990: Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec) walther@59990: | _ => raise ERROR "finish_phase: unvered case get_obj" Walther@60494: val (_, pI, mI) = References.select_input ospec spec Walther@60556: val ctxt = Ctree.get_ctxt pt pos Walther@60586: val mpc = (#model o MethodC.from_store ctxt) mI Walther@60586: val model = (#model o Problem.from_store ctxt) pI Walther@60586: val (pits, mits) = I_Model.complete_method (oris, mpc, model, probl) walther@59990: val pt = Ctree.update_pblppc pt p pits walther@59990: val pt = Ctree.update_metppc pt p mits walther@59990: in (pt, (p, Pos.Met)) end Walther@60556: Walther@60654: (* Walther@60654: do all specification in one single step: Walther@60654: bypass completion of Problem.model and go immediately for MethodC: I_Model.complete' walther@59990: *) Walther@60654: fun do_all (pt, (*old* )pos as( *old*) (p, _)) = walther@59990: let Walther@60654: val (o_model, o_refs as (_, _, met_id), ctxt) = case Ctree.get_obj I pt p of Walther@60654: Ctree.PblObj {origin = (o_model, o_refs, _), ctxt, ...} Walther@60654: => (o_model, o_refs, ctxt) walther@59990: | _ => raise ERROR "do_all: uncovered case get_obj" Walther@60654: val mod_pat = MethodC.from_store ctxt met_id |> #model Walther@60654: val i_model = map (I_Model.complete' mod_pat) o_model Walther@60654: (*no parse, ^^^ takes existing terms; ctxt already created by O_Model.init*) Walther@60654: val (pt, _) = Ctree.cupdate_problem pt p (o_refs, i_model, i_model, ctxt) walther@59990: in walther@59990: (pt, (p, Pos.Met)) walther@59990: end walther@59990: walther@59946: (**)end(**)