# HG changeset patch # User haftmann # Date 1290891736 -3600 # Node ID 77a468590560f188014148b2e12384ae3738548c # Parent 782399904d9cc97b8cfe6f5754c59740d2745366# Parent 4dd4901a724289b09ad730b61d0ccfc52f0847f0 merged diff -r 782399904d9c -r 77a468590560 src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Sat Nov 27 20:48:06 2010 +0100 +++ b/src/HOL/ex/Eval_Examples.thy Sat Nov 27 22:02:16 2010 +0100 @@ -9,26 +9,26 @@ text {* evaluation oracle *} lemma "True \ False" by eval -lemma "\ (Suc 0 = Suc 1)" by eval -lemma "[] = ([]\ int list)" by eval +lemma "Suc 0 \ Suc 1" by eval +lemma "[] = ([] :: int list)" by eval lemma "[()] = [()]" by eval -lemma "fst ([]::nat list, Suc 0) = []" by eval +lemma "fst ([] :: nat list, Suc 0) = []" by eval text {* SML evaluation oracle *} lemma "True \ False" by evaluation -lemma "\ (Suc 0 = Suc 1)" by evaluation -lemma "[] = ([]\ int list)" by evaluation +lemma "Suc 0 \ Suc 1" by evaluation +lemma "[] = ([] :: int list)" by evaluation lemma "[()] = [()]" by evaluation -lemma "fst ([]::nat list, Suc 0) = []" by evaluation +lemma "fst ([] :: nat list, Suc 0) = []" by evaluation text {* normalization *} lemma "True \ False" by normalization -lemma "\ (Suc 0 = Suc 1)" by normalization -lemma "[] = ([]\ int list)" by normalization +lemma "Suc 0 \ Suc 1" by normalization +lemma "[] = ([] :: int list)" by normalization lemma "[()] = [()]" by normalization -lemma "fst ([]::nat list, Suc 0) = []" by normalization +lemma "fst ([] :: nat list, Suc 0) = []" by normalization text {* term evaluation *} @@ -47,10 +47,10 @@ value [SML] "nat 100" value [nbe] "nat 100" -value "(10\int) \ 12" -value [code] "(10\int) \ 12" -value [SML] "(10\int) \ 12" -value [nbe] "(10\int) \ 12" +value "(10::int) \ 12" +value [code] "(10::int) \ 12" +value [SML] "(10::int) \ 12" +value [nbe] "(10::int) \ 12" value "max (2::int) 4" value [code] "max (2::int) 4" @@ -62,29 +62,29 @@ value [SML] "of_int 2 / of_int 4 * (1::rat)" value [nbe] "of_int 2 / of_int 4 * (1::rat)" -value "[]::nat list" -value [code] "[]::nat list" -value [SML] "[]::nat list" -value [nbe] "[]::nat list" +value "[] :: nat list" +value [code] "[] :: nat list" +value [SML] "[] :: nat list" +value [nbe] "[] :: nat list" value "[(nat 100, ())]" value [code] "[(nat 100, ())]" value [SML] "[(nat 100, ())]" value [nbe] "[(nat 100, ())]" - text {* a fancy datatype *} -datatype ('a, 'b) bair = - Bair "'a\order" 'b - | Shift "('a, 'b) cair" - | Dummy unit -and ('a, 'b) cair = - Cair 'a 'b +datatype ('a, 'b) foo = + Foo "'a\order" 'b + | Bla "('a, 'b) bar" + | Dummy nat +and ('a, 'b) bar = + Bar 'a 'b + | Blubb "('a, 'b) foo" -value "Shift (Cair (4::nat) [Suc 0])" -value [code] "Shift (Cair (4::nat) [Suc 0])" -value [SML] "Shift (Cair (4::nat) [Suc 0])" -value [nbe] "Shift (Cair (4::nat) [Suc 0])" +value "Bla (Bar (4::nat) [Suc 0])" +value [code] "Bla (Bar (4::nat) [Suc 0])" +value [SML] "Bla (Bar (4::nat) [Suc 0])" +value [nbe] "Bla (Bar (4::nat) [Suc 0])" end diff -r 782399904d9c -r 77a468590560 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Nov 27 20:48:06 2010 +0100 +++ b/src/Pure/Isar/code.ML Sat Nov 27 22:02:16 2010 +0100 @@ -316,7 +316,7 @@ val data = case Datatab.lookup datatab kind of SOME data => data | NONE => invoke_init kind; - val result as (x, data') = f (dest data); + val result as (_, data') = f (dest data); val _ = Synchronized.change dataref ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); in result end; @@ -358,11 +358,13 @@ of SOME ty => ty | NONE => (Type.strip_sorts o Sign.the_const_type thy) c; +fun args_number thy = length o fst o strip_type o const_typ thy; + fun subst_signature thy c ty = let - fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) = + fun mk_subst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_subst tys1 tys2 - | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty)) + | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty)) in case lookup_typ thy c of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty' | NONE => ty @@ -370,7 +372,10 @@ fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t); -fun args_number thy = length o fst o strip_type o const_typ thy; +fun logical_typscheme thy (c, ty) = + (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); + +fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty); (* datatypes *) @@ -407,13 +412,14 @@ val _ = if (tyco' : string) <> tyco then error "Different type constructors in constructor set" else (); - val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts - in ((tyco, sorts), c :: cs) end; + val sorts'' = + map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts + in ((tyco, sorts''), c :: cs) end; fun inst vs' (c, (vs, ty)) = let val the_v = the o AList.lookup (op =) (vs ~~ vs'); val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; - val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty')); + val (vs'', _) = logical_typscheme thy (c, ty'); in (c, (vs'', (fst o strip_type) ty')) end; val c' :: cs' = map (ty_sorts thy) cs; val ((tyco, sorts), cs'') = fold add cs' (apsnd single c'); @@ -439,7 +445,7 @@ fun get_type_of_constr_or_abstr thy c = case (snd o strip_type o const_typ thy) c - of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco + of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end | _ => NONE; @@ -592,11 +598,6 @@ fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; -fun logical_typscheme thy (c, ty) = - (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); - -fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty); - fun mk_proj tyco vs ty abs rep = let val ty_abs = Type (tyco, map TFree vs); @@ -641,19 +642,19 @@ else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) end; -fun desymbolize_tvars thy thms = +fun desymbolize_tvars thms = let val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; in map (Thm.certify_instantiate (tvar_subst, [])) thms end; -fun desymbolize_vars thy thm = +fun desymbolize_vars thm = let val vs = Term.add_vars (Thm.prop_of thm) []; val var_subst = mk_desymbolization I I Var vs; in Thm.certify_instantiate ([], var_subst) thm end; -fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); +fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars; (* abstype certificates *) @@ -672,13 +673,12 @@ 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 + val _ = (fst o dest_Var) param handle TERM _ => bad "Not an abstype certificate"; val _ = if param = rhs then () else bad "Not an abstype certificate"; val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty); val ty = domain_type ty'; - val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty')); - val ty_abs = range_type ty'; + val (vs', _) = logical_typscheme thy (abs, ty'); in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; @@ -716,7 +716,7 @@ fun concretify_abs thy tyco abs_thm = let - val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco; + val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco; val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm val ty = fastype_of lhs; val ty_abs = (fastype_of o snd o dest_comb) lhs; @@ -742,13 +742,16 @@ fun empty_cert thy c = let - val raw_ty = const_typ thy c; - val tvars = Term.add_tvar_namesT raw_ty []; - val tvars' = case AxClass.class_of_param thy c - of SOME class => [TFree (Name.aT, [class])] - | NONE => Name.invent_list [] Name.aT (length tvars) - |> map (fn v => TFree (v, [])); - val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; + val raw_ty = Logic.unvarifyT_global (const_typ thy c); + val (vs, _) = logical_typscheme thy (c, raw_ty); + val sortargs = case AxClass.class_of_param thy c + of SOME class => [[class]] + | NONE => (case get_type_of_constr_or_abstr thy c + of SOME (tyco, _) => (map snd o fst o the) + (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c) + | NONE => replicate (length vs) []); + val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs); + val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty val chead = build_head thy (c, ty); in Equations (Thm.weaken chead Drule.dummy_thm, []) end; @@ -767,19 +770,19 @@ fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; val sorts = map_transpose inter_sorts vss; val vts = Name.names Name.context Name.aT sorts; - val thms as thm :: _ = + val thms' = map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms; - val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms)))); + val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); fun head_conv ct = if can Thm.dest_comb ct then Conv.fun_conv head_conv ct else Conv.rewr_conv head_thm ct; val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); - val cert_thm = Conjunction.intr_balanced (map rewrite_head thms); + val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); in Equations (cert_thm, propers) end; fun cert_of_proj thy c tyco = let - val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco; + val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco; val _ = if c = rep then () else error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); in Projection (mk_proj tyco vs ty abs rep, tyco) end; @@ -824,7 +827,7 @@ Thm.prop_of cert_thm |> Logic.dest_conjunction_balanced (length propers); in (vs, fold (add_rhss_of_eqn thy) equations []) end - | typargs_deps_of_cert thy (Projection (t, tyco)) = + | typargs_deps_of_cert thy (Projection (t, _)) = (fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = let @@ -864,7 +867,7 @@ o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)] - | pretty_cert thy (Abstract (abs_thm, tyco)) = + | pretty_cert thy (Abstract (abs_thm, _)) = [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; fun bare_thms_of_cert thy (cert as Equations _) = @@ -1118,7 +1121,7 @@ fun del_eqn thm thy = case mk_eqn_liberal thy thm of SOME (thm, _) => let - fun del_eqn' (Default eqns) = empty_fun_spec + fun del_eqn' (Default _) = empty_fun_spec | del_eqn' (Eqns eqns) = Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns) | del_eqn' spec = spec @@ -1130,7 +1133,7 @@ (* cases *) -fun case_cong thy case_const (num_args, (pos, constrs)) = +fun case_cong thy case_const (num_args, (pos, _)) = let val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context; val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;