# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255618284 -7200
# Node ID d3a432bd09f09339b59b34a2a60b95047dec52ac
# Parent  ab53ddefc542af8a9c3376a20ea2174dc6e4a774
Description of the problem with get_fun.

diff -r ab53ddefc542 -r d3a432bd09f0 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 16:36:20 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 16:51:24 2009 +0200
@@ -381,7 +381,30 @@
   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
-(*consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
+(*
+
+Christian:
+
+When "get_fun" gets a function type, it should call itself
+recursively for the right side of the arrow and call itself
+recursively with the flag swapped for left side. This way
+for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS).
+
+Examples of what it should do from Peter's code follow:
+
+- mkabs ``\x : 'a list.x``;
+> val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term
+- mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``;
+> val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)``
+- mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``;
+> val it =
+``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) -->
+   finite_set_ABS) (\x. y)`` : term
+
+It currently doesn't do it, the following code generates a wrong
+function and the second ML block fails to typecheck for this reason:
+
+*)
 
 ML {*
     get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
@@ -390,12 +413,20 @@
  |> writeln
 *}
 
+ML {*
+    get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
+ |> fst
+ |> cterm_of @{theory}
+*}
+
+(* The followng also fails due to incorrect types... *)
+consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 local_setup {*
   fn lthy => (Toplevel.program (fn () =>
     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
   )) |> snd
 *}
-*)
+
 
 term vr'
 term ap'