# HG changeset patch
# User bulwahn
# Date 1315564389 -7200
# Node ID 0b3d3570ab3134c0cf3732f1d8bece86b28da81f
# Parent  8ac91e7b6024b657224fbf13ca42f0ea6e38cf77
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types

diff -r 8ac91e7b6024 -r 0b3d3570ab31 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Sep 08 12:23:11 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 09 12:33:09 2011 +0200
@@ -598,22 +598,21 @@
     apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
   | annotate_term (_, t) tvar_names = (t, tvar_names)
 
-fun annotate_eqns thy eqns = 
+fun annotate_eqns thy (c, ty) eqns = 
   let
     val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
     val erase = map_types (fn _ => Type_Infer.anyT [])
     val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
-    fun add_annotations ((args, (rhs, some_abs)), (SOME th, proper)) =
+    fun add_annotations (args, (rhs, some_abs)) =
       let
-        val (lhs, drhs) = Logic.dest_equals (prop_of (Thm.unvarify_global th))
-        val drhs' = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase drhs))))
-        val (rhs', _) = annotate_term (drhs', rhs) []
+        val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
+        val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
+        val (rhs', _) = annotate_term (reinferred_rhs, rhs) []
      in
-        ((args, (rhs', some_abs)), (SOME th, proper))
+        (args, (rhs', some_abs))
      end
-     | add_annotations eqn = eqn
   in
-    map add_annotations eqns
+    map (apfst add_annotations) eqns
   end;
 
 (* translation *)
@@ -640,7 +639,7 @@
     fun stmt_fun cert =
       let
         val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
-        val eqns' = annotate_eqns thy eqns
+        val eqns' = annotate_eqns thy (c, ty) eqns
         val some_case_cong = Code.get_case_cong thy c;
       in
         fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs