author haftmann Sat, 14 Nov 2015 08:45:51 +0100 changeset 61667 4b53042d7a40 parent 61666 f1b257607981 child 61668 9a51e4dfc5d9
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
```--- a/src/HOL/Tools/code_evaluation.ML	Sat Nov 14 13:48:49 2015 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Sat Nov 14 08:45:51 2015 +0100
@@ -48,11 +48,21 @@
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;

-fun ensure_term_of (tyco, (raw_vs, _)) thy =
+fun ensure_term_of (tyco, (vs, _)) thy =
let
val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
-  in if need_inst then add_term_of tyco raw_vs thy else thy end;
+  in if need_inst then add_term_of tyco vs thy else thy end;
+
+fun for_term_of_instance tyco vs f thy =
+  let
+    val algebra = Sign.classes_of thy;
+  in
+    case try (Sorts.mg_domain algebra tyco) @{sort term_of} of
+      NONE => thy
+    | SOME sorts => f tyco (map2 (fn (v, sort) => fn sort' =>
+        (v, Sorts.inter_sort algebra (sort, sort'))) vs sorts) thy
+  end;

(* code equations for datatypes *)
@@ -67,17 +77,18 @@
map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
(HOLogic.reflect_term t));
val cty = Thm.global_ctyp_of thy ty;
+    val _ = writeln ("typ: " ^ Syntax.string_of_typ_global thy (Thm.typ_of cty));
+    val _ = writeln ("arg: " ^ Syntax.string_of_term_global thy (Thm.term_of arg));
+    val _ = writeln ("rhs: " ^ Syntax.string_of_term_global thy (Thm.term_of rhs));
in
@{thm term_of_anything}
|> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
+    |> tap (fn _ => writeln "instantiated")
|> Thm.varifyT_global
end;

-fun add_term_of_code tyco raw_vs raw_cs thy =
+fun add_term_of_code tyco vs raw_cs thy =
let
-    val algebra = Sign.classes_of thy;
-    val vs = map (fn (v, sort) =>
-      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
val ty = Type (tyco, map TFree vs);
val cs = (map o apsnd o apsnd o map o map_atyps)
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
@@ -89,10 +100,8 @@
end;

-fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
-  let
-    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of};
-  in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
+fun ensure_term_of_code (tyco, (vs, cs)) =
+  for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs);

(* code equations for abstypes *)
@@ -110,11 +119,8 @@
|> Thm.varifyT_global
end;

-fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
+fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy =
let
-    val algebra = Sign.classes_of thy;
-    val vs = map (fn (v, sort) =>
-      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
val ty = Type (tyco, map TFree vs);
val ty_rep = map_atyps
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
@@ -126,10 +132,9 @@