(* Title:  BaseDefinitions/store.sml

   Author: Walther Neuper

   (c) due to copyright terms

A tree for storing collections of Problem, Method and Thy_Html.

*)

signature STORE_TREE =

sig

  type key

  datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list

(*vvv merge *)

  val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list

(*vvv insert *)

  val insrt: key -> 'a -> string list -> 'a ptyp list -> 'a ptyp list

(*vvv get *)

  val get_py: 'a ptyp list -> key -> (*rev*)key -> 'a

(*vvv update *)

  val update_ptyps: key -> string list -> 'a -> 'a ptyp list -> 'a ptyp list

(*vvv apply *)

  val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> key -> (*rev*)key -> 'b

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

  (*NONE*)

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

  (*NONE*)

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

end

(**)

structure Store(**): STORE_TREE(**) =

struct

(**)

type key = string list; (*will become pblID, methID, theID*)

(*/------- to Store -------\*)

(* A tree for storing data defined in different theories 

  for access from the Interpreter and from dialogue authoring 

  using a string list as key.

  'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)

datatype 'a ptyp =

	Ptyp of string *  (* element of the key                                                        *)

		'a list *       (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)

			                 presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata    *)

		('a ptyp) list; (* the children nodes                                                        *)

(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge

  function for trees / ptyps *)

fun merge_ptyps ([], pt) = pt

  | merge_ptyps (pt, []) = pt

  | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =

      if k = k'

      then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)

      else x' :: merge_ptyps (xs, xs');

fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]

  | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =

    ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ "    k'= " ^ k');*)

    if k = k'

    then ((Ptyp (k', [pbt], ps)) :: pys)

    else  ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))

    )			 

  | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =

    ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)

    if k = k'

    then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)

    else 

      if length pys = 0

      then error ("insert: not found " ^ (strs2str (d(* : pblID*))))

      else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))

    )

  | insrt _ _ _ _ = raise ERROR "";

fun app_py p f (d(*:pblID*)) (k(*:pblRD*)) =

  let

    fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);

    fun app_py' _ [] = py_err ()

      | app_py' [] _ = py_err ()

      | app_py' [k0] ((p' as Ptyp (k', _, _  )) :: ps) =

        if k0 = k' then f p' else app_py' [k0] ps

      | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =

        if k0 = k'' then app_py' ks ps else app_py' k' ps';

  in app_py' k p end;

fun get_py p =

  let

    fun extract_py (Ptyp (_, [py], _)) = py

      | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");

  in app_py p extract_py end;

fun update_ptyps ID _ _ [] =

    error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")

  | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =

    if i = key

    then 

      if length pys = 0

      then ((Ptyp (key, [data], [])) :: pyss)

      else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")

    else py :: update_ptyps ID [i] data pyss

  | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =

    if i = key

    then ((Ptyp (key,  d, update_ptyps ID is data pys)) :: pyss)

    else (py :: (update_ptyps ID (i :: is) data pyss))

  | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";

(*\------- to Store -------/*)

(**)end(**)