68 fun fn_isa_to_met "equal" = "=" |
67 fun fn_isa_to_met "equal" = "=" |
69 | fn_isa_to_met x = x; |
68 | fn_isa_to_met x = x; |
70 |
69 |
71 fun metis_lit b c args = (b, (c, args)); |
70 fun metis_lit b c args = (b, (c, args)); |
72 |
71 |
73 fun hol_type_to_fol (CombTVar (x, _)) = Metis.Term.Var x |
72 fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s |
74 | hol_type_to_fol (CombTFree (s, _)) = Metis.Term.Fn (s, []) |
73 | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, []) |
75 | hol_type_to_fol (CombType ((s, _), tps)) = |
74 | metis_term_from_combtyp (CombType ((s, _), tps)) = |
76 Metis.Term.Fn (s, map hol_type_to_fol tps); |
75 Metis.Term.Fn (s, map metis_term_from_combtyp tps); |
77 |
76 |
78 (*These two functions insert type literals before the real literals. That is the |
77 (*These two functions insert type literals before the real literals. That is the |
79 opposite order from TPTP linkup, but maybe OK.*) |
78 opposite order from TPTP linkup, but maybe OK.*) |
80 |
79 |
81 fun hol_term_to_fol_FO tm = |
80 fun hol_term_to_fol_FO tm = |
82 case strip_combterm_comb tm of |
81 case strip_combterm_comb tm of |
83 (CombConst ((c, _), _, tys), tms) => |
82 (CombConst ((c, _), _, tys), tms) => |
84 let val tyargs = map hol_type_to_fol tys |
83 let val tyargs = map metis_term_from_combtyp tys |
85 val args = map hol_term_to_fol_FO tms |
84 val args = map hol_term_to_fol_FO tms |
86 in Metis.Term.Fn (c, tyargs @ args) end |
85 in Metis.Term.Fn (c, tyargs @ args) end |
87 | (CombVar ((v, _), _), []) => Metis.Term.Var v |
86 | (CombVar ((v, _), _), []) => Metis.Term.Var v |
88 | _ => raise Fail "hol_term_to_fol_FO"; |
87 | _ => raise Fail "hol_term_to_fol_FO"; |
89 |
88 |
90 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s |
89 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s |
91 | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = |
90 | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = |
92 Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) |
91 Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist) |
93 | hol_term_to_fol_HO (CombApp (tm1, tm2)) = |
92 | hol_term_to_fol_HO (CombApp (tm1, tm2)) = |
94 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); |
93 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); |
95 |
94 |
96 (*The fully-typed translation, to avoid type errors*) |
95 (*The fully-typed translation, to avoid type errors*) |
97 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); |
96 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]); |
98 |
97 |
99 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty) |
98 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty) |
100 | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = |
99 | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = |
101 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) |
100 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) |
102 | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = |
101 | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = |
103 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), |
102 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), |
104 type_of_combterm tm); |
103 type_of_combterm tm); |
105 |
104 |
106 fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = |
105 fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = |
107 let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm |
106 let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm |
108 val tylits = if p = "equal" then [] else map hol_type_to_fol tys |
107 val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys |
109 val lits = map hol_term_to_fol_FO tms |
108 val lits = map hol_term_to_fol_FO tms |
110 in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end |
109 in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end |
111 | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = |
110 | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = |
112 (case strip_combterm_comb tm of |
111 (case strip_combterm_comb tm of |
113 (CombConst(("equal", _), _, _), tms) => |
112 (CombConst(("equal", _), _, _), tms) => |
221 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t |
220 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t |
222 | strip_happ args x = (x, args); |
221 | strip_happ args x = (x, args); |
223 |
222 |
224 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
223 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
225 |
224 |
226 fun fol_type_to_isa _ (Metis.Term.Var v) = |
225 fun hol_type_from_metis_term _ (Metis.Term.Var v) = |
227 (case strip_prefix tvar_prefix v of |
226 (case strip_prefix tvar_prefix v of |
228 SOME w => make_tvar w |
227 SOME w => make_tvar w |
229 | NONE => make_tvar v) |
228 | NONE => make_tvar v) |
230 | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = |
229 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = |
231 (case strip_prefix type_const_prefix x of |
230 (case strip_prefix type_const_prefix x of |
232 SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys) |
231 SOME tc => Term.Type (invert_const tc, |
|
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 tfree_prefix x of |
235 SOME tf => mk_tfree ctxt tf |
235 SOME tf => mk_tfree ctxt tf |
236 | NONE => raise Fail ("fol_type_to_isa: " ^ 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_fol_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_fol_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 tvar_prefix v of |
245 SOME w => Type (make_tvar w) |
245 SOME w => Type (make_tvar w) |
246 | NONE => |
246 | NONE => |
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 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 fixed_var_prefix x of |
315 SOME v => Free (v, fol_type_to_isa ctxt ty) |
315 SOME v => Free (v, hol_type_from_metis_term ctxt ty) |
316 | NONE => raise Fail ("hol_term_from_fol_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*) |
325 (case strip_prefix const_prefix x of |
325 (case strip_prefix 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 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_fol_FT bad const: " ^ x); |
330 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); |
331 hol_term_from_fol_PT ctxt t)) |
331 hol_term_from_metis_PT ctxt t)) |
332 | cvt t = (trace_msg (fn () => "hol_term_from_fol_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_fol_PT ctxt t) |
333 hol_term_from_metis_PT ctxt t) |
334 in fol_tm |> cvt end |
334 in fol_tm |> cvt end |
335 |
335 |
336 fun hol_term_from_fol FT = hol_term_from_fol_FT |
336 fun hol_term_from_metis FT = hol_term_from_metis_FT |
337 | hol_term_from_fol _ = hol_term_from_fol_PT |
337 | hol_term_from_metis _ = hol_term_from_metis_PT |
338 |
338 |
339 fun hol_terms_from_fol ctxt mode skolems fol_tms = |
339 fun hol_terms_from_fol ctxt mode skolems fol_tms = |
340 let val ts = map (hol_term_from_fol mode ctxt) fol_tms |
340 let val ts = map (hol_term_from_metis mode ctxt) fol_tms |
341 val _ = trace_msg (fn () => " calling type inference:") |
341 val _ = trace_msg (fn () => " calling type inference:") |
342 val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts |
342 val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts |
343 val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt |
343 val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt |
344 val _ = app (fn t => trace_msg |
344 val _ = app (fn t => trace_msg |
345 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
345 (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
772 |
772 |
773 val type_has_top_sort = |
773 val type_has_top_sort = |
774 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
774 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
775 |
775 |
776 fun generic_metis_tac mode ctxt ths i st0 = |
776 fun generic_metis_tac mode ctxt ths i st0 = |
777 let val _ = trace_msg (fn () => |
777 let |
|
778 val _ = trace_msg (fn () => |
778 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
779 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
779 in |
780 in |
780 if exists_type type_has_top_sort (prop_of st0) then |
781 if exists_type type_has_top_sort (prop_of st0) then |
781 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
782 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
782 else |
783 else |
783 (Meson.MESON (maps neg_clausify) |
784 Meson.MESON (maps Clausifier.neg_clausify) |
784 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
785 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
785 ctxt i) st0 |
786 ctxt i st0 |
786 handle ERROR msg => raise METIS ("generic_metis_tac", msg) |
787 handle ERROR msg => raise METIS ("generic_metis_tac", msg) |
787 end |
788 end |
788 handle METIS (loc, msg) => |
789 handle METIS (loc, msg) => |
789 if mode = HO then |
790 if mode = HO then |
790 (warning ("Metis: Falling back on \"metisFT\"."); |
791 (warning ("Metis: Falling back on \"metisFT\"."); |