(* Title:  BridgeLibisabelle/present-tool.sml

   Author: Walther Neuper

   (c) due to copyright terms

This code remains in order to

keep tests of interaction Java-frontend <-> Kernel running.

*)

signature PRESENTATION_TOOL =

sig

  type ketype

  val ketype2str: ketype -> string

  val str2ketype': string -> ketype

  type kestoreID

  val pblID2guh : Proof.context -> Problem.id -> Check_Unique.id

  val metID2guh : (*Proof.context ->*) MethodC.id -> Check_Unique.id

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

  val guh2kestoreID : Check_Unique.id -> string list

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_pbls ()) 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_";

(* 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 ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID)

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

fun metID2guh metID =

  (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID)

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

fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID

  | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID

  | kestoreID2guh _ ketyp kestoreID =

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

(**)end(**);