(* 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

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

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

   val s_add_general: State_Steps.T ->

     Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'

   val add_hard:

     theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out

   val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->

     string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool

   val get_eval: string -> Pos.pos ->Ctree.ctree ->

     string * ThyC.id * (string * Rule_Def.eval_fn)

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

   (*NONE*)                                                     

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

   val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list

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

 end

 (**)

 structure Solve_Step(** ): SOLVE_STEP( **) =

 struct

 (**)

 (** get data from Calc.T **)

 (* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *)

 fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

     (rew_ord', erls, ca)

   | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

     (rew_ord', erls, ca)

   | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

     (rew_ord', erls, ca)

   | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");

 fun get_ruleset _ p pt = 

   let 

     val (pbl, p', rls') = Ctree.parent_node pt p

   in                                                      

     if pbl

     then 

       let 

         val thy' = Ctree.get_obj Ctree.g_domID pt p'

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

 	    in ("OK", thy', rew_ord', erls, false) end

      else 

       let

         val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)

 		    val (rew_ord', erls, _) = rew_info rls'

 		  in ("OK", thy', rew_ord', erls, false) end

   end;

 fun get_eval scrop p pt = 

   let

     val (pbl, p', rls') =  Ctree.parent_node pt p

   in

     if pbl

     then

       let

         val thy' = Ctree.get_obj Ctree.g_domID pt p'

         val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')

         val opt = assoc (scr_isa_fns, scrop)

 	    in

 	      case opt of

 	        SOME isa_fn => ("OK", thy', isa_fn)

 	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))

 	    end

     else 

 		  let

 		    val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);

 		    val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)

 		  in

 		    case assoc (scr_isa_fns, scrop) of

 		      SOME isa_fn => ("OK",thy',isa_fn)

 		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))

 		  end

   end;

 (** Solve_Step.check **)

 (*

   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.Apply_Method mI) (pt, (p, _)) =

       let

         val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of

           Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)

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

         val {where_, ...} = Specify.get_pbt pI

         val pres = map (Model.mk_env probl |> subst_atomic) where_

         val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)

           then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres

           else ctxt

       in

         Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))

       end

   | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =

       let 

         val (msg, thy', isa_fn) = get_eval op_ p pt;

         val f = Calc.current_formula cs;

       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) (_, _) = (*TODO: only applicable, if evaluating to True*)

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

   | check (Tactic.Check_elementwise pred) cs =

       let 

         val f = Calc.current_formula cs;

       in

         Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))

       end

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

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

   | check Tactic.Or_to_List cs =

        let 

         val f = Calc.current_formula cs;

         val ls = Prog_Expr.or2list f;

       in

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

       end

   | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = 

       let

         val (msg, thy', ro, rls', _) = get_ruleset thm p pt;

         val thy = ThyC.get_theory thy';

         val f = Calc.current_formula cs;

       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 ((thm |> fst |> quote) ^ " not applicable") 

         else Applicable.No msg

       end

   | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (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 {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);

         val f = Calc.current_formula cs;

         val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)

       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

   | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =

       let 

         val pp = Ctree.par_pblobj pt p; 

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

         val f = Calc.current_formula cs;

       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 (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (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 = Calc.current_formula cs;

     	  val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)

       in 

         case Rewrite.rewrite_set_inst_ thy 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")

       end

   | check (Tactic.Subproblem (domID, pblID)) (_, _) = 

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

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

    | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =

       let

         val pp = Ctree.par_pblobj pt p

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

         val f = Calc.current_formula cs;

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

 		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)

 		    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) (cs as (pt, (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 = Calc.current_formula cs;

       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) cs =

       Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))

   | 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);

 (** Solve_Step.add **)

 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) = 

     (case topt of 

       SOME t => 

         let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t

         in (pos, c, Generate.EmptyMout, pt) end

     | NONE => (pos, [], Generate.EmptyMout, pt))

   | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)

     let

       val p =

         let val (ps, p') = split_last p (* no connex to prev.ppobj *)

 	      in if p' = 0 then ps @ [1] else p end

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

     in

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

     end

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

     let

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

       val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)

       (* replace the old PrfOjb ~~~~~ *)

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

       val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)

     in

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

     end

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

     (*append after existing PrfObj    vvvvvvvvvvvvv*)

     add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))

   | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =

     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 (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

     let

       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f

         (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;

       val pt = Ctree.update_branch pt p Ctree.TransitiveB

     in

       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

     end

  | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

    let

      val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete

      val pt = Ctree.update_branch pt p Ctree.TransitiveB

    in

     ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

    end

   | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

     let

       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 

         (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete

       val pt = Ctree.update_branch pt p Ctree.TransitiveB

     in

       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

     end

   | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

     let

       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 

         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete

       val pt = Ctree.update_branch pt p Ctree.TransitiveB

     in

       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

     end

   | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =

       let

         val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete

       in

         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)

       end

   | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =

       let

         val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete

       in

         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

       end

   | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =

       let

         val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete

       in

         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

       end

   | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =

       let

         val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete

       in

         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)

       end

   | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =

       let

         val (pt,c) =

           Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete

         in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt) 

         end

   | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =

       let

         val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete

       in

         ((p,Pos.Res), c, Generate.FormKF f', pt)

       end

   | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))

       (l as (_, ctxt)) (pt, (p, _)) =

       let

   	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))

   	      (oris, (domID, pblID, metID), hdl, ctxt_specify)

   	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f

       in

         ((p, Pos.Pbl), c, Generate.FormKF f, pt)

       end

   | add m' _ (_, pos) =

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

 (* LI switches between solve-phase and specify-phase *)

 fun add_general tac ic cs =

   if Tactic.for_specify' tac

   then Specify_Step.add tac ic cs

   else add tac ic cs

 (* the order of State_Steps is reversed: insert last element first  *)

 fun s_add_general [] ptp = ptp

   | s_add_general tacis (pt, c, _) = 

     let

       val (tacis', (_, tac_, (p, is))) = split_last tacis

 	    val (p', c', _, pt') = add_general tac_ is (pt, p)

     in

       s_add_general tacis' (pt', c@c', p')

     end

 (* a still undeveloped concept: do a calculation without LI *)

 fun add_hard _(*thy*) m' (p, p_) pt =

   let  

     val p = case p_ of

       Pos.Frm => p | Pos.Res => Pos.lev_on p

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

   in

     add_general m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))

   end

 (**)end(**);