221 | strip_happ args x = (x, args); |
221 | strip_happ args x = (x, args); |
222 |
222 |
223 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
223 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
224 |
224 |
225 fun hol_type_from_metis_term _ (Metis.Term.Var v) = |
225 fun hol_type_from_metis_term _ (Metis.Term.Var v) = |
226 (case strip_prefix tvar_prefix v of |
226 (case strip_prefix_and_undo_ascii tvar_prefix v of |
227 SOME w => make_tvar w |
227 SOME w => make_tvar w |
228 | NONE => make_tvar v) |
228 | NONE => make_tvar v) |
229 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = |
229 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = |
230 (case strip_prefix type_const_prefix x of |
230 (case strip_prefix_and_undo_ascii type_const_prefix x of |
231 SOME tc => Term.Type (invert_const tc, |
231 SOME tc => Term.Type (invert_const tc, |
232 map (hol_type_from_metis_term ctxt) tys) |
232 map (hol_type_from_metis_term ctxt) tys) |
233 | NONE => |
233 | NONE => |
234 case strip_prefix tfree_prefix x of |
234 case strip_prefix_and_undo_ascii tfree_prefix x of |
235 SOME tf => mk_tfree ctxt tf |
235 SOME tf => mk_tfree ctxt tf |
236 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); |
236 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); |
237 |
237 |
238 (*Maps metis terms to isabelle terms*) |
238 (*Maps metis terms to isabelle terms*) |
239 fun hol_term_from_metis_PT ctxt fol_tm = |
239 fun hol_term_from_metis_PT ctxt fol_tm = |
240 let val thy = ProofContext.theory_of ctxt |
240 let val thy = ProofContext.theory_of ctxt |
241 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ |
241 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ |
242 Metis.Term.toString fol_tm) |
242 Metis.Term.toString fol_tm) |
243 fun tm_to_tt (Metis.Term.Var v) = |
243 fun tm_to_tt (Metis.Term.Var v) = |
244 (case strip_prefix tvar_prefix v of |
244 (case strip_prefix_and_undo_ascii tvar_prefix v of |
245 SOME w => Type (make_tvar w) |
245 SOME w => Type (make_tvar w) |
246 | NONE => |
246 | NONE => |
247 case strip_prefix schematic_var_prefix v of |
247 case strip_prefix_and_undo_ascii schematic_var_prefix v of |
248 SOME w => Term (mk_var (w, HOLogic.typeT)) |
248 SOME w => Term (mk_var (w, HOLogic.typeT)) |
249 | NONE => Term (mk_var (v, HOLogic.typeT)) ) |
249 | NONE => Term (mk_var (v, HOLogic.typeT)) ) |
250 (*Var from Metis with a name like _nnn; possibly a type variable*) |
250 (*Var from Metis with a name like _nnn; possibly a type variable*) |
251 | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
251 | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
252 | tm_to_tt (t as Metis.Term.Fn (".",_)) = |
252 | tm_to_tt (t as Metis.Term.Fn (".",_)) = |
259 end |
259 end |
260 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) |
260 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) |
261 and applic_to_tt ("=",ts) = |
261 and applic_to_tt ("=",ts) = |
262 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) |
262 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) |
263 | applic_to_tt (a,ts) = |
263 | applic_to_tt (a,ts) = |
264 case strip_prefix const_prefix a of |
264 case strip_prefix_and_undo_ascii const_prefix a of |
265 SOME b => |
265 SOME b => |
266 let val c = invert_const b |
266 let val c = invert_const b |
267 val ntypes = num_type_args thy c |
267 val ntypes = num_type_args thy c |
268 val nterms = length ts - ntypes |
268 val nterms = length ts - ntypes |
269 val tts = map tm_to_tt ts |
269 val tts = map tm_to_tt ts |
277 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
277 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
278 " the terms are \n" ^ |
278 " the terms are \n" ^ |
279 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
279 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
280 end |
280 end |
281 | NONE => (*Not a constant. Is it a type constructor?*) |
281 | NONE => (*Not a constant. Is it a type constructor?*) |
282 case strip_prefix type_const_prefix a of |
282 case strip_prefix_and_undo_ascii type_const_prefix a of |
283 SOME b => |
283 SOME b => |
284 Type (Term.Type (invert_const b, types_of (map tm_to_tt ts))) |
284 Type (Term.Type (invert_const b, types_of (map tm_to_tt ts))) |
285 | NONE => (*Maybe a TFree. Should then check that ts=[].*) |
285 | NONE => (*Maybe a TFree. Should then check that ts=[].*) |
286 case strip_prefix tfree_prefix a of |
286 case strip_prefix_and_undo_ascii tfree_prefix a of |
287 SOME b => Type (mk_tfree ctxt b) |
287 SOME b => Type (mk_tfree ctxt b) |
288 | NONE => (*a fixed variable? They are Skolem functions.*) |
288 | NONE => (*a fixed variable? They are Skolem functions.*) |
289 case strip_prefix fixed_var_prefix a of |
289 case strip_prefix_and_undo_ascii fixed_var_prefix a of |
290 SOME b => |
290 SOME b => |
291 let val opr = Term.Free(b, HOLogic.typeT) |
291 let val opr = Term.Free(b, HOLogic.typeT) |
292 in apply_list opr (length ts) (map tm_to_tt ts) end |
292 in apply_list opr (length ts) (map tm_to_tt ts) end |
293 | NONE => raise Fail ("unexpected metis function: " ^ a) |
293 | NONE => raise Fail ("unexpected metis function: " ^ a) |
294 in |
294 in |
300 (*Maps fully-typed metis terms to isabelle terms*) |
300 (*Maps fully-typed metis terms to isabelle terms*) |
301 fun hol_term_from_metis_FT ctxt fol_tm = |
301 fun hol_term_from_metis_FT ctxt fol_tm = |
302 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ |
302 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ |
303 Metis.Term.toString fol_tm) |
303 Metis.Term.toString fol_tm) |
304 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = |
304 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = |
305 (case strip_prefix schematic_var_prefix v of |
305 (case strip_prefix_and_undo_ascii schematic_var_prefix v of |
306 SOME w => mk_var(w, dummyT) |
306 SOME w => mk_var(w, dummyT) |
307 | NONE => mk_var(v, dummyT)) |
307 | NONE => mk_var(v, dummyT)) |
308 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = |
308 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = |
309 Const ("op =", HOLogic.typeT) |
309 Const ("op =", HOLogic.typeT) |
310 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = |
310 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = |
311 (case strip_prefix const_prefix x of |
311 (case strip_prefix_and_undo_ascii const_prefix x of |
312 SOME c => Const (invert_const c, dummyT) |
312 SOME c => Const (invert_const c, dummyT) |
313 | NONE => (*Not a constant. Is it a fixed variable??*) |
313 | NONE => (*Not a constant. Is it a fixed variable??*) |
314 case strip_prefix fixed_var_prefix x of |
314 case strip_prefix_and_undo_ascii fixed_var_prefix x of |
315 SOME v => Free (v, hol_type_from_metis_term ctxt ty) |
315 SOME v => Free (v, hol_type_from_metis_term ctxt ty) |
316 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) |
316 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) |
317 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = |
317 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = |
318 cvt tm1 $ cvt tm2 |
318 cvt tm1 $ cvt tm2 |
319 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
319 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
320 cvt tm1 $ cvt tm2 |
320 cvt tm1 $ cvt tm2 |
321 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
321 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
322 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = |
322 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = |
323 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) |
323 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) |
324 | cvt (t as Metis.Term.Fn (x, [])) = |
324 | cvt (t as Metis.Term.Fn (x, [])) = |
325 (case strip_prefix const_prefix x of |
325 (case strip_prefix_and_undo_ascii const_prefix x of |
326 SOME c => Const (invert_const c, dummyT) |
326 SOME c => Const (invert_const c, dummyT) |
327 | NONE => (*Not a constant. Is it a fixed variable??*) |
327 | NONE => (*Not a constant. Is it a fixed variable??*) |
328 case strip_prefix fixed_var_prefix x of |
328 case strip_prefix_and_undo_ascii fixed_var_prefix x of |
329 SOME v => Free (v, dummyT) |
329 SOME v => Free (v, dummyT) |
330 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); |
330 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); |
331 hol_term_from_metis_PT ctxt t)) |
331 hol_term_from_metis_PT ctxt t)) |
332 | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t); |
332 | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t); |
333 hol_term_from_metis_PT ctxt t) |
333 hol_term_from_metis_PT ctxt t) |
403 handle Option => |
403 handle Option => |
404 (trace_msg (fn() => "List.find failed for the variable " ^ x ^ |
404 (trace_msg (fn() => "List.find failed for the variable " ^ x ^ |
405 " in " ^ Display.string_of_thm ctxt i_th); |
405 " in " ^ Display.string_of_thm ctxt i_th); |
406 NONE) |
406 NONE) |
407 fun remove_typeinst (a, t) = |
407 fun remove_typeinst (a, t) = |
408 case strip_prefix schematic_var_prefix a of |
408 case strip_prefix_and_undo_ascii schematic_var_prefix a of |
409 SOME b => SOME (b, t) |
409 SOME b => SOME (b, t) |
410 | NONE => case strip_prefix tvar_prefix a of |
410 | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of |
411 SOME _ => NONE (*type instantiations are forbidden!*) |
411 SOME _ => NONE (*type instantiations are forbidden!*) |
412 | NONE => SOME (a,t) (*internal Metis var?*) |
412 | NONE => SOME (a,t) (*internal Metis var?*) |
413 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
413 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
414 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) |
414 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) |
415 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |
415 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |