equal
deleted
inserted
replaced
5 Supplements term with a locally minmal, complete set of type constraints. |
5 Supplements term with a locally minmal, complete set of type constraints. |
6 Complete: The constraints suffice to infer the term's types. |
6 Complete: The constraints suffice to infer the term's types. |
7 Minimal: Reducing the set of constraints further will make it incomplete. |
7 Minimal: Reducing the set of constraints further will make it incomplete. |
8 |
8 |
9 When configuring the pretty printer appropriately, the constraints will show up |
9 When configuring the pretty printer appropriately, the constraints will show up |
10 as type annotations when printing the term. This allows the term to be reparsed |
10 as type annotations when printing the term. This allows the term to be printed |
11 without a change of types. |
11 and reparsed without a change of types. |
12 |
12 |
13 NOTE: Terms should be unchecked before calling annotate_types to avoid awkward |
13 NOTE: Terms should be unchecked before calling annotate_types to avoid awkward |
14 syntax. |
14 syntax. |
15 *) |
15 *) |
16 |
16 |
85 let |
85 let |
86 val thy = Proof_Context.theory_of ctxt |
86 val thy = Proof_Context.theory_of ctxt |
87 val get_types = post_fold_term_type (K cons) [] |
87 val get_types = post_fold_term_type (K cons) [] |
88 in |
88 in |
89 fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty |
89 fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty |
|
90 handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Annotate: match_types" |
90 end |
91 end |
91 |
92 |
92 |
93 |
93 (* (3) handle trivial tfrees *) |
94 (* (3) handle trivial tfrees *) |
94 fun handle_trivial_tfrees ctxt (t', subst) = |
95 fun handle_trivial_tfrees ctxt (t', subst) = |