1 (* Title: BaseDefinitions/unparseC.sml
2 Author: Walther Neuper 2018
3 (c) copyright due to lincense terms
5 TODO: use "Rule" for renaming identifiers.
6 Some stuff waits for later rounds of restructuring, e.g. TermC.empty
9 signature UNPARSE_ISAC =
12 type subst = (term * term) list
17 val term: term -> string
18 (*val term_ctxt: Proof.context -> term -> string*)
19 val term_in_ctxt: Proof.context -> term -> string
20 (*val term_thy: theory -> term -> string*)
21 val term_in_thy: theory -> term -> string
23 val term_opt: term option -> string
25 val terms_short: term list -> string
26 (*val terms_thy: theory -> term list -> string*)
27 val terms_in_thy: theory -> term list -> string
29 val typ: typ -> string
30 (*val typ_thyID: ThyC.thyID -> typ -> string*)
31 val typ_by_thyID: ThyC.thyID -> typ -> string
33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
34 val terms: term list -> string
35 (*val term_thyID: ThyC.thyID -> term -> string*)
36 val term_by_thyID: ThyC.thyID -> term -> string
37 val terms_to_strings: term list -> string list
38 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
44 structure UnparseC(**): UNPARSE_ISAC(**) =
48 type term_as_string = string;
49 type subst = (term * term) list;
51 fun term_in_ctxt ctxt t =
53 val ctxt' = Config.put show_markup false ctxt
54 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
55 fun term_by_thyID thyID t =
57 val ctxt' = Config.put show_markup false (Proof_Context.init_global
58 (ThyC.Thy_Info_get_theory thyID))
59 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
60 fun term_in_thy thy t =
62 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
63 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
65 fun term t = term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") t;
66 fun term_in_thy thy t = term_in_ctxt (ThyC.thy2ctxt thy) t;
67 fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';
68 fun terms_to_strings ts = map term ts; (* terms_to_strings [t1,t2] = ["1 + 2", "abc"]; *)
69 val terms = strs2str o terms_to_strings; (* terms [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
70 val terms_short = strs2str' o terms_to_strings; (* terms_short [t1,t2] = "[1 + 2,abc]"; *)
71 fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"
72 | term_opt NONE = "NONE";
74 fun type_to_string'' (thyID : ThyC.thyID) t =
76 val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
77 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
78 fun typ typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
79 fun typ_by_thyID thy typ = type_to_string'' thy typ; (*legacy*)
81 val type_empty = Type ("empty",[]);
82 val term_empty = Const ("empty", Type("'a", []));