(* Title: read and write access to the calctree

   Author: Walther Neuper 2017

   (c) due to copyright terms

*)

signature CALC_TREE_ACCESS =

sig

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

  val update_ctxt : CTbasic.ctree -> CTbasic.pos -> Proof.context -> CTbasic.ctree

  val update_env : CTbasic.ctree -> CTbasic.pos -> (Selem.istate * Proof.context) option -> CTbasic.ctree

  val update_domID : CTbasic.ctree -> CTbasic.pos -> Celem.domID -> CTbasic.ctree

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

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

  val update_metID : CTbasic.ctree -> CTbasic.pos -> Celem.metID -> CTbasic.ctree

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

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

  val update_pblID : CTbasic.ctree -> CTbasic.pos -> Celem.pblID -> CTbasic.ctree

  val update_oris : CTbasic.ctree -> CTbasic.pos ->  Model.ori list -> CTbasic.ctree

  val update_orispec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree

  val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree

  val update_tac : CTbasic.ctree -> CTbasic.pos -> Tac.tac -> CTbasic.ctree

  val cappend_form :  CTbasic.ctree ->  CTbasic.pos ->  Selem.istate * Proof.context -> term ->

    CTbasic.ctree *  CTbasic.pos' list

  val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context ->

    Selem.fmz ->  Model.ori list * Celem.spec * term -> CTbasic.ctree * CTbasic.pos' list

  val append_result : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context ->

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

  val append_atomic :                                                          (* for solve.sml *)

     CTbasic.pos -> Selem.istate * Proof.context -> term -> Tac.tac -> Selem.result ->

     CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree

  val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context -> term ->

    Tac.tac -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list

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

  val cappend_parent : CTbasic.ctree -> int list -> Selem.istate * Proof.context -> term ->

    Tac.tac -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list

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

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

    (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option -> CTbasic.ctree

  val append_problem : int list -> Selem.istate * Proof.context -> Selem.fmz ->

    Model.ori list * spec * term -> CTbasic.ctree -> CTbasic.ctree

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

end

(**)

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

struct

(**)

open CTbasic

(* for use by appl_obj *) 

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

      branch, result, ostate}) =

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

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

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

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

      branch, result, ostate}) =

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

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

	     ostate = ostate}

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

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

      branch, result, ostate}) =

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

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

	     ostate = ostate}

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

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

      branch, result, ostate}) =

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

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

	     ostate = ostate}

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

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

      branch, result, ostate}) =

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

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

	     ostate = ostate}

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

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

      branch, result, ostate}) =

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

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

	     ostate = ostate}

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

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

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

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

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

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

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

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

    PrfObj {cell = cell, 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 {cell, origin, fmz, spec, probl, meth,

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

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

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

      ostate = ostate}

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

fun repl_env e (PblObj {cell, origin, fmz, spec, probl, meth,

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

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

      meth = meth, ctxt = ctxt, env = e, loc = loc, branch = branch, result = result,

      ostate = ostate}

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

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

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

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

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

      ostate = ostate}

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

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

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

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

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

      ostate = ostate}

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

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

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

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

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

      ostate = ostate}

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

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

      ostate = ostate}

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

      result, ostate}) =

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

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

      ostate = ostate}

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

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

      result = result, ostate = ostate};

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

fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos; (* for use on PblObj, 

  otherwise use fun generate1; compare fun get_ctxt*)

fun update_env    pt pos x = appl_obj (repl_env    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;

(* called by Take *)

fun append_form p l f pt = 

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

		  branch = NoBranch, result = (Celem.e_term, []), 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;

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

    (Nd (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec = Celem.empty_spec,

	  	probl = [], meth = [], ctxt = Selem.e_ctxt, env = NONE, loc = (SOME l, NONE),

	  	branch = TransitiveB, result = (Celem.e_term, []), ostate = Incomplete}, []))

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

    insert_pt (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec  = Celem.empty_spec,

	   probl = [], meth = [], ctxt = Selem.e_ctxt, env = NONE, loc = (SOME l, NONE),

	   branch = TransitiveB, result = (Celem.e_term, []), 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));

(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)

fun append_parent p l f r b pt = 

  let

    val (ll, f) =

      if existpt p pt andalso Tac.is_empty_tac (get_obj g_tac pt p)

		  then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p) 

		  else ((SOME l, NONE), f)

  in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll,

	   branch = b, result = (Celem.e_term, []), ostate= Incomplete}) pt p

	end;

fun cappend_parent pt p loc f r b =                                          (* for tests only *)

  apfst (append_parent p loc f r b) (cut_tree pt (p, Und));

fun append_atomic p l f r f' s pt = 

  let

    val (iss, f) =

      if existpt p pt andalso Tac.is_empty_tac (get_obj g_tac pt p)

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

		  else ((NONE, SOME l), f)

  in

    insert_pt (PrfObj {cell = NONE, 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 !?!

*)

fun cappend_atomic pt p ist_res f r f' s = 

      if existpt p pt andalso Tac.is_empty_tac (get_obj g_tac pt p)

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

	      let

          val (ist_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 (Selem.e_istate, Selem.e_ctxt) f r f' s pt

	        val pt = update_loc' pt p (SOME ist_form, SOME ist_res)

	      in (pt, cs) end

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

fun append_result pt p l f s =

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

end