# HG changeset patch # User huffman # Date 1235174840 28800 # Node ID e54d4d41fe8f0f7aec35fb00e55bdcbcb9fb8db0 # Parent c7f0c1b8001b608765bd7da883bf605e23b7f989# Parent bd786c37af84da6df4795e1e9cb9b1b1679ed081 merged diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 16:07:20 2009 -0800 @@ -77,7 +77,7 @@ @{thm mod_self}, @{thm "zmod_self"}, @{thm mod_by_0}, @{thm div_by_0}, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, - @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, + @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, Suc_plus1] addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 16:07:20 2009 -0800 @@ -99,7 +99,7 @@ addsimps [refl,nat_mod_add_eq, @{thm "mod_self"}, @{thm "zmod_self"}, @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, - @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, + @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Divides.thy Fri Feb 20 16:07:20 2009 -0800 @@ -795,12 +795,6 @@ apply (auto simp add: Suc_diff_le le_mod_geq) done -lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)" -by simp - -lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)" -by simp - subsubsection {* The Divides Relation *} diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 16:07:20 2009 -0800 @@ -436,8 +436,8 @@ *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] -declare nat_mod_div_trivial[algebra] -declare nat_mod_mod_trivial[algebra] +declare mod_div_trivial[algebra] +declare mod_mod_trivial[algebra] declare conjunct1[OF DIVISION_BY_ZERO, algebra] declare conjunct2[OF DIVISION_BY_ZERO, algebra] declare zmod_zdiv_equality[symmetric,algebra] @@ -448,8 +448,8 @@ declare zmod_zminus2[algebra] declare zdiv_zero[algebra] declare zmod_zero[algebra] -declare zmod_1[algebra] -declare zdiv_1[algebra] +declare mod_by_1[algebra] +declare div_by_1[algebra] declare zmod_minus1_right[algebra] declare zdiv_minus1_right[algebra] declare mod_div_trivial[algebra] diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/IntDiv.thy Fri Feb 20 16:07:20 2009 -0800 @@ -547,34 +547,6 @@ simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *} -(* The following 8 lemmas are made unnecessary by the above simprocs: *) - -lemmas div_pos_pos_number_of = - div_pos_pos [of "number_of v" "number_of w", standard] - -lemmas div_neg_pos_number_of = - div_neg_pos [of "number_of v" "number_of w", standard] - -lemmas div_pos_neg_number_of = - div_pos_neg [of "number_of v" "number_of w", standard] - -lemmas div_neg_neg_number_of = - div_neg_neg [of "number_of v" "number_of w", standard] - - -lemmas mod_pos_pos_number_of = - mod_pos_pos [of "number_of v" "number_of w", standard] - -lemmas mod_neg_pos_number_of = - mod_neg_pos [of "number_of v" "number_of w", standard] - -lemmas mod_pos_neg_number_of = - mod_pos_neg [of "number_of v" "number_of w", standard] - -lemmas mod_neg_neg_number_of = - mod_neg_neg [of "number_of v" "number_of w", standard] - - lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w", standard] @@ -584,15 +556,6 @@ text{*Special-case simplification *} -lemma zmod_1 [simp]: "a mod (1::int) = 0" -apply (cut_tac a = a and b = 1 in pos_mod_sign) -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) -apply (auto simp del:pos_mod_bound pos_mod_sign) -done - -lemma zdiv_1 [simp]: "a div (1::int) = a" -by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) - lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" apply (cut_tac a = a and b = "-1" in neg_mod_sign) apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound) diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Presburger.thy Fri Feb 20 16:07:20 2009 -0800 @@ -412,19 +412,15 @@ "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" by (rule eq_number_of_eq) -lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \ n dvd m" -unfolding dvd_eq_mod_eq_0[symmetric] .. - -lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \ n dvd m" -unfolding zdvd_iff_zmod_eq_0[symmetric] .. +declare dvd_eq_mod_eq_0[symmetric, presburger] declare mod_1[presburger] declare mod_0[presburger] -declare zmod_1[presburger] +declare mod_by_1[presburger] declare zmod_zero[presburger] declare zmod_self[presburger] declare mod_self[presburger] declare mod_by_0[presburger] -declare nat_mod_div_trivial[presburger] +declare mod_div_trivial[presburger] declare div_mod_equality2[presburger] declare div_mod_equality[presburger] declare mod_div_equality2[presburger] diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 16:07:20 2009 -0800 @@ -129,7 +129,7 @@ @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, - @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, + @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] @ @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Tools/datatype_package.ML Fri Feb 20 16:07:20 2009 -0800 @@ -659,7 +659,7 @@ | pretty_constr (co, [ty']) = (Pretty.block o Pretty.breaks) [Syntax.pretty_term ctxt (Const (co, ty' --> ty)), - Syntax.pretty_typ ctxt ty'] + pretty_typ_br ty'] | pretty_constr (co, tys) = (Pretty.block o Pretty.breaks) (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 16:07:20 2009 -0800 @@ -216,7 +216,7 @@ (** Final simplification for the CancelFactor simprocs **) val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq - [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}]; + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; fun cancel_simplify_meta_eq cancel_th ss th = simplify_one ss (([th, cancel_th]) MRS trans); diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 16:07:20 2009 -0800 @@ -95,7 +95,7 @@ lemma z1pdiv2: "(2 * b + 1) div 2 = (b::int)" by arith -lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2, +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, simplified int_one_le_iff_zero_less, simplified, standard] lemma axxbyy: diff -r c7f0c1b8001b -r e54d4d41fe8f src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Fri Feb 20 11:58:00 2009 -0800 +++ b/src/HOL/ex/Eval_Examples.thy Fri Feb 20 16:07:20 2009 -0800 @@ -1,6 +1,4 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) +(* Author: Florian Haftmann, TU Muenchen *) header {* Small examples for evaluation mechanisms *} diff -r c7f0c1b8001b -r e54d4d41fe8f src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Pure/Isar/code.ML Fri Feb 20 16:07:20 2009 -0800 @@ -35,7 +35,7 @@ val these_raw_eqns: theory -> string -> (thm * bool) list val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option - val get_case_scheme: theory -> string -> (int * string list) option + val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool val default_typscheme: theory -> string -> (string * sort) list * typ @@ -111,7 +111,7 @@ (** logical and syntactical specification of executable code **) -(* defining equations *) +(* code equations *) type eqns = bool * (thm * bool) list lazy; (*default flag, theorems with linear flag (perhaps lazy)*) @@ -136,7 +136,7 @@ Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); fun drop (thm', linear') = if (linear orelse not linear') andalso matches_args (args_of thm') then - (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true) + (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true) else false; in (thm, linear) :: filter_out drop thms end; @@ -409,7 +409,7 @@ in (Pretty.writeln o Pretty.chunks) [ Pretty.block ( - Pretty.str "defining equations:" + Pretty.str "code equations:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_eqn) eqns ), @@ -452,7 +452,7 @@ val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms'; fun unify ty env = Sign.typ_unify thy (ty1, ty) env handle Type.TUNIFY => - error ("Type unificaton failed, while unifying defining equations\n" + error ("Type unificaton failed, while unifying code equations\n" ^ (cat_lines o map Display.string_of_thm) thms ^ "\nwith types\n" ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys)); @@ -463,7 +463,7 @@ fun check_linear (eqn as (thm, linear)) = if linear then eqn else Code_Unit.bad_thm - ("Duplicate variables on left hand side of defining equation:\n" + ("Duplicate variables on left hand side of code equation:\n" ^ Display.string_of_thm thm); fun mk_eqn thy linear = @@ -525,22 +525,13 @@ then SOME tyco else NONE | _ => NONE; -fun get_constr_typ thy c = - case get_datatype_of_constr thy c - of SOME tyco => let - val (vs, cos) = get_datatype thy tyco; - val SOME tys = AList.lookup (op =) cos c; - val ty = tys ---> Type (tyco, map TFree vs); - in SOME (Logic.varifyT ty) end - | NONE => NONE; - fun recheck_eqn thy = Code_Unit.error_thm (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy)); fun recheck_eqns_const thy c eqns = let fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm - then eqn else error ("Wrong head of defining equation,\nexpected constant " + then eqn else error ("Wrong head of code equation,\nexpected constant " ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) in map (cert o recheck_eqn thy) eqns end; @@ -554,11 +545,11 @@ let val c = Code_Unit.const_eqn thm; val _ = if not default andalso (is_some o AxClass.class_of_param thy) c - then error ("Rejected polymorphic equation for overloaded constant:\n" + then error ("Rejected polymorphic code equation for overloaded constant:\n" ^ Display.string_of_thm thm) else (); val _ = if not default andalso (is_some o get_datatype_of_constr thy) c - then error ("Rejected equation for datatype constructor:\n" + then error ("Rejected code equation for datatype constructor:\n" ^ Display.string_of_thm thm) else (); in change_eqns false c (add_thm thy default (thm, linear)) thy end @@ -583,7 +574,12 @@ fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); -fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy); +fun get_case_scheme thy c = case Symtab.lookup ((fst o the_cases o the_exec) thy) c + of SOME (base_case_scheme as (_, case_pats)) => + if forall (is_some o get_datatype_of_constr thy) case_pats + then SOME (1 + Int.max (1, length case_pats), base_case_scheme) + else NONE + | NONE => NONE; val is_undefined = Symtab.defined o snd o the_cases o the_exec; @@ -727,18 +723,16 @@ fun default_typscheme thy c = let - val typscheme = curry (Code_Unit.typscheme thy) c - val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes - o curry Const "" o Sign.the_const_type thy; + fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const + o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c; + fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty); in case AxClass.class_of_param thy c - of SOME class => the_const_type c - |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class]))) - |> typscheme - | NONE => (case get_constr_typ thy c - of SOME ty => typscheme ty - | NONE => (case get_eqns thy c - of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm)) - | [] => typscheme (the_const_type c))) end; + of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c)) + | NONE => if is_some (get_datatype_of_constr thy c) + then strip_sorts (the_const_typscheme c) + else case get_eqns thy c + of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm)) + | [] => strip_sorts (the_const_typscheme c) end; end; (*local*) diff -r c7f0c1b8001b -r e54d4d41fe8f src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Pure/Isar/code_unit.ML Fri Feb 20 16:07:20 2009 -0800 @@ -34,7 +34,7 @@ val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * typ list) list) - (*defining equations*) + (*code equations*) val assert_eqn: theory -> thm -> thm val mk_eqn: theory -> thm -> thm * bool val assert_linear: (string -> bool) -> thm * bool -> thm * bool @@ -76,10 +76,11 @@ fun typscheme thy (c, ty) = let - fun dest (TVar ((v, 0), sort)) = (v, sort) + val ty' = Logic.unvarifyT ty; + fun dest (TFree (v, sort)) = (v, sort) | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); - val vs = map dest (Sign.const_typargs thy (c, ty)); - in (vs, ty) end; + val vs = map dest (Sign.const_typargs thy (c, ty')); + in (vs, Type.strip_sorts ty') end; fun inst_thm thy tvars' thm = let @@ -313,10 +314,10 @@ val ((tyco, sorts), cs'') = fold add cs' (apsnd single c'); val vs = Name.names Name.context Name.aT sorts; val cs''' = map (inst vs) cs''; - in (tyco, (vs, cs''')) end; + in (tyco, (vs, rev cs''')) end; -(* defining equations *) +(* code equations *) fun assert_eqn thy thm = let @@ -351,7 +352,7 @@ ^ Display.string_of_thm thm) | check 0 (Var _) = () | check _ (Var _) = bad_thm - ("Variable with application on left hand side of defining equation\n" + ("Variable with application on left hand side of code equation\n" ^ Display.string_of_thm thm) | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty @@ -363,7 +364,7 @@ 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 defining equation\n" + ^ "\nof code equation\n" ^ Display.string_of_thm thm ^ "\nis incompatible with declared function type\n" ^ string_of_typ thy ty_decl) @@ -388,7 +389,7 @@ fun assert_linear is_cons (thm, false) = (thm, false) | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true) else bad_thm - ("Duplicate variables on left hand side of defining equation:\n" + ("Duplicate variables on left hand side of code equation:\n" ^ Display.string_of_thm thm); diff -r c7f0c1b8001b -r e54d4d41fe8f src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Tools/code/code_funcgr.ML Fri Feb 20 16:07:20 2009 -0800 @@ -317,13 +317,13 @@ in val _ = - OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val _ = - OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); diff -r c7f0c1b8001b -r e54d4d41fe8f src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Tools/code/code_target.ML Fri Feb 20 16:07:20 2009 -0800 @@ -418,7 +418,7 @@ val program4 = Graph.subgraph (member (op =) names_all) program3; val empty_funs = filter_out (member (op =) abortable) (Code_Thingol.empty_funs program3); - val _ = if null empty_funs then () else error ("No defining equations for " + val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); in serializer module args (labelled_name thy program2) reserved includes diff -r c7f0c1b8001b -r e54d4d41fe8f src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Tools/code/code_thingol.ML Fri Feb 20 16:07:20 2009 -0800 @@ -453,7 +453,7 @@ let val err_class = Sorts.class_error (Syntax.pp_global thy) e; val err_thm = case thm - of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => ""; + of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => ""; val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^ Syntax.string_of_sort_global thy sort; in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end; @@ -582,9 +582,8 @@ fun stmt_classparam class = ensure_class thy algbr funcgr class #>> (fn class => Classparam (c, class)); - fun stmt_fun ((vs, raw_ty), raw_thms) = + fun stmt_fun ((vs, ty), raw_thms) = let - val ty = Logic.unvarifyT raw_ty; (*FIXME change convention here*) val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty then raw_thms else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms; @@ -643,11 +642,6 @@ val ts_clause = nth_drop t_pos ts; fun mk_clause (co, num_co_args) t = let - val _ = if (is_some o Code.get_datatype_of_constr thy) co then () - else error ("Non-constructor " ^ quote co - ^ " encountered in case pattern" - ^ (case thm of NONE => "" - | SOME thm => ", in equation\n" ^ Display.string_of_thm thm)) val (vs, body) = Term.strip_abs_eta num_co_args t; val not_undefined = case body of (Const (c, _)) => not (Code.is_undefined thy c) @@ -702,9 +696,7 @@ translate_case thy algbr funcgr thm case_scheme ((c, ty), ts) and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) = case Code.get_case_scheme thy c - of SOME (base_case_scheme as (_, case_pats)) => - translate_app_case thy algbr funcgr thm - (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts + of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts | NONE => translate_app_const thy algbr funcgr thm c_ty_ts; diff -r c7f0c1b8001b -r e54d4d41fe8f src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Tools/code/code_wellsorted.ML Fri Feb 20 16:07:20 2009 -0800 @@ -50,9 +50,9 @@ fun complete_proper_sort thy = Sign.complete_sort thy #> filter (can (AxClass.get_info thy)); -fun inst_params thy tyco class = +fun inst_params thy tyco = map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) - ((#params o AxClass.get_info thy) class); + o maps (#params o AxClass.get_info thy); fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) @@ -100,12 +100,11 @@ case AList.lookup (op =) arities inst of SOME classess => (classess, ([], [])) | NONE => let + val all_classes = complete_proper_sort thy [class]; + val superclasses = remove (op =) class all_classes val classess = map (complete_proper_sort thy) (Sign.arity_sorts thy tyco [class]); - val superclasses = [class] - |> complete_proper_sort thy - |> remove (op =) class; - val inst_params = inst_params thy tyco class; + val inst_params = inst_params thy tyco all_classes; in (classess, (superclasses, inst_params)) end; fun add_classes thy arities eqngr c_k new_classes vardeps_data = @@ -225,7 +224,7 @@ let fun class_relation (x, _) _ = x; fun type_constructor tyco xs class = - inst_params thy tyco class @ (maps o maps) fst xs; + inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs; fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); in flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra @@ -388,13 +387,13 @@ in val _ = - OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val _ = - OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); diff -r c7f0c1b8001b -r e54d4d41fe8f src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Feb 20 11:58:00 2009 -0800 +++ b/src/Tools/nbe.ML Fri Feb 20 16:07:20 2009 -0800 @@ -389,8 +389,8 @@ val ts' = take_until is_dict ts; val c = const_of_idx idx; val (_, T) = Code.default_typscheme thy c; - val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; - val typidx' = typidx + maxidx_of_typ T' + 1; + val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T; + val typidx' = typidx + 1; in of_apps bounds (Term.Const (c, T'), ts') typidx' end | of_univ bounds (Free (name, ts)) typidx = of_apps bounds (Term.Free (name, dummyT), ts) typidx