From 1d6b1d381bfbb5b4ffce18af22853b0355a78a34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Aug 2016 13:58:10 -0700 Subject: [PATCH] refactor(library/init): rename measurable to has_sizeof --- library/init/default.lean | 2 +- library/init/measurable.lean | 61 ------------------- ...tance.lean => mk_has_sizeof_instance.lean} | 46 +++++++------- library/init/sizeof.lean | 61 +++++++++++++++++++ tests/lean/run/size_of1.lean | 6 +- tests/lean/struct_class.lean.expected.out | 4 +- 6 files changed, 90 insertions(+), 90 deletions(-) delete mode 100644 library/init/measurable.lean rename library/init/meta/{mk_measurable_instance.lean => mk_has_sizeof_instance.lean} (58%) create mode 100644 library/init/sizeof.lean diff --git a/library/init/default.lean b/library/init/default.lean index 69d4bc508d..92c86421fd 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -11,4 +11,4 @@ import init.funext init.function init.subtype init.classical init.simplifier import init.monad init.option init.state init.fin init.list init.char init.string init.to_string import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe import init.meta init.instances -import init.wf init.wf_k init.sigma_lex init.measurable +import init.wf init.wf_k init.sigma_lex init.sizeof diff --git a/library/init/measurable.lean b/library/init/measurable.lean deleted file mode 100644 index eaa1e88cb4..0000000000 --- a/library/init/measurable.lean +++ /dev/null @@ -1,61 +0,0 @@ -/- -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura - -Types with a nat-valued complexity measure. --/ -prelude -import init.nat init.meta.mk_measurable_instance -open nat tactic - -inductive measurable [class] (A : Type) := -mk : (A → nat) → measurable A - -definition size_of {A : Type} [s : measurable A] : A → nat := -measurable.rec_on s (λ f, f) - -definition prop_measurable [instance] (p : Prop) : measurable p := -measurable.mk (λ t, zero) - -definition nat_measurable [instance] : measurable nat := -measurable.mk (λ a, a) - -definition Type_measurable [instance] : measurable Type := -measurable.mk (λ t, zero) - -definition Prop_measurable [instance] : measurable Prop := -measurable.mk (λ t, zero) - -definition fn_measurable [instance] (A : Type) (B : A → Type) : measurable (Π x, B x) := -measurable.mk (λf, zero) - -definition option.measurable [instance] (A : Type) [measurable A] : measurable (option A) := -by mk_measurable_instance - -definition prod_measurable [instance] (A B : Type) [measurable A] [measurable B] : measurable (prod A B) := -by mk_measurable_instance - -definition sum_measurable [instance] (A B : Type) [measurable A] [measurable B] : measurable (sum A B) := -by mk_measurable_instance - -definition list_measurable [instance] (A : Type) [measurable A] : measurable (list A) := -by mk_measurable_instance - -definition unit_measurable [instance] : measurable unit := -by mk_measurable_instance - -definition bool_measurable [instance] : measurable bool := -by mk_measurable_instance - -definition sigma_measurable [instance] (A : Type) (B : A → Type) [measurable A] [∀ x, measurable (B x)] : measurable (Σ x, B x) := -by mk_measurable_instance - -definition subtype_mesurable [instance] (A : Type) (P : A → Prop) [measurable A] : measurable {x \ P x} := -by mk_measurable_instance - -definition pos_num_measurable [instance] : measurable pos_num := -by mk_measurable_instance - -definition num_measurable [instance] : measurable num := -by mk_measurable_instance diff --git a/library/init/meta/mk_measurable_instance.lean b/library/init/meta/mk_has_sizeof_instance.lean similarity index 58% rename from library/init/meta/mk_measurable_instance.lean rename to library/init/meta/mk_has_sizeof_instance.lean index 17f7e8e56f..05db726121 100644 --- a/library/init/meta/mk_measurable_instance.lean +++ b/library/init/meta/mk_has_sizeof_instance.lean @@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -Helper tactic for constructing measurable instance. +Helper tactic for constructing has_sizeof instance. -/ prelude import init.meta.rec_util init.combinator @@ -12,55 +12,55 @@ import init.meta.constructor_tactic namespace tactic open expr environment list -/- Retrieve the name of the type we are building a measurable instance for. -/ -private meta_definition get_measurable_type_name : tactic name := +/- Retrieve the name of the type we are building a has_sizeof instance for. -/ +private meta_definition get_has_sizeof_type_name : tactic name := do { (app (const n _) t) ← target >>= whnf | failed, - when (n ≠ `measurable) failed, + when (n ≠ `has_sizeof) failed, (const I _) ← return (get_app_fn t) | failed, return I } <|> -fail "mk_measurable_instance tactic failed, target type is expected to be of the form (measurable ...)" +fail "mk_has_sizeof_instance tactic failed, target type is expected to be of the form (has_sizeof ...)" /- Try to synthesize constructor argument using type class resolution -/ -private meta_definition mk_measurable_instance_for (a : expr) (use_default : bool) : tactic expr := +private meta_definition mk_has_sizeof_instance_for (a : expr) (use_default : bool) : tactic expr := do t ← infer_type a, do { - m ← mk_app `measurable [t], + m ← mk_app `has_sizeof [t], inst ← mk_instance m, - mk_app `size_of [t, inst, a] } + mk_app `sizeof [t, inst, a] } <|> if use_default = tt then return (const `nat.zero []) else do f ← pp t, - fail (to_fmt "mk_measurable_instance failed, failed to generate instance for" ++ format.nest 2 (format.line ++ f)) + fail (to_fmt "mk_has_sizeof_instance failed, failed to generate instance for" ++ format.nest 2 (format.line ++ f)) -private meta_definition mk_sizes_of : bool → name → name → list name → nat → tactic (list expr) +private meta_definition mk_sizeof : bool → name → name → list name → nat → tactic (list expr) | _ _ _ [] num_rec := return [] | use_default I_name F_name (fname::fnames) num_rec := do field ← get_local fname, rec ← is_type_app_of field I_name, - sz ← if rec = tt then mk_brec_on_rec_value F_name num_rec else mk_measurable_instance_for field use_default, - szs ← mk_sizes_of use_default I_name F_name fnames (if rec = tt then num_rec + 1 else num_rec), + sz ← if rec = tt then mk_brec_on_rec_value F_name num_rec else mk_has_sizeof_instance_for field use_default, + szs ← mk_sizeof use_default I_name F_name fnames (if rec = tt then num_rec + 1 else num_rec), return (sz :: szs) private meta_definition mk_sum : list expr → expr | [] := app (const `nat.succ []) (const `nat.zero []) | (e::es) := app (app (const `nat.add []) e) (mk_sum es) -private meta_definition measurable_case (use_default : bool) (I_name F_name : name) (field_names : list name) : tactic unit := -do szs ← mk_sizes_of use_default I_name F_name field_names 0, +private meta_definition has_sizeof_case (use_default : bool) (I_name F_name : name) (field_names : list name) : tactic unit := +do szs ← mk_sizeof use_default I_name F_name field_names 0, exact (mk_sum szs) -private meta_definition for_each_measurable_goal : bool → name → name → list (list name) → tactic unit -| d I_name F_name [] := now <|> fail "mk_measurable_instance failed, unexpected number of cases" +private meta_definition for_each_has_sizeof_goal : bool → name → name → list (list name) → tactic unit +| d I_name F_name [] := now <|> fail "mk_has_sizeof_instance failed, unexpected number of cases" | d I_name F_name (ns::nss) := do - solve1 (measurable_case d I_name F_name ns), - for_each_measurable_goal d I_name F_name nss + solve1 (has_sizeof_case d I_name F_name ns), + for_each_has_sizeof_goal d I_name F_name nss -meta_definition mk_measurable_instance_core (use_default : bool) : tactic unit := -do I_name ← get_measurable_type_name, +meta_definition mk_has_sizeof_instance_core (use_default : bool) : tactic unit := +do I_name ← get_has_sizeof_type_name, constructor, env ← get_env, v_name : name ← return `_v, @@ -72,10 +72,10 @@ do I_name ← get_measurable_type_name, else intro v_name >> return (), arg_names : list (list name) ← mk_constructors_arg_names I_name `_p, get_local v_name >>= λ v, cases_using v (join arg_names), - for_each_measurable_goal use_default I_name F_name arg_names + for_each_has_sizeof_goal use_default I_name F_name arg_names -meta_definition mk_measurable_instance : tactic unit := -mk_measurable_instance_core ff +meta_definition mk_has_sizeof_instance : tactic unit := +mk_has_sizeof_instance_core ff end tactic diff --git a/library/init/sizeof.lean b/library/init/sizeof.lean new file mode 100644 index 0000000000..f726f9f392 --- /dev/null +++ b/library/init/sizeof.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura + +Types with a nat-valued complexity measure. +-/ +prelude +import init.nat init.meta.mk_has_sizeof_instance +open nat tactic + +structure has_sizeof [class] (A : Type) := +(sizeof : A → nat) + +definition sizeof {A : Type} [s : has_sizeof A] : A → nat := +has_sizeof.sizeof + +definition prop_has_sizeof [instance] (p : Prop) : has_sizeof p := +has_sizeof.mk (λ t, zero) + +definition nat_has_sizeof [instance] : has_sizeof nat := +has_sizeof.mk (λ a, a) + +definition Type_has_sizeof [instance] : has_sizeof Type := +has_sizeof.mk (λ t, zero) + +definition Prop_has_sizeof [instance] : has_sizeof Prop := +has_sizeof.mk (λ t, zero) + +definition fn_has_sizeof [instance] (A : Type) (B : A → Type) : has_sizeof (Π x, B x) := +has_sizeof.mk (λf, zero) + +definition option.has_sizeof [instance] (A : Type) [has_sizeof A] : has_sizeof (option A) := +by mk_has_sizeof_instance + +definition prod_has_sizeof [instance] (A B : Type) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) := +by mk_has_sizeof_instance + +definition sum_has_sizeof [instance] (A B : Type) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) := +by mk_has_sizeof_instance + +definition list_has_sizeof [instance] (A : Type) [has_sizeof A] : has_sizeof (list A) := +by mk_has_sizeof_instance + +definition unit_has_sizeof [instance] : has_sizeof unit := +by mk_has_sizeof_instance + +definition bool_has_sizeof [instance] : has_sizeof bool := +by mk_has_sizeof_instance + +definition sigma_has_sizeof [instance] (A : Type) (B : A → Type) [has_sizeof A] [∀ x, has_sizeof (B x)] : has_sizeof (Σ x, B x) := +by mk_has_sizeof_instance + +definition subtype_has_sizeof [instance] (A : Type) (P : A → Prop) [has_sizeof A] : has_sizeof {x \ P x} := +by mk_has_sizeof_instance + +definition pos_num_has_sizeof [instance] : has_sizeof pos_num := +by mk_has_sizeof_instance + +definition num_has_sizeof [instance] : has_sizeof num := +by mk_has_sizeof_instance diff --git a/tests/lean/run/size_of1.lean b/tests/lean/run/size_of1.lean index 9323d91db8..454e12d6c0 100644 --- a/tests/lean/run/size_of1.lean +++ b/tests/lean/run/size_of1.lean @@ -1,10 +1,10 @@ open tactic -example : size_of [tt, tt] < size_of [tt, ff, tt] := +example : sizeof [tt, tt] < sizeof [tt, ff, tt] := dec_trivial -example : size_of [tt, tt] = size_of [ff, ff] := +example : sizeof [tt, tt] = sizeof [ff, ff] := dec_trivial -example : size_of (3:nat) < size_of ([3] : list nat) := +example : sizeof (3:nat) < sizeof ([3] : list nat) := dec_trivial diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 08a758fe86..caf17364fc 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -21,6 +21,7 @@ has_mul : Type → Type has_neg : Type → Type has_one : Type → Type has_ordering : Type → Type +has_sizeof : Type → Type has_sub : Type → Type has_to_format : Type → Type has_to_pexpr : Type → Type @@ -28,7 +29,6 @@ has_to_string : Type → Type has_to_tactic_format : Type → Type has_zero : Type → Type inhabited : Type → Type -measurable : Type → Type monad : (Type → Type) → Type nonempty : Type → Prop point : Type → Type → Type @@ -58,6 +58,7 @@ has_mul : Type → Type has_neg : Type → Type has_one : Type → Type has_ordering : Type → Type +has_sizeof : Type → Type has_sub : Type → Type has_to_format : Type → Type has_to_pexpr : Type → Type @@ -65,7 +66,6 @@ has_to_string : Type → Type has_to_tactic_format : Type → Type has_zero : Type → Type inhabited : Type → Type -measurable : Type → Type monad : (Type → Type) → Type nonempty : Type → Prop point : Type → Type → Type