(* Title:  BridgeLibisabelle/present-tool.sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature PRESENTATION_TOOL =

sig

  datatype ketype = Exp_ | Met_ | Pbl_ | Thy_

  val ketype2str: ketype -> string

  val ketype2str': ketype -> string

  val str2ketype': string -> ketype

  type kestoreID

  val pblID2guh : Problem.id -> Check_Unique.id

  val metID2guh : MethodC.id -> Check_Unique.id

  val kestoreID2guh : ketype -> kestoreID -> Check_Unique.id

  val guh2kestoreID : Check_Unique.id -> string list          (* for interface.sml *)

end

(**)

structure Ptool(**) : PRESENTATION_TOOL(**) =

struct

(**)

(* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)

fun guh2kestoreID guh =

  case (implode o (take_fromto 1 4) o Symbol.explode) guh of

	  "pbl_" =>

	    let

	      fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =

	        if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns

	        | node _ _ _ = raise ERROR "Ptool.guh2kestoreID node: uncovered fun def."

	      and nodes _ _ [] = NONE 

	        | nodes ids gu (n :: ns) = case node ids gu n of

	            SOME id => SOME id

			      | NONE =>  nodes ids gu ns

	    in case nodes [] guh (get_ptyps ()) of

	      SOME id => rev id

	    | NONE => raise ERROR ("Ptool.guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in ptyps")

      end

  | "met_" =>

	    let

	      fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =

	        if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns

	        | node _ _ _ = raise ERROR "Ptool.guh2kestoreID node: uncovered fun def."

	      and nodes _ _ [] = NONE 

	        | nodes ids gu (n :: ns) = case node ids gu n of

	            SOME id => SOME id

				    | NONE =>  nodes ids gu ns

	    in case nodes [] guh (get_mets ()) of

	      SOME id => id

	    | NONE => raise ERROR ("Ptool.guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in mets")

      end

  | _ => raise ERROR ("Ptool.guh2kestoreID called with \"" ^ guh ^ "\":");

(* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)

datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;

fun ketype2str Exp_ = "Exp_"

  | ketype2str Thy_ = "Thy_"

  | ketype2str Pbl_ = "Pbl_"

  | ketype2str Met_ = "Met_";

fun ketype2str' Exp_ = "Example"

  | ketype2str' Thy_ = "Theory"

  | ketype2str' Pbl_ = "Problem"

  | ketype2str' Met_ = "MethodC";

(* for conversion from XML *)

fun str2ketype' "exp" = Exp_

  | str2ketype' "thy" = Thy_

  | str2ketype' "pbl" = Pbl_

  | str2ketype' "met" = Met_

  | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)

(*either ThyC.id or Problem.id or MethodC.id*)

type kestoreID = string list;

(* make a guh from a reference to an element in the kestore;

   EXCEPT theory hierarchy ... compare 'fun keref2xml'    *)

fun pblID2guh pblID = (((#guh o Problem.from_store) pblID)

  handle _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));

fun metID2guh metID = (((#guh o MethodC.from_store) metID)

  handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));

fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID

  | kestoreID2guh Met_ kestoreID = metID2guh kestoreID

  | kestoreID2guh ketype kestoreID =

    raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");

(**)end(**);