(* Title:  Specify/solve-step.sml

   Author: Walther Neuper

   (c) due to copyright terms

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

*)

signature SOLVE_STEP =

sig

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

(* ---- 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 Solve_Step(** ): SOLVE_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.CAScmd ct') _ =

    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))  

  | check (m as Tactic.Calculate op_) (pt, (p, p_)) =

    if member op = [Pos.Pbl, Pos.Met] p_

    then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))

    else

      let 

        val (msg,thy',isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;

        val f = case p_ of

          Frm => Ctree.get_obj Ctree.g_form pt p

    	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

      	| _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

      in

        if msg = "OK"

        then

    	    case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of

    	      SOME (f', (id, thm))

    	        => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))

    	    | NONE => Applicable.No ("'calculate "^op_^"' not applicable") 

        else Applicable.No msg                                              

      end

  | check (Tactic.Check_Postcond pI) (_, (p, p_)) =

      if member op = [Pos.Pbl, Pos.Met] p_                  

      then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))

      else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))

  | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))

    else

      let 

        val pp = Ctree.par_pblobj pt p; 

        val thy' = Ctree.get_obj Ctree.g_domID pt pp;

        val thy = ThyC.get_theory thy'

        val metID = (Ctree.get_obj Ctree.g_metID pt pp)

        val {crls, ...} =  Specify.get_met metID

        val (f, asm) = case p_ of

          Frm => (Ctree.get_obj Ctree.g_form pt p , [])

        | Pos.Res => Ctree.get_obj Ctree.g_result pt p

        | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

        val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;

      in

        Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))

      end

(*RM* )| Derive of Rule_Set.id( *RM*)

  | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"

  | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')        (* always applicable *)

  | check  (Tactic.Apply_Assumption cts') _ =

    raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))

    (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)

  | check Tactic.Or_to_List (pt, (p, p_)) =

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))

    else

      let 

        val f = case p_ of

          Frm => Ctree.get_obj Ctree.g_form pt p

    	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

        | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

      in (let val ls = Prog_Expr.or2list f

          in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end) 

         handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)

      end

  | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) = 

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))

    else

      let

        val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;

        val thy = ThyC.get_theory thy';

        val f = case p_ of

          Frm => Ctree.get_obj Ctree.g_form pt p

	      | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

	      | _ => error ("Solve_Step.check Rewrite: call by " ^ Pos.pos'2str (p, p_));

      in

        if msg = "OK" 

        then

          case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of

            SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))

          | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable") 

        else Applicable.No msg

      end

  | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) = 

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))

    else

      let 

        val pp = Ctree.par_pblobj pt p;

        val thy' = Ctree.get_obj Ctree.g_domID pt pp;

        val thy = ThyC.get_theory thy';

        val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);

        val (f, _) = case p_ of (*p 12.4.00 unnecessary*)

                      Frm => (Ctree.get_obj Ctree.g_form pt p, p)

                    | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)

                    | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

      in 

        let

          val subst = Subst.T_from_input thy subs;

        in

          case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of

            SOME (f',asm) =>

              Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))

          | NONE => Applicable.No ((fst thm'')^" not applicable")

        end

        handle _ => Applicable.No ("syntax error in "^(subs2str subs))

      end

  | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))

    else

      let 

        val pp = Ctree.par_pblobj pt p; 

        val thy' = Ctree.get_obj Ctree.g_domID pt pp;

        val (f, _) = case p_ of

          Frm => (Ctree.get_obj Ctree.g_form pt p, p)

    	  | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)

    	  | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

      in

        case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of

          SOME (f', asm)

            => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))

          | NONE => Applicable.No (rls ^ " not applicable")

      end

  | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (pt, (p, p_)) =

    if member op = [Pos.Pbl, Pos.Met] p_ 

    then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))

    else

      let 

        val pp = Ctree.par_pblobj pt p;

        val thy' = Ctree.get_obj Ctree.g_domID pt pp;

        val thy = ThyC.get_theory thy';

        val (f, _) = case p_ of

          Frm => (Ctree.get_obj Ctree.g_form pt p, p)

    	  | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)

    	  | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

    	  val subst = Subst.T_from_input thy subs;

      in 

        case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of

          SOME (f',asm)

            => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))

        | NONE => Applicable.No (rls ^ " not applicable")

        handle _ => Applicable.No ("syntax error in " ^(subs2str subs))

      end

  | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) = 

     if Pos.on_specification p_

     then

       Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))

     else (*some fields filled later in LI*)

       Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], 

			   TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))

    (*Substitute combines two different kind of "substitution":

      (1) subst_atomic: for ?a..?z

      (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)

  | check (m as Tactic.Substitute sube) (pt, (p, p_)) =

      if member op = [Pos.Pbl, Pos.Met] p_ 

      then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))

      else 

        let

          val pp = Ctree.par_pblobj pt p

          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)

          val f = case p_ of

		        Frm => Ctree.get_obj Ctree.g_form pt p

		      | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

      	  | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

		      val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)

		      val subte = Subst.input_to_terms sube

		      val subst = Subst.T_from_string_eqs thy sube

		      val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

		    in

		      if foldl and_ (true, map TermC.contains_Var subte)

		      then (*1*)

		        let val f' = subst_atomic subst f

		        in if f = f'

		          then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")

		          else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))

		        end

		      else (*2*)

		        case Rewrite.rewrite_terms_ thy ro erls subte f of

		          SOME (f', _) =>  Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))

		        | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")

		    end

  | check (Tactic.Tac id) (pt, (p, p_)) =

    let 

      val pp = Ctree.par_pblobj pt p; 

      val thy' = Ctree.get_obj Ctree.g_domID pt pp;

      val thy = ThyC.get_theory thy';

      val f = case p_ of

         Frm => Ctree.get_obj Ctree.g_form pt p

      | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"

  	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

      | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

    in case id of

      "subproblem_equation_dummy" =>

  	  if TermC.is_expliceq f

  	  then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))

  	  else Applicable.No "applicable only to equations made explicit"

    | "solve_equation_dummy" =>

  	  let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);

  	  in

  	    if id' <> "subproblem_equation_dummy"

  	    then Applicable.No "no subproblem"

  	    else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq

  		    then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))

  		    else error ("Solve_Step.check: f= " ^ f')

      end

    | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))

    end

  | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)

  | check (Tactic.Begin_Trans) (pt, (p, p_)) =

    let

      val (f, _) = case p_ of   (*p 12.4.00 unnecessary, implizit Take in gen*)

        Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)

      | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)

      | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

    in (Applicable.Yes (Tactic.Begin_Trans' f))

      handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds  syntaxerror in '" ^ UnparseC.term f ^ "'")

    end

  | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)

    if p_ = Pos.Res 

	  then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))

    else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"

  | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''

  | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);

(**)end(**);