(* Title:  CalcElements/theoryC.sml

   Author: Walther Neuper

   (c) due to copyright terms

Probably this structure can be dropped due to improved reflection in Isabelle.

*)

signature THEORY_ISAC =

sig

  eqtype thyID

  eqtype domID

  eqtype theory'

  val Thy_Info_get_theory: string -> theory

  val thy2ctxt': string -> Proof.context

  val thy2ctxt: theory -> Proof.context

  val Isac: 'a -> theory

  val e_domID: domID

  val string_of_thy: theory -> theory'

  val theory2domID: theory -> theory'

  val theory2thyID: theory -> thyID

  val theory2theory': theory -> theory'

  val theory2str: theory -> theory'

  val thyID2theory': thyID -> thyID

  val theory'2thyID: theory' -> theory'

  val thyID_of_derivation_name: string -> string

(* ---- 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 ThyC(**): THEORY_ISAC(**) =

struct

(**)

(* Since Isabelle2017 sessions in theory identifiers are enforced.

  However, we leave theory identifiers short, in particular in use as keys into KEStore. *)

fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)

fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)

fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)

fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)

type thyID = string;   (* WN.3.11.03 TODO: replace domID with thyID*)

type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)

type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)

val e_domID = "e_domID" : domID;

fun string_of_thy thy = Context.theory_name thy: theory';

val theory2domID = string_of_thy;

val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;

val theory2theory' = string_of_thy;

val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)

fun thyID2theory' (thyID:thyID) = thyID;

fun theory'2thyID (theory':theory') = theory';

fun thyID_of_derivation_name dn = hd (space_explode "." dn);

(**)end(**)