(* Title:  BaseDefinitions/store.sml

   Author: Walther Neuper

   (c) due to copyright terms

A tree for storing collections of Problem and MethodC.

*)

signature STORE_TREE =

sig

  type key = string list

  datatype 'a node = Node of string * 'a list * 'a node list

  type 'a T = 'a node list

  val merge: 'a T * 'a T -> 'a T

  val insert: key -> 'a -> string list -> 'a T -> 'a T

  val scan : string list -> 'a T -> string list list

  val get: 'a T -> key -> (*rev*)key -> 'a

  val get_all: 'a T -> 'a list

  val update: key -> string list -> 'a -> 'a T -> 'a T

  val apply: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b

(*from isac_test for Minisubpbl*)

  val get_node: string list -> string list -> 'a T -> 'a node

end

(**)

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

struct

(**)

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

(* 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 node =

	Node 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 node) list; (* the children nodes                                                        *)

type 'a T = ('a node) list

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

  function for trees / ptyps *)

fun merge ([], pt) = pt

  | merge (pt, []) = pt

  | merge ((x' as Node (k, _, ps)) :: xs, (xs' as Node (k', y, ps') :: ys)) =

      if k = k'

      then Node (k, y, merge (ps, ps')) :: merge (xs, ys)

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

fun insert _ pbt [k] [] = [Node (k, [pbt], [])]

  | insert d pbt [k] ((Node (k', [p], ps)) :: pys) =

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

    if k = k'

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

    else  ((Node (k', [p], ps)) :: (insert d pbt [k] pys))

    )			 

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

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

    if k = k'

    then ((Node (k', [p], insert d pbt ks ps)) :: pys)

    else 

      if length pys = 0

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

      else ((Node (k', [p], ps)) :: (insert d pbt (k :: ks) pys))

    )

  | insert _ _ _ _ = raise ERROR "";

fun scan _  [] = [] (* no base case, for empty doms only *)

  | scan id ((Node ((i, _, []))) :: []) = [id @ [i]]

  | scan id ((Node ((i, _, pl))) :: []) = scan (id @ [i]) pl

  | scan id ((Node ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)

  | scan id ((Node ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);

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

  let

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

    fun app_py' _ [] = py_err ()

      | app_py' [] _ = py_err ()

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

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

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

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

  in app_py' k p end;

fun get p =

  let

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

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

  in apply p extract_py end;

fun get_all ptyp =

let

  fun scan [] = []

    | scan ((Node ((_, data, []))) :: []) = data

    | scan ((Node ((_, data, pl))) :: []) = data @ scan pl

    | scan ((Node ((_, data, []))) :: ps) = data @ scan ps

    | scan ((Node ((_, data, pl))) :: ps) = data @ scan pl @ scan ps

in scan ptyp end

fun update ID _ _ [] =

    raise ERROR ("update: " ^ strs2str' ID ^ " does not exist")

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

    if i = key

    then 

      if length pys = 0

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

      else raise ERROR ("update: " ^ strs2str' ID ^ " has descendants")

    else py :: update ID [i] data pyss

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

    if i = key

    then ((Node (key,  d, update ID is data pys)) :: pyss)

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

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

fun get_node(*1*) _ revkey [] = raise ERROR ("Store.get_node []: not found: " ^ strs2str revkey)

  | get_node(*2*) (key as (k1 :: _)) revkey ((node as Node (key', _, [])) :: ns) = (*spec.case same l.*)

(writeln ("get_node 2 " ^ key');

    if k1 = key' then node

    else get_node key revkey ns (*continue on same level*)

)

  | get_node(*3*) [k1] revkey ((node as Node (key', _, bs)) :: ns) =

(writeln ("get_node 3 " ^ key');

    if k1 = key' then node

    else get_node [k1] revkey ns

)

  | get_node(*4*) (key as (k1 :: ks)) revkey (Node (key', _, bs) :: ns) =

(writeln ("get_node 4 " ^ key');

    if k1 = key'

    then get_node_down ks revkey bs

    else get_node key revkey ns

)

  | get_node(*5*) _ revkey _ =

    raise ERROR ("Store.get_node: probably more than one node element for " ^ strs2str revkey)

and get_node_down(*6*) [k1] revkey ((node as Node (key', _, _)) :: ns) = (*base case go down*)

(writeln ("get_node_down 6 " ^ key');

    if k1 = key' then node

    else get_node [k1] revkey ns

)

  | get_node_down(*7*) (key as (k1 :: ks)) revkey (Node (key', _, bs) :: ns) =

(writeln ("get_node_down 7 " ^ key');

    if k1 = key'

    then get_node_down ks revkey bs

    else get_node key revkey ns

)

  | get_node_down(*8*) _ revkey _ =

    raise ERROR ("Store.get_node: probably more than one node element for " ^ strs2str revkey)

(**)end(**)