(* Title:  BaseDefinitions/thmC-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

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

*)

signature THEOREM_ISAC_DEF =

sig

  type thm'

  type thm''

  eqtype thmID

  val id_of_thm: Rule_Def.rule -> string

  val string_of_thmI: thm -> string

  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_Def.rule -> thm

(* required only for ProgLang/ListC *)

  val numerals_to_Free: thm -> thm          (* belongs to ThmC  *)

  val int_of_str_opt: string -> int option  (* belongs to TermC *)

  val numbers_to_string: term -> term       (* belongs to TermC *)

  val uminus_to_string: term -> term        (* belongs to TermC *)

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

  val thm2str: thm -> string

  val thms2str : thm list -> string

  val string_of_thm': theory -> thm -> string

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

  val string_of_thm: thm -> string

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

end

(**)

structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =

struct

(**)

(* 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_Def.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 string possible, without points)       *)

(*

  ad thm': there are two kinds of theorems ...

  (1) defined in isabelle

  (2) not known, eg. calc_thm, instantiated rls

      the latter have a thmid "#..."

  and thus outside isa we ALWAYS transport both (thmID, ThmC_Def.string_of_thmI)

  and have a special assoc_thm / assoc_rls in this interface

*)

type thm' = thmID * UnparseC.term_as_string;(*WN060610 deprecated in favour of thm'';

WN180324: used in TODO review:

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

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

| Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.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_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)

fun string_of_thm' thy thm = UnparseC.term_in_ctxt (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_Def.Thm (id, _)) = id

  | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string 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 thm_of_thm (Rule_Def.Thm (_, thm)) = thm

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

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

fun int_of_str_opt str = 

  let

    val ss = Symbol.explode str

    val ss' = case ss of "(" :: s => drop_last s | _ => ss

    val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')

  in

    case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE

  end;

(** transform binary numeralsstrings **)

(*Makarius 100308, hacked by WN*)

val numbers_to_string =

  let

    fun dest_num t =

      (case try HOLogic.dest_number t of

        SOME (T, i) =>

          (*if T = @{typ int} orelse T = @{typ real} then WN*)

            SOME (Free (signed_string_of_int i, T))

          (*else NONE  WN*)

      | NONE => NONE);

    fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)

      | to_str (t as (u1 $ u2)) =

          (case dest_num t of

            SOME t' => t'

          | NONE => to_str u1 $ to_str u2)

      | to_str t = perhaps dest_num t;

  in to_str end

val uminus_to_string =

  let

	  fun dest_num t =

	    case t of

	      (Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) => 

	        (case int_of_str_opt s of

	          SOME i => SOME (Free (signed_string_of_int (~1 * i), T))

	        | NONE => NONE)

	    | _ => NONE;

    fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)

      | to_str (t as (u1 $ u2)) =

          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)

      | to_str t = perhaps dest_num t;

  in to_str end;

fun numerals_to_Free thm =

  let

    val (deriv, 

	   {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, 

	    hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm

    val prop' = numbers_to_string prop;

  in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end;

(**)end(**)