1.1 --- a/src/Tools/isac/calcelems.sml Wed Jul 23 14:32:19 2014 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Wed Jul 23 16:55:42 2014 +0200
1.3 @@ -203,9 +203,61 @@
1.4 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.5 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
1.6
1.7 +(*ad thm':
1.8 + there are two kinds of theorems ...
1.9 + (1) known by isabelle
1.10 + (2) not known, eg. calc_thm, instantiated rls
1.11 + the latter have a thmid "#..."
1.12 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
1.13 + and have a special assoc_thm / assoc_rls in this interface *)
1.14 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.15 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.16 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.17 +
1.18 +fun term_to_string' ctxt t =
1.19 + let
1.20 + val ctxt' = Config.put show_markup false ctxt
1.21 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.22 +fun term_to_string'' (thyID : thyID) t =
1.23 + let
1.24 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.25 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.26 +fun term_to_string''' thy t =
1.27 + let
1.28 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.29 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.30 +
1.31 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
1.32 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
1.33
1.34 +fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
1.35 +fun terms2strs ts = map term2str ts;
1.36 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.37 +val terms2str = strs2str o terms2strs;
1.38 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
1.39 +val terms2str' = strs2str' o terms2strs;
1.40 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
1.41 +
1.42 +fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
1.43 + | termopt2str NONE = "NONE";
1.44 +
1.45 +fun type_to_string' ctxt t =
1.46 + let
1.47 + val ctxt' = Config.put show_markup false ctxt
1.48 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.49 +fun type_to_string'' (thyID : thyID) t =
1.50 + let
1.51 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.52 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.53 +fun type_to_string''' thy t =
1.54 + let
1.55 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.56 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.57 +
1.58 +fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
1.59 +val string_of_typ = type2str; (*legacy*)
1.60 +fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
1.61 +
1.62 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
1.63
1.64 val e_rule = Thm ("refl", @{thm refl});
1.65 @@ -283,17 +335,6 @@
1.66 val e_term = Const("empty", Type("'a", []));
1.67 val e_scr = Prog e_term;
1.68
1.69 -(*ad thm':
1.70 - there are two kinds of theorems ...
1.71 - (1) known by isabelle
1.72 - (2) not known, eg. calc_thm, instantiated rls
1.73 - the latter have a thmid "#..."
1.74 - and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
1.75 - and have a special assoc_thm / assoc_rls in this interface *)
1.76 -type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.77 -type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.78 -type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.79 -
1.80 fun string_of_thy thy = Context.theory_name thy: theory';
1.81 val theory2domID = string_of_thy;
1.82 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.83 @@ -715,47 +756,6 @@
1.84 handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.85 (*get the string for stac from rule*)
1.86
1.87 -fun term_to_string' ctxt t =
1.88 - let
1.89 - val ctxt' = Config.put show_markup false ctxt
1.90 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.91 -fun term_to_string'' (thyID : thyID) t =
1.92 - let
1.93 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.94 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.95 -fun term_to_string''' thy t =
1.96 - let
1.97 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.98 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
1.99 -
1.100 -fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t;
1.101 -fun terms2strs ts = map term2str ts;
1.102 -(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.103 -val terms2str = strs2str o terms2strs;
1.104 -(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
1.105 -val terms2str' = strs2str' o terms2strs;
1.106 -(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
1.107 -
1.108 -fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
1.109 - | termopt2str NONE = "NONE";
1.110 -
1.111 -fun type_to_string' ctxt t =
1.112 - let
1.113 - val ctxt' = Config.put show_markup false ctxt
1.114 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.115 -fun type_to_string'' (thyID : thyID) t =
1.116 - let
1.117 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
1.118 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.119 -fun type_to_string''' thy t =
1.120 - let
1.121 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
1.122 - in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
1.123 -
1.124 -fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
1.125 -val string_of_typ = type2str; (*legacy*)
1.126 -fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
1.127 -
1.128 fun subst2str (s:subst) =
1.129 (strs2str o
1.130 (map (linefeed o pair2str o