(* 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: term -> term_as_string

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

   val term_in_thy: theory -> term -> term_as_string

   val term_opt: term option -> term_as_string

   val terms_short: term list -> term_as_string

   val terms_in_thy: theory -> term list -> term_as_string

   val typ: typ -> term_as_string

   val typ_by_thyID: ThyC.id -> typ -> term_as_string

   val terms: term list -> 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;

 \<^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'' (thyID : ThyC.id) t =

   let

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

       (ThyC.get_theory thyID))

   in

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

   end;

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

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

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

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

 (**)end(**)