wneuper/isa: comparison src/Tools/isac/Specify/specify-step.sml

equal deleted inserted replaced

-:439e23525491
+:e3fe057158b2
 val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of
 Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
 	      val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
 	      val pbl = I_Model.init_POS ctxt o_model model_patt
-in Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])) end
+in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
 let
 val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
 Ctree.PblObj {origin = (_, (dI, _, _), _), spec = (dI', _, _), probl = itms, ctxt, ...}
 => (dI, dI', itms, ctxt)
 	val thy = if dI' = ThyC.id_empty then dI else dI';
 in
 case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
 NONE => Applicable.No
 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
-	      | SOME (rf as (pI', _)) =>
+	      | SOME (pI', (i_model, prec)) =>
 	   if pI' = pI
 	   then Applicable.No
 	     (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
-	   else Applicable.Yes (Tactic.Refine_Problem' rf)
+	   else Applicable.Yes (Tactic.Refine_Problem' (pI', (I_Model.OLD_to_POS i_model, prec)))
 end
 | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
 let
 val (oris, ctxt) = case Ctree.get_obj I pt p of
 Ctree.PblObj {origin = (oris, _, _), ctxt, ...} => (oris, ctxt)
 end
 | check (Tactic.Specify_Method mID) (ctree, pos) =
 let
 val (o_model, _, i_model) = complete_for mID (ctree, pos)
 in
-Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model))
+Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
 end
 | check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
 let
 		    val (oris,  pI,  pI', probl, meth, ctxt) = case Ctree.get_obj I pt p of
 		      Ctree.PblObj {origin = (oris, (_, pI, _), _), spec = (_, pI', _), probl, meth, ctxt, ...}
 val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
 then (false, (I_Model.OLD_to_POS (I_Model.init model), []))
 else M_Match.by_i_models ctxt oris
 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls)
 in
-Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (I_Model.TEST_to_OLD i_model, preconds))))
+Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))
 end
 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
 | check tac (ctree, pos) =
 let
 end;
 (* exceed line length, because result type will change *)
 fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
 let
-val pt = Ctree.update_pbl pt p itms
+val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
-	    val pt = Ctree.update_met pt p met
+	    val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD met)
 in
 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
 end
 | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
 case p_ of
-Pos.Pbl => Ctree.update_pbl pt p itmlist
+Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
-	     | Pos.Met => Ctree.update_met pt p itmlist
+	     | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
 | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
 (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
 case p_ of
-Pos.Pbl => Ctree.update_pbl pt p itmlist
+Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
-	     | Pos.Met => Ctree.update_met pt p itmlist
+	     | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
 | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
 (pos, [],  Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
 case p_ of
-Pos.Pbl => Ctree.update_pbl pt p itmlist
+Pos.Pbl => Ctree.update_pbl pt p (I_Model.TEST_to_OLD itmlist)
-	     | Pos.Met => Ctree.update_met pt p itmlist
+	     | Pos.Met => Ctree.update_met pt p (I_Model.TEST_to_OLD itmlist)
 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
 | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
 (pos, [] , Test_Out.PpcKF  (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
 Ctree.update_domID pt p domID)
 | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
 let
-val pt = Ctree.update_pbl pt p itms
+val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD itms)
 val pt = Ctree.update_pblID pt p pI
 in
 ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
 end
 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
 let
 val pt = Ctree.update_oris pt p oris
-val pt = Ctree.update_met pt p itms
+val pt = Ctree.update_met pt p (I_Model.TEST_to_OLD itms)
 val pt = Ctree.update_metID pt p mID
 in
 ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
 end
 | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
 let
-val pt = Ctree.update_pbl pt p pbl
+val pt = Ctree.update_pbl pt p (I_Model.TEST_to_OLD pbl)
 val pt = Ctree.update_orispec pt p (domID, pIre, metID)
 in
 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
 end
 | add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =

changeset 60774	e3fe057158b2
parent 60771	1b072aab8f4e
child 60775	c31ae770d74c