diff -r 386671ef36bd -r f5f641c05794 QuotMain.thy --- a/QuotMain.thy Fri Oct 16 03:26:54 2009 +0200 +++ b/QuotMain.thy Fri Oct 16 08:48:56 2009 +0200 @@ -250,6 +250,8 @@ ML {* lookup @{theory} @{type_name list} *} +term fun_map + ML {* datatype flag = absF | repF @@ -269,6 +271,19 @@ val ftys = map (op -->) tys in (case (lookup (ProofContext.theory_of lthy) s) of + SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) + | NONE => raise ERROR ("no map association for type " ^ s)) + end + + fun get_fun_fun s fs_tys = + let + val (fs, tys) = split_list fs_tys + val ([oty1, oty2], [nty1, nty2]) = split_list tys + val oty = Type (s, [oty2, nty1]) + val nty = Type (s, [oty1, nty2]) + val ftys = map (op -->) tys + in + (case (lookup (ProofContext.theory_of lthy) s) of SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) | NONE => raise ERROR ("no map association for type " ^ s)) end @@ -285,7 +300,7 @@ 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] + get_fun_fun "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") ) @@ -302,8 +317,7 @@ ML {* get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |> fst - |> Syntax.string_of_term @{context} - |> writeln + |> type_of *} text {* @@ -331,7 +345,7 @@ *} -ML {* +(*ML {* get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |> fst |> type_of @@ -341,9 +355,9 @@ ML {* get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |> fst - |> Syntax.string_of_term @{context} - |> writeln + |> cterm_of @{theory} *} +*) ML {* get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}