(* Title:  CalcElements/thmC.sml

    Author: Walther Neuper

    (c) due to copyright terms

 TODO: use "ThmC" for renaming identifiers.

 Probably this structure can be dropped due to improvements of Isabelle.

 *)

 signature THEOREM_ISAC =

 sig

 (*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)

 (*/------- to ThmC.sml ------\*)

   eqtype thmID

   type thm'

   type thm''

   val thmID_of_derivation_name: string -> string

   val thmID_of_derivation_name': thm -> string

   val thm''_of_thm: thm -> thm''

   val thm_of_thm: Rule.rule -> thm

   val string_of_thmI: thm -> string

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

   val thm2str: thm -> string

   val thms2str : thm list -> string

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

   val string_of_thm: thm -> string

   val string_of_thm': theory -> thm -> string

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

 (*/------- to ThmC.sml ------\*)

     val id_of_thm: Rule.rule -> string

 (*\------- to ThmC.sml ------/*)

 end

 (**)

 structure ThmC(**): THEOREM_ISAC(**) =

 struct

 (**)

 (*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)

 (* TODO CLEANUP Thm:

 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;

                    (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI

 thmID            : type for data from user input + program

 thmDeriv         : type for thy_hierarchy ONLY

 obsolete types   : thm' (SEE "ad thm'"), thm''. 

 revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.

 activate         : thmID_of_derivation_name'

 *)

 type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)

 type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:

 val thm'2xml : int -> ThmC.thm' -> Celem.xml

 val assoc_thm': theory -> ThmC.thm' -> thm

 | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')

 *)

 (* tricky combination of (string, term) for theorems in Isac:

   * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)

     by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.

   * case 2 "sym_..": Global_Theory.get_thm..RS sym

   * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:

     from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)

 *)

 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)

 fun thm2str thm =

   let

     val t = Thm.prop_of thm

     val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))

     val ctxt' = Config.put show_markup false ctxt

   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

 fun thms2str thms = (strs2str o (map thm2str)) thms

 (*check for [.] as caused by "fun assoc_thm'"*)

 fun string_of_thm thm = UnparseC.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)

 fun string_of_thm' thy thm = UnparseC.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)

 fun string_of_thmI thm =

   let 

     val str = (de_quote o string_of_thm) thm

     val (a, b) = split_nlast (5, Symbol.explode str)

   in 

     case b of

       [" ", " ","[", ".", "]"] => implode a

     | _ => str

   end

 fun id_of_thm (Rule.Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)

   | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))

 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);

 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm

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

 fun thm_of_thm (Rule.Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)

   | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))

 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''

 (**)end(**)