(* Title:  BaseDefinitions/unparseC.sml

   Author: Walther Neuper 2018

   (c) copyright due to lincense terms

*)

signature UNPARSE_ISAC =

sig

  eqtype term_as_string

  val term_empty: term

  val typ_empty: typ

(*val term: Proof.context -> term -> term_as_string *)

  val term_in_ctxt: Proof.context -> term -> term_as_string

  val term: term -> term_as_string

(*replace by ^^^*)

  val term_in_thy: theory -> term -> term_as_string

(*val term_opt: Proof.context -> term option -> term_as_string *)

  val term_opt: term option -> term_as_string

  val terms: term list -> term_as_string

(*replace by ^^^*)

  val terms_in_ctxt: Proof.context -> term list -> term_as_string

(*replace by ^^^*)

  val terms_in_thy: theory -> term list -> term_as_string

(*val terms_short: Proof.context -> term list -> term_as_string*)

  val terms_short: term list -> term_as_string

(*val typ: Proof.context -> typ -> term_as_string*)

  val typ_in_ctxt: Proof.context -> typ -> term_as_string

\<^isac_test>\<open>

  val term_by_thyID: ThyC.id -> term -> term_as_string

  val terms_to_strings: term list -> term_as_string list

\<close>

end

(**)

structure UnparseC(**): UNPARSE_ISAC(**) =

struct

(**)

type term_as_string = string;

fun term_in_ctxt ctxt t =

  let

    val ctxt' = Config.put show_markup false ctxt;

  in

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

  end;

fun terms_in_ctxt ctxt ts = ts |> map (term_in_ctxt ctxt) |> strs2str';

\<^isac_test>\<open>

fun term_by_thyID thyID t =

  let

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

      (ThyC.get_theory thyID));

  in

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

  end;

\<close>

fun term t = term_in_ctxt (ThyC.id_to_ctxt "Isac_Knowledge") t;

fun term_in_thy thy t = term_in_ctxt (Proof_Context.init_global thy) t;

fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';

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

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

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

fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"

  | term_opt NONE = "NONE";

fun type_to_string' ctxt typ =

  Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ

fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ

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

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

(**)end(**)