walther@59920: (* Title:  Specify/specify-step.sml
walther@59920:    Author: Walther Neuper
walther@59920:    (c) due to copyright terms
walther@59923:                                                                           
walther@59920: Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.
walther@59920: *)
walther@59920: 
walther@59920: signature SPECIFY_STEP =
walther@59920: sig
walther@59922:   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@60009: 
walther@60154:   val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
walther@59920: end
walther@59920: 
walther@59920: (**)
walther@59920: structure Specify_Step(**): SPECIFY_STEP(**) =
walther@59920: struct
walther@59920: (**)
walther@59920: 
walther@60014: fun complete_for mID (ctree, pos) =
walther@60009:   let
walther@60009:     val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
walther@60009:        ...} = Calc.specify_data (ctree, pos);
Walther@60557:     val ctxt = Ctree.get_ctxt ctree pos
Walther@60494:     val (dI, _, _) = References.select_input o_refs refs;
Walther@60559:     val {ppc = m_patt, pre, prls, ...} = MethodC.from_store ctxt mID
walther@60009:     val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
walther@60009:     val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
Walther@60578:     val thy = ThyC.get_theory_PIDE ctxt dI
walther@60009:     val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
walther@60009:   in
walther@60009:     (o_model', ctxt', i_model)
walther@60009:   end
walther@60009: 
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@59930: fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))
walther@59930:     (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
walther@59930:   | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
walther@59930:   | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
walther@59930:     (*required for corner cases, e.g. test setup in inssort.sml*)
walther@59930:   | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
walther@59930:   | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
walther@59930:   | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
Walther@60556:   | check Tactic.Model_Problem (pt, pos as (p, _)) =
walther@59930:       let 
walther@59930:         val pI' = case Ctree.get_obj I pt p of
walther@59930:           Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
walther@59930:         | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
Walther@60585: 	      val {model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
Walther@60585: 	      val pbl = I_Model.init model
walther@59930:       in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
walther@59930:   | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
walther@59923:       let
walther@59923:         val (dI, dI', itms) = case Ctree.get_obj I pt p of
walther@59923:             Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
walther@59923:               => (dI, dI', itms)
walther@59930:           | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
walther@59923:       	val thy = if dI' = ThyC.id_empty then dI else dI';
walther@59923:       in
walther@59960:         case Refine.problem (ThyC.get_theory thy) pI itms of
walther@59930:           NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
walther@59923: 	      | SOME (rf as (pI', _)) =>
walther@59923:       	   if pI' = pI
walther@59930:       	   then Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
walther@59923:       	   else Applicable.Yes (Tactic.Refine_Problem' rf)
walther@59923:     end
Walther@60556:   | check (Tactic.Refine_Tacitly pI) (pt, pos as (p, _)) =
walther@59930:      let 
walther@59930:        val oris = case Ctree.get_obj I pt p of
walther@59930:          Ctree.PblObj {origin = (oris, _, _), ...} => oris
walther@59930:        | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
Walther@60556:        val ctxt = Ctree.get_ctxt pt pos
walther@59930:      in
Walther@60559:        case Refine.refine_ori ctxt oris pI of
walther@59930: 	       SOME pblID => 
walther@60154: 	         Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, MethodC.id_empty, [(*filled later*)]))
walther@59930: 	     | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")
walther@59930:      end
walther@60009:   | check (Tactic.Specify_Method mID) (ctree, pos) =
walther@60009:       let
walther@60014:         val (o_model, _, i_model) = complete_for mID (ctree, pos)
walther@60009:       in
walther@60009:         Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
walther@60009:       end
Walther@60556:   | check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
walther@59923:       let
Walther@60578: 		    val (oris, dI, pI, dI', pI', itms, ctxt) = case Ctree.get_obj I pt p of
Walther@60578: 		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ctxt, ...}
Walther@60578: 		        => (oris, dI, pI, dI', pI', itms, ctxt)
walther@59930:         | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
Walther@60578: 	      val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
Walther@60585:         val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
walther@59923:         val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
Walther@60585:           then (false, (I_Model.init model, []))
Walther@60585:           else M_Match.match_itms_oris thy itms (model, where_, where_rls) oris;
walther@59923:        in
walther@59930:          Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
walther@59930:        end
walther@59930:   | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
walther@59922:   | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
walther@59922:   | check tac (_, pos) =
walther@59922:       raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
walther@59920: 
walther@59933: (* exceed line length, because result type will change *)
walther@59933: fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
walther@59933:       let
walther@59933:         val pt = Ctree.update_pbl pt p itms
walther@59933:   	    val pt = Ctree.update_met pt p met
walther@59933:       in
walther@59969:         (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
walther@59933:       end
walther@59933:   | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 
walther@59969:       (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
walther@59933:          case p_ of
walther@59933:            Pos.Pbl => Ctree.update_pbl pt p itmlist
walther@59933:   	     | Pos.Met => Ctree.update_met pt p itmlist
walther@59933:          | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
walther@59933:   | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 
walther@59969:       (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
walther@59933:          case p_ of
walther@59933:            Pos.Pbl => Ctree.update_pbl pt p itmlist
walther@59933:   	     | Pos.Met => Ctree.update_met pt p itmlist
walther@59933:          | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
walther@59933:   | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 
walther@59969:       (pos, [],  Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
walther@59933:          case p_ of
walther@59933:            Pos.Pbl => Ctree.update_pbl pt p itmlist
walther@59933:   	     | Pos.Met => Ctree.update_met pt p itmlist
walther@59933:          | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
walther@59933:   | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) = 
walther@59969:       (pos, [] , Test_Out.PpcKF  (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
walther@59933:         Ctree.update_domID pt p domID)
walther@59933:   | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
walther@59933:       let
walther@59933:         val pt = Ctree.update_pbl pt p itms
walther@59933:         val pt = Ctree.update_pblID pt p pI
walther@59933:       in
walther@59969:         ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
walther@59933:       end
walther@59933:   | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
walther@59933:       let
walther@59933:         val pt = Ctree.update_oris pt p oris
walther@59934:         val pt = Ctree.update_met pt p itms                            
walther@59933:         val pt = Ctree.update_metID pt p mID
walther@59933:       in
walther@59969:         ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
walther@59933:       end
walther@59933:   | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) = 
walther@59933:       let
walther@59933:         val pt = Ctree.update_pbl pt p pbl
walther@59933:         val pt = Ctree.update_orispec pt p (domID, pIre, metID)
walther@59933:       in
walther@59969:         (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
walther@59933:       end
walther@59933:   | add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =
walther@59933:       let
walther@59933:         val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p
walther@59933:         val pt = Ctree.update_spec pt p (dI, pI, mI)
walther@59933:       in
walther@59969:         (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
walther@59933:       end
walther@59933:   | add (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =
walther@59933:       let
walther@59933:         val (pt, c) = Ctree.cappend_form pt p l t
walther@59933:         val pt = Ctree.update_branch pt p Ctree.TransitiveB
walther@59933:         val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
walther@59933:         val (pt, c') = Ctree.cappend_form pt p l t
walther@59933:       in
walther@59959:         ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
walther@59933:       end
walther@59933:   | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
walther@59933:       let
walther@59933:         val p' = Pos.lev_up p
walther@59933:         val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
walther@59933:       in
walther@59959:         ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
walther@59933:       end
walther@59933:   | add m' _ (_, pos) =
walther@59933:       raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
walther@59920: 
walther@59920: (**)end(**);