src/Pure/Isar/code.ML
changeset 36209 566be5d48090
parent 36202 43ea1f28fc7c
child 36610 bafd82950e24
     1.1 --- a/src/Pure/Isar/code.ML	Mon Apr 19 12:15:06 2010 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Apr 19 15:31:56 2010 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4    val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
     1.5    val constrain_cert: theory -> sort list -> cert -> cert
     1.6    val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
     1.7 -  val equations_of_cert: theory -> cert ->
     1.8 -    ((string * sort) list * typ) * ((string option * (term list * term)) * (thm option * bool)) list
     1.9 +  val equations_of_cert: theory -> cert -> ((string * sort) list * typ)
    1.10 +    * (((term * string option) list * (term * string option)) * (thm option * bool)) list
    1.11    val bare_thms_of_cert: theory -> cert -> thm list
    1.12    val pretty_cert: theory -> cert -> Pretty.T list
    1.13  
    1.14 @@ -461,6 +461,16 @@
    1.15    in not (has_duplicates (op =) ((fold o fold_aterms)
    1.16      (fn Var (v, _) => cons v | _ => I) args [])) end;
    1.17  
    1.18 +fun check_decl_ty thy (c, ty) =
    1.19 +  let
    1.20 +    val ty_decl = Sign.the_const_type thy c;
    1.21 +  in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
    1.22 +    else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.23 +      ^ "\nof constant " ^ quote c
    1.24 +      ^ "\nis incompatible with declared type\n"
    1.25 +      ^ string_of_typ thy ty_decl)
    1.26 +  end; 
    1.27 +
    1.28  fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
    1.29    let
    1.30      fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
    1.31 @@ -496,7 +506,7 @@
    1.32                then ()
    1.33                else bad (quote c ^ " is not a constructor, on left hand side of equation")
    1.34              else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
    1.35 -          end else bad ("Pattern not allowed, but constant " ^ quote c ^ " encountered on left hand side")
    1.36 +          end else bad ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side")
    1.37      val _ = map (check 0) args;
    1.38      val _ = if allow_nonlinear orelse is_linear thm then ()
    1.39        else bad "Duplicate variables on left hand side of equation";
    1.40 @@ -506,13 +516,7 @@
    1.41        else bad "Constructor as head in equation";
    1.42      val _ = if not (is_abstr thy c) then ()
    1.43        else bad "Abstractor as head in equation";
    1.44 -    val ty_decl = Sign.the_const_type thy c;
    1.45 -    val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
    1.46 -      then () else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.47 -        ^ "\nof equation\n"
    1.48 -        ^ Display.string_of_thm_global thy thm
    1.49 -        ^ "\nis incompatible with declared function type\n"
    1.50 -        ^ string_of_typ thy ty_decl)
    1.51 +    val _ = check_decl_ty thy (c, ty);
    1.52    in () end;
    1.53  
    1.54  fun gen_assert_eqn thy check_patterns (thm, proper) =
    1.55 @@ -645,19 +649,21 @@
    1.56  
    1.57  fun check_abstype_cert thy proto_thm =
    1.58    let
    1.59 -    val thm = meta_rewrite thy proto_thm;
    1.60 +    val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
    1.61      fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
    1.62      val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
    1.63        handle TERM _ => bad "Not an equation"
    1.64             | THM _ => bad "Not a proper equation";
    1.65 -    val ((abs, raw_ty), ((rep, _), param)) = (apsnd (apfst dest_Const o dest_comb)
    1.66 +    val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
    1.67          o apfst dest_Const o dest_comb) lhs
    1.68        handle TERM _ => bad "Not an abstype certificate";
    1.69 +    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
    1.70 +      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
    1.71 +    val _ = check_decl_ty thy (abs, raw_ty);
    1.72 +    val _ = check_decl_ty thy (rep, rep_ty);
    1.73      val var = (fst o dest_Var) param
    1.74        handle TERM _ => bad "Not an abstype certificate";
    1.75      val _ = if param = rhs then () else bad "Not an abstype certificate";
    1.76 -    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
    1.77 -      then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
    1.78      val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
    1.79      val ty = domain_type ty';
    1.80      val ty_abs = range_type ty';
    1.81 @@ -821,22 +827,23 @@
    1.82            |> Local_Defs.expand [snd (get_head thy cert_thm)]
    1.83            |> Thm.varifyT_global
    1.84            |> Conjunction.elim_balanced (length propers);
    1.85 -      in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
    1.86 +        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
    1.87 +      in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
    1.88    | equations_of_cert thy (Projection (t, tyco)) =
    1.89        let
    1.90          val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
    1.91          val tyscm = typscheme_projection thy t;
    1.92          val t' = map_types Logic.varifyT_global t;
    1.93 -      in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
    1.94 +        fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
    1.95 +      in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
    1.96    | equations_of_cert thy (Abstract (abs_thm, tyco)) =
    1.97        let
    1.98          val tyscm = typscheme_abs thy abs_thm;
    1.99          val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
   1.100 -        val _ = fold_aterms (fn Const (c, _) => if c = abs
   1.101 -          then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
   1.102 -          else I | _ => I) (Thm.prop_of abs_thm);
   1.103 +        fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
   1.104        in
   1.105 -        (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT_global abs_thm), true))])
   1.106 +        (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
   1.107 +          (SOME (Thm.varifyT_global abs_thm), true))])
   1.108        end;
   1.109  
   1.110  fun pretty_cert thy (cert as Equations _) =
   1.111 @@ -1111,12 +1118,13 @@
   1.112      val (old_constrs, some_old_proj) =
   1.113        case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
   1.114         of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
   1.115 -        | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
   1.116 +        | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
   1.117          | [] => ([], NONE)
   1.118      val outdated_funs = case some_old_proj
   1.119       of NONE => old_constrs
   1.120        | SOME old_proj => Symtab.fold
   1.121 -          (fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
   1.122 +          (fn (c, ((_, spec), _)) =>
   1.123 +            if member (op =) (the_list (associated_abstype spec)) tyco
   1.124              then insert (op =) c else I)
   1.125              ((the_functions o the_exec) thy) (old_proj :: old_constrs);
   1.126      fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.127 @@ -1162,7 +1170,7 @@
   1.128  fun add_abstype proto_thm thy =
   1.129    let
   1.130      val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
   1.131 -      check_abstype_cert thy proto_thm;
   1.132 +      error_thm (check_abstype_cert thy) proto_thm;
   1.133    in
   1.134      thy
   1.135      |> del_eqns abs