(* Title:  CalcElements/rule.sml

   Author: Walther Neuper 2018

   (c) copyright due to lincense terms

Some stuff waits for later rounds of restructuring, e.g. Rule.e_term

*)

signature RULE =

sig

  datatype rule = datatype Rule_Def.rule

  datatype program = datatype Rule_Def.program

  eqtype cterm'

  type subst = (term * term) list

  eqtype errpatID

  type errpat = errpatID * term list * thm list

  val scr2str: program -> string

  val e_term: term                                           (* shift up to Unparse *)

  val e_type: typ                                            (* shift up to Unparse *)

  val type2str: typ -> string

  val term_to_string': Proof.context -> term -> string       (* shift up to Unparse *)

  val term2str: term -> string                               (* shift up to Unparse *)

  val termopt2str: term option -> string                     (* shift up to Unparse *)

  val terms2str: term list -> string                         (* shift up to Unparse *)

  val terms2strs: term list -> string list

  val term_to_string'': ThyC.thyID -> term -> string         (* shift up to Unparse *)

  val term_to_string''': theory -> term -> string            (* shift up to Unparse *)

  val t2str: theory -> term -> string

  val ts2str: theory -> term list -> string                  (* shift up to Unparse *)

  val string_of_typ: typ -> string                           (* shift up to Unparse *)

  val string_of_typ_thy: ThyC.thyID -> typ -> string         (* shift up to Unparse *)

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

  val terms2str': term list -> string                        (* shift up to Unparse *)

  val thm2str: thm -> string

  val thms2str : thm list -> string

  val string_of_thmI: thm -> string

  val string_of_thm': theory -> thm -> string                (* shift up to Unparse *)

  val errpats2str : errpat list -> string

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

    val string_of_thm: thm -> string                           (* shift up to Unparse *)

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

end

(**)

structure Rule(**): RULE(**) =

struct

(**)

datatype rule = datatype Rule_Def.rule

datatype program = datatype Rule_Def.program

type calc = Rule_Def.calc                                                        (*..from Rule_Def*)

type calID = Rule_Def.calID;                                                     (*..from Rule_Def*)

(* eval function calling sml code during rewriting.

Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,

  see "fun rule2stac": instead of 

    Num_Calc: calID * eval_fn -> rule

  would be better

    Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)

type eval_fn = Rule_Def.eval_fn                                                  (*..from Rule_Def*)

type cterm' = string;

type subst = (term * term) list;

fun term_to_string' ctxt t =

  let

    val ctxt' = Config.put show_markup false ctxt

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

fun term_to_string'' thyID t =

  let

    val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))

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

fun term_to_string''' thy t =

  let

    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)

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

fun term2str t = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") t;

fun t2str thy t = term_to_string' (ThyC.thy2ctxt thy) t;

fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';

fun terms2strs ts = map term2str ts;     (* terms2strs [t1,t2] = ["1 + 2", "abc"];      *)

val terms2str = strs2str o terms2strs;   (* terms2str  [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)

val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]";         *)

fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"

  | termopt2str NONE = "NONE";

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

(* error patterns and fill patterns *)

type errpatID = string

type errpat =

  errpatID    (* one identifier for a list of patterns                       

                 DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)

  * term list (* error patterns                                              *)

  * thm list  (* thms related to error patterns; note that respective lhs 

                 do not match (which reflects student's error).

                 fillpatterns are stored with these thms.                    *)

fun errpat2str (id, tms, thms) =

  "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms

fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats

fun type_to_string'' (thyID : ThyC.thyID) t =

  let

    val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))

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

fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)

val string_of_typ = type2str; (*legacy*)

fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)

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

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

fun string_of_thm' thy thm = 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 scr2str EmptyScr = "EmptyScr"

  | scr2str (Prog s) = "Prog " ^ term2str s

  | scr2str (Rfuns _)  = "Rfuns";

val e_type = Type ("empty",[]);

val e_term = Const ("empty", Type("'a", []));

end (*struct*)