273 (case (lookup (ProofContext.theory_of lthy) s) of |
277 (case (lookup (ProofContext.theory_of lthy) s) of |
274 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
278 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
275 | NONE => raise ERROR ("no map association for type " ^ s)) |
279 | NONE => raise ERROR ("no map association for type " ^ s)) |
276 end |
280 end |
277 |
281 |
278 fun get_fun_fun s fs_tys = |
282 fun get_fun_fun fs_tys = |
279 let |
283 let |
280 val (fs, tys) = split_list fs_tys |
284 val (fs, tys) = split_list fs_tys |
281 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
285 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
282 val oty = Type (s, [nty1, oty2]) |
286 val oty = Type ("fun", [nty1, oty2]) |
283 val nty = Type (s, [oty1, nty2]) |
287 val nty = Type ("fun", [oty1, nty2]) |
284 val _ = tracing (Syntax.string_of_typ @{context} oty) |
|
285 val ftys = map (op -->) tys |
288 val ftys = map (op -->) tys |
286 in |
289 in |
287 (case (lookup (ProofContext.theory_of lthy) s) of |
290 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
288 SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) |
|
289 | NONE => raise ERROR ("no map association for type " ^ s)) |
|
290 end |
291 end |
291 |
292 |
292 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
293 fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) |
293 | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) |
294 | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) |
294 |
295 |
297 in |
298 in |
298 if ty = qty |
299 if ty = qty |
299 then (get_const flag) |
300 then (get_const flag) |
300 else (case ty of |
301 else (case ty of |
301 TFree _ => (mk_identity ty, (ty, ty)) |
302 TFree _ => (mk_identity ty, (ty, ty)) |
302 | Type (_, []) => (mk_identity ty, (ty, ty)) |
303 | Type (_, []) => (mk_identity ty, (ty, ty)) |
303 | Type ("fun" , [ty1, ty2]) => |
304 | Type ("fun" , [ty1, ty2]) => |
304 get_fun_fun "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
305 get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
305 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
306 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
306 | _ => raise ERROR ("no type variables") |
307 | _ => raise ERROR ("no type variables") |
307 ) |
308 ) |
308 end |
309 end |
309 *} |
310 *} |
310 |
311 |
311 term fun_map |
312 ML {* |
312 |
313 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
313 ML {* |
|
314 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) list) * nat"} |
|
315 |> fst |
314 |> fst |
316 |> Syntax.string_of_term @{context} |
315 |> Syntax.string_of_term @{context} |
317 |> writeln |
316 |> writeln |
318 *} |
317 *} |
319 |
318 |
320 ML {* |
319 ML {* |
321 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
320 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
322 |> fst |
321 |> fst |
323 |> type_of |
322 |> Syntax.string_of_term @{context} |
324 *} |
323 |> writeln |
325 |
324 *} |
326 text {* |
325 |
327 |
326 ML {* |
328 Christian: |
327 get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
329 |
328 |> fst |
330 When "get_fun" gets a function type, it should call itself |
329 |> Syntax.pretty_term @{context} |
331 recursively for the right side of the arrow and call itself |
330 |> Pretty.string_of |
332 recursively with the flag swapped for left side. This way |
331 |> writeln |
333 for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS). |
|
334 |
|
335 Examples of what it should do from Peter's code follow: |
|
336 |
|
337 - mkabs ``\x : 'a list.x``; |
|
338 > val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term |
|
339 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
340 > val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)`` |
|
341 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
342 > val it = |
|
343 ``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) --> |
|
344 finite_set_ABS) (\x. y)`` : term |
|
345 |
|
346 It currently doesn't do it, the following code generates a wrong |
|
347 function and the second ML block fails to typecheck for this reason: |
|
348 |
|
349 *} |
|
350 |
|
351 ML {* |
|
352 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt"} |
|
353 |> fst |
|
354 |> cterm_of @{theory} |
|
355 *} |
332 *} |
356 |
333 |
357 text {* produces the definition for a lifted constant *} |
334 text {* produces the definition for a lifted constant *} |
358 |
335 |
359 ML {* |
336 ML {* |