(* Title:  calculation abstracted from Ctree

   Author: Walther Neuper 200117

   (c) due to copyright terms

 *)

signature CALCULATION =

sig

  type T

  type result

  val current_formula: T -> term

  val specify_data: T -> Ctree.specify_data

  val solve_data: T -> Ctree.solve_data

  val references: T -> References.T

  type state_pre

  type state_post

\<^isac_test>\<open>

(*val state_pre_empty: state_pre*)

  val state_empty_pre: state_pre

\<close>

(*val state_post_empty: state_post*)

  val state_empty_post: state_post

end

(**)

structure Calc(**): CALCULATION(**) =

struct

(**)

type T = Ctree.state;

type result = (term * term list);

fun current_formula (pt, (p, p_)) =

      case p_ of

        Pos.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_));

fun specify_data (pt, p) =

  case Ctree.get_obj I pt (fst p) of

    Ctree.PblObj specify_data => specify_data

  | _ => raise ERROR "Calc.specify_data called with PrfObj"

fun solve_data (pt, p) =

  case Ctree.get_obj I pt (fst p) of

    Ctree.PrfObj solve_data => solve_data

  | _ => raise ERROR "Calc.solve_data called with PblObj"

fun references (pt, pos as (p, p_)) =

  let

    val (p', _) = if Pos.on_specification pos then pos else (Ctree.par_pblobj pt p, p_)

  in

    References.select_input (#2 (Ctree.get_obj Ctree.g_origin pt p')) (Ctree.get_obj Ctree.g_spec pt p')

  end

(** state to be deleted **)

(*

  These states follow a design which is inadequate for PIDE:

  state_pre holds Calc.T and State_Steps.T to be applied next,

  Calc.state_post holds State_Steps.T which generated the Calc.T.

  This design aimed at observing several Step's, re-do etc --

  this has to be addresses in another layer.

*)

type state_pre = T * State_Steps.T;

\<^isac_test>\<open>

val state_empty_pre = ((Ctree.EmptyPtree, Pos.e_pos'), [State_Steps.single_empty]);

\<close>

type state_post = 

  State_Steps.T * 

  Pos.pos' list * (* a "continuous" sequence deleted by State_Steps.T *)     

  T;

val state_empty_post = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos'));

(**)end(**)