(* Title: read and write access to the calctree

   Author: Walther Neuper 2017

   (c) due to copyright terms

*)

signature CALC_TREE_ACCESS =

sig

  val get_last_formula: CTbasic.state -> term

  val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree

  val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree

  val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree    (* =vvv= ? *)

  val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)

  val update_metID : CTbasic.ctree -> Pos.pos -> Method.id -> CTbasic.ctree

  val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree    (* =vvv= ? *)

  val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.itm list -> CTbasic.ctree (* =^^^= ? *)

  val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree

  val update_oris : CTbasic.ctree -> Pos.pos ->  Model_Def.ori list -> CTbasic.ctree

  val update_orispec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree

  val update_spec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree

  val update_tac : CTbasic.ctree -> Pos.pos -> Tactic.input -> CTbasic.ctree

  (* original write access *)

  val cappend_form :  CTbasic.ctree ->  Pos.pos ->  Istate_Def.T * Proof.context -> term ->

    CTbasic.ctree *  Pos.pos' list

  val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->

    Celem.fmz -> Model_Def.ori list * Spec.T * term * Proof.context

    -> CTbasic.ctree * Pos.pos' list

  val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context

    -> CTbasic.ctree * Pos.pos' list

  val append_atomic :                                                          (* for solve.sml *)

     Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->

       term -> Tactic.input -> Celem.result -> CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree

  val cappend_atomic : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->

    Tactic.input -> Celem.result -> CTbasic.ostate -> CTbasic.ctree * Pos.pos' list

  val append_result : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->

    Celem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list

  val update_loc' : CTbasic.ctree -> Pos.pos ->

    (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree

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

  (*NONE*)

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

  val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree

  val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Celem.fmz ->

    Model_Def.ori list * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree

  val update_problem: Pos.pos -> Spec.T * Model_Def.itm list * Model_Def.itm list * Proof.context

    -> CTbasic.ctree -> CTbasic.ctree

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

end

(**)

structure CTaccess(**): CALC_TREE_ACCESS(**) =

struct

(**)

open CTbasic

open Pos

fun get_last_formula (pt, (p, _)) =

  let

    val res = get_obj g_res pt p

  in

    if res = TermC.empty

    then get_obj g_form pt p

    else res

  end

(** update elements of ctree; TODO: TRY TO REPLACE BY cappend_*  **)

(* for use by appl_obj *) 

fun repl_pbl x (PblObj {origin, fmz, spec, probl = _, meth, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = spec, probl= x, meth = meth,

      ctxt = ctxt, loc = loc, branch = branch, result = result, ostate = ostate}

  | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";

fun repl_met x (PblObj {origin, fmz, spec, probl, meth = _, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz= fmz, spec = spec, probl = probl,

	     meth = x, ctxt = ctxt, loc = loc, branch = branch, result = result,

	     ostate = ostate}

  | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";

fun repl_spec x (PblObj {origin, fmz, spec = _, probl, meth, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = x, probl = probl,

	    meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

	     ostate = ostate}                                                            

  | repl_spec  _ _ = raise PTREE "repl_domID takes no PrfObj";

fun repl_domID x (PblObj {origin, fmz, spec = (_, p, m), probl, meth, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec= (x, p, m), probl = probl,

	    meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

	     ostate = ostate}

  | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";

fun repl_pblID x (PblObj {origin, fmz, spec= (d, _, m), probl, meth, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec= (d, x, m), probl = probl,

	    meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

	     ostate = ostate}

  | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";

fun repl_metID x (PblObj {origin, fmz, spec = (d, p,_), probl, meth, ctxt, loc, 

      branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = (d, p, x), probl = probl,

	    meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

	     ostate = ostate}

  | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";

fun repl_result l f' s (PrfObj {form, tac, loc = _, branch, result = _ , ostate = _}) =

    PrfObj {form = form, tac = tac, loc = l, branch = branch, result = f', ostate = s}

  | repl_result l f' s (PblObj {origin, fmz, spec, probl, meth, ctxt, loc = _,

      branch, result = _ , ostate= _}) =

    PblObj {origin = origin, fmz= fmz, spec = spec, probl = probl,

      meth = meth, ctxt = ctxt, loc = l, branch = branch, result = f', ostate = s};

fun repl_tac x (PrfObj {form, tac = _, loc, branch, result, ostate}) =

    PrfObj {form = form, tac = x, loc = loc, branch = branch,

      result = result, ostate = ostate}

  | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";

fun repl_ctxt x (PblObj {origin, fmz, spec, probl, meth,

      ctxt = _, loc, branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = spec, probl = probl,

      meth = meth, ctxt = x, loc = loc, branch = branch, result = result,

      ostate = ostate}

  | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";

fun repl_oris oris (PblObj {origin = (_, spe, hdf),fmz, spec, probl, meth,

      ctxt, loc, branch, result, ostate}) =

    PblObj {origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,

      meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

      ostate = ostate}

  | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";

fun repl_orispec spe (PblObj {origin = (oris, _, hdf), fmz, spec, probl, meth,

      ctxt, loc, branch, result, ostate}) =

    PblObj {origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,

      meth = meth, ctxt = ctxt, loc = loc, branch = branch, result = result,

      ostate = ostate}

  | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";

fun repl_loc l (PblObj {origin, fmz, spec, probl, meth,

      ctxt, loc = _ , branch, result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = spec, probl = probl,

      meth = meth, ctxt = ctxt, loc = l, branch = branch, result = result,

      ostate = ostate}

  | repl_loc l (PrfObj {form, tac, loc = _, branch, result, ostate}) =

       PrfObj {form = form, tac = tac, loc= l, branch = branch, result = result,

      ostate = ostate}

fun repl_branch b (PblObj {origin, fmz, spec, probl, meth, ctxt, loc, branch = _,

      result, ostate}) =

    PblObj {origin = origin, fmz = fmz, spec = spec, probl = probl,

      meth = meth, ctxt = ctxt, loc = loc, branch = b, result = result,

      ostate = ostate}

  | repl_branch b (PrfObj {form, tac, loc, branch = _, result, ostate}) =

    PrfObj {form = form, tac = tac, loc = loc, branch = b,

      result = result, ostate = ostate};

(** update elements of ctree; a second!!! interface for writing **)

fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;

fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;

fun update_met    pt pos x = appl_obj (repl_met    x) pt pos;

fun update_metppc pt pos x = appl_obj (repl_met    x) pt pos;		   

fun update_metID  pt pos x = appl_obj (repl_metID  x) pt pos;

fun update_pbl    pt pos x = appl_obj (repl_pbl    x) pt pos;

fun update_pblppc pt pos x = appl_obj (repl_pbl    x) pt pos;

fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;

fun update_oris   pt pos x = appl_obj (repl_oris   x) pt pos;

fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;

fun update_spec   pt pos x = appl_obj (repl_spec   x) pt pos;

fun update_tac    pt pos x = appl_obj (repl_tac    x) pt pos;

fun update_loc'   pt pos x = appl_obj (repl_loc    x) pt pos;

(** add steps to the ctree; THIS PROBABLY SHOULD BE THE ONLY WRITE ACCESS **)

(* insert a term into the Ctree, which waits for application of a Tactic to complete a step*)

fun append_form p l f pt = 

  insert_pt (PrfObj {form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE),

		  branch = NoBranch, result = (TermC.empty, []), ostate = Incomplete}) pt p;

fun cappend_form pt p loc f =

  let

    val (pt', cs) = cut_tree pt (p, Frm)

    val pt'' = append_form p loc f pt'

  in (pt'', cs) end;

(* insert a complete step with term, Tactic and result into the Ctree*)

fun append_atomic p (ic_form, ic_res) f r f' s pt = 

  let

    val (iss, f) =

      if existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p)

      (* ^^^^^^^   ^^ probably is cut, so this     ^^^^^^^^^^^^^^^^^^ might cause

          exception PTREE "get_obj: pos = ... does not exist", (!) WHICH IS NOT RECOGNISED BY if *)

		  then ((fst (get_obj g_loc pt p), SOME ic_res), get_obj g_form pt p) (*after Take*)

		  else ((ic_form, SOME ic_res), f)

  in

    insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,

		   result = f', ostate = s}) pt p

  end;

(* 20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:

   detail - generate - cappend: inserted, not appended !!!

   cut decided in applicable_in !?! and represented by flag ? *)

fun cappend_atomic pt p ic_res f r f' s = 

  if existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p)

  then (*after Take: transfer Frm and respective istate*)

	  let

      val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)

	    val (pt, cs) = cut_tree pt (p, Frm)

	    val pt = append_atomic p (SOME ic_form, ic_res) f r f' s pt

	  in

	    (pt, cs)

	  end

  else apfst (append_atomic p (NONE, ic_res) f r f' s) (cut_tree pt (p, Frm));

(* insert a new SubProblem' and create a new PblObj in the Ctree *)

fun append_problem [] l fmz (strs, spec, hdf, ctxt_specify) _ =

    (Nd (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec = Spec.empty,

	  	probl = [], meth = [], ctxt = ctxt_specify, loc = (SOME l, NONE),

	  	branch = TransitiveB, result = (TermC.empty, []), ostate = Incomplete}, []))

  | append_problem p l fmz (strs, spec, hdf, ctxt_specify) pt =

    insert_pt (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec  = Spec.empty,

	   probl = [], meth = [], ctxt = ctxt_specify, loc = (SOME l, NONE),

	   branch = TransitiveB, result = (TermC.empty, []), ostate= Incomplete}) pt p;

fun cappend_problem _ [] loc fmz ori = (append_problem [] loc fmz ori EmptyPtree, [])

  | cappend_problem pt p loc fmz ori = 

    apfst (append_problem p loc fmz ori) (cut_tree pt (p, Frm));

(* update data in an existing PblObj; ?TODO: delete all Ctree.update_ *)

fun update_problem p (spec, probl, meth, ctxt_specify) pt =

  let

    val (fmz, origin, loc, branch, result, ostate) =

      case get_obj I pt p of

        PblObj {fmz, origin, loc, branch, result, ostate, ...} =>

          (fmz, origin, loc, branch, result, ostate)

      | _ => raise ERROR "update_problem: uncovered case"

  in

    insert_pt (PblObj {origin = origin, fmz = fmz, spec  = spec, probl = probl, meth = meth,

      ctxt = ctxt_specify, loc = loc, branch = branch, result = result, ostate = ostate})

      pt p

  end

(* update a PblObj; cut_tree might be a hack; await intro. of PIDE *)

fun cupdate_problem pt p data =

  let

    val (pt', c') = cut_tree pt (lev_on_total p, Und)

    val (pt'', c'') = cut_tree pt' (lev_dn p, Und)

  in

    (update_problem p data pt'', c' @ c'')

  end

(* append a result from application of a Tactic,

   in case of SubProblem' this is Check_Postcond' *)

fun append_result pt p ist_ctxt f s =

  (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME ist_ctxt) f s) pt p, []);

(**)end(**)