equal
deleted
inserted
replaced
59 val s_not: term -> term |
59 val s_not: term -> term |
60 val s_not_conj: term list -> term list |
60 val s_not_conj: term list -> term list |
61 val s_conjs: term list -> term |
61 val s_conjs: term list -> term |
62 val s_disjs: term list -> term |
62 val s_disjs: term list -> term |
63 val s_dnf: term list list -> term list |
63 val s_dnf: term list list -> term list |
|
64 |
|
65 val mk_partial_compN: int -> typ -> typ -> term -> term |
64 |
66 |
65 val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
67 val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
66 typ list -> term -> term -> term -> term |
68 typ list -> term -> term -> term -> term |
67 val unfold_let: term -> term |
69 val unfold_let: term -> term |
68 val massage_mutual_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> |
70 val massage_mutual_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> |
210 |> AList.coalesce (op =) |
212 |> AList.coalesce (op =) |
211 |> map (fn (c, css) => c :: s_dnf css) |
213 |> map (fn (c, css) => c :: s_dnf css) |
212 |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)]) |
214 |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)]) |
213 end; |
215 end; |
214 |
216 |
|
217 fun mk_partial_comp gT fT g = |
|
218 let val T = domain_type fT --> range_type gT in |
|
219 Const (@{const_name Fun.comp}, gT --> fT --> T) $ g |
|
220 end; |
|
221 |
|
222 fun mk_partial_compN 0 _ _ g = g |
|
223 | mk_partial_compN n gT fT g = |
|
224 let val g' = mk_partial_compN (n - 1) gT (range_type fT) g in |
|
225 mk_partial_comp (fastype_of g') fT g' |
|
226 end; |
|
227 |
|
228 fun mk_compN bound_Ts n (g, f) = |
|
229 let val typof = curry fastype_of1 bound_Ts in |
|
230 mk_partial_compN n (typof g) (typof f) g $ f |
|
231 end; |
|
232 |
215 fun factor_out_types ctxt massage destU U T = |
233 fun factor_out_types ctxt massage destU U T = |
216 (case try destU U of |
234 (case try destU U of |
217 SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt |
235 SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt |
218 | NONE => invalid_map ctxt); |
236 | NONE => invalid_map ctxt); |
219 |
237 |
221 let |
239 let |
222 val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs; |
240 val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs; |
223 val flat_fs' = map_args flat_fs; |
241 val flat_fs' = map_args flat_fs; |
224 in |
242 in |
225 permute_like (op aconv) flat_fs fs flat_fs' |
243 permute_like (op aconv) flat_fs fs flat_fs' |
226 end; |
|
227 |
|
228 fun mk_partial_comp gT fT g = |
|
229 let val T = domain_type fT --> range_type gT in |
|
230 Const (@{const_name Fun.comp}, gT --> fT --> T) $ g |
|
231 end; |
|
232 |
|
233 fun mk_compN' 0 _ _ g = g |
|
234 | mk_compN' n gT fT g = |
|
235 let val g' = mk_compN' (n - 1) gT (range_type fT) g in |
|
236 mk_partial_comp (fastype_of g') fT g' |
|
237 end; |
|
238 |
|
239 fun mk_compN bound_Ts n (g, f) = |
|
240 let val typof = curry fastype_of1 bound_Ts in |
|
241 mk_compN' n (typof g) (typof f) g $ f |
|
242 end; |
244 end; |
243 |
245 |
244 fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
246 fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
245 let |
247 let |
246 val typof = curry fastype_of1 bound_Ts; |
248 val typof = curry fastype_of1 bound_Ts; |