max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init): rename measurable to has_sizeof

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-08 13:58:10 -07:00
parent 139c15878d
commit 1d6b1d381b
6 changed files with 90 additions and 90 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/default.lean
View file

@ -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

61
library/init/measurable.lean
View file

@ -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

46
library/init/meta/mk_measurable_instance.lean → library/init/meta/mk_has_sizeof_instance.lean
View file

@ -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

61
library/init/sizeof.lean Normal file
View file

@ -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

6
tests/lean/run/size_of1.lean
View file

@ -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

4
tests/lean/struct_class.lean.expected.out
View file

@ -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