26 val no_type_enc : string |
26 val no_type_enc : string |
27 val full_type_encs : string list |
27 val full_type_encs : string list |
28 val partial_type_encs : string list |
28 val partial_type_encs : string list |
29 val default_metis_lam_trans : string |
29 val default_metis_lam_trans : string |
30 |
30 |
31 val metis_call : string -> string -> string |
|
32 val forall_of : term -> term -> term |
31 val forall_of : term -> term -> term |
33 val exists_of : term -> term -> term |
32 val exists_of : term -> term -> term |
|
33 val type_enc_aliases : (string * string list) list |
34 val unalias_type_enc : string -> string list |
34 val unalias_type_enc : string -> string list |
35 val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option -> |
35 val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option -> |
36 (string, string atp_type) atp_term -> term |
36 (string, string atp_type) atp_term -> term |
37 val prop_of_atp : Proof.context -> bool -> int Symtab.table -> |
37 val prop_of_atp : Proof.context -> bool -> int Symtab.table -> |
38 (string, string, (string, string atp_type) atp_term, string) atp_formula -> term |
38 (string, string, (string, string atp_type) atp_term, string) atp_formula -> term |
81 |
81 |
82 fun unalias_type_enc s = |
82 fun unalias_type_enc s = |
83 AList.lookup (op =) type_enc_aliases s |> the_default [s] |
83 AList.lookup (op =) type_enc_aliases s |> the_default [s] |
84 |
84 |
85 val default_metis_lam_trans = combsN |
85 val default_metis_lam_trans = combsN |
86 |
|
87 fun metis_call type_enc lam_trans = |
|
88 let |
|
89 val type_enc = |
|
90 (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of |
|
91 [alias] => alias |
|
92 | _ => type_enc) |
|
93 val opts = |
|
94 [] |> type_enc <> partial_typesN ? cons type_enc |
|
95 |> lam_trans <> default_metis_lam_trans ? cons lam_trans |
|
96 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
|
97 |
86 |
98 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s |
87 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s |
99 | term_name' _ = "" |
88 | term_name' _ = "" |
100 |
89 |
101 fun lambda' v = Term.lambda_name (term_name' v, v) |
90 fun lambda' v = Term.lambda_name (term_name' v, v) |