(* Title:  MathEngine/me-misc.sml

   Author: Walther Neuper

   (c) due to copyright terms

Code from Specify/* to be re-allocated in MathEngine/* and later.

*)

signature MATHENGINE_MISCELLANEOUS =

sig

  val pt_extract : Proof.context -> Calc.T -> Ctree.ptform * Tactic.input option * term list 

  val get_interval : Proof.context -> Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list

(*should be in isac_test*)

  val pt_model: Ctree.ppobj -> Pos.pos_ -> Ctree.ptform

  val pt_form: Ctree.ppobj -> Ctree.ptform

\<^isac_test>\<open>

(**)

\<close>

end

(**)

structure ME_Misc(**): MATHENGINE_MISCELLANEOUS(**) =

struct

(**)

(*T_TESTold* )

fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =

    let

      val (_, _, metID) = Ctree.get_somespec' spec spec'

	    val where_ = if metID = MethodC.id_empty then []

	      else

	        let

	          val {where_rls, where_ = where_, ...} = MethodC.from_store ctxt metID

	          val (_, where_) = Pre_Conds.check ctxt where_rls where_ meth 0

		      in where_ end

	    val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 where_))

    in

      Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)

    end

( *T_TEST**)

fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =

    let

      val (_, _, metID) = Ctree.get_somespec' spec spec'

	    val where_ = if metID = MethodC.id_empty then []

	      else

	        let

	          val {where_rls, where_, model, ...} = MethodC.from_store ctxt metID

	          val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_

              (model, I_Model.OLD_to_TEST meth)

		      in where_ end

	    val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 where_))

    in

      Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)

    end

(*T_TESTnew*)

(*T_TESTold* )

  | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =

    let

      val (_, pI, _) = Ctree.get_somespec' spec spec'

      val where_ = if pI = Problem.id_empty then []

	      else

	        let

	          val {where_rls, where_, ...} = Problem.from_store ctxt pI

	          val (_, where_) = Pre_Conds.check ctxt where_rls where_ probl 0

	        in where_ end

	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))

    in

      Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)

    end

( *T_TEST*)

  | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =

    let

      val (_, pI, _) = Ctree.get_somespec' spec spec'

      val where_ = if pI = Problem.id_empty then []

	      else

	        let

	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI

	          val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_

              (model, I_Model.OLD_to_TEST probl)

	        in where_ end

	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))

    in

      Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)

    end

(*T_TESTnew*)

 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"

fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form

  | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ctxt, ...}) =

    let

      val (dI, pI, _) = Ctree.get_somespec' spec spec'

      val {cas, model, ...} = Problem.from_store ctxt pI

      val env_model = Pre_Conds.environment_TEST model (I_Model.OLD_to_TEST probl)

    in case cas of

      NONE => Ctree.Form (Auto_Prog.pblterm dI pI)

    | SOME t => Ctree.Form (subst_atomic env_model t)

    end

(* pt_extract returns

      # the formula at pos

      # the tactic applied to this formula

      # the list of assumptions generated at this formula

	(by application of another tac to the preceding formula !)

   pos is assumed to come from the frontend, ie. generated by moveDown.

   Notes: cannot be in ctree.sml, because ModSpec has to be calculated. 

   TODO 110417 get assumptions from ctxt !?

*)

fun pt_extract ctxt (pt, ([], Pos.Res)) =

    (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)

    let

      val (f, asm) = Ctree.get_obj Ctree.g_result pt []

    in (Ctree.Form f, NONE, asm) end

  | pt_extract ctxt (pt, (p, Pos.Res)) =

    let

      val (f, asm) = Ctree.get_obj Ctree.g_result pt p

      val tac =

        if Ctree.last_onlev pt p

        then

          if Ctree.is_pblobj' pt (Pos.lev_up p)

          then

            let

              val pI = case Ctree.get_obj I pt (Pos.lev_up p) of

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

              | _ => raise ERROR "pt_extract last_onlev: uncovered case get_obj"

            in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end

		      else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)

		    else

		      let val p' = Pos.lev_on p

		      in

		        if Ctree.is_pblobj' pt p'

		        then

		          let

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

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

		            | _ => raise ERROR "pt_extract \<not>last_onlev: uncovered case get_obj"

		          in SOME (Tactic.Subproblem (dI, pI)) end

		        else

		          if f = Ctree.get_obj Ctree.g_form pt p'

		          then SOME (Ctree.get_obj Ctree.g_tac pt p') (*because this Frm ~~~is not on worksheet*)

		          else SOME (Tactic.Take (UnparseC.term ctxt (Ctree.get_obj Ctree.g_form pt p')))

		      end

    in (Ctree.Form f, tac, asm) end

  | pt_extract ctxt (pt, (p, p_(*Frm,Pbl*))) =

      let

        val ppobj = Ctree.get_obj I pt p

        val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p

        val tac = Ctree.g_tac ppobj

      in (f, SOME tac, []) end

(** get an 'interval' 'from' 'to' of formulae from a ctree **)

(* WN0401 this functionality belongs to ctree.sml *)

fun eq_pos' (p1, Pos.Frm) (p2, Pos.Frm) = p1 = p2

  | eq_pos' (p1, Pos.Res) (p2, Pos.Res) = p1 = p2

  | eq_pos' (p1, Pos.Pbl) (p2, p2_) =

    p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)

  | eq_pos' (p1, Pos.Met) (p2, p2_) =

    p1 = p2 andalso (case p2_ of Pos.Pbl => true | Pos.Met => true | _ => false)

  | eq_pos' _ _ = false;

(* get an 'interval' from the ctree; 'interval' is w.r.t. the 

   total ordering Position#compareTo(Position p) in the java-code

val get_interval = fn :

      pos' ->     : from is "move_up 1st-element" to return

      pos' -> 	  : to the last element to be returned; from < to

      int -> 	    : level: 0 gets the flattest sub-tree possible, 999 the deepest

      ctree -> 	  : 

      (pos' * 	  : of the formula

       Term.term) : the formula

	  list                                                           *)

fun get_interval ctxt from to level pt =

  let

    fun get_inter c (from) (to) lev pt =

	    if eq_pos' from to orelse from = ([], Pos.Res)

	    then

	      let val (f, tacopt, _) = pt_extract ctxt (pt, from)

	      in case f of

	        Ctree.ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)] 

	      | Ctree.Form t => c @ [(from, t, tacopt)]

	      end

	    else 

	      if lev < Pos.lev_of from

	      then (get_inter c (Ctree.move_dn [] pt from) to lev pt)

		      handle (Ctree.PTREE _(*from move_dn too far*)) => c

		    else

		      let

		        val (f, tacopt, _) = pt_extract ctxt (pt, from)

		        val term = case f of

		          Ctree.ModSpec (_,_,headline,_,_,_) => headline

				    | Ctree.Form t => t

		      in (get_inter (c @ [(from, term, tacopt)]) (Ctree.move_dn [] pt from) to lev pt)

		        handle (Ctree.PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]

		      end

  in get_inter [] from to level pt end

(**)end(*struct*)