(* Title:  Specify/specify-step.sml

   Author: Walther Neuper

   (c) due to copyright terms

Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.

*)

signature SPECIFY_STEP =

sig

  val check: Tactic.input -> Calc.T -> Applicable.T

  val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*NONE*)                                                     

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  (*NONE*)                                                     

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure Specify_Step(**): SPECIFY_STEP(**) =

struct

(**)

(*

  check tactics (input by the user, mostly) for applicability

  and determine as much of the result of the tactic as possible initially.

*)

fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))

    (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)

  | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))

  | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))

    (*required for corner cases, e.g. test setup in inssort.sml*)

  | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')

  | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')

  | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')

  | check Tactic.Model_Problem (pt, (p, _)) =

      let 

        val pI' = case Ctree.get_obj I pt p of

          Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'

        | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"

	      val {ppc, ...} = Specify.get_pbt pI'

	      val pbl = Generate.init_pbl ppc

      in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end

  | check (Tactic.Refine_Problem pI) (pt, (p, _)) =

      let

        val (dI, dI', itms) = case Ctree.get_obj I pt p of

            Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}

              => (dI, dI', itms)

          | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"

      	val thy = if dI' = ThyC.id_empty then dI else dI';

      in

        case Specify.refine_pbl (ThyC.get_theory thy) pI itms of

          NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")

	      | SOME (rf as (pI', _)) =>

      	   if pI' = pI

      	   then Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")

      	   else Applicable.Yes (Tactic.Refine_Problem' rf)

    end

  | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =

     let 

       val oris = case Ctree.get_obj I pt p of

         Ctree.PblObj {origin = (oris, _, _), ...} => oris

       | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"

     in

       case Specify.refine_ori oris pI of

	       SOME pblID => 

	         Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [(*filled later*)]))

	     | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")

     end

  | check (Tactic.Specify_Method mID) _ =

      Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled later*)], [(*filled later*)]))

  | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =

      let

		    val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of

		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}

		        => (oris, dI, pI, dI', pI', itms)

        | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"

	      val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');

        val {ppc, where_, prls, ...} = Specify.get_pbt pID;

        val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty

          then (false, (Generate.init_pbl ppc, []))

          else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;

       in

         Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))

       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 (_, pos) =

      raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);

(* 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_met pt p met

      in

        (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

      end

  | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 

      (pos, [], Generate.PpcKF (Generate.Upblmet,Specify.itms2itemppc (Proof_Context.theory_of ctxt) [][]),

         case p_ of

           Pos.Pbl => Ctree.update_pbl pt p itmlist

  	     | Pos.Met => Ctree.update_met pt p itmlist

         | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))

  | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 

      (pos, [], (Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] [])),

         case p_ of

           Pos.Pbl => Ctree.update_pbl pt p itmlist

  	     | Pos.Met => Ctree.update_met pt p itmlist

         | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))

  | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = 

      (pos, [],  Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []),

         case p_ of

           Pos.Pbl => Ctree.update_pbl pt p itmlist

  	     | Pos.Met => Ctree.update_met pt p itmlist

         | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))

  | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) = 

      (pos, [] , Generate.PpcKF  (Generate.Upblmet, Specify.itms2itemppc (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_pblID pt p pI

      in

        ((p, Pos.Pbl), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (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_metID pt p mID

      in

        ((p, Pos.Met), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (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_orispec pt p (domID, pIre, metID)

      in

        (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

      end

  | add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =

      let

        val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p

        val pt = Ctree.update_spec pt p (dI, pI, mI)

      in

        (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

      end

  | add (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =

      let

        val (pt, c) = Ctree.cappend_form pt p l t

        val pt = Ctree.update_branch pt p Ctree.TransitiveB

        val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p

        val (pt, c') = Ctree.cappend_form pt p l t

      in

        ((p, Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)

      end

  | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)

      let

        val p' = Pos.lev_up p

        val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete

      in

        ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)

      end

  | add m' _ (_, pos) =

      raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)

(**)end(**);