267 val oty = Type (s, otys) |
269 val oty = Type (s, otys) |
268 val nty = Type (s, ntys) |
270 val nty = Type (s, ntys) |
269 val ftys = map (op -->) tys |
271 val ftys = map (op -->) tys |
270 in |
272 in |
271 (case (lookup (ProofContext.theory_of lthy) s) of |
273 (case (lookup (ProofContext.theory_of lthy) s) of |
|
274 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
|
275 | NONE => raise ERROR ("no map association for type " ^ s)) |
|
276 end |
|
277 |
|
278 fun get_fun_fun s fs_tys = |
|
279 let |
|
280 val (fs, tys) = split_list fs_tys |
|
281 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
|
282 val oty = Type (s, [oty2, nty1]) |
|
283 val nty = Type (s, [oty1, nty2]) |
|
284 val ftys = map (op -->) tys |
|
285 in |
|
286 (case (lookup (ProofContext.theory_of lthy) s) of |
272 SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) |
287 SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) |
273 | NONE => raise ERROR ("no map association for type " ^ s)) |
288 | NONE => raise ERROR ("no map association for type " ^ s)) |
274 end |
289 end |
275 |
290 |
276 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
291 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
283 then (get_const flag) |
298 then (get_const flag) |
284 else (case ty of |
299 else (case ty of |
285 TFree _ => (mk_identity ty, (ty, ty)) |
300 TFree _ => (mk_identity ty, (ty, ty)) |
286 | Type (_, []) => (mk_identity ty, (ty, ty)) |
301 | Type (_, []) => (mk_identity ty, (ty, ty)) |
287 | Type ("fun" , [ty1, ty2]) => |
302 | Type ("fun" , [ty1, ty2]) => |
288 get_fun_aux "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
303 get_fun_fun "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
289 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
304 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
290 | _ => raise ERROR ("no type variables") |
305 | _ => raise ERROR ("no type variables") |
291 ) |
306 ) |
292 end |
307 end |
293 *} |
308 *} |
329 It currently doesn't do it, the following code generates a wrong |
343 It currently doesn't do it, the following code generates a wrong |
330 function and the second ML block fails to typecheck for this reason: |
344 function and the second ML block fails to typecheck for this reason: |
331 |
345 |
332 *} |
346 *} |
333 |
347 |
334 ML {* |
348 (*ML {* |
335 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
349 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
336 |> fst |
350 |> fst |
337 |> type_of |
351 |> type_of |
338 *} |
352 *} |
339 |
353 |
340 |
354 |
341 ML {* |
355 ML {* |
342 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
356 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
343 |> fst |
357 |> fst |
344 |> Syntax.string_of_term @{context} |
358 |> cterm_of @{theory} |
345 |> writeln |
359 *} |
346 *} |
360 *) |
347 |
361 |
348 ML {* |
362 ML {* |
349 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
363 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
350 |> fst |
364 |> fst |
351 |> type_of |
365 |> type_of |