1.1 --- a/src/HOL/ex/Eval_Examples.thy Fri Nov 26 23:14:14 2010 +0100
1.2 +++ b/src/HOL/ex/Eval_Examples.thy Fri Nov 26 23:50:14 2010 +0100
1.3 @@ -75,16 +75,17 @@
1.4
1.5 text {* a fancy datatype *}
1.6
1.7 -datatype ('a, 'b) bair =
1.8 - Bair "'a\<Colon>order" 'b
1.9 - | Shift "('a, 'b) cair"
1.10 - | Dummy unit
1.11 -and ('a, 'b) cair =
1.12 - Cair 'a 'b
1.13 +datatype ('a, 'b) foo =
1.14 + Foo "'a\<Colon>order" 'b
1.15 + | Bla "('a, 'b) bar"
1.16 + | Dummy nat
1.17 +and ('a, 'b) bar =
1.18 + Bar 'a 'b
1.19 + | Blubb "('a, 'b) foo"
1.20
1.21 -value "Shift (Cair (4::nat) [Suc 0])"
1.22 -value [code] "Shift (Cair (4::nat) [Suc 0])"
1.23 -value [SML] "Shift (Cair (4::nat) [Suc 0])"
1.24 -value [nbe] "Shift (Cair (4::nat) [Suc 0])"
1.25 +value "Bla (Bar (4::nat) [Suc 0])"
1.26 +value [code] "Bla (Bar (4::nat) [Suc 0])"
1.27 +value [SML] "Bla (Bar (4::nat) [Suc 0])"
1.28 +value [nbe] "Bla (Bar (4::nat) [Suc 0])"
1.29
1.30 end
2.1 --- a/src/Pure/Isar/code.ML Fri Nov 26 23:14:14 2010 +0100
2.2 +++ b/src/Pure/Isar/code.ML Fri Nov 26 23:50:14 2010 +0100
2.3 @@ -316,7 +316,7 @@
2.4 val data = case Datatab.lookup datatab kind
2.5 of SOME data => data
2.6 | NONE => invoke_init kind;
2.7 - val result as (x, data') = f (dest data);
2.8 + val result as (_, data') = f (dest data);
2.9 val _ = Synchronized.change dataref
2.10 ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
2.11 in result end;
2.12 @@ -360,9 +360,9 @@
2.13
2.14 fun subst_signature thy c ty =
2.15 let
2.16 - fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
2.17 + fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
2.18 fold2 mk_subst tys1 tys2
2.19 - | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
2.20 + | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty))
2.21 in case lookup_typ thy c
2.22 of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
2.23 | NONE => ty
2.24 @@ -407,8 +407,9 @@
2.25 val _ = if (tyco' : string) <> tyco
2.26 then error "Different type constructors in constructor set"
2.27 else ();
2.28 - val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
2.29 - in ((tyco, sorts), c :: cs) end;
2.30 + val sorts'' =
2.31 + map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
2.32 + in ((tyco, sorts''), c :: cs) end;
2.33 fun inst vs' (c, (vs, ty)) =
2.34 let
2.35 val the_v = the o AList.lookup (op =) (vs ~~ vs');
2.36 @@ -439,7 +440,7 @@
2.37
2.38 fun get_type_of_constr_or_abstr thy c =
2.39 case (snd o strip_type o const_typ thy) c
2.40 - of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
2.41 + of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
2.42 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
2.43 | _ => NONE;
2.44
2.45 @@ -641,19 +642,19 @@
2.46 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
2.47 end;
2.48
2.49 -fun desymbolize_tvars thy thms =
2.50 +fun desymbolize_tvars thms =
2.51 let
2.52 val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
2.53 val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
2.54 in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
2.55
2.56 -fun desymbolize_vars thy thm =
2.57 +fun desymbolize_vars thm =
2.58 let
2.59 val vs = Term.add_vars (Thm.prop_of thm) [];
2.60 val var_subst = mk_desymbolization I I Var vs;
2.61 in Thm.certify_instantiate ([], var_subst) thm end;
2.62
2.63 -fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
2.64 +fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
2.65
2.66
2.67 (* abstype certificates *)
2.68 @@ -672,13 +673,12 @@
2.69 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
2.70 val _ = check_decl_ty thy (abs, raw_ty);
2.71 val _ = check_decl_ty thy (rep, rep_ty);
2.72 - val var = (fst o dest_Var) param
2.73 + val _ = (fst o dest_Var) param
2.74 handle TERM _ => bad "Not an abstype certificate";
2.75 val _ = if param = rhs then () else bad "Not an abstype certificate";
2.76 val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
2.77 val ty = domain_type ty';
2.78 val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
2.79 - val ty_abs = range_type ty';
2.80 in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
2.81
2.82
2.83 @@ -716,7 +716,7 @@
2.84
2.85 fun concretify_abs thy tyco abs_thm =
2.86 let
2.87 - val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
2.88 + val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
2.89 val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
2.90 val ty = fastype_of lhs;
2.91 val ty_abs = (fastype_of o snd o dest_comb) lhs;
2.92 @@ -746,8 +746,11 @@
2.93 val tvars = Term.add_tvar_namesT raw_ty [];
2.94 val tvars' = case AxClass.class_of_param thy c
2.95 of SOME class => [TFree (Name.aT, [class])]
2.96 - | NONE => Name.invent_list [] Name.aT (length tvars)
2.97 - |> map (fn v => TFree (v, []));
2.98 + | NONE => (case get_type_of_constr_or_abstr thy c
2.99 + of SOME (tyco, _) => map TFree ((fst o the)
2.100 + (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c))
2.101 + | NONE => Name.invent_list [] Name.aT (length tvars)
2.102 + |> map (fn v => TFree (v, [])));
2.103 val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
2.104 val chead = build_head thy (c, ty);
2.105 in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
2.106 @@ -767,19 +770,19 @@
2.107 fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
2.108 val sorts = map_transpose inter_sorts vss;
2.109 val vts = Name.names Name.context Name.aT sorts;
2.110 - val thms as thm :: _ =
2.111 + val thms' =
2.112 map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
2.113 - val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
2.114 + val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
2.115 fun head_conv ct = if can Thm.dest_comb ct
2.116 then Conv.fun_conv head_conv ct
2.117 else Conv.rewr_conv head_thm ct;
2.118 val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
2.119 - val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
2.120 + val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
2.121 in Equations (cert_thm, propers) end;
2.122
2.123 fun cert_of_proj thy c tyco =
2.124 let
2.125 - val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
2.126 + val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
2.127 val _ = if c = rep then () else
2.128 error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
2.129 in Projection (mk_proj tyco vs ty abs rep, tyco) end;
2.130 @@ -824,7 +827,7 @@
2.131 Thm.prop_of cert_thm
2.132 |> Logic.dest_conjunction_balanced (length propers);
2.133 in (vs, fold (add_rhss_of_eqn thy) equations []) end
2.134 - | typargs_deps_of_cert thy (Projection (t, tyco)) =
2.135 + | typargs_deps_of_cert thy (Projection (t, _)) =
2.136 (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
2.137 | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
2.138 let
2.139 @@ -864,7 +867,7 @@
2.140 o snd o equations_of_cert thy) cert
2.141 | pretty_cert thy (Projection (t, _)) =
2.142 [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
2.143 - | pretty_cert thy (Abstract (abs_thm, tyco)) =
2.144 + | pretty_cert thy (Abstract (abs_thm, _)) =
2.145 [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
2.146
2.147 fun bare_thms_of_cert thy (cert as Equations _) =
2.148 @@ -1118,7 +1121,7 @@
2.149
2.150 fun del_eqn thm thy = case mk_eqn_liberal thy thm
2.151 of SOME (thm, _) => let
2.152 - fun del_eqn' (Default eqns) = empty_fun_spec
2.153 + fun del_eqn' (Default _) = empty_fun_spec
2.154 | del_eqn' (Eqns eqns) =
2.155 Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
2.156 | del_eqn' spec = spec
2.157 @@ -1130,7 +1133,7 @@
2.158
2.159 (* cases *)
2.160
2.161 -fun case_cong thy case_const (num_args, (pos, constrs)) =
2.162 +fun case_cong thy case_const (num_args, (pos, _)) =
2.163 let
2.164 val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
2.165 val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;