--- 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]
--- 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]
--- 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 *}
--- 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]
--- 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)
--- 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 \<longleftrightarrow> n dvd m"
-unfolding dvd_eq_mod_eq_0[symmetric] ..
-
-lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> 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]
--- 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]
--- 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)) ::
--- 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);
--- 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:
--- 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 *}
--- 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*)
--- 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);
--- 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)));
--- 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
--- 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;
--- 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)));
--- 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