35 eqtype errpatID (*..from Rule_Def*) |
30 eqtype errpatID (*..from Rule_Def*) |
36 type errpat = errpatID * term list * thm list |
31 type errpat = errpatID * term list * thm list |
37 |
32 |
38 val scr2str: program -> string |
33 val scr2str: program -> string |
39 |
34 |
40 (*/------- to theoryC.sml -------------------------\*) |
|
41 val thy2ctxt: theory -> Proof.context |
|
42 val thy2ctxt': string -> Proof.context |
|
43 val Thy_Info_get_theory: string -> theory |
|
44 eqtype thyID |
|
45 eqtype domID |
|
46 val e_domID: domID |
|
47 eqtype theory' |
|
48 val theory'2thyID: theory' -> theory' |
|
49 val theory2theory': theory -> theory' |
|
50 val theory2thyID: theory -> thyID |
|
51 val thyID2theory': thyID -> thyID |
|
52 val string_of_thy: theory -> theory' |
|
53 val theory2domID: theory -> theory' |
|
54 val Isac: 'a -> theory |
|
55 val string_of_thmI: thm -> string |
|
56 (*\------- to theoryC.sml -------------------------/*) |
|
57 |
|
58 val e_term: term (* shift up to Unparse *) |
35 val e_term: term (* shift up to Unparse *) |
59 val e_type: typ (* shift up to Unparse *) |
36 val e_type: typ (* shift up to Unparse *) |
60 val type2str: typ -> string |
37 val type2str: typ -> string |
61 val term_to_string': Proof.context -> term -> string (* shift up to Unparse *) |
38 val term_to_string': Proof.context -> term -> string (* shift up to Unparse *) |
62 val term2str: term -> string (* shift up to Unparse *) |
39 val term2str: term -> string (* shift up to Unparse *) |
63 val termopt2str: term option -> string (* shift up to Unparse *) |
40 val termopt2str: term option -> string (* shift up to Unparse *) |
64 val theory2str: theory -> theory' (* shift up to Unparse *) |
|
65 val terms2str: term list -> string (* shift up to Unparse *) |
41 val terms2str: term list -> string (* shift up to Unparse *) |
66 val terms2strs: term list -> string list |
42 val terms2strs: term list -> string list |
67 val term_to_string'': thyID -> term -> string (* shift up to Unparse *) |
43 val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *) |
68 val term_to_string''': theory -> term -> string (* shift up to Unparse *) |
44 val term_to_string''': theory -> term -> string (* shift up to Unparse *) |
69 val t2str: theory -> term -> string |
45 val t2str: theory -> term -> string |
70 val ts2str: theory -> term list -> string (* shift up to Unparse *) |
46 val ts2str: theory -> term list -> string (* shift up to Unparse *) |
71 val string_of_typ: typ -> string (* shift up to Unparse *) |
47 val string_of_typ: typ -> string (* shift up to Unparse *) |
72 val string_of_typ_thy: thyID -> typ -> string (* shift up to Unparse *) |
48 val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *) |
73 |
49 |
74 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
50 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
75 val terms2str': term list -> string (* shift up to Unparse *) |
51 val terms2str': term list -> string (* shift up to Unparse *) |
76 val thm2str: thm -> string |
52 val thm2str: thm -> string |
77 val thms2str : thm list -> string |
53 val thms2str : thm list -> string |
|
54 val string_of_thmI: thm -> string |
78 val string_of_thm': theory -> thm -> string (* shift up to Unparse *) |
55 val string_of_thm': theory -> thm -> string (* shift up to Unparse *) |
79 val errpats2str : errpat list -> string |
56 val errpats2str : errpat list -> string |
80 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
57 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
81 val string_of_thm: thm -> string (* shift up to Unparse *) |
58 val string_of_thm: thm -> string (* shift up to Unparse *) |
82 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
59 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
124 | assoc' ((keyi, xi) :: pairs, key) = |
101 | assoc' ((keyi, xi) :: pairs, key) = |
125 if key = keyi then SOME xi else assoc' (pairs, key); |
102 if key = keyi then SOME xi else assoc' (pairs, key); |
126 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro)) |
103 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro)) |
127 handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); |
104 handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); |
128 |
105 |
129 (* Since Isabelle2017 sessions in theory identifiers are enforced. |
|
130 However, we leave theory identifiers short, in particular in use as keys into KEStore. *) |
|
131 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID) |
|
132 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*) |
|
133 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*) |
|
134 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*) |
|
135 |
|
136 fun term_to_string' ctxt t = |
106 fun term_to_string' ctxt t = |
137 let |
107 let |
138 val ctxt' = Config.put show_markup false ctxt |
108 val ctxt' = Config.put show_markup false ctxt |
139 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
109 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
140 fun term_to_string'' thyID t = |
110 fun term_to_string'' thyID t = |
141 let |
111 let |
142 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID)) |
112 val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID)) |
143 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
113 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
144 fun term_to_string''' thy t = |
114 fun term_to_string''' thy t = |
145 let |
115 let |
146 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy) |
116 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy) |
147 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
117 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
148 |
118 |
149 fun term2str t = term_to_string' (thy2ctxt' "Isac_Knowledge") t; |
119 fun term2str t = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") t; |
150 fun t2str thy t = term_to_string' (thy2ctxt thy) t; |
120 fun t2str thy t = term_to_string' (ThyC.thy2ctxt thy) t; |
151 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str'; |
121 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str'; |
152 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *) |
122 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *) |
153 val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *) |
123 val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *) |
154 val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *) |
124 val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *) |
155 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")" |
125 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")" |
174 fillpatterns are stored with these thms. *) |
144 fillpatterns are stored with these thms. *) |
175 fun errpat2str (id, tms, thms) = |
145 fun errpat2str (id, tms, thms) = |
176 "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms |
146 "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms |
177 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats |
147 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats |
178 |
148 |
179 (*ad thm': |
|
180 there are two kinds of theorems ... |
|
181 (1) known by isabelle |
|
182 (2) not known, eg. calc_thm, instantiated rls |
|
183 the latter have a thmid "#..." |
|
184 and thus outside isa we ALWAYS transport both (thmID, string_of_thmI) |
|
185 and have a special assoc_thm / assoc_rls in this interface *) |
|
186 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) |
|
187 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) |
|
188 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*) |
|
189 val e_domID = "e_domID" : domID; |
|
190 |
149 |
191 fun string_of_thy thy = Context.theory_name thy: theory'; |
150 fun type_to_string'' (thyID : ThyC.thyID) t = |
192 val theory2domID = string_of_thy; |
|
193 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; |
|
194 val theory2theory' = string_of_thy; |
|
195 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) |
|
196 |
|
197 fun thyID2theory' (thyID:thyID) = thyID; |
|
198 fun theory'2thyID (theory':theory') = theory'; |
|
199 |
|
200 fun type_to_string'' (thyID : thyID) t = |
|
201 let |
151 let |
202 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID)) |
152 val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID)) |
203 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end; |
153 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end; |
204 fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*) |
154 fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*) |
205 val string_of_typ = type2str; (*legacy*) |
155 val string_of_typ = type2str; (*legacy*) |
206 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*) |
156 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*) |
207 |
157 |
208 (*check for [.] as caused by "fun assoc_thm'"*) |
158 (*check for [.] as caused by "fun assoc_thm'"*) |
209 fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm) |
159 fun string_of_thm thm = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm) |
210 fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm) |
160 fun string_of_thm' thy thm = term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm) |
211 fun string_of_thmI thm = |
161 fun string_of_thmI thm = |
212 let |
162 let |
213 val str = (de_quote o string_of_thm) thm |
163 val str = (de_quote o string_of_thm) thm |
214 val (a, b) = split_nlast (5, Symbol.explode str) |
164 val (a, b) = split_nlast (5, Symbol.explode str) |
215 in |
165 in |