(* Interpret/thy-read.sml

   authors: Walther Neuper 2002, 2006

  (c) due to copyright terms

tools for rewriting, reverse rewriting, context to thy concerning rewriting

*)

signature THEORY_STORE_READ =

sig

  val thy_containing_thm : string -> string * string

  val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id

  val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string

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

  (*  NONE *)

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

  val isabthys: unit -> theory list

  val knowthys: unit -> theory list

  val partID': ThyC.id -> string

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

end 

(**)

structure Thy_Read(**): THEORY_STORE_READ(**) =

struct

(**)

(* group the theories defined in Isac, compare Build_Thydata:

  section "Get and group the theories defined in Isac" *) 

fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)

  let

    val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata")

  in

    drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)

  end

fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*)

  let

    fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)

      let

        val allthys = filter_out (member Context.eq_thy

          [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret", 

            ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) 

          (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))

      in

        take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 

        allthys)

      end

    val isacthys' = isacthys ()

    val proglang_parent = ThyC.get_theory "ProgLang"

  in

    take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')

  end

fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)

  let

    fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)

      let                                                        

        val allthys = filter_out (member Context.eq_thy

          [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret", 

            ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) 

          (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))

      in

        take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 

        allthys)

      end

    val isacthys' = isacthys ()

    val proglang_parent = ThyC.get_theory "ProgLang"

  in

    drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')

  end

fun partID thy = 

  if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"

  else if member Context.eq_thy (progthys ()) thy then "IsacScripts"

  else if member Context.eq_thy (isabthys ()) thy then "Isabelle"

  else error ("closure of thys in Isac is broken by " ^ Context.theory_name thy)

fun partID' thy' = partID (ThyC.get_theory thy')

fun thy_containing_thm thmDeriv =

  let

    val isabthys' = map Context.theory_name (isabthys ());

  in

    if member op= isabthys' (ThyC.cut_id thmDeriv)

    then ("Isabelle", ThyC.cut_id thmDeriv)

    else ("IsacKnowledge", ThyC.cut_id thmDeriv)

  end

(* which theory in ancestors of thy' contains a ruleset *)

fun thy_containing_rls thy' rls' =

  let

    val thy = ThyC.get_theory thy'

  in

    case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of

      SOME (thy'', _) => (partID' thy'', thy'')

    | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")

  end

(* this function cannot work as long as the datastructure does not contain thy' *)

fun thy_containing_cal thy' sop =

  let

    val thy = ThyC.get_theory thy'

  in

    case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of

      SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")

    | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")

  end

(**)end(**)