(* Title:  BaseDefinitions/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 id

  val cut_id: string -> id

  val last_isabelle_thy: theory

  val session_specify_names: id list

  val session_interpret_names: id list

  val get_theory: id -> theory         (* restricted to Isac_Knowledge *)

  val id_to_ctxt: id -> Proof.context

  val to_ctxt: theory -> Proof.context (* inverse of Proof_Context.theory_of *)

  val id_empty: id

  val Isac: 'a -> theory

  val parent_of: theory -> theory -> theory

  val sub_common : theory * theory -> theory

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

  (*NONE*)

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

  val get_thy: id -> theory            (* restricted to session Isac *)

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

end

(**)

structure ThyC(**): THEORY_ISAC(**) =

struct

(**)

type id = string;

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

val last_isabelle_thy = @{theory Complex_Main}

val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",

  "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calculate",

  "BaseDefinitions", "Know_Store"]

val session_interpret_names = ["Interpret"]

fun get_thy thyID =

  if member op = session_specify_names thyID

  then Thy_Info.get_theory ("Specify." ^ thyID)

  else if member op = session_interpret_names thyID

  then Thy_Info.get_theory ("Interpret." ^ thyID)

  else Thy_Info.get_theory ("Isac." ^ thyID);

fun get_theory thy =   

    if thy = "empty_thy_id"

    then (get_thy "Base_Tools") (*lower bound of Knowledge*)

    else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");

fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');

fun to_ctxt thy = Proof_Context.init_global thy;

val id_empty = "empty_thy_id";

fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");

fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;

fun sub_common (thy1, thy2) =

  if Context.subthy (thy1, thy2) then

    thy2

  else if Context.subthy (thy2, thy1) then

      thy1

    else get_theory "Isac_Knowledge"

(**)end(**)