# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255656414 -7200
# Node ID 386671ef36bdc1d080478cb7226978728619270a
# Parent  d3a432bd09f09339b59b34a2a60b95047dec52ac
fixed the problem with function types; but only type_of works; cterm_of does not work

diff -r d3a432bd09f0 -r 386671ef36bd QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 16:51:24 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 03:26:54 2009 +0200
@@ -247,11 +247,15 @@
   update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
+
 ML {* lookup @{theory} @{type_name list} *}
 
 ML {*
 datatype flag = absF | repF
 
+fun negF absF = repF
+  | negF repF = absF
+
 fun get_fun flag rty qty lthy ty =
 let
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
@@ -280,6 +284,8 @@
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty))
+        | Type ("fun" , [ty1, ty2]) => 
+                 get_fun_aux "fun" [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
         | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
         | _ => raise ERROR ("no type variables")
        )
@@ -287,19 +293,80 @@
 *}
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"}
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+  get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
+text {*
+
+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 repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+ |> fst
+ |> type_of
+*}
+
+
+ML {*
+    get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
+    get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
+ |> fst
+ |> type_of
+*}
+
+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
+*}
+
+
+
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -381,53 +448,6 @@
   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
-(*
-
-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"}
- |> fst
- |> Syntax.string_of_term @{context}
- |> 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'
 term ap'