# HG changeset patch
# User haftmann
# Date 1271683916 -7200
# Node ID 566be5d48090fdd3b1713bfdaf83770137925720
# Parent  398dd97e49a576d0142eef69582b8e4de1bd156a
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates

diff -r 398dd97e49a5 -r 566be5d48090 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Apr 19 12:15:06 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon Apr 19 15:31:56 2010 +0200
@@ -35,8 +35,8 @@
   val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
   val constrain_cert: theory -> sort list -> cert -> cert
   val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
-  val equations_of_cert: theory -> cert ->
-    ((string * sort) list * typ) * ((string option * (term list * term)) * (thm option * bool)) list
+  val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
+    * (((term * string option) list * (term * string option)) * (thm option * bool)) list
   val bare_thms_of_cert: theory -> cert -> thm list
   val pretty_cert: theory -> cert -> Pretty.T list
 
@@ -461,6 +461,16 @@
   in not (has_duplicates (op =) ((fold o fold_aterms)
     (fn Var (v, _) => cons v | _ => I) args [])) end;
 
+fun check_decl_ty thy (c, ty) =
+  let
+    val ty_decl = Sign.the_const_type thy c;
+  in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
+    else bad_thm ("Type\n" ^ string_of_typ thy ty
+      ^ "\nof constant " ^ quote c
+      ^ "\nis incompatible with declared type\n"
+      ^ string_of_typ thy ty_decl)
+  end; 
+
 fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
   let
     fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
@@ -496,7 +506,7 @@
               then ()
               else bad (quote c ^ " is not a constructor, on left hand side of equation")
             else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
-          end else bad ("Pattern not allowed, but constant " ^ quote c ^ " encountered on left hand side")
+          end else bad ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side")
     val _ = map (check 0) args;
     val _ = if allow_nonlinear orelse is_linear thm then ()
       else bad "Duplicate variables on left hand side of equation";
@@ -506,13 +516,7 @@
       else bad "Constructor as head in equation";
     val _ = if not (is_abstr thy c) then ()
       else bad "Abstractor as head in equation";
-    val ty_decl = Sign.the_const_type thy c;
-    val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
-      then () else bad_thm ("Type\n" ^ string_of_typ thy ty
-        ^ "\nof equation\n"
-        ^ Display.string_of_thm_global thy thm
-        ^ "\nis incompatible with declared function type\n"
-        ^ string_of_typ thy ty_decl)
+    val _ = check_decl_ty thy (c, ty);
   in () end;
 
 fun gen_assert_eqn thy check_patterns (thm, proper) =
@@ -645,19 +649,21 @@
 
 fun check_abstype_cert thy proto_thm =
   let
-    val thm = meta_rewrite thy proto_thm;
+    val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
     fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
     val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
       handle TERM _ => bad "Not an equation"
            | THM _ => bad "Not a proper equation";
-    val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb)
+    val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
         o apfst dest_Const o dest_comb) lhs
       handle TERM _ => bad "Not an abstype certificate";
+    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
+      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
+    val _ = check_decl_ty thy (abs, raw_ty);
+    val _ = check_decl_ty thy (rep, rep_ty);
     val var = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";
-    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
-      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
     val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
     val ty_abs = range_type ty';
@@ -821,22 +827,23 @@
           |> Local_Defs.expand [snd (get_head thy cert_thm)]
           |> Thm.varifyT_global
           |> Conjunction.elim_balanced (length propers);
-      in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
+      in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
   | equations_of_cert thy (Projection (t, tyco)) =
       let
         val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
         val tyscm = typscheme_projection thy t;
         val t' = map_types Logic.varifyT_global t;
-      in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
+        fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
+      in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
   | equations_of_cert thy (Abstract (abs_thm, tyco)) =
       let
         val tyscm = typscheme_abs thy abs_thm;
         val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
-        val _ = fold_aterms (fn Const (c, _) => if c = abs
-          then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
-          else I | _ => I) (Thm.prop_of abs_thm);
+        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
       in
-        (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))])
+        (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
+          (SOME (Thm.varifyT_global abs_thm), true))])
       end;
 
 fun pretty_cert thy (cert as Equations _) =
@@ -1111,12 +1118,13 @@
     val (old_constrs, some_old_proj) =
       case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
        of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
-        | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
+        | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
         | [] => ([], NONE)
     val outdated_funs = case some_old_proj
      of NONE => old_constrs
       | SOME old_proj => Symtab.fold
-          (fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
+          (fn (c, ((_, spec), _)) =>
+            if member (op =) (the_list (associated_abstype spec)) tyco
             then insert (op =) c else I)
             ((the_functions o the_exec) thy) (old_proj :: old_constrs);
     fun drop_outdated_cases cases = fold Symtab.delete_safe
@@ -1162,7 +1170,7 @@
 fun add_abstype proto_thm thy =
   let
     val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
-      check_abstype_cert thy proto_thm;
+      error_thm (check_abstype_cert thy) proto_thm;
   in
     thy
     |> del_eqns abs