245 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
245 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
246 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
246 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
247 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
247 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
248 *} |
248 *} |
249 |
249 |
|
250 |
250 ML {* lookup @{theory} @{type_name list} *} |
251 ML {* lookup @{theory} @{type_name list} *} |
251 |
252 |
252 ML {* |
253 ML {* |
253 datatype flag = absF | repF |
254 datatype flag = absF | repF |
|
255 |
|
256 fun negF absF = repF |
|
257 | negF repF = absF |
254 |
258 |
255 fun get_fun flag rty qty lthy ty = |
259 fun get_fun flag rty qty lthy ty = |
256 let |
260 let |
257 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
261 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
258 |
262 |
278 if ty = qty |
282 if ty = qty |
279 then (get_const flag) |
283 then (get_const flag) |
280 else (case ty of |
284 else (case ty of |
281 TFree _ => (mk_identity ty, (ty, ty)) |
285 TFree _ => (mk_identity ty, (ty, ty)) |
282 | Type (_, []) => (mk_identity ty, (ty, ty)) |
286 | Type (_, []) => (mk_identity ty, (ty, ty)) |
|
287 | Type ("fun" , [ty1, ty2]) => |
|
288 get_fun_aux "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
283 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
289 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
284 | _ => raise ERROR ("no type variables") |
290 | _ => raise ERROR ("no type variables") |
285 ) |
291 ) |
286 end |
292 end |
287 *} |
293 *} |
288 |
294 |
289 ML {* |
295 ML {* |
290 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"} |
296 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) list) * nat"} |
291 |> fst |
297 |> fst |
292 |> Syntax.string_of_term @{context} |
298 |> Syntax.string_of_term @{context} |
293 |> writeln |
299 |> writeln |
294 *} |
300 *} |
295 |
301 |
296 ML {* |
302 ML {* |
297 get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"} |
303 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
298 |> fst |
304 |> fst |
299 |> Syntax.string_of_term @{context} |
305 |> Syntax.string_of_term @{context} |
300 |> writeln |
306 |> writeln |
301 *} |
307 *} |
|
308 |
|
309 text {* |
|
310 |
|
311 Christian: |
|
312 |
|
313 When "get_fun" gets a function type, it should call itself |
|
314 recursively for the right side of the arrow and call itself |
|
315 recursively with the flag swapped for left side. This way |
|
316 for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS). |
|
317 |
|
318 Examples of what it should do from Peter's code follow: |
|
319 |
|
320 - mkabs ``\x : 'a list.x``; |
|
321 > val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term |
|
322 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
323 > val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)`` |
|
324 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
325 > val it = |
|
326 ``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) --> |
|
327 finite_set_ABS) (\x. y)`` : term |
|
328 |
|
329 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: |
|
331 |
|
332 *} |
|
333 |
|
334 ML {* |
|
335 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
|
336 |> fst |
|
337 |> type_of |
|
338 *} |
|
339 |
|
340 |
|
341 ML {* |
|
342 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
|
343 |> fst |
|
344 |> Syntax.string_of_term @{context} |
|
345 |> writeln |
|
346 *} |
|
347 |
|
348 ML {* |
|
349 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
350 |> fst |
|
351 |> type_of |
|
352 *} |
|
353 |
|
354 ML {* |
|
355 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
356 |> fst |
|
357 |> cterm_of @{theory} |
|
358 *} |
|
359 |
|
360 (* The followng also fails due to incorrect types... *) |
|
361 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
|
362 local_setup {* |
|
363 fn lthy => (Toplevel.program (fn () => |
|
364 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
|
365 )) |> snd |
|
366 *} |
|
367 |
|
368 |
302 |
369 |
303 text {* produces the definition for a lifted constant *} |
370 text {* produces the definition for a lifted constant *} |
304 |
371 |
305 ML {* |
372 ML {* |
306 fun get_const_def nconst oconst rty qty lthy = |
373 fun get_const_def nconst oconst rty qty lthy = |
378 local_setup {* |
445 local_setup {* |
379 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
446 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
380 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
447 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
381 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
448 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
382 *} |
449 *} |
383 |
|
384 (* |
|
385 |
|
386 Christian: |
|
387 |
|
388 When "get_fun" gets a function type, it should call itself |
|
389 recursively for the right side of the arrow and call itself |
|
390 recursively with the flag swapped for left side. This way |
|
391 for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS). |
|
392 |
|
393 Examples of what it should do from Peter's code follow: |
|
394 |
|
395 - mkabs ``\x : 'a list.x``; |
|
396 > val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term |
|
397 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
398 > val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)`` |
|
399 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
400 > val it = |
|
401 ``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) --> |
|
402 finite_set_ABS) (\x. y)`` : term |
|
403 |
|
404 It currently doesn't do it, the following code generates a wrong |
|
405 function and the second ML block fails to typecheck for this reason: |
|
406 |
|
407 *) |
|
408 |
|
409 ML {* |
|
410 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
411 |> fst |
|
412 |> Syntax.string_of_term @{context} |
|
413 |> writeln |
|
414 *} |
|
415 |
|
416 ML {* |
|
417 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
418 |> fst |
|
419 |> cterm_of @{theory} |
|
420 *} |
|
421 |
|
422 (* The followng also fails due to incorrect types... *) |
|
423 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
|
424 local_setup {* |
|
425 fn lthy => (Toplevel.program (fn () => |
|
426 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
|
427 )) |> snd |
|
428 *} |
|
429 |
|
430 |
450 |
431 term vr' |
451 term vr' |
432 term ap' |
452 term ap' |
433 term ap' |
453 term ap' |
434 thm VR'_def AP'_def LM'_def |
454 thm VR'_def AP'_def LM'_def |