(* 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 T

  eqtype id

  val make_thm: theory -> term -> thm       (* required for Calculate.thy  *)

  val string_of_thm: thm -> string

  val string_of_thms: thm list -> string

(* required in ProgLang BEFORE definition in ---------------vvv   *)

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

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

  val num_to_Free: 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. --------- *)

  (*NONE*)

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

  (*NONE*)

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

end

(**)

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

struct

(**)

type id = string; (* key into Know_Store, without point *)

type T = id * Thm.thm;

fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);

fun string_of_thm 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 string_of_thms thms = (strs2str o (map string_of_thm)) thms

fun int_opt_of_string 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 Isabelle's binary numerals to "Free (string, T)" **)

val num_to_Free = (* Makarius 100308 *)

  let

    fun dest_num t =

      (case try HOLogic.dest_number t of

        SOME (T, i) => SOME (Free (signed_string_of_int i, T))

      | 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_opt_of_string 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' = num_to_Free prop;

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

(**)end(**)