From 71685e4dd67c62ba62cdff13e8edd5612bf1b9cc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Mar 2017 17:47:49 -0700 Subject: [PATCH] feat(frontends/lean): add support for `t.` and `t.` when t is a composite term Replace `^.` with `.` in the stdlib --- library/data/bitvec.lean | 2 +- library/data/hash_map.lean | 4 +- library/data/stream.lean | 2 +- library/data/vector.lean | 2 +- library/init/algebra/field.lean | 4 +- library/init/algebra/group.lean | 6 +- library/init/algebra/order.lean | 4 +- library/init/algebra/ordered_ring.lean | 6 +- library/init/algebra/ring.lean | 10 +- library/init/classical.lean | 14 +- library/init/data/array.lean | 28 +-- library/init/data/fin/ops.lean | 28 +-- library/init/data/int/basic.lean | 8 +- library/init/data/int/order.lean | 6 +- library/init/data/nat/lemmas.lean | 14 +- library/init/data/option/instances.lean | 3 +- library/init/data/set.lean | 2 +- library/init/data/string/basic.lean | 2 +- library/init/logic.lean | 18 +- library/init/meta/async_tactic.lean | 14 +- library/init/meta/comp_value_tactics.lean | 2 +- library/init/meta/converter.lean | 26 +-- library/init/meta/decl_cmds.lean | 20 +- library/init/meta/declaration.lean | 4 +- library/init/meta/environment.lean | 6 +- library/init/meta/expr.lean | 4 +- library/init/meta/format.lean | 2 +- library/init/meta/fun_info.lean | 12 +- library/init/meta/inductive_compiler.lean | 4 +- library/init/meta/interactive.lean | 56 ++--- library/init/meta/match_tactic.lean | 10 +- library/init/meta/name.lean | 4 +- library/init/meta/rb_map.lean | 20 +- library/init/meta/relation_tactics.lean | 12 +- library/init/meta/smt/congruence_closure.lean | 2 +- library/init/meta/smt/interactive.lean | 2 +- library/init/meta/tactic.lean | 12 +- library/init/meta/transfer.lean | 50 ++--- library/init/propext.lean | 8 +- library/init/relator.lean | 4 +- library/init/wf.lean | 2 +- library/tools/debugger/cli.lean | 40 ++-- library/tools/debugger/util.lean | 28 +-- library/tools/mini_crush/default.lean | 36 ++-- library/tools/mini_crush/nano_crush.lean | 30 +-- library/tools/super/cdcl.lean | 2 +- library/tools/super/cdcl_solver.lean | 148 ++++++------- library/tools/super/clause.lean | 60 +++--- library/tools/super/clause_ops.lean | 56 ++--- library/tools/super/clausifier.lean | 74 +++---- library/tools/super/datatypes.lean | 20 +- library/tools/super/defs.lean | 8 +- library/tools/super/demod.lean | 40 ++-- library/tools/super/equality.lean | 18 +- library/tools/super/factoring.lean | 26 +-- library/tools/super/inhabited.lean | 18 +- library/tools/super/lpo.lean | 4 +- library/tools/super/misc_preprocessing.lean | 16 +- library/tools/super/prover.lean | 10 +- library/tools/super/prover_state.lean | 198 +++++++++--------- library/tools/super/resolution.lean | 40 ++-- library/tools/super/selection.lean | 34 +-- library/tools/super/simp.lean | 8 +- library/tools/super/splitting.lean | 44 ++-- library/tools/super/subsumption.lean | 34 +-- library/tools/super/superposition.lean | 66 +++--- library/tools/super/trim.lean | 6 +- library/tools/super/utils.lean | 6 +- src/frontends/lean/builtin_exprs.cpp | 37 ---- src/frontends/lean/parser.cpp | 21 +- src/frontends/lean/scanner.cpp | 68 +++++- src/frontends/lean/scanner.h | 15 +- 72 files changed, 840 insertions(+), 810 deletions(-) diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 440e26bd41..c1c19e2429 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -101,7 +101,7 @@ section arith protected def mul (x y : bitvec n) : bitvec n := let f := λ r b, cond b (r + r + y) (r + r) in - (to_list x)^.foldl f 0 + (to_list x).foldl f 0 instance : has_mul (bitvec n) := ⟨bitvec.mul⟩ end arith diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean index 36eab7ba3d..b4969259e1 100644 --- a/library/data/hash_map.lean +++ b/library/data/hash_map.lean @@ -43,7 +43,7 @@ def find_aux (a : α) : list (Σ a, β a) → option (β a) if h : a' = a then some (eq.rec_on h b) else find_aux t def contains_aux (a : α) (l : list (Σ a, β a)) : bool := -(find_aux a l)^.is_some +(find_aux a l).is_some def find (m : hash_map α β) (a : α) : option (β a) := match m with @@ -52,7 +52,7 @@ match m with end def contains (m : hash_map α β) (a : α) : bool := -(find m a)^.is_some +(find m a).is_some def fold [decidable_eq α] (m : hash_map α β) (d : δ) (f : δ → Π a, β a → δ) : δ := fold_buckets m.buckets d f diff --git a/library/data/stream.lean b/library/data/stream.lean index f7e75add86..e5021e2dba 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -434,7 +434,7 @@ lemma map_append_stream (f : α → β) : ∀ (l : list α) (s : stream α), map | [] s := rfl | (list.cons a l) s := by rw [cons_append_stream, list.map_cons, map_cons, cons_append_stream, map_append_stream] -lemma drop_append_stream : ∀ (l : list α) (s : stream α), drop l^.length (l ++ₛ s) = s +lemma drop_append_stream : ∀ (l : list α) (s : stream α), drop l.length (l ++ₛ s) = s | [] s := by reflexivity | (list.cons a l) s := by rw [list.length_cons, add_one_eq_succ, drop_succ, cons_append_stream, tail_cons, drop_append_stream] diff --git a/library/data/vector.lean b/library/data/vector.lean index 734129cf4a..7fe2f6614b 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -10,7 +10,7 @@ import data.list universes u v w -def vector (α : Type u) (n : ℕ) := { l : list α // l^.length = n } +def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n } namespace vector variables {α : Type u} {β : Type v} {φ : Type w} diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean index eb1dd758bb..2aaf7ae773 100644 --- a/library/init/algebra/field.lean +++ b/library/init/algebra/field.lean @@ -126,7 +126,7 @@ eq.symm (eq_one_div_of_mul_eq_one this) lemma division_ring.one_div_neg_eq_neg_one_div {a : α} (h : a ≠ 0) : 1 / (- a) = - (1 / a) := have -1 ≠ (0:α), from (suppose -1 = 0, absurd (eq.symm (calc - 1 = -(-1) : (neg_neg (1:α))^.symm + 1 = -(-1) : (neg_neg (1:α)).symm ... = -0 : by rw this ... = (0:α) : neg_zero)) zero_ne_one), calc @@ -385,7 +385,7 @@ lemma eq_of_one_div_eq_one_div {a b : α} (h : 1 / a = 1 / b) : a = b := decidable.by_cases (assume ha : a = 0, have hb : b = 0, from eq_zero_of_one_div_eq_zero (by rw [-h, ha, div_zero]), - hb^.symm ▸ ha) + hb.symm ▸ ha) (assume ha : a ≠ 0, have hb : b ≠ 0, from ne_zero_of_one_div_ne_zero (h ▸ (one_div_ne_zero ha)), division_ring.eq_of_one_div_eq_one_div ha hb h) diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean index be09502af1..991816c2c7 100644 --- a/library/init/algebra/group.lean +++ b/library/init/algebra/group.lean @@ -126,7 +126,7 @@ by simp [h] lemma eq_inv_of_mul_eq_one [group α] {a b : α} (h : a * b = 1) : a = b⁻¹ := have a⁻¹ = b, from inv_eq_of_mul_eq_one h, -by simp [this^.symm] +by simp [this.symm] lemma eq_mul_inv_of_mul_eq [group α] {a b c : α} (h : a * c = b) : a = b * c⁻¹ := by simp [h.symm] @@ -287,9 +287,9 @@ meta def multiplicative_to_additive_pairs : list (name × name) := /- Transport multiplicative to additive -/ meta def transport_multiplicative_to_additive : command := let dict := rb_map.of_list multiplicative_to_additive_pairs in -multiplicative_to_additive_pairs^.foldl (λ t ⟨src, tgt⟩, do +multiplicative_to_additive_pairs.foldl (λ t ⟨src, tgt⟩, do env ← get_env, - if (env.get tgt)^.to_bool = ff + if (env.get tgt).to_bool = ff then t >> transport_with_dict dict src tgt else t) skip diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index 694451ecde..db99f8fa9f 100644 --- a/library/init/algebra/order.lean +++ b/library/init/algebra/order.lean @@ -140,7 +140,7 @@ have a ≤ c, from le_trans (le_of_lt' h₁) h₂, or.elim (lt_or_eq_of_le this) (λ h : a < c, h) (λ h : a = c, - have b ≤ a, from h^.symm ▸ h₂, + have b ≤ a, from h.symm ▸ h₂, have a = b, from le_antisymm (le_of_lt' h₁) this, absurd h₁ (this ▸ lt_irrefl' a)) @@ -174,7 +174,7 @@ or.elim (le_total a b) (λ h : a = b, or.inr (or.inl h))) (λ h : b ≤ a, or.elim (lt_or_eq_of_le h) (λ h : b < a, or.inr (or.inr h)) - (λ h : b = a, or.inr (or.inl h^.symm))) + (λ h : b = a, or.inr (or.inl h.symm))) lemma le_of_not_gt [linear_strong_order_pair α] {a b : α} (h : ¬ a > b) : a ≤ b := match lt_trichotomy a b with diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean index 6ec644b7a2..1e3c36c5be 100644 --- a/library/init/algebra/ordered_ring.lean +++ b/library/init/algebra/ordered_ring.lean @@ -342,18 +342,18 @@ match lt_trichotomy 0 a with | or.inl hlt₂ := have 0 < a * b, from mul_pos hlt₁ hlt₂, begin rw h at this, exact absurd this (lt_irrefl _) end - | or.inr (or.inl heq₂) := or.inr heq₂^.symm + | or.inr (or.inl heq₂) := or.inr heq₂.symm | or.inr (or.inr hgt₂) := have 0 > a * b, from mul_neg_of_pos_of_neg hlt₁ hgt₂, begin rw h at this, exact absurd this (lt_irrefl _) end end -| or.inr (or.inl heq₁) := or.inl heq₁^.symm +| or.inr (or.inl heq₁) := or.inl heq₁.symm | or.inr (or.inr hgt₁) := match lt_trichotomy 0 b with | or.inl hlt₂ := have 0 > a * b, from mul_neg_of_neg_of_pos hgt₁ hlt₂, begin rw h at this, exact absurd this (lt_irrefl _) end - | or.inr (or.inl heq₂) := or.inr heq₂^.symm + | or.inr (or.inl heq₂) := or.inr heq₂.symm | or.inr (or.inr hgt₂) := have 0 < a * b, from mul_pos_of_neg_of_neg hgt₁ hgt₂, begin rw h at this, exact absurd this (lt_irrefl _) end diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean index ab1d561c0a..e25a8055ca 100644 --- a/library/init/algebra/ring.lean +++ b/library/init/algebra/ring.lean @@ -78,13 +78,13 @@ lemma ring.mul_zero [ring α] (a : α) : a * 0 = 0 := have a * 0 + 0 = a * 0 + a * 0, from calc a * 0 + 0 = a * (0 + 0) : by simp ... = a * 0 + a * 0 : by rw left_distrib, -show a * 0 = 0, from (add_left_cancel this)^.symm +show a * 0 = 0, from (add_left_cancel this).symm lemma ring.zero_mul [ring α] (a : α) : 0 * a = 0 := have 0 * a + 0 = 0 * a + 0 * a, from calc 0 * a + 0 = (0 + 0) * a : by simp ... = 0 * a + 0 * a : by rewrite right_distrib, -show 0 * a = 0, from (add_left_cancel this)^.symm +show 0 * a = 0, from (add_left_cancel this).symm instance ring.to_semiring [s : ring α] : semiring α := { s with @@ -169,13 +169,13 @@ section integral_domain lemma eq_of_mul_eq_mul_right {a b c : α} (ha : a ≠ 0) (h : b * a = c * a) : b = c := have b * a - c * a = 0, from sub_eq_zero_of_eq h, have (b - c) * a = 0, by rw [mul_sub_right_distrib, this], - have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this)^.resolve_right ha, + have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha, eq_of_sub_eq_zero this lemma eq_of_mul_eq_mul_left {a b c : α} (ha : a ≠ 0) (h : a * b = a * c) : b = c := have a * b - a * c = 0, from sub_eq_zero_of_eq h, have a * (b - c) = 0, by rw [mul_sub_left_distrib, this], - have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this)^.resolve_left ha, + have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha, eq_of_sub_eq_zero this lemma eq_zero_of_mul_eq_self_right {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 := @@ -186,7 +186,7 @@ section integral_domain h₁ this, have a * b - a = 0, by simp [h₂], have a * (b - 1) = 0, by rwa [mul_sub_left_distrib, mul_one], - show a = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this)^.resolve_right hb + show a = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hb lemma eq_zero_of_mul_eq_self_left {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 := eq_zero_of_mul_eq_self_right h₁ (by rwa mul_comm at h₂) diff --git a/library/init/classical.lean b/library/init/classical.lean index 4c7781f711..f2e6688545 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -17,10 +17,10 @@ noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop) : λ h, choice (let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩) noncomputable def some {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α := -(indefinite_description p h)^.val +(indefinite_description p h).val theorem some_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (some h) := -(indefinite_description p h)^.property +(indefinite_description p h).property /- Diaconescu's theorem: using function extensionality and propositional extensionality, we can get excluded middle from this. -/ @@ -75,7 +75,7 @@ theorem exists_true_of_nonempty {α : Sort u} (h : nonempty α) : ∃ x : α, tr nonempty.elim h (take x, ⟨x, trivial⟩) noncomputable def inhabited_of_nonempty {α : Sort u} (h : nonempty α) : inhabited α := -⟨(indefinite_description _ (exists_true_of_nonempty h))^.val⟩ +⟨(indefinite_description _ (exists_true_of_nonempty h)).val⟩ noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : inhabited α := @@ -106,19 +106,19 @@ noncomputable theorem strong_indefinite_description {α : Sort u} (p : α → Pr (h : nonempty α) : { x : α // (∃ y : α, p y) → p x} := match (prop_decidable (∃ x : α, p x)) with | (is_true hp) := let xp := indefinite_description _ hp in - ⟨xp^.val, λ h', xp^.property⟩ + ⟨xp.val, λ h', xp.property⟩ | (is_false hn) := ⟨@inhabited.default _ (inhabited_of_nonempty h), λ h, absurd h hn⟩ end /- the Hilbert epsilon function -/ noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α := -(strong_indefinite_description p h)^.val +(strong_indefinite_description p h).val theorem epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop) (hex : ∃ y, p y) : p (@epsilon α h p) := -have aux : (∃ y, p y) → p ((strong_indefinite_description p h)^.val), - from (strong_indefinite_description p h)^.property, +have aux : (∃ y, p y) → p ((strong_indefinite_description p h).val), + from (strong_indefinite_description p h).property, aux hex theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : diff --git a/library/init/data/array.lean b/library/init/data/array.lean index 78873cc8ad..35f5ee82dd 100644 --- a/library/init/data/array.lean +++ b/library/init/data/array.lean @@ -17,28 +17,28 @@ namespace array variables {α : Type u} {β : Type w} {n : nat} def read (a : array α n) (i : fin n) : α := -a^.data i +a.data i def read' [inhabited α] (a : array α n) (i : nat) : α := -if h : i < n then a^.read ⟨i,h⟩ else default α +if h : i < n then a.read ⟨i,h⟩ else default α def write (a : array α n) (i : fin n) (v : α) : array α n := -{data := λ j, if i = j then v else a^.read j} +{data := λ j, if i = j then v else a.read j} def write' (a : array α n) (i : nat) (v : α) : array α n := -if h : i < n then a^.write ⟨i, h⟩ v else a +if h : i < n then a.write ⟨i, h⟩ v else a lemma push_back_idx {j n} : j < n + 1 → j ≠ n → j < n := λ h₁ h₂, nat.lt_of_le_and_ne (nat.le_of_lt_succ h₁) h₂ def push_back (a : array α n) (v : α) : array α (n+1) := -{data := λ ⟨j, h₁⟩, if h₂ : j = n then v else a^.read ⟨j, push_back_idx h₁ h₂⟩} +{data := λ ⟨j, h₁⟩, if h₂ : j = n then v else a.read ⟨j, push_back_idx h₁ h₂⟩} lemma pop_back_idx {j n} : j < n → j < n + 1 := λ h, nat.lt.step h def pop_back (a : array α (n+1)) : array α n := -{data := λ ⟨j, h⟩, a^.read ⟨j, pop_back_idx h⟩} +{data := λ ⟨j, h⟩, a.read ⟨j, pop_back_idx h⟩} lemma lt_aux_1 {a b c : nat} : a + c < b → a < b := λ h, lt_of_le_of_lt (nat.le_add_right a c) h @@ -57,10 +57,10 @@ lt_of_le_of_lt (nat.sub_le _ _) this def foreach_aux (f : fin n → α → α) : Π (i : nat), i < n → array α n → array α n | 0 h a := let i : fin n := ⟨n - 1, lt_aux_2 h⟩ in - a^.write i (f i (a^.read i)) + a.write i (f i (a.read i)) | (j+1) h a := let i : fin n := ⟨n - 2 - j, lt_aux_3 h⟩ in - foreach_aux j (lt_aux_1 h) (a^.write i (f i (a^.read i))) + foreach_aux j (lt_aux_1 h) (a.write i (f i (a.read i))) def foreach : Π {n}, array α n → (fin n → α → α) → array α n | 0 a f:= a @@ -70,15 +70,15 @@ def map {α} {n} (f : α → α) (a : array α n) : array α n := foreach a (λ _, f) def map₂ {α} {n} (f : α → α → α) (a b : array α n) : array α n := -foreach b (λ i, f (a^.read i)) +foreach b (λ i, f (a.read i)) def iterate_aux (f : fin n → α → β → β) : Π (i : nat), i < n → array α n → β → β | 0 h a b := let i : fin n := ⟨n - 1, lt_aux_2 h⟩ in - f i (a^.read i) b + f i (a.read i) b | (j+1) h a b := let i : fin n := ⟨n - 2 - j, lt_aux_3 h⟩ in - iterate_aux j (lt_aux_1 h) a (f i (a^.read i) b) + iterate_aux j (lt_aux_1 h) a (f i (a.read i) b) def iterate : Π {n}, array α n → β → (fin n → α → β → β) → β | 0 a b fn := b @@ -90,17 +90,17 @@ iterate a b (λ _, f) def rev_iterate_aux (f : fin n → α → β → β) : Π (i : nat), i < n → array α n → β → β | 0 h a b := let z : fin n := ⟨0, h⟩ in - f z (a^.read z) b + f z (a.read z) b | (j+1) h a b := let i : fin n := ⟨j+1, h⟩ in - rev_iterate_aux j (lt_aux_1 h) a (f i (a^.read i) b) + rev_iterate_aux j (lt_aux_1 h) a (f i (a.read i) b) def rev_iterate : Π {n : nat}, array α n → β → (fin n → α → β → β) → β | 0 a b fn := b | (n+1) a b fn := rev_iterate_aux fn n (nat.lt_succ_self _) a b def to_list (a : array α n) : list α := -a^.rev_iterate [] (λ _ v l, v :: l) +a.rev_iterate [] (λ _ v l, v :: l) instance [has_to_string α] : has_to_string (array α n) := ⟨to_string ∘ to_list⟩ diff --git a/library/init/data/fin/ops.lean b/library/init/data/fin/ops.lean index e5541a6fa2..68b5863665 100644 --- a/library/init/data/fin/ops.lean +++ b/library/init/data/fin/ops.lean @@ -71,32 +71,32 @@ instance decidable_lt : ∀ (a b : fin n), decidable (a < b) instance decidable_le : ∀ (a b : fin n), decidable (a ≤ b) | ⟨a, _⟩ ⟨b, _⟩ := by apply nat.decidable_le -lemma add_def (a b : fin n) : (a + b)^.val = (a^.val + b^.val) % n := -show (fin.add a b)^.val = (a^.val + b^.val) % n, from +lemma add_def (a b : fin n) : (a + b).val = (a.val + b.val) % n := +show (fin.add a b).val = (a.val + b.val) % n, from by cases a; cases b; simp [fin.add] -lemma mul_def (a b : fin n) : (a * b)^.val = (a^.val * b^.val) % n := -show (fin.mul a b)^.val = (a^.val * b^.val) % n, from +lemma mul_def (a b : fin n) : (a * b).val = (a.val * b.val) % n := +show (fin.mul a b).val = (a.val * b.val) % n, from by cases a; cases b; simp [fin.mul] -lemma sub_def (a b : fin n) : (a - b)^.val = a^.val - b^.val := -show (fin.sub a b)^.val = a^.val - b^.val, from +lemma sub_def (a b : fin n) : (a - b).val = a.val - b.val := +show (fin.sub a b).val = a.val - b.val, from by cases a; cases b; simp [fin.sub] -lemma mod_def (a b : fin n) : (a % b)^.val = a^.val % b^.val := -show (fin.mod a b)^.val = a^.val % b^.val, from +lemma mod_def (a b : fin n) : (a % b).val = a.val % b.val := +show (fin.mod a b).val = a.val % b.val, from by cases a; cases b; simp [fin.mod] -lemma div_def (a b : fin n) : (a / b)^.val = a^.val / b^.val := -show (fin.div a b)^.val = a^.val / b^.val, from +lemma div_def (a b : fin n) : (a / b).val = a.val / b.val := +show (fin.div a b).val = a.val / b.val, from by cases a; cases b; simp [fin.div] -lemma lt_def (a b : fin n) : (a < b) = (a^.val < b^.val) := -show (fin.lt a b) = (a^.val < b^.val), from +lemma lt_def (a b : fin n) : (a < b) = (a.val < b.val) := +show (fin.lt a b) = (a.val < b.val), from by cases a; cases b; simp [fin.lt] -lemma le_def (a b : fin n) : (a ≤ b) = (a^.val ≤ b^.val) := -show (fin.le a b) = (a^.val ≤ b^.val), from +lemma le_def (a b : fin n) : (a ≤ b) = (a.val ≤ b.val) := +show (fin.le a b) = (a.val ≤ b.val), from by cases a; cases b; simp [fin.le] end fin diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index d10c74c33c..8ae5da68d1 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -131,7 +131,7 @@ begin { intro k, cases k, { intro e, cases (nat.le.dest (nat.le_of_sub_eq_zero e)) with k h, - rw [h^.symm, nat.add_sub_cancel_left], + rw [h.symm, nat.add_sub_cancel_left], apply hp }, { intro heq, assert h : m ≤ n, @@ -205,7 +205,7 @@ protected lemma rel_neg_of_nat {m} : ∀{n}, rel_int_nat_nat (neg_of_nat n) (m, | (nat.succ n) := rel_int_nat_nat.neg protected lemma rel_eq : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ iff)) - eq (λa b, a^.1 + b^.2 = b^.1 + a^.2) + eq (λa b, a.1 + b.2 = b.1 + a.2) | ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := calc of_nat p = of_nat p' ↔ (m + m') + p = (m + m') + p' : by rw [of_nat_eq_of_nat_iff, add_left_cancel_iff] @@ -248,7 +248,7 @@ protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_ by simp, show rel_int_nat_nat (sub_nat_nat p (n' + 1)) (m + p + m', m + (m' + n' + 1)), begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m'))^.symm], + rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], apply int.rel_sub_nat_nat end | ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := @@ -258,7 +258,7 @@ protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_ by simp, show rel_int_nat_nat (sub_nat_nat p' (n + 1)) (m + (m' + p'), (m + n + 1) + m'), begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m'))^.symm], + rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], apply int.rel_sub_nat_nat end | ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index d98449e5b4..bf6b8249f9 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -61,7 +61,7 @@ end lemma le_of_coe_nat_le_coe_nat {m n : ℕ} (h : (↑m : ℤ) ≤ ↑n) : m ≤ n := le.elim h (take k, assume hk : ↑m + ↑k = ↑n, - have m + k = n, from int.coe_nat_inj ((int.coe_nat_add m k)^.trans hk), + have m + k = n, from int.coe_nat_inj ((int.coe_nat_add m k).trans hk), nat.le.intro this) lemma coe_nat_le_coe_nat_iff (m n : ℕ) : (↑m : ℤ) ≤ ↑n ↔ m ≤ n := @@ -84,10 +84,10 @@ lemma coe_nat_lt_coe_nat_iff (n m : ℕ) : (↑n : ℤ) < ↑m ↔ n < m := begin rw [lt_iff_add_one_le, -int.coe_nat_succ, coe_nat_le_coe_nat_iff], reflexivity end lemma lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : (↑m : ℤ) < ↑n) : m < n := -(coe_nat_lt_coe_nat_iff _ _)^.mp h +(coe_nat_lt_coe_nat_iff _ _).mp h lemma coe_nat_lt_coe_nat_of_lt {m n : ℕ} (h : m < n) : (↑m : ℤ) < ↑n := -(coe_nat_lt_coe_nat_iff _ _)^.mpr h +(coe_nat_lt_coe_nat_iff _ _).mpr h /- show that the integers form an ordered additive group -/ diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 4e527e33d0..a269e2087d 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -744,7 +744,7 @@ exists.elim (nat.le.dest h) by rw [-hl, nat.add_sub_cancel_left, add_comm k, -add_assoc, nat.add_sub_cancel]) protected lemma sub_eq_iff_eq_add {a b c : ℕ} (ab : b ≤ a) : a - b = c ↔ a = c + b := -⟨take c_eq, begin rw [c_eq^.symm, nat.sub_add_cancel ab] end, +⟨take c_eq, begin rw [c_eq.symm, nat.sub_add_cancel ab] end, take a_eq, begin rw [a_eq, nat.add_sub_cancel] end⟩ protected lemma lt_of_sub_eq_succ {m n l : ℕ} (H : m - n = nat.succ l) : n < m := @@ -923,11 +923,11 @@ begin cases decidable.em (0 < k ∧ k ≤ m) with h h', -- 0 < k ∧ k ≤ m { assert h' : m - k < m, - { apply nat.sub_lt _ h^.left, - apply lt_of_lt_of_le h^.left h^.right }, + { apply nat.sub_lt _ h.left, + apply lt_of_lt_of_le h.left h.right }, rw [div_def, mod_def, if_pos h, if_pos h], simp [left_distrib,IH _ h'], - rw [-nat.add_sub_assoc h^.right,nat.add_sub_cancel_left] }, + rw [-nat.add_sub_assoc h.right,nat.add_sub_cancel_left] }, -- ¬ (0 < k ∧ k ≤ m) { rw [div_def, mod_def, if_neg h', if_neg h'], simp }, end @@ -991,7 +991,7 @@ lemma div_eq_of_lt {a b : ℕ} (h₀ : a < b) begin rw [div_def a,if_neg], intro h₁, - apply not_le_of_gt h₀ h₁^.right + apply not_le_of_gt h₀ h₁.right end -- this is a Galois connection @@ -1065,7 +1065,7 @@ begin cases lt_or_ge p (b^succ w) with h₁ h₁, -- base case: p < b^succ w { assert h₂ : p / b < b^w, - { apply (div_lt_iff_lt_mul p _ b_pos)^.mpr, + { apply (div_lt_iff_lt_mul p _ b_pos).mpr, simp at h₁, simp [h₁] }, rw [mod_eq_of_lt h₁,mod_eq_of_lt h₂], simp [mod_add_div], }, -- step: p ≥ b^succ w @@ -1078,7 +1078,7 @@ begin rw [mod_eq_sub_mod h₄ h₁,IH _ h₂,pow_succ], apply congr, apply congr_arg, { assert h₃ : p / b ≥ b^w, - { apply (le_div_iff_mul_le _ p b_pos)^.mpr, simp [h₅] }, + { apply (le_div_iff_mul_le _ p b_pos).mpr, simp [h₅] }, simp [nat.sub_mul_div _ _ _ b_pos h₅,mod_eq_sub_mod h₄ h₃] }, { simp [nat.sub_mul_mod p (b^w) _ b_pos h₅] } } end diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index 5cee35bbbd..f365d9b3f7 100644 --- a/library/init/data/option/instances.lean +++ b/library/init/data/option/instances.lean @@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import .basic +import init.data.option.basic import init.meta.tactic - universes u v @[inline] def option_bind {α : Type u} {β : Type v} : option α → (α → option β) → option β diff --git a/library/init/data/set.lean b/library/init/data/set.lean index 8994a8ee6f..e0b69fb347 100644 --- a/library/init/data/set.lean +++ b/library/init/data/set.lean @@ -85,7 +85,7 @@ instance : functor set := intros, apply funext, intro c, dsimp [image, set_of], exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩, - λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂^.symm ▸ h₃⟩⟩⟩ + λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂ .symm ▸ h₃⟩⟩⟩ -- TODO(Leo): fix extra space after h₂ end} end set diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 379758e7b1..b52fd151ad 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -48,4 +48,4 @@ private def to_nat_core : list char → nat → nat to_nat_core cs (char.to_nat c - char.to_nat #"0" + r*10) def string.to_nat (s : string) : nat := -to_nat_core s^.reverse 0 +to_nat_core s.reverse 0 diff --git a/library/init/logic.lean b/library/init/logic.lean index 56186bc2fe..1c949707a5 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -78,10 +78,10 @@ lemma trans_rel_left {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : h₂ ▸ h₁ lemma trans_rel_right {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := -h₁^.symm ▸ h₂ +h₁.symm ▸ h₂ lemma of_eq_true {p : Prop} (h : p = true) : p := -h^.symm ▸ trivial +h.symm ▸ trivial lemma not_of_eq_false {p : Prop} (h : p = false) : ¬p := assume hp, h ▸ hp @@ -114,7 +114,7 @@ namespace ne lemma irrefl (h : a ≠ a) : false := h rfl lemma symm (h : a ≠ b) : b ≠ a := - assume (h₁ : b = a), h (h₁^.symm) + assume (h₁ : b = a), h (h₁.symm) end ne lemma false_of_ne {α : Sort u} {a : α} : a ≠ a → false := ne.irrefl @@ -248,7 +248,7 @@ lemma iff.elim_left : (a ↔ b) → a → b := iff.mp lemma iff.elim_right : (a ↔ b) → b → a := iff.mpr lemma iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) := -iff.intro (λ h, and.intro h^.mp h^.mpr) (λ h, iff.intro h^.left h^.right) +iff.intro (λ h, and.intro h.mp h.mpr) (λ h, iff.intro h.left h.right) attribute [refl] lemma iff.refl (a : Prop) : a ↔ a := @@ -512,9 +512,9 @@ iff.trans iff.comm (iff_false a) iff_true_intro iff.rfl @[congr] lemma iff_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d) := -(iff_iff_implies_and_implies a b)^.trans - ((and_congr (imp_congr h₁ h₂) (imp_congr h₂ h₁))^.trans - (iff_iff_implies_and_implies c d)^.symm) +(iff_iff_implies_and_implies a b).trans + ((and_congr (imp_congr h₁ h₂) (imp_congr h₂ h₁)).trans + (iff_iff_implies_and_implies c d).symm) /- implies simp rule -/ @[simp] lemma implies_true_iff (a : Prop) : (a → true) ↔ true := @@ -638,7 +638,7 @@ section else is_false (iff.mp (not_iff_not_of_iff h) hp) def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q := - decidable_of_decidable_of_iff hp h^.to_iff + decidable_of_decidable_of_iff hp h.to_iff protected def or.by_cases [decidable p] [decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α := @@ -671,7 +671,7 @@ section else is_true (assume h, absurd h hp) instance [decidable p] [decidable q] : decidable (p ↔ q) := - decidable_of_decidable_of_iff and.decidable (iff_iff_implies_and_implies p q)^.symm + decidable_of_decidable_of_iff and.decidable (iff_iff_implies_and_implies p q).symm end instance {α : Sort u} [decidable_eq α] (a b : α) : decidable (a ≠ b) := diff --git a/library/init/meta/async_tactic.lean b/library/init/meta/async_tactic.lean index 437db13a07..6ce3407f47 100644 --- a/library/init/meta/async_tactic.lean +++ b/library/init/meta/async_tactic.lean @@ -30,21 +30,21 @@ s ← read, return $ task.delay $ λ _, meta def prove_goal_async (tac : tactic unit) : tactic unit := do ctx ← local_context, revert_lst ctx, tgt ← target, tgt ← instantiate_mvars tgt, -env ← get_env, tgt ← return $ env^.unfold_untrusted_macros tgt, -when tgt^.has_meta_var (fail "goal contains metavariables"), -params ← return tgt^.collect_univ_params, +env ← get_env, tgt ← return $ env.unfold_untrusted_macros tgt, +when tgt.has_meta_var (fail "goal contains metavariables"), +params ← return tgt.collect_univ_params, lemma_name ← new_aux_decl_name, proof ← run_async (do goal_meta ← mk_meta_var tgt, set_goals [goal_meta], - monad.for' ctx (λc, intro c^.local_pp_name), + monad.for' ctx (λc, intro c.local_pp_name), tac, proof ← instantiate_mvars goal_meta, - proof ← return $ env^.unfold_untrusted_macros proof, - when proof^.has_meta_var $ fail "async proof failed: contains metavariables", + proof ← return $ env.unfold_untrusted_macros proof, + when proof.has_meta_var $ fail "async proof failed: contains metavariables", return proof), add_decl $ declaration.thm lemma_name params tgt proof, -exact (expr.const lemma_name (params^.map level.param)) +exact (expr.const lemma_name (params.map level.param)) namespace interactive open interactive.types diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean index cc0dc329b6..34259f1432 100644 --- a/library/init/meta/comp_value_tactics.lean +++ b/library/init/meta/comp_value_tactics.lean @@ -19,7 +19,7 @@ open expr meta def comp_val : tactic unit := do t ← target, guard (is_app t), - type ← infer_type t^.app_arg, + type ← infer_type t.app_arg, (do is_def_eq type (const `nat []), (do (a, b) ← is_ne t, pr ← mk_nat_val_ne_proof a b, diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean index c3f4687796..3a2454480b 100644 --- a/library/init/meta/converter.lean +++ b/library/init/meta/converter.lean @@ -36,9 +36,9 @@ match o₁, o₂ with | _, none := return o₁ | some p₁, some p₂ := do env ← get_env, - match env^.trans_for r with + match env.trans_for r with | some trans := do pr ← mk_app trans [p₁, p₂], return $ some pr - | none := fail $ "converter failed, relation '" ++ r^.to_string ++ "' is not transitive" + | none := fail $ "converter failed, relation '" ++ r.to_string ++ "' is not transitive" end end @@ -83,7 +83,7 @@ meta def whnf (md : transparency := reducible) : conv unit := λ r e, do n ← tactic.whnf e md, return ⟨(), n, none⟩ meta def dsimp : conv unit := -λ r e, do s ← simp_lemmas.mk_default, n ← s^.dsimplify e, return ⟨(), n, none⟩ +λ r e, do s ← simp_lemmas.mk_default, n ← s.dsimplify e, return ⟨(), n, none⟩ meta def try (c : conv unit) : conv unit := c <|> return () @@ -99,7 +99,7 @@ lhs >>= trace meta def apply_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit := λ r e, do - (new_e, pr) ← s^.rewrite prove r e, + (new_e, pr) ← s.rewrite prove r e, return ⟨(), new_e, some pr⟩ meta def apply_lemmas (s : simp_lemmas) : conv unit := @@ -109,7 +109,7 @@ apply_lemmas_core s failed meta def apply_propext_lemmas_core (s : simp_lemmas) (prove : tactic unit) : conv unit := λ r e, do guard (r = `eq), - (new_e, pr) ← s^.rewrite prove `iff e, + (new_e, pr) ← s.rewrite prove `iff e, new_pr ← mk_app `propext [pr], return ⟨(), new_e, some new_pr⟩ @@ -120,7 +120,7 @@ private meta def mk_refl_proof (r : name) (e : expr) : tactic expr := do env ← get_env, match (environment.refl_for env r) with | (some refl) := do pr ← mk_app refl [e], return pr - | none := fail $ "converter failed, relation '" ++ r^.to_string ++ "' is not reflexive" + | none := fail $ "converter failed, relation '" ++ r.to_string ++ "' is not reflexive" end meta def to_tactic (c : conv unit) : name → expr → tactic (expr × expr) := @@ -176,11 +176,11 @@ meta def funext (c : conv unit) : conv unit := let aux_type := expr.pi n bi d (expr.const `true []), (result, _) ← solve_aux aux_type $ do { x ← intro1, - c_result ← c r (b^.instantiate_var x), - let rhs := expr.lam n bi d (c_result^.rhs^.abstract x), - match c_result^.proof : _ → tactic (conv_result unit) with + c_result ← c r (b.instantiate_var x), + let rhs := expr.lam n bi d (c_result.rhs.abstract x), + match c_result.proof : _ → tactic (conv_result unit) with | some pr := do - let aux_pr := expr.lam n bi d (pr^.abstract x), + let aux_pr := expr.lam n bi d (pr.abstract x), new_pr ← mk_app `funext [lhs, rhs, aux_pr], return ⟨(), rhs, some new_pr⟩ | none := return ⟨(), rhs, none⟩ @@ -192,7 +192,7 @@ meta def congr_core (c_f c_a : conv unit) : conv unit := guard (r = `eq), (expr.app f a) ← return lhs, f_type ← infer_type f >>= tactic.whnf, - guard (f_type^.is_arrow), + guard (f_type.is_arrow), ⟨(), new_f, of⟩ ← try c_f r f, ⟨(), new_a, oa⟩ ← try c_a r a, rhs ← return $ new_f new_a, @@ -276,8 +276,8 @@ do (r, lhs, rhs) ← (target_lhs_rhs <|> fail "conversion failed, target is not do new_lhs_fmt ← pp new_lhs, rhs_fmt ← pp rhs, fail (to_fmt "conversion failed, expected" ++ - rhs_fmt^.indent 4 ++ format.line ++ "provided" ++ - new_lhs_fmt^.indent 4)), + rhs_fmt.indent 4 ++ format.line ++ "provided" ++ + new_lhs_fmt.indent 4)), exact pr end conv diff --git a/library/init/meta/decl_cmds.lean b/library/init/meta/decl_cmds.lean index adf52d4b02..92717a9e1c 100644 --- a/library/init/meta/decl_cmds.lean +++ b/library/init/meta/decl_cmds.lean @@ -8,10 +8,10 @@ import init.meta.tactic init.meta.rb_map open tactic private meta def apply_replacement (replacements : name_map name) (e : expr) : expr := -e^.replace (λ e d, +e.replace (λ e d, match e with | expr.const n ls := - match replacements^.find n with + match replacements.find n with | some new_n := some (expr.const new_n ls) | none := none end @@ -37,16 +37,16 @@ e^.replace (λ e d, lemma g_lemma : forall a, g a > 0 := ... -/ meta def copy_decl_updating_type (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command := do env ← get_env, - decl ← env^.get src_decl_name, - let decl := decl^.update_name $ new_decl_name, - let decl := decl^.update_type $ apply_replacement replacements decl^.type, - let decl := decl^.update_value $ expr.const src_decl_name (decl^.univ_params^.map level.param), + decl ← env.get src_decl_name, + let decl := decl.update_name $ new_decl_name, + let decl := decl.update_type $ apply_replacement replacements decl.type, + let decl := decl.update_value $ expr.const src_decl_name (decl.univ_params.map level.param), add_decl decl meta def copy_decl_using (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command := do env ← get_env, - decl ← env^.get src_decl_name, - let decl := decl^.update_name $ new_decl_name, - let decl := decl^.update_type $ apply_replacement replacements decl^.type, - let decl := decl^.map_value $ apply_replacement replacements, + decl ← env.get src_decl_name, + let decl := decl.update_name $ new_decl_name, + let decl := decl.update_type $ apply_replacement replacements decl.type, + let decl := decl.map_value $ apply_replacement replacements, add_decl decl diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index 83be55f3ca..6e7dc01a93 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -81,7 +81,7 @@ meta def type : declaration → expr meta def value : declaration → expr | (defn _ _ _ v _ _) := v -| (thm _ _ _ v) := v^.get +| (thm _ _ _ v) := v.get | _ := default expr meta def value_task : declaration → task expr @@ -107,7 +107,7 @@ meta def update_value : declaration → expr → declaration | d new_v := d meta def update_value_task : declaration → task expr → declaration -| (defn n ls t v h tr) new_v := defn n ls t new_v^.get h tr +| (defn n ls t v h tr) new_v := defn n ls t new_v.get h tr | (thm n ls t v) new_v := thm n ls t new_v | d new_v := d diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index fe3e128e37..a3eb3701b5 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -31,7 +31,7 @@ meta constant add : environment → declaration → exceptional envi /- Retrieve a declaration from the environment -/ meta constant get : environment → name → exceptional declaration meta def contains (env : environment) (d : name) : bool := -match env^.get d with +match env.get d with | exceptional.success _ := tt | exceptional.exception ._ _ := ff end @@ -98,10 +98,10 @@ end /-- Return true if 'n' has been declared in the current file -/ meta def in_current_file (env : environment) (n : name) : bool := -(env^.decl_olean n)^.is_none && env^.contains n +(env.decl_olean n).is_none && env.contains n meta def is_definition (env : environment) (n : name) : bool := -match env^.get n with +match env.get n with | exceptional.success (declaration.defn _ _ _ _ _ _) := tt | _ := ff end diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index dfacd0648c..525871af5f 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -63,7 +63,7 @@ meta constant expr.is_annotation : expr → option (name × expr) meta def expr.erase_annotations : expr → expr | e := - match e^.is_annotation with + match e.is_annotation with | some (_, a) := expr.erase_annotations a | none := e end @@ -104,7 +104,7 @@ meta constant expr.abstract_local : expr → name → expr meta constant expr.abstract_locals : expr → list name → expr meta def expr.abstract : expr → expr → expr -| e (expr.local_const n m bi t) := e^.abstract_local n +| e (expr.local_const n m bi t) := e.abstract_local n | e _ := e meta constant expr.instantiate_univ_params : expr → list (name × level) → expr diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean index 37eb548193..9b302ea30c 100644 --- a/library/init/meta/format.lean +++ b/library/init/meta/format.lean @@ -83,7 +83,7 @@ meta instance : has_to_format char := meta def list.to_format {α : Type u} [has_to_format α] : list α → format | [] := to_fmt "[]" -| xs := to_fmt "[" ++ group (nest 1 $ format.join $ list.intersperse ("," ++ line) $ xs^.map to_fmt) ++ to_fmt "]" +| xs := to_fmt "[" ++ group (nest 1 $ format.join $ list.intersperse ("," ++ line) $ xs.map to_fmt) ++ to_fmt "]" meta instance {α : Type u} [has_to_format α] : has_to_format (list α) := ⟨list.to_format⟩ diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean index 37c75d3353..27d3cacc56 100644 --- a/library/init/meta/fun_info.lean +++ b/library/init/meta/fun_info.lean @@ -111,19 +111,19 @@ meta constant get_spec_prefix_size (t : expr) (nargs : nat) (md := semireducible private meta def is_next_explicit : list param_info → bool | [] := tt -| (p::ps) := bnot p^.is_implicit && bnot p^.is_inst_implicit +| (p::ps) := bnot p.is_implicit && bnot p.is_inst_implicit meta def fold_explicit_args_aux {α} (f : α → expr → tactic α) : list expr → list param_info → α → tactic α | [] _ a := return a | (e::es) ps a := if is_next_explicit ps - then f a e >>= fold_explicit_args_aux es ps^.tail - else fold_explicit_args_aux es ps^.tail a + then f a e >>= fold_explicit_args_aux es ps.tail + else fold_explicit_args_aux es ps.tail a meta def fold_explicit_args {α} (e : expr) (a : α) (f : α → expr → tactic α) : tactic α := -if e^.is_app then do - info ← get_fun_info e^.get_app_fn (some e^.get_app_num_args), - fold_explicit_args_aux f e^.get_app_args info^.params a +if e.is_app then do + info ← get_fun_info e.get_app_fn (some e.get_app_num_args), + fold_explicit_args_aux f e.get_app_args info.params a else return a end tactic diff --git a/library/init/meta/inductive_compiler.lean b/library/init/meta/inductive_compiler.lean index bdb4c98f73..dd305914f1 100644 --- a/library/init/meta/inductive_compiler.lean +++ b/library/init/meta/inductive_compiler.lean @@ -23,7 +23,7 @@ private meta def simp_assumption (ls : simp_lemmas) (e : expr) : tactic (expr × private meta def simp_at_assumption (S : simp_lemmas := simp_lemmas.mk) (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := do when (expr.is_local_constant h = ff) (fail "tactic fsimp_at failed, the given expression is not a hypothesis"), htype ← infer_type h, - S ← S^.append extra_lemmas, + S ← S.append extra_lemmas, (new_htype, heq) ← simp_assumption S htype, assert (expr.local_pp_name h) new_htype, mk_app `iff.mp [heq, h] >>= exact, @@ -31,7 +31,7 @@ do when (expr.is_local_constant h = ff) (fail "tactic fsimp_at failed, the given private meta def fsimp (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := do S ← return (simp_lemmas.mk), - S ← S^.append extra_lemmas, + S ← S.append extra_lemmas, simplify_goal S cfg >> try triv >> try (reflexivity reducible) private meta def at_end (e : expr) : ℕ → tactic (list (option expr)) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 069606b363..d61a4baada 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -53,14 +53,14 @@ private meta def maybe_paren : list format → format | fs := paren (join fs) private meta def unfold (e : expr) : tactic expr := -do (expr.const f_name f_lvls) ← return e^.get_app_fn | failed, +do (expr.const f_name f_lvls) ← return e.get_app_fn | failed, env ← get_env, - decl ← env^.get f_name, - new_f ← decl^.instantiate_value_univ_params f_lvls, - head_beta (expr.mk_app new_f e^.get_app_args) + decl ← env.get f_name, + new_f ← decl.instantiate_value_univ_params f_lvls, + head_beta (expr.mk_app new_f e.get_app_args) private meta def concat (f₁ f₂ : list format) := -if f₁^.empty then f₂ else if f₂^.empty then f₁ else f₁ ++ [" "] ++ f₂ +if f₁.empty then f₂ else if f₂.empty then f₁ else f₁ ++ [" "] ++ f₂ private meta def parser_desc_aux : expr → tactic (list format) | ```(ident) := return ["id"] @@ -98,8 +98,8 @@ private meta def parser_desc_aux : expr → tactic (list format) | ```(%%p₁ <|> %%p₂) := do f₁ ← parser_desc_aux p₁, f₂ ← parser_desc_aux p₂, - return $ if f₁^.empty then [maybe_paren f₂ ++ "?"] else - if f₂^.empty then [maybe_paren f₁ ++ "?"] else + return $ if f₁.empty then [maybe_paren f₂ ++ "?"] else + if f₂.empty then [maybe_paren f₁ ++ "?"] else [paren $ join $ f₁ ++ [to_fmt " | "] ++ f₂] | ```(brackets %%l %%r %%p) := do f ← parser_desc_aux p, @@ -118,14 +118,14 @@ private meta def parser_desc_aux : expr → tactic (list format) meta def param_desc : expr → tactic format | ```(parse %%p) := join <$> parser_desc_aux p | ```(opt_param %%t ._) := (++ "?") <$> pp t -| e := if is_constant e ∧ (const_name e)^.components^.ilast = `itactic +| e := if is_constant e ∧ (const_name e).components.ilast = `itactic then return $ to_fmt "{ tactic }" else paren <$> pp e end interactive namespace tactic meta def report_resolve_name_failure {α : Type} (e : expr) (n : name) : tactic α := -if e^.is_choice_macro +if e.is_choice_macro then fail ("failed to resolve name '" ++ to_string n ++ "', it is overloaded") else fail ("failed to resolve name '" ++ to_string n ++ "', unexpected result") @@ -279,17 +279,17 @@ meta instance rw_rule_has_quote : has_quote rw_rule := ⟨λ ⟨p, s, r⟩, ``(rw_rule.mk %%(quote p) %%(quote s) %%(quote r))⟩ private meta def rw_goal (m : transparency) (rs : list rw_rule) : tactic unit := -rs^.mfor' $ λ r, save_info r^.pos >> to_expr' r^.rule >>= rewrite_core m tt tt occurrences.all r^.symm +rs.mfor' $ λ r, save_info r.pos >> to_expr' r.rule >>= rewrite_core m tt tt occurrences.all r.symm private meta def rw_hyp (m : transparency) (rs : list rw_rule) (hname : name) : tactic unit := -rs^.mfor' $ λ r, +rs.mfor' $ λ r, do h ← get_local hname, - save_info r^.pos, - e ← to_expr' r^.rule, - rewrite_at_core m tt tt occurrences.all r^.symm e h + save_info r.pos, + e ← to_expr' r.rule, + rewrite_at_core m tt tt occurrences.all r.symm e h private meta def rw_hyps (m : transparency) (rs : list rw_rule) (hs : list name) : tactic unit := -hs^.mfor' (rw_hyp m rs) +hs.mfor' (rw_hyp m rs) meta def rw_rule_p (ep : parser pexpr) : parser rw_rule := rw_rule.mk <$> cur_pos <*> (option.is_some <$> (tk "-")?) <*> ep @@ -310,10 +310,10 @@ meta def rw_rules : parser rw_rules_t := private meta def rw_core (m : transparency) (rs : parse rw_rules) (loc : parse location) : tactic unit := match loc with -| [] := rw_goal m rs^.rules -| hs := rw_hyps m rs^.rules hs +| [] := rw_goal m rs.rules +| hs := rw_hyps m rs.rules hs end >> try (reflexivity reducible) - >> (returnopt rs^.end_pos >>= save_info <|> skip) + >> (returnopt rs.end_pos >>= save_info <|> skip) meta def rewrite : parse rw_rules → parse location → tactic unit := rw_core reducible @@ -471,7 +471,7 @@ do e ← i_to_expr q, tactic.injection_with e hs private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas | s [] := return s -| s (n::ns) := do s' ← s^.add_simp n, add_simps s' ns +| s (n::ns) := do s' ← s.add_simp n, add_simps s' ns private meta def report_invalid_simp_lemma {α : Type} (n : name): tactic α := fail ("invalid simplification lemma '" ++ to_string n ++ "' (use command 'set_option trace.simp_lemmas true' for more details)") @@ -481,13 +481,13 @@ do p ← resolve_name n, match p.to_raw_expr with | const n _ := - (do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s^.add_simp n) + (do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s.add_simp n) <|> - (do eqns ← get_eqn_lemmas_for tt n, guard (eqns^.length > 0), save_const_type_info n ref, add_simps s eqns) + (do eqns ← get_eqn_lemmas_for tt n, guard (eqns.length > 0), save_const_type_info n ref, add_simps s eqns) <|> report_invalid_simp_lemma n | _ := - (do e ← i_to_expr p, b ← is_valid_simp_lemma reducible e, guard b, try (save_type_info e ref), s^.add e) + (do e ← i_to_expr p, b ← is_valid_simp_lemma reducible e, guard b, try (save_type_info e ref), s.add e) <|> report_invalid_simp_lemma n end @@ -497,7 +497,7 @@ let e := p.to_raw_expr in match e with | (const c []) := simp_lemmas.resolve_and_add s c e | (local_const c _ _ _) := simp_lemmas.resolve_and_add s c e -| _ := do new_e ← i_to_expr p, s^.add new_e +| _ := do new_e ← i_to_expr p, s.add new_e end private meta def simp_lemmas.append_pexprs : simp_lemmas → list pexpr → tactic simp_lemmas @@ -508,8 +508,8 @@ private meta def mk_simp_set (attr_names : list name) (hs : list pexpr) (ex : li do s₀ ← join_user_simp_lemmas attr_names, s₁ ← simp_lemmas.append_pexprs s₀ hs, -- add equational lemmas, if any - ex ← ex^.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n), - return $ simp_lemmas.erase s₁ $ ex^.join + ex ← ex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n), + return $ simp_lemmas.erase s₁ $ ex.join private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit | s := do @@ -532,7 +532,7 @@ private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → t private meta def simp_core (cfg : simp_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (loc : list name) : tactic unit := do s ← mk_simp_set attr_names hs ids, - s ← s^.append ctx, + s ← s.append ctx, match loc : _ → tactic unit with | [] := simp_goal cfg s | _ := simp_hyps cfg s loc @@ -639,12 +639,12 @@ private meta def to_qualified_name_core : name → list name → tactic name | n (ns::nss) := do curr ← return $ ns ++ n, env ← get_env, - if env^.contains curr then return curr + if env.contains curr then return curr else to_qualified_name_core n nss private meta def to_qualified_name (n : name) : tactic name := do env ← get_env, - if env^.contains n then return n + if env.contains n then return n else do ns ← open_namespaces, to_qualified_name_core n ns diff --git a/library/init/meta/match_tactic.lean b/library/init/meta/match_tactic.lean index a79d0e386e..cf68ce78a6 100644 --- a/library/init/meta/match_tactic.lean +++ b/library/init/meta/match_tactic.lean @@ -105,11 +105,11 @@ do ctx ← local_context, meta instance : has_to_tactic_format pattern := ⟨λp, do - t ← pp p^.target, - mo ← pp p^.moutput, - uo ← pp p^.uoutput, - u ← pp p^.nuvars, - m ← pp p^.nmvars, + t ← pp p.target, + mo ← pp p.moutput, + uo ← pp p.uoutput, + u ← pp p.nuvars, + m ← pp p.nmvars, return $ to_fmt "pattern.mk (" ++ t ++ ") " ++ uo ++ " " ++ mo ++ " " ++ u ++ " " ++ m ++ "" ⟩ end tactic diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index e55e4e0090..a545eb0a14 100644 --- a/library/init/meta/name.lean +++ b/library/init/meta/name.lean @@ -61,7 +61,7 @@ private def name.components' : name -> list name | (mk_numeral v n) := mk_numeral v anonymous :: name.components' n def name.components (n : name) : list name := -(name.components' n)^.reverse +(name.components' n).reverse def name.to_string : name → string := name.to_string_with_sep "." @@ -91,7 +91,7 @@ meta constant name.append_after : name → nat → name meta def name.is_prefix_of : name → name → bool | p name.anonymous := ff | p n := - if p = n then tt else name.is_prefix_of p n^.get_prefix + if p = n then tt else name.is_prefix_of p n.get_prefix meta def name.replace_prefix : name → name → name → name | anonymous p p' := anonymous diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean index 38c4fd7aab..8105a587c7 100644 --- a/library/init/meta/rb_map.lean +++ b/library/init/meta/rb_map.lean @@ -51,7 +51,7 @@ meta def filter {A B} [has_ordering A] (m : rb_map A B) (f : B → Prop) [decida fold m (mk _ _) $ λa b m', if f b then insert m' a b else m' meta def mfold {key data α :Type} {m : Type → Type} [monad m] (mp : rb_map key data) (a : α) (fn : key → data → α → m α) : m α := -mp^.fold (return a) (λ k d act, act >>= fn k d) +mp.fold (return a) (λ k d act, act >>= fn k d) end rb_map @@ -152,25 +152,25 @@ private meta def format_key {key} [has_to_format key] (k : key) (first : bool) : namespace rb_set meta def insert {key} (s : rb_set key) (k : key) : rb_set key := -s^.insert k () +s.insert k () meta def erase {key} (s : rb_set key) (k : key) : rb_set key := -s^.erase k +s.erase k meta def contains {key} (s : rb_set key) (k : key) : bool := -s^.contains k +s.contains k meta def size {key} (s : rb_set key) : nat := -s^.size +s.size meta def fold {key α : Type} (s : rb_set key) (a : α) (fn : key → α → α) : α := -s^.fold a (λ k _ a, fn k a) +s.fold a (λ k _ a, fn k a) meta def mfold {key α :Type} {m : Type → Type} [monad m] (s : rb_set key) (a : α) (fn : key → α → m α) : m α := -s^.fold (return a) (λ k act, act >>= fn k) +s.fold (return a) (λ k act, act >>= fn k) meta def to_list {key : Type} (s : rb_set key) : list key := -s^.fold [] list.cons +s.fold [] list.cons meta instance {key} [has_to_format key] : has_to_format (rb_set key) := ⟨λ m, group $ to_fmt "{" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k p, (fst p ++ format_key k (snd p), ff)))) ++ @@ -191,7 +191,7 @@ meta constant size : name_set → nat meta constant fold {α :Type} : name_set → α → (name → α → α) → α meta def to_list (s : name_set) : list name := -s^.fold [] list.cons +s.fold [] list.cons meta instance : has_to_format name_set := ⟨λ m, group $ to_fmt "{" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k p, (fst p ++ format_key k (snd p), ff)))) ++ @@ -201,6 +201,6 @@ meta def of_list (l : list name) : name_set := list.foldl name_set.insert mk_name_set l meta def mfold {α :Type} {m : Type → Type} [monad m] (ns : name_set) (a : α) (fn : name → α → m α) : m α := -ns^.fold (return a) (λ k act, act >>= fn k) +ns.fold (return a) (λ k act, act >>= fn k) end name_set diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean index 3e70cbbd2e..ca6b4785e5 100644 --- a/library/init/meta/relation_tactics.lean +++ b/library/init/meta/relation_tactics.lean @@ -29,13 +29,13 @@ relation_tactic md environment.trans_for "transitivity" meta def relation_lhs_rhs : expr → tactic (name × expr × expr) := λ e, do - (const c _) ← return e^.get_app_fn, + (const c _) ← return e.get_app_fn, env ← get_env, - (some (arity, lhs_pos, rhs_pos)) ← return $ env^.relation_info c, + (some (arity, lhs_pos, rhs_pos)) ← return $ env.relation_info c, args ← return $ get_app_args e, - guard (args^.length = arity), - (some lhs) ← return $ args^.nth lhs_pos, - (some rhs) ← return $ args^.nth rhs_pos, + guard (args.length = arity), + (some lhs) ← return $ args.nth lhs_pos, + (some rhs) ← return $ args.nth rhs_pos, return (c, lhs, rhs) meta def target_lhs_rhs : tactic (name × expr × expr) := @@ -45,7 +45,7 @@ meta def subst_vars_aux : list expr → tactic unit | [] := failed | (h::hs) := do o ← try_core (subst h), - if o^.is_none then subst_vars_aux hs + if o.is_none then subst_vars_aux hs else return () /-- Try to apply subst exhaustively -/ diff --git a/library/init/meta/smt/congruence_closure.lean b/library/init/meta/smt/congruence_closure.lean index 67580199bc..5e03494ded 100644 --- a/library/init/meta/smt/congruence_closure.lean +++ b/library/init/meta/smt/congruence_closure.lean @@ -71,7 +71,7 @@ meta def in_singlenton_eqc (s : cc_state) (e : expr) : bool := s.next e = e meta def eqc_size (s : cc_state) (e : expr) : nat := -(s.eqc_of e)^.length +(s.eqc_of e).length meta def fold_eqc_core {α} (s : cc_state) (f : α → expr → α) (first : expr) : expr → α → α | c a := diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 97cc7ca1a5..f5eaa95640 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -22,7 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit := tac >> solve_goals meta def istep {α : Type} (line : nat) (col : nat) (tac : smt_tactic α) : smt_tactic unit := -λ ss ts, (@scope_trace _ line col ((tac >> solve_goals) ss ts))^.clamp_pos line col +λ ss ts, (@scope_trace _ line col ((tac >> solve_goals) ss ts)).clamp_pos line col meta def execute (tac : smt_tactic unit) : tactic unit := using_smt tac diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index ac6fb3e304..1ee45825e0 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -28,7 +28,7 @@ meta instance : has_to_format tactic_state := ⟨tactic_state.to_format⟩ meta instance : has_to_string tactic_state := -⟨λ s, (to_fmt s)^.to_string s.get_options⟩ +⟨λ s, (to_fmt s).to_string s.get_options⟩ @[reducible] meta def tactic := interaction_monad tactic_state @[reducible] meta def tactic_result := interaction_monad.result tactic_state @@ -192,7 +192,7 @@ do s ← read, meta def get_decl (n : name) : tactic declaration := do s ← read, - (env s)^.get n + (env s).get n meta def trace {α : Type u} [has_to_tactic_format α] (a : α) : tactic unit := do fmt ← pp a, @@ -348,9 +348,9 @@ structure apply_cfg := (use_instances := tt) /-- Apply the expression `e` to the main goal, the unification is performed using the transparency mode in `cfg`. - If cfg^.approx is `tt`, then fallback to first-order unification, and approximate context during unification. - If cfg^.all is `tt`, then all unassigned meta-variables are added as new goals. - If cfg^.use_instances is `tt`, then use type class resolution to instantiate unassigned meta-variables. + If cfg.approx is `tt`, then fallback to first-order unification, and approximate context during unification. + If cfg.all is `tt`, then all unassigned meta-variables are added as new goals. + If cfg.use_instances is `tt`, then use type class resolution to instantiate unassigned meta-variables. It returns a list of all introduced meta variables, even the assigned ones. -/ meta constant apply_core (e : expr) (cfg : apply_cfg := {}) : tactic (list expr) /- Create a fresh meta universe variable. -/ @@ -461,7 +461,7 @@ meta def step {α : Type u} (t : tactic α) : tactic unit := t >>[tactic] cleanup meta def istep {α : Type u} (line col : ℕ) (t : tactic α) : tactic unit := -λ s, (@scope_trace _ line col (step t s))^.clamp_pos line col +λ s, (@scope_trace _ line col (step t s)).clamp_pos line col meta def is_prop (e : expr) : tactic bool := do t ← infer_type e, diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean index b487e9bd83..cefd6af980 100644 --- a/library/init/meta/transfer.lean +++ b/library/init/meta/transfer.lean @@ -45,9 +45,9 @@ private meta structure rel_data := meta instance has_to_tactic_format_rel_data : has_to_tactic_format rel_data := ⟨λr, do - R ← pp r^.relation, - α ← pp r^.in_type, - β ← pp r^.out_type, + R ← pp r.relation, + α ← pp r.in_type, + β ← pp r.out_type, return $ to_fmt "(" ++ R ++ ": rel (" ++ α ++ ") (" ++ β ++ "))" ⟩ private meta structure rule_data := @@ -61,13 +61,13 @@ private meta structure rule_data := meta instance has_to_tactic_format_rule_data : has_to_tactic_format rule_data := ⟨λr, do - pr ← pp r^.pr, - up ← pp r^.uparams, - mp ← pp r^.params, - ua ← pp r^.uargs, - ma ← pp r^.args, - pat ← pp r^.pat^.target, - out ← pp r^.out, + pr ← pp r.pr, + up ← pp r.uparams, + mp ← pp r.params, + ua ← pp r.uargs, + ma ← pp r.args, + pat ← pp r.pat.target, + out ← pp r.out, return $ to_fmt "{ ⟨" ++ pat ++ "⟩ pr: " ++ pr ++ " → " ++ out ++ ", " ++ up ++ " " ++ mp ++ " " ++ ua ++ " " ++ ma ++ " }" ⟩ private meta def get_lift_fun : expr → tactic (list rel_data × expr) @@ -89,7 +89,7 @@ private meta def analyse_rule (u' : list name) (pr : expr) : tactic rule_data := (params, app (app r f) g) ← mk_local_pis t, (arg_rels, R) ← get_lift_fun r, args ← monad.for (enum arg_rels) (λ⟨n, a⟩, - prod.mk <$> mk_local_def (mk_simple_name ("a_" ++ to_string n)) a^.in_type <*> pure a), + prod.mk <$> mk_local_def (mk_simple_name ("a_" ++ to_string n)) a.in_type <*> pure a), a_vars ← return $ fmap prod.fst args, p ← head_beta (app_of_list f a_vars), p_data ← return $ mark_occurences (app R p) params, @@ -101,9 +101,9 @@ private meta def analyse_rule (u' : list name) (pr : expr) : tactic rule_data := private meta def analyse_decls : list name → tactic (list rule_data) := monad.mapm (λn, do d ← get_decl n, - c ← return d^.univ_params^.length, + c ← return d.univ_params.length, ls ← monad.for (range c) (λ_, mk_fresh_name), - analyse_rule ls (const n (ls^.map level.param))) + analyse_rule ls (const n (ls.map level.param))) private meta def split_params_args : list (expr × bool) → list expr → list (expr × option expr) × list expr | ((lc, tt) :: ps) (e :: es) := let (ps', es') := split_params_args ps es in ((lc, some e) :: ps', es') @@ -138,21 +138,21 @@ It return (`a`, pr : `R a b`) -/ meta def compute_transfer : list rule_data → list expr → expr → tactic (expr × expr × list expr) | rds ctxt e := do -- Select matching rule - (i, ps, args, ms, rd) ← first (rds^.for (λrd, do - (l, m) ← match_pattern_core semireducible rd^.pat e, - level_map ← monad.for rd^.uparams (λl, prod.mk l <$> mk_meta_univ), - inst_univ ← return $ (λe, instantiate_univ_params e (level_map ++ zip rd^.uargs l)), - (ps, args) ← return $ split_params_args (list.map (prod.map inst_univ id) rd^.params) m, + (i, ps, args, ms, rd) ← first (rds.for (λrd, do + (l, m) ← match_pattern_core semireducible rd.pat e, + level_map ← monad.for rd.uparams (λl, prod.mk l <$> mk_meta_univ), + inst_univ ← return $ (λe, instantiate_univ_params e (level_map ++ zip rd.uargs l)), + (ps, args) ← return $ split_params_args (list.map (prod.map inst_univ id) rd.params) m, (ps, ms) ← param_substitutions ctxt ps, /- this checks type class parameters -/ return (instantiate_locals ps ∘ inst_univ, ps, args, ms, rd))), - (bs, hs, mss) ← monad.for (zip rd^.args args) (λ⟨⟨_, d⟩, e⟩, do + (bs, hs, mss) ← monad.for (zip rd.args args) (λ⟨⟨_, d⟩, e⟩, do -- Argument has function type - (args, r) ← get_lift_fun (i d^.relation), + (args, r) ← get_lift_fun (i d.relation), ((a_vars, b_vars), (R_vars, bnds)) ← monad.for (enum args) (λ⟨n, arg⟩, do - a ← mk_local_def (("a" ++ to_string n) : string) arg^.in_type, - b ← mk_local_def (("b" ++ to_string n) : string) arg^.out_type, - R ← mk_local_def (("R" ++ to_string n) : string) (arg^.relation a b), + a ← mk_local_def (("a" ++ to_string n) : string) arg.in_type, + b ← mk_local_def (("b" ++ to_string n) : string) arg.out_type, + R ← mk_local_def (("R" ++ to_string n) : string) (arg.relation a b), return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip), rds' ← monad.for R_vars (analyse_rule []), @@ -164,8 +164,8 @@ meta def compute_transfer : list rule_data → list expr → expr → tactic (ex return (b', [a, b', lambdas (list.join bnds) pr], ms)) >>= (return ∘ prod.map id unzip ∘ unzip), -- Combine - b ← head_beta (app_of_list (i rd^.out) bs), - pr ← return $ app_of_list (i rd^.pr) (fmap prod.snd ps ++ list.join hs), + b ← head_beta (app_of_list (i rd.out) bs), + pr ← return $ app_of_list (i rd.pr) (fmap prod.snd ps ++ list.join hs), return (b, pr, ms ++ list.join mss) meta def transfer (ds : list name) : tactic unit := do diff --git a/library/init/propext.lean b/library/init/propext.lean index 87d080adbd..bb6fde2f56 100644 --- a/library/init/propext.lean +++ b/library/init/propext.lean @@ -12,13 +12,13 @@ constant propext {a b : Prop} : (a ↔ b) → a = b universes u v lemma forall_congr_eq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x := -propext (forall_congr (λ a, (h a)^.to_iff)) +propext (forall_congr (λ a, (h a).to_iff)) lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) := -propext (imp_congr h₁^.to_iff h₂^.to_iff) +propext (imp_congr h₁.to_iff h₂.to_iff) lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) := -propext (imp_congr_ctx h₁^.to_iff (λ hc, (h₂ hc)^.to_iff)) +propext (imp_congr_ctx h₁.to_iff (λ hc, (h₂ hc).to_iff)) lemma eq_true_intro {a : Prop} (h : a) : a = true := propext (iff_true_intro h) @@ -32,7 +32,7 @@ propext h theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := propext (iff.intro (assume h, iff.to_eq h) - (assume h, h^.to_iff)) + (assume h, h.to_iff)) lemma eq_false {a : Prop} : (a = false) = (¬ a) := have (a ↔ false) = (¬ a), from propext (iff_false a), diff --git a/library/init/relator.lean b/library/init/relator.lean index 806bf5fa9b..019dc3525a 100644 --- a/library/init/relator.lean +++ b/library/init/relator.lean @@ -50,8 +50,8 @@ variables {α : Type u₁} {β : Type u₂} (R : α → β → Prop) lemma rel_forall_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) := take p q Hrel, - ⟨take H b, exists.elim (t^.right b) (take a Rab, (Hrel Rab)^.mp (H _)), - take H a, exists.elim (t^.left a) (take b Rab, (Hrel Rab)^.mpr (H _))⟩ + ⟨take H b, exists.elim (t.right b) (take a Rab, (Hrel Rab).mp (H _)), + take H a, exists.elim (t.left a) (take b Rab, (Hrel Rab).mpr (H _))⟩ lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ iff)) eq eq') : left_unique R | a b c (ab : R a b) (cb : R c b) := diff --git a/library/init/wf.lean b/library/init/wf.lean index 5b2bddb96d..5a6aae1e4b 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -167,7 +167,7 @@ section @prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) p (xa, xb) lt (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁) - (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂^.symm (ihb b₁ (eq.rec_on eq₃ h))), + (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂.symm (ihb b₁ (eq.rec_on eq₃ h))), aux rfl rfl))) -- The lexicographical order of well founded relations is well-founded diff --git a/library/tools/debugger/cli.lean b/library/tools/debugger/cli.lean index da384ee2d5..cac54e070c 100644 --- a/library/tools/debugger/cli.lean +++ b/library/tools/debugger/cli.lean @@ -49,7 +49,7 @@ match args with fn ← return $ to_qualified_name arg, ok ← is_valid_fn_prefix fn, if ok then - return {s with fn_bps := fn :: list.filter (λ fn', fn ≠ fn') s^.fn_bps} + return {s with fn_bps := fn :: list.filter (λ fn', fn ≠ fn') s.fn_bps} else vm.put_str "invalid 'break' command, given name is not the prefix for any function\n" >> return s @@ -62,7 +62,7 @@ meta def remove_breakpoint (s : state) (args : list string) : vm state := match args with | [arg] := do fn ← return $ to_qualified_name arg, - return {s with fn_bps := list.filter (λ fn', fn ≠ fn') s^.fn_bps} + return {s with fn_bps := list.filter (λ fn', fn ≠ fn') s.fn_bps} | _ := vm.put_str "invalid 'rbreak ' command, incorrect number of arguments\n" >> return s @@ -72,7 +72,7 @@ meta def show_breakpoints : list name → vm unit | [] := return () | (fn::fns) := do vm.put_str " ", - vm.put_str fn^.to_string, + vm.put_str fn.to_string, vm.put_str "\n", show_breakpoints fns @@ -87,7 +87,7 @@ do sz ← vm.call_stack_size, meta def pidx_cmd : nat → list string → vm unit | frame [arg] := do - idx ← return $ arg^.to_nat, + idx ← return $ arg.to_nat, sz ← vm.stack_size, (bp, ep) ← vm.call_stack_var_range frame, if bp + idx >= ep then @@ -96,9 +96,9 @@ meta def pidx_cmd : nat → list string → vm unit v ← vm.pp_stack_obj (bp+idx), (n, t) ← vm.stack_obj_info (bp+idx), opts ← vm.get_options, - vm.put_str n^.to_string, + vm.put_str n.to_string, vm.put_str " := ", - vm.put_str (v^.to_string opts), + vm.put_str (v.to_string opts), vm.put_str "\n" | _ _ := vm.put_str "invalid 'pidx ' command, incorrect number of arguments\n" @@ -111,9 +111,9 @@ meta def print_var : nat → nat → name → vm unit if n = v then do v ← vm.pp_stack_obj i, opts ← vm.get_options, - vm.put_str n^.to_string, + vm.put_str n.to_string, vm.put_str " := ", - vm.put_str (v^.to_string opts), + vm.put_str (v.to_string opts), vm.put_str "\n" else print_var (i+1) ep v @@ -147,7 +147,7 @@ meta def cmd_loop_core : state → nat → list string → vm state else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame [] else if cmd = "bs" then do vm.put_str "breakpoints\n", - show_breakpoints s^.fn_bps, + show_breakpoints s.fn_bps, cmd_loop_core s frame default_cmd else if cmd = "up" ∨ cmd = "u" then do frame ← up_cmd frame, cmd_loop_core s frame ["u"] else if cmd = "down" ∨ cmd = "d" then do frame ← down_cmd frame, cmd_loop_core s frame ["d"] @@ -168,7 +168,7 @@ def prune_active_bps_core (csz : nat) : list (nat × name) → list (nat × name meta def prune_active_bps (s : state) : vm state := do sz ← vm.call_stack_size, - return {s with active_bps := prune_active_bps_core sz s^.active_bps} + return {s with active_bps := prune_active_bps_core sz s.active_bps} meta def updt_csz (s : state) : vm state := do sz ← vm.call_stack_size, @@ -176,11 +176,11 @@ do sz ← vm.call_stack_size, meta def init_transition (s : state) : vm state := do opts ← vm.get_options, - if opts^.get_bool `server ff then return {s with md := mode.done} + if opts.get_bool `server ff then return {s with md := mode.done} else do bps ← vm.get_attribute `breakpoint, new_s ← return {s with fn_bps := bps}, - if opts^.get_bool `debugger.autorun ff then + if opts.get_bool `debugger.autorun ff then return {new_s with md := mode.run} else do vm.put_str "Lean debugger\n", @@ -191,20 +191,20 @@ do opts ← vm.get_options, meta def step_transition (s : state) : vm state := do sz ← vm.call_stack_size, - if sz = s^.csz then return s + if sz = s.csz then return s else do show_curr_fn "step", cmd_loop s ["s"] meta def bp_reached (s : state) : vm bool := (do fn ← vm.curr_fn, - return $ s^.fn_bps^.any (λ p, p^.is_prefix_of fn)) + return $ s.fn_bps.any (λ p, p.is_prefix_of fn)) <|> return ff meta def in_active_bps (s : state) : vm bool := do sz ← vm.call_stack_size, - match s^.active_bps with + match s.active_bps with | [] := return ff | (csz, _)::_ := return (sz = csz) end @@ -217,15 +217,15 @@ do b1 ← in_active_bps s, show_curr_fn "breakpoint", fn ← vm.curr_fn, sz ← vm.call_stack_size, - new_s ← return $ {s with active_bps := (sz, fn) :: s^.active_bps}, + new_s ← return $ {s with active_bps := (sz, fn) :: s.active_bps}, cmd_loop new_s ["r"] meta def step_fn (s : state) : vm state := do s ← prune_active_bps s, - if s^.md = mode.init then do new_s ← init_transition s, updt_csz new_s - else if s^.md = mode.done then return s - else if s^.md = mode.step then do new_s ← step_transition s, updt_csz new_s - else if s^.md = mode.run then do new_s ← run_transition s, updt_csz new_s + if s.md = mode.init then do new_s ← init_transition s, updt_csz new_s + else if s.md = mode.done then return s + else if s.md = mode.step then do new_s ← step_transition s, updt_csz new_s + else if s.md = mode.run then do new_s ← run_transition s, updt_csz new_s else return s @[vm_monitor] diff --git a/library/tools/debugger/util.lean b/library/tools/debugger/util.lean index 96020ad1ae..94ab930be0 100644 --- a/library/tools/debugger/util.lean +++ b/library/tools/debugger/util.lean @@ -11,20 +11,20 @@ def split_core : string → string → list string | (c::cs) [] := if is_space c then split_core cs [] else split_core cs [c] | (c::cs) r := - if is_space c then r^.reverse :: split_core cs [] else split_core cs (c::r) + if is_space c then r.reverse :: split_core cs [] else split_core cs (c::r) | [] [] := [] -| [] r := [r^.reverse] +| [] r := [r.reverse] def split (s : string) : list string := -(split_core s [])^.reverse +(split_core s []).reverse def to_qualified_name_core : string → string → name -| [] r := if r = "" then name.anonymous else mk_simple_name r^.reverse +| [] r := if r = "" then name.anonymous else mk_simple_name r.reverse | (c::cs) r := if is_space c then to_qualified_name_core cs r else if c = #"." then if r = "" then to_qualified_name_core cs [] - else name.mk_string r^.reverse (to_qualified_name_core cs []) + else name.mk_string r.reverse (to_qualified_name_core cs []) else to_qualified_name_core cs (c::r) def to_qualified_name (s : string) : name := @@ -47,16 +47,16 @@ do { d ← vm.get_decl fn, some p ← return (vm_decl.pos d) | failure, file ← get_file fn, - return (file ++ ":" ++ p^.line^.to_string ++ ":" ++ p^.column^.to_string) + return (file ++ ":" ++ p.line.to_string ++ ":" ++ p.column.to_string) } <|> return "" meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit := do pos ← pos_info fn, - vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header), + vm.put_str ("[" ++ frame.to_string ++ "] " ++ header), if header = "" then return () else vm.put_str " ", - vm.put_str (fn^.to_string ++ " at " ++ pos ++ "\n") + vm.put_str (fn.to_string ++ " at " ++ pos ++ "\n") meta def show_curr_fn (header : string) : vm unit := do fn ← vm.curr_fn, @@ -65,10 +65,10 @@ do fn ← vm.curr_fn, meta def is_valid_fn_prefix (p : name) : vm bool := do env ← vm.get_env, - return $ env^.fold ff (λ d r, + return $ env.fold ff (λ d r, r || - let n := d^.to_name in - p^.is_prefix_of n) + let n := d.to_name in + p.is_prefix_of n) meta def show_frame (frame_idx : nat) : vm unit := do sz ← vm.call_stack_size, @@ -78,7 +78,7 @@ do sz ← vm.call_stack_size, meta def type_to_string : option expr → nat → vm string | none i := do o ← vm.stack_obj i, - match o^.kind with + match o.kind with | vm_obj_kind.simple := return "[tagged value]" | vm_obj_kind.constructor := return "[constructor]" | vm_obj_kind.closure := return "[closure]" @@ -97,7 +97,7 @@ meta def type_to_string : option expr → nat → vm string | (some type) i := do fmt ← vm.pp_expr type, opts ← vm.get_options, - return (fmt^.to_string opts) + return (fmt.to_string opts) meta def show_vars_core : nat → nat → nat → vm unit | c i e := @@ -105,7 +105,7 @@ meta def show_vars_core : nat → nat → nat → vm unit else do (n, type) ← vm.stack_obj_info i, type_str ← type_to_string type i, - vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n", + vm.put_str $ "#" ++ c.to_string ++ " " ++ n.to_string ++ " : " ++ type_str ++ "\n", show_vars_core (c+1) (i+1) e meta def show_vars (frame : nat) : vm unit := diff --git a/library/tools/mini_crush/default.lean b/library/tools/mini_crush/default.lean index 995def3a22..64c2fccf68 100644 --- a/library/tools/mini_crush/default.lean +++ b/library/tools/mini_crush/default.lean @@ -14,7 +14,7 @@ namespace mini_crush open tactic meta def size (e : expr) : nat := -e^.fold 1 (λ e _ n, n+1) +e.fold 1 (λ e _ n, n+1) /- Collect relevant functions -/ @@ -28,53 +28,53 @@ meta def is_auto_construction : name → bool meta def is_relevant_fn (n : name) : tactic bool := do env ← get_env, - if ¬env^.is_definition n ∨ is_auto_construction n then return ff - else if env^.in_current_file n then return tt + if ¬env.is_definition n ∨ is_auto_construction n then return ff + else if env.in_current_file n then return tt else in_open_namespaces n meta def collect_revelant_fns_aux : name_set → expr → tactic name_set | s e := -e^.mfold s $ λ t _ s, +e.mfold s $ λ t _ s, match t with | expr.const c _ := - if s^.contains c then return s + if s.contains c then return s else mcond (is_relevant_fn c) - (do new_s ← return $ if c^.is_internal then s else s^.insert c, + (do new_s ← return $ if c.is_internal then s else s.insert c, d ← get_decl c, - collect_revelant_fns_aux new_s d^.value) + collect_revelant_fns_aux new_s d.value) (return s) | _ := return s end meta def collect_revelant_fns : tactic name_set := do ctx ← local_context, - s₁ ← ctx^.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set, + s₁ ← ctx.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set, target >>= collect_revelant_fns_aux s₁ meta def add_relevant_eqns (s : simp_lemmas) : tactic simp_lemmas := do fns ← collect_revelant_fns, - fns^.mfold s (λ fn s, get_eqn_lemmas_for tt fn >>= mfoldl simp_lemmas.add_simp s) + fns.mfold s (λ fn s, get_eqn_lemmas_for tt fn >>= mfoldl simp_lemmas.add_simp s) meta def add_relevant_eqns_h (hs : hinst_lemmas) : tactic hinst_lemmas := do fns ← collect_revelant_fns, - fns^.mfold hs (λ fn hs, get_eqn_lemmas_for tt fn >>= mfoldl (λ hs d, hs^.add <$> hinst_lemma.mk_from_decl d) hs) + fns.mfold hs (λ fn hs, get_eqn_lemmas_for tt fn >>= mfoldl (λ hs d, hs.add <$> hinst_lemma.mk_from_decl d) hs) /- Collect terms that are inductive datatypes -/ meta def is_inductive (e : expr) : tactic bool := do type ← infer_type e, - C ← return type^.get_app_fn, + C ← return type.get_app_fn, env ← get_env, - return $ C^.is_constant && env^.is_inductive C^.const_name + return $ C.is_constant && env.is_inductive C.const_name meta def collect_inductive_aux : expr_set → expr → tactic expr_set | S e := - if S^.contains e then return S + if S.contains e then return S else do - new_S ← mcond (is_inductive e) (return $ S^.insert e) (return S), + new_S ← mcond (is_inductive e) (return $ S.insert e) (return S), match e with | expr.app _ _ := fold_explicit_args e new_S collect_inductive_aux - | expr.pi _ _ d b := if e^.is_arrow then collect_inductive_aux S d >>= flip collect_inductive_aux b else return new_S + | expr.pi _ _ d b := if e.is_arrow then collect_inductive_aux S d >>= flip collect_inductive_aux b else return new_S | _ := return new_S end @@ -83,7 +83,7 @@ collect_inductive_aux mk_expr_set meta def collect_inductive_from_target : tactic (list expr) := do S ← target >>= collect_inductive, - return $ list.qsort (λ e₁ e₂, size e₁ < size e₂) $ S^.to_list + return $ list.qsort (λ e₁ e₂, size e₁ < size e₂) $ S.to_list meta def collect_inductive_hyps : tactic (list expr) := local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return r)) [] @@ -156,7 +156,7 @@ do { meta def try_all_aux {α β : Type} (ts : α → tactic β) : list α → list (α × β × nat × snapshot) → tactic (list (α × β × nat × snapshot)) | [] [] := failed -| [] rs := return rs^.reverse +| [] rs := return rs.reverse | (v::vs) rs := do r ← try_and_save (ts v), match r with @@ -176,7 +176,7 @@ do es ← collect_inductive_from_target, when_tracing `mini_crush (do p ← pp e, trace (to_fmt "Splitting on '" ++ p ++ to_fmt "'")), cases e; simph_intros_using s cfg; try (close_aux hs)) es, rs ← return $ flip list.qsort rs (λ ⟨e₁, _, n₁, _⟩ ⟨e₂, _, n₂, _⟩, if n₁ ≠ n₂ then n₁ < n₂ else size e₁ < size e₂), - return $ rs^.map (λ ⟨_, _, _, s⟩, ((), s)) + return $ rs.map (λ ⟨_, _, _, s⟩, ((), s)) meta def search_cases (max_depth : nat) (s : simp_lemmas) (hs : hinst_lemmas) (cfg : simp_config) (s_name : name) : tactic unit := diff --git a/library/tools/mini_crush/nano_crush.lean b/library/tools/mini_crush/nano_crush.lean index 3651e09cf3..65b39f4bae 100644 --- a/library/tools/mini_crush/nano_crush.lean +++ b/library/tools/mini_crush/nano_crush.lean @@ -12,7 +12,7 @@ namespace nano_crush open tactic meta def size (e : expr) : nat := -e^.fold 1 (λ e _ n, n+1) +e.fold 1 (λ e _ n, n+1) /- Collect relevant functions -/ @@ -26,51 +26,51 @@ meta def is_auto_construction : name → bool meta def is_relevant_fn (n : name) : tactic bool := do env ← get_env, - if ¬env^.is_definition n ∨ is_auto_construction n then return ff - else if env^.in_current_file n then return tt + if ¬env.is_definition n ∨ is_auto_construction n then return ff + else if env.in_current_file n then return tt else in_open_namespaces n meta def collect_revelant_fns_aux : name_set → expr → tactic name_set | s e := -e^.mfold s $ λ t _ s, +e.mfold s $ λ t _ s, match t with | expr.const c _ := - if s^.contains c then return s + if s.contains c then return s else mcond (is_relevant_fn c) - (do new_s ← return $ if c^.is_internal then s else s^.insert c, + (do new_s ← return $ if c.is_internal then s else s.insert c, d ← get_decl c, - collect_revelant_fns_aux new_s d^.value) + collect_revelant_fns_aux new_s d.value) (return s) | _ := return s end meta def collect_revelant_fns : tactic name_set := do ctx ← local_context, - s₁ ← ctx^.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set, + s₁ ← ctx.mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set, target >>= collect_revelant_fns_aux s₁ meta def add_relevant_eqns (hs : hinst_lemmas) : tactic hinst_lemmas := do fns ← collect_revelant_fns, - fns^.mfold hs (λ fn hs, get_eqn_lemmas_for tt fn >>= mfoldl (λ hs d, hs^.add <$> hinst_lemma.mk_from_decl d) hs) + fns.mfold hs (λ fn hs, get_eqn_lemmas_for tt fn >>= mfoldl (λ hs d, hs.add <$> hinst_lemma.mk_from_decl d) hs) /- Collect terms that are inductive datatypes -/ meta def is_inductive (e : expr) : tactic bool := do type ← infer_type e, - C ← return type^.get_app_fn, + C ← return type.get_app_fn, env ← get_env, - return $ C^.is_constant && env^.is_inductive C^.const_name + return $ C.is_constant && env.is_inductive C.const_name open expr meta def collect_inductive_aux : expr_set → expr → tactic expr_set | S e := - if S^.contains e then return S + if S.contains e then return S else do - new_S ← mcond (is_inductive e) (return $ S^.insert e) (return S), + new_S ← mcond (is_inductive e) (return $ S.insert e) (return S), match e with | app _ _ := fold_explicit_args e new_S collect_inductive_aux - | pi _ _ d b := if e^.is_arrow then collect_inductive_aux S d >>= flip collect_inductive_aux b else return new_S + | pi _ _ d b := if e.is_arrow then collect_inductive_aux S d >>= flip collect_inductive_aux b else return new_S | _ := return new_S end @@ -81,7 +81,7 @@ open list meta def collect_inductive_from_target : tactic (list expr) := do S ← target >>= collect_inductive, - return $ qsort ((<) on size) S^.to_list + return $ qsort ((<) on size) S.to_list meta def collect_inductive_hyps : tactic (list expr) := local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return r)) [] diff --git a/library/tools/super/cdcl.lean b/library/tools/super/cdcl.lean index a891281ad3..c734be1019 100644 --- a/library/tools/super/cdcl.lean +++ b/library/tools/super/cdcl.lean @@ -14,7 +14,7 @@ res ← cdcl.solve (cdcl.theory_solver_of_tactic th_solver) local_false clauses, match res with | (cdcl.result.unsat proof) := exact proof | (cdcl.result.sat interp) := - let interp' := do e ← interp^.to_list, [if e.2 = tt then e.1 else ```(not %%e.1)] in + let interp' := do e ← interp.to_list, [if e.2 = tt then e.1 else ```(not %%e.1)] in do pp_interp ← pp interp', fail (to_fmt "satisfying assignment: " ++ pp_interp) end diff --git a/library/tools/super/cdcl_solver.lean b/library/tools/super/cdcl_solver.lean index f7eac8e3da..b512f66b8d 100644 --- a/library/tools/super/cdcl_solver.lean +++ b/library/tools/super/cdcl_solver.lean @@ -101,7 +101,7 @@ meta def initial (local_false : expr) : state := { } meta def watches_for (st : state) (pl : prop_lit) : watch_map := -(st^.watches^.find pl)^.get_or_else (rb_map.mk _ _) +(st.watches.find pl).get_or_else (rb_map.mk _ _) end state @@ -115,14 +115,14 @@ meta def fail {A B} [has_to_format B] (b : B) : solver A := @tactic.fail A B _ b meta def get_local_false : solver expr := -do st ← state_t.read, return st^.local_false +do st ← state_t.read, return st.local_false meta def mk_var_core (v : prop_var) (ph : bool) : solver unit := do -state_t.modify $ λst, match st^.vars^.find v with +state_t.modify $ λst, match st.vars.find v with | (some _) := st | none := { st with - vars := st^.vars^.insert v ⟨ph, none⟩, - unassigned := st^.unassigned^.insert v v + vars := st.vars.insert v ⟨ph, none⟩, + unassigned := st.unassigned.insert v v } end @@ -132,36 +132,36 @@ meta def set_conflict (proof : proof_term) : solver unit := state_t.modify $ λst, { st with conflict := some proof } meta def has_conflict : solver bool := -do st ← state_t.read, return st^.conflict^.is_some +do st ← state_t.read, return st.conflict.is_some meta def push_trail (elem : trail_elem) : solver unit := do st ← state_t.read, -match st^.vars^.find elem^.var with -| none := fail $ "unknown variable: " ++ elem^.var^.to_string -| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem^.var^.to_string +match st.vars.find elem.var with +| none := fail $ "unknown variable: " ++ elem.var.to_string +| some ⟨_, some _⟩ := fail $ "adding already assigned variable to trail: " ++ elem.var.to_string | some ⟨_, none⟩ := state_t.write { st with - vars := st^.vars^.insert elem^.var ⟨elem^.phase, some elem^.hyp⟩, - unassigned := st^.unassigned^.erase elem^.var, - trail := elem :: st^.trail, - unitp_queue := elem^.var :: st^.unitp_queue + vars := st.vars.insert elem.var ⟨elem.phase, some elem.hyp⟩, + unassigned := st.unassigned.erase elem.var, + trail := elem :: st.trail, + unitp_queue := elem.var :: st.unitp_queue } end meta def pop_trail_core : solver (option trail_elem) := do st ← state_t.read, -match st^.trail with +match st.trail with | elem :: rest := do state_t.write { st with trail := rest, - vars := st^.vars^.insert elem^.var ⟨elem^.phase, none⟩, - unassigned := st^.unassigned^.insert elem^.var elem^.var, + vars := st.vars.insert elem.var ⟨elem.phase, none⟩, + unassigned := st.unassigned.insert elem.var elem.var, unitp_queue := [] }, return $ some elem | [] := return none end meta def is_decision_level_zero : solver bool := -do st ← state_t.read, return $ st^.trail^.for_all $ λelem, ¬elem^.is_decision +do st ← state_t.read, return $ st.trail.for_all $ λelem, ¬elem.is_decision meta def revert_to_decision_level_zero : unit → solver unit | () := do is_dl0 ← is_decision_level_zero, @@ -172,11 +172,11 @@ meta def formula_of_lit (local_false : expr) (v : prop_var) (ph : bool) := if ph then v else imp v local_false meta def lookup_var (v : prop_var) : solver (option var_state) := -do st ← state_t.read, return $ st^.vars^.find v +do st ← state_t.read, return $ st.vars.find v meta def add_propagation (v : prop_var) (ph : bool) (just : proof_term) (just_is_dn : bool) : solver unit := do v_st ← lookup_var v, local_false ← get_local_false, match v_st with -| none := fail $ "propagating unknown variable: " ++ v^.to_string +| none := fail $ "propagating unknown variable: " ++ v.to_string | some ⟨assg_ph, some proof⟩ := if ph = assg_ph then return () @@ -200,11 +200,11 @@ hyp ← return $ local_const hyp_name hyp_name binder_info.default (formula_of_l push_trail $ trail_elem.dec v ph hyp meta def lookup_lit (l : clause.literal) : solver (option (bool × proof_hyp)) := -do var_st_opt ← lookup_var l^.formula, match var_st_opt with +do var_st_opt ← lookup_var l.formula, match var_st_opt with | none := return none | some ⟨ph, none⟩ := return none | some ⟨ph, some proof⟩ := - return $ some (if l^.is_neg then bnot ph else ph, proof) + return $ some (if l.is_neg then bnot ph else ph, proof) end meta def lit_is_false (l : clause.literal) : solver bool := @@ -217,57 +217,57 @@ meta def lit_is_not_false (l : clause.literal) : solver bool := do isf ← lit_is_false l, return $ bnot isf meta def cls_is_false (c : clause) : solver bool := -lift list.band $ mapm lit_is_false c^.get_lits +lift list.band $ mapm lit_is_false c.get_lits private meta def unit_propg_cls' : clause → solver (option prop_var) | c := -if c^.num_lits = 0 then return (some c^.proof) -else let hd := c^.get_lit 0 in +if c.num_lits = 0 then return (some c.proof) +else let hd := c.get_lit 0 in do lit_st ← lookup_lit hd, match lit_st with -| some (ff, isf_prf) := unit_propg_cls' (c^.inst isf_prf) +| some (ff, isf_prf) := unit_propg_cls' (c.inst isf_prf) | _ := return none end meta def unit_propg_cls : clause → solver unit | c := do has_confl ← has_conflict, if has_confl then return () else -if c^.num_lits = 0 then do set_conflict c^.proof -else let hd := c^.get_lit 0 in +if c.num_lits = 0 then do set_conflict c.proof +else let hd := c.get_lit 0 in do lit_st ← lookup_lit hd, match lit_st with -| some (ff, isf_prf) := unit_propg_cls (c^.inst isf_prf) +| some (ff, isf_prf) := unit_propg_cls (c.inst isf_prf) | some (tt, _) := return () | none := -do fls_prf_opt ← unit_propg_cls' (c^.inst (expr.mk_var 0)), +do fls_prf_opt ← unit_propg_cls' (c.inst (expr.mk_var 0)), match fls_prf_opt with | some fls_prf := do -fls_prf' ← return $ lam `H binder_info.default c^.type^.binding_domain fls_prf, -if hd^.is_neg then - add_propagation hd^.formula ff fls_prf' ff +fls_prf' ← return $ lam `H binder_info.default c.type.binding_domain fls_prf, +if hd.is_neg then + add_propagation hd.formula ff fls_prf' ff else - add_propagation hd^.formula tt fls_prf' tt + add_propagation hd.formula tt fls_prf' tt | none := return () end end private meta def modify_watches_for (pl : prop_lit) (f : watch_map → watch_map) : solver unit := state_t.modify $ λst, { st with - watches := st^.watches^.insert pl $ f $ st^.watches_for pl + watches := st.watches.insert pl $ f $ st.watches_for pl } private meta def add_watch (n : name) (c : clause) (i j : ℕ) : solver unit := -let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in -modify_watches_for pl $ λw, w^.insert n (i,j,c) +let l := c.get_lit i, pl := prop_lit.of_cls_lit l in +modify_watches_for pl $ λw, w.insert n (i,j,c) private meta def remove_watch (n : name) (c : clause) (i : ℕ) : solver unit := -let l := c^.get_lit i, pl := prop_lit.of_cls_lit l in -modify_watches_for pl $ λw, w^.erase n +let l := c.get_lit i, pl := prop_lit.of_cls_lit l in +modify_watches_for pl $ λw, w.erase n private meta def set_watches (n : name) (c : clause) : solver unit := -if c^.num_lits = 0 then - set_conflict c^.proof -else if c^.num_lits = 1 then +if c.num_lits = 0 then + set_conflict c.proof +else if c.num_lits = 1 then unit_propg_cls c else do - not_false_lits ← filter (λi, lit_is_not_false (c^.get_lit i)) (list.range c^.num_lits), + not_false_lits ← filter (λi, lit_is_not_false (c.get_lit i)) (list.range c.num_lits), match not_false_lits with | [] := do add_watch n c 0 1, @@ -289,38 +289,38 @@ remove_watch n c i₂, set_watches n c meta def mk_clause (c : clause) : solver unit := do -c : clause ← c^.distinct, -for c^.get_lits (λl, mk_var l^.formula), +c : clause ← c.distinct, +for c.get_lits (λl, mk_var l.formula), revert_to_decision_level_zero (), -state_t.modify $ λst, { st with clauses := c :: st^.clauses }, +state_t.modify $ λst, { st with clauses := c :: st.clauses }, c_name ← mk_fresh_name, set_watches c_name c meta def unit_propg_var (v : prop_var) : solver unit := -do st ← state_t.read, if st^.conflict^.is_some then return () else -match st^.vars^.find v with -| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v^.to_string -| none := fail $ "unknown variable: " ++ v^.to_string +do st ← state_t.read, if st.conflict.is_some then return () else +match st.vars.find v with +| some ⟨ph, none⟩ := fail $ "propagating unassigned variable: " ++ v.to_string +| none := fail $ "unknown variable: " ++ v.to_string | some ⟨ph, some _⟩ := - let watches := st^.watches_for $ prop_lit.of_var_and_phase v (bnot ph) in - for' watches^.to_list $ λw, update_watches w.1 w.2.2.2 w.2.1 w.2.2.1 + let watches := st.watches_for $ prop_lit.of_var_and_phase v (bnot ph) in + for' watches.to_list $ λw, update_watches w.1 w.2.2.2 w.2.1 w.2.2.1 end meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem → clause | proof (trail_elem.dec v ph hyp :: es) := - let abs_prf := abstract_local proof hyp^.local_uniq_name in + let abs_prf := abstract_local proof hyp.local_uniq_name in if has_var abs_prf then clause.close_const (analyze_conflict' proof es) hyp else analyze_conflict' proof es | proof (trail_elem.propg v ph l_prf hyp :: es) := - let abs_prf := abstract_local proof hyp^.local_uniq_name in + let abs_prf := abstract_local proof hyp.local_uniq_name in if has_var abs_prf then - analyze_conflict' (app (lam hyp^.local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es + analyze_conflict' (app (lam hyp.local_pp_name binder_info.default (formula_of_lit local_false v ph) abs_prf) l_prf) es else analyze_conflict' proof es | proof (trail_elem.dbl_neg_propg v ph l_prf hyp :: es) := - let abs_prf := abstract_local proof hyp^.local_uniq_name in + let abs_prf := abstract_local proof hyp.local_uniq_name in if has_var abs_prf then analyze_conflict' (app l_prf (lambdas [hyp] proof)) es else @@ -328,12 +328,12 @@ meta def analyze_conflict' (local_false : expr) : proof_term → list trail_elem | proof [] := ⟨0, 0, proof, local_false, local_false⟩ meta def analyze_conflict (proof : proof_term) : solver clause := -do st ← state_t.read, return $ analyze_conflict' st^.local_false proof st^.trail +do st ← state_t.read, return $ analyze_conflict' st.local_false proof st.trail meta def add_learned (c : clause) : solver unit := do prf_abbrev_name ← mk_fresh_name, -c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c^.type }, -state_t.modify $ λst, { st with learned := ⟨c', c^.proof⟩ :: st^.learned }, +c' ← return { c with proof := local_const prf_abbrev_name prf_abbrev_name binder_info.default c.type }, +state_t.modify $ λst, { st with learned := ⟨c', c.proof⟩ :: st.learned }, c_name ← mk_fresh_name, set_watches c_name c' @@ -343,7 +343,7 @@ if ¬isf then state_t.modify (λst, { st with conflict := none }) else do removed_elem ← pop_trail_core, - if removed_elem^.is_some then + if removed_elem.is_some then backtrack_with conflict_clause else return () @@ -351,14 +351,14 @@ else do meta def replace_learned_clauses' : proof_term → list learned_clause → proof_term | proof [] := proof | proof (⟨c, actual_proof⟩ :: lcs) := - let abs_prf := abstract_local proof c^.proof^.local_uniq_name in + let abs_prf := abstract_local proof c.proof.local_uniq_name in if has_var abs_prf then - replace_learned_clauses' (elet c^.proof^.local_pp_name c^.type actual_proof abs_prf) lcs + replace_learned_clauses' (elet c.proof.local_pp_name c.type actual_proof abs_prf) lcs else replace_learned_clauses' proof lcs meta def replace_learned_clauses (proof : proof_term) : solver proof_term := -do st ← state_t.read, return $ replace_learned_clauses' proof st^.learned +do st ← state_t.read, return $ replace_learned_clauses' proof st.learned meta inductive result | unsat : proof_term → result @@ -368,8 +368,8 @@ variable theory_solver : solver (option proof_term) meta def unit_propg : unit → solver unit | () := do st ← state_t.read, -if st^.conflict^.is_some then return () else -match st^.unitp_queue with +if st.conflict.is_some then return () else +match st.unitp_queue with | [] := return () | (v::vs) := do state_t.write { st with unitp_queue := vs }, @@ -380,28 +380,28 @@ end private meta def run' : unit → solver result | () := do unit_propg (), st ← state_t.read, -match st^.conflict with +match st.conflict with | some conflict := do conflict_clause ← analyze_conflict conflict, - if conflict_clause^.num_lits = 0 then do - proof ← replace_learned_clauses conflict_clause^.proof, + if conflict_clause.num_lits = 0 then do + proof ← replace_learned_clauses conflict_clause.proof, return (result.unsat proof) else do backtrack_with conflict_clause, add_learned conflict_clause, run' () | none := - match st^.unassigned^.min with + match st.unassigned.min with | none := do theory_conflict ← theory_solver, match theory_conflict with | some conflict := do set_conflict conflict, run' () - | none := return $ result.sat (st^.vars^.map (λvar_st, var_st^.phase)) + | none := return $ result.sat (st.vars.map (λvar_st, var_st.phase)) end | some unassigned := - match st^.vars^.find unassigned with + match st.vars.find unassigned with | some ⟨ph, none⟩ := do add_decision unassigned ph, run' () - | _ := fail $ "unassigned variable is assigned: " ++ unassigned^.to_string + | _ := fail $ "unassigned variable is assigned: " ++ unassigned.to_string end end end @@ -414,11 +414,11 @@ return res.1 meta def theory_solver_of_tactic (th_solver : tactic unit) : cdcl.solver (option cdcl.proof_term) := do s ← state_t.read, ↑do -hyps ← return $ s^.trail^.map (λe, e^.hyp), -subgoal ← mk_meta_var s^.local_false, +hyps ← return $ s.trail.map (λe, e.hyp), +subgoal ← mk_meta_var s.local_false, goals ← get_goals, set_goals [subgoal], -hvs ← for hyps (λhyp, assertv hyp^.local_pp_name hyp^.local_type hyp), +hvs ← for hyps (λhyp, assertv hyp.local_pp_name hyp.local_type hyp), solved ← (do th_solver, now, return tt) <|> return ff, set_goals goals, if solved then do diff --git a/library/tools/super/clause.lean b/library/tools/super/clause.lean index 5ae10b74a0..a718023288 100644 --- a/library/tools/super/clause.lean +++ b/library/tools/super/clause.lean @@ -29,7 +29,7 @@ meta def inst (c : clause) (e : expr) : clause := (if num_quants c > 0 then mk (num_quants c - 1) (num_lits c) else mk 0 (num_lits c - 1)) -(app (proof c) e) (instantiate_var (binding_body (type c)) e) c^.local_false +(app (proof c) e) (instantiate_var (binding_body (type c)) e) c.local_false meta def instn (c : clause) (es : list expr) : clause := foldr (λe c', inst c' e) c es @@ -49,11 +49,11 @@ match e with let abst_type' := abstract_local (type c) (local_uniq_name e) in let type' := pi pp binder_info.default t (abstract_local (type c) uniq) in let abs_prf := abstract_local (proof c) uniq in - let proof' := lambdas [e] c^.proof in + let proof' := lambdas [e] c.proof in if num_quants c > 0 ∨ has_var abst_type' then - { c with num_quants := c^.num_quants + 1, proof := proof', type := type' } + { c with num_quants := c.num_quants + 1, proof := proof', type := type' } else - { c with num_lits := c^.num_lits + 1, proof := proof', type := type' } + { c with num_lits := c.num_lits + 1, proof := proof', type := type' } | _ := ⟨0, 0, default expr, default expr, default expr⟩ end @@ -80,7 +80,7 @@ private meta def parse_clause (local_false : expr) : expr → expr → tactic cl lc_n ← mk_fresh_name, lc ← return $ local_const lc_n n bi d, c ← parse_clause (app proof lc) (instantiate_var b lc), - return $ c^.close_const $ local_const lc_n n binder_info.default d + return $ c.close_const $ local_const lc_n n binder_info.default d | proof ```(not %%formula) := parse_clause proof ```(%%formula → false) | proof type := if type = local_false then do @@ -121,11 +121,11 @@ meta def is_neg : literal → bool | (left _) := tt | (right _) := ff -meta def is_pos (l : literal) : bool := bnot l^.is_neg +meta def is_pos (l : literal) : bool := bnot l.is_neg meta def to_formula (l : literal) : expr := -if l^.is_neg -then app (const ``not []) l^.formula +if l.is_neg +then app (const ``not []) l.formula else formula l meta def type_str : literal → string @@ -134,30 +134,30 @@ meta def type_str : literal → string meta instance : has_to_tactic_format literal := ⟨λl, do -pp_f ← pp l^.formula, -return $ to_fmt l^.type_str ++ " (" ++ pp_f ++ ")"⟩ +pp_f ← pp l.formula, +return $ to_fmt l.type_str ++ " (" ++ pp_f ++ ")"⟩ end literal private meta def get_binding_body : expr → ℕ → expr | e 0 := e -| e (i+1) := get_binding_body e^.binding_body i +| e (i+1) := get_binding_body e.binding_body i meta def get_binder (e : expr) (i : nat) := binding_domain (get_binding_body e i) meta def validate (c : clause) : tactic unit := do -concl ← return $ get_binding_body c^.type c^.num_binders, -unify concl c^.local_false - <|> (do pp_concl ← pp concl, pp_lf ← pp c^.local_false, +concl ← return $ get_binding_body c.type c.num_binders, +unify concl c.local_false + <|> (do pp_concl ← pp concl, pp_lf ← pp c.local_false, fail $ to_fmt "wrong local false: " ++ pp_concl ++ " =!= " ++ pp_lf), -type' ← infer_type c^.proof, -unify c^.type type' <|> (do pp_ty ← pp c^.type, pp_ty' ← pp type', +type' ← infer_type c.proof, +unify c.type type' <|> (do pp_ty ← pp c.type, pp_ty' ← pp type', fail (to_fmt "wrong type: " ++ pp_ty ++ " =!= " ++ pp_ty')) meta def get_lit (c : clause) (i : nat) : literal := let bind := get_binder (type c) (num_quants c + i) in -match is_local_not c^.local_false bind with +match is_local_not c.local_false bind with | some formula := literal.right formula | none := literal.left bind end @@ -166,16 +166,16 @@ meta def lits_where (c : clause) (p : literal → bool) : list nat := list.filter (λl, p (get_lit c l)) (range (num_lits c)) meta def get_lits (c : clause) : list literal := -list.map (get_lit c) (range c^.num_lits) +list.map (get_lit c) (range c.num_lits) private meta def tactic_format (c : clause) : tactic format := do -c ← c^.open_metan c^.num_quants, -pp (do l ← c.1^.get_lits, [l^.to_formula]) +c ← c.open_metan c.num_quants, +pp (do l ← c.1.get_lits, [l.to_formula]) meta instance : has_to_tactic_format clause := ⟨tactic_format⟩ meta def is_maximal (gt : expr → expr → bool) (c : clause) (i : nat) : bool := -list.empty (list.filter (λj, gt (get_lit c j)^.formula (get_lit c i)^.formula) (range c^.num_lits)) +list.empty (list.filter (λj, gt (get_lit c j).formula (get_lit c i).formula) (range c.num_lits)) meta def normalize (c : clause) : tactic clause := do opened ← open_constn c (num_binders c), @@ -190,9 +190,9 @@ meta def whnf_head_lit (c : clause) : tactic clause := do atom' ← whnf $ literal.formula $ get_lit c 0, return $ if literal.is_neg (get_lit c 0) then - { c with type := ```(%%atom' → %%(binding_body c^.type)) } + { c with type := ```(%%atom' → %%(binding_body c.type)) } else - { c with type := ```(not %%atom' → %%(c^.type^.binding_body)) } + { c with type := ```(not %%atom' → %%(c.type.binding_body)) } end clause @@ -209,7 +209,7 @@ inst_exprs ← mapm instantiate_mvars exprs_with_metas, metas ← return $ inst_exprs >>= get_metas, match list.filter (λm, ¬has_meta_var (get_meta_type m)) metas with | [] := - if metas^.empty then + if metas.empty then return [] else do for' metas (λm, do trace (expr.to_string m), t ← infer_type m, trace (expr.to_string t)), @@ -233,16 +233,16 @@ clause.inst_mvars $ clause.close_constn qf' bs private meta def distinct' (local_false : expr) : list expr → expr → clause | [] proof := ⟨ 0, 0, proof, local_false, local_false ⟩ | (h::hs) proof := - let (dups, rest) := partition (λh' : expr, h^.local_type = h'^.local_type) hs, + let (dups, rest) := partition (λh' : expr, h.local_type = h'.local_type) hs, proof_wo_dups := foldl (λproof (h' : expr), - instantiate_var (abstract_local proof h'^.local_uniq_name) h) + instantiate_var (abstract_local proof h'.local_uniq_name) h) proof dups in - (distinct' rest proof_wo_dups)^.close_const h + (distinct' rest proof_wo_dups).close_const h meta def distinct (c : clause) : tactic clause := do -(qf, vs) ← c^.open_constn c^.num_quants, -(fls, hs) ← qf^.open_constn qf^.num_lits, -return $ (distinct' c^.local_false hs fls^.proof)^.close_constn vs +(qf, vs) ← c.open_constn c.num_quants, +(fls, hs) ← qf.open_constn qf.num_lits, +return $ (distinct' c.local_false hs fls.proof).close_constn vs end clause diff --git a/library/tools/super/clause_ops.lean b/library/tools/super/clause_ops.lean index 21a5182554..6f42e1742d 100644 --- a/library/tools/super/clause_ops.lean +++ b/library/tools/super/clause_ops.lean @@ -14,61 +14,61 @@ meta def on_left_at {m} [monad m] (c : clause) (i : ℕ) [has_monad_lift_t tactic m] -- f gets a type and returns a list of proofs of that type (f : expr → m (list (list expr × expr))) : m (list clause) := do -op ← c^.open_constn (c^.num_quants + i), -@guard tactic _ (op.1^.get_lit 0)^.is_neg _, -new_hyps ← f (op.1^.get_lit 0)^.formula, -return $ new_hyps^.map (λnew_hyp, - (op.1^.inst new_hyp.2)^.close_constn (op.2 ++ new_hyp.1)) +op ← c.open_constn (c.num_quants + i), +@guard tactic _ (op.1.get_lit 0).is_neg _, +new_hyps ← f (op.1.get_lit 0).formula, +return $ new_hyps.map (λnew_hyp, + (op.1.inst new_hyp.2).close_constn (op.2 ++ new_hyp.1)) meta def on_left_at_dn {m} [monad m] [alternative m] (c : clause) (i : ℕ) [has_monad_lift_t tactic m] -- f gets a hypothesis of ¬type and returns a list of proofs of false (f : expr → m (list (list expr × expr))) : m (list clause) := do -qf ← c^.open_constn c^.num_quants, -op ← qf.1^.open_constn c^.num_lits, -lci ← (op.2^.nth i)^.to_monad, -@guard tactic _ (qf.1^.get_lit i)^.is_neg _, -h ← mk_local_def `h $ imp (qf.1^.get_lit i)^.formula c^.local_false, +qf ← c.open_constn c.num_quants, +op ← qf.1.open_constn c.num_lits, +lci ← (op.2.nth i).to_monad, +@guard tactic _ (qf.1.get_lit i).is_neg _, +h ← mk_local_def `h $ imp (qf.1.get_lit i).formula c.local_false, new_hyps ← f h, -return $ new_hyps^.map $ λnew_hyp, - (((clause.mk 0 0 new_hyp.2 c^.local_false c^.local_false)^.close_const h)^.inst - (op.1^.close_const lci)^.proof)^.close_constn - (qf.2 ++ op.2^.remove_nth i ++ new_hyp.1) +return $ new_hyps.map $ λnew_hyp, + (((clause.mk 0 0 new_hyp.2 c.local_false c.local_false).close_const h).inst + (op.1.close_const lci).proof).close_constn + (qf.2 ++ op.2.remove_nth i ++ new_hyp.1) meta def on_right_at {m} [monad m] (c : clause) (i : ℕ) [has_monad_lift_t tactic m] -- f gets a hypothesis and returns a list of proofs of false (f : expr → m (list (list expr × expr))) : m (list clause) := do -op ← c^.open_constn (c^.num_quants + i), -@guard tactic _ ((op.1^.get_lit 0)^.is_pos) _, -h ← mk_local_def `h (op.1^.get_lit 0)^.formula, +op ← c.open_constn (c.num_quants + i), +@guard tactic _ ((op.1.get_lit 0).is_pos) _, +h ← mk_local_def `h (op.1.get_lit 0).formula, new_hyps ← f h, -return $ new_hyps^.map (λnew_hyp, - (op.1^.inst (lambdas [h] new_hyp.2))^.close_constn (op.2 ++ new_hyp.1)) +return $ new_hyps.map (λnew_hyp, + (op.1.inst (lambdas [h] new_hyp.2)).close_constn (op.2 ++ new_hyp.1)) meta def on_right_at' {m} [monad m] (c : clause) (i : ℕ) [has_monad_lift_t tactic m] -- f gets a hypothesis and returns a list of proofs (f : expr → m (list (list expr × expr))) : m (list clause) := do -op ← c^.open_constn (c^.num_quants + i), -@guard tactic _ ((op.1^.get_lit 0)^.is_pos) _, -h ← mk_local_def `h (op.1^.get_lit 0)^.formula, +op ← c.open_constn (c.num_quants + i), +@guard tactic _ ((op.1.get_lit 0).is_pos) _, +h ← mk_local_def `h (op.1.get_lit 0).formula, new_hyps ← f h, for new_hyps (λnew_hyp, do type ← infer_type new_hyp.2, - nh ← mk_local_def `nh $ imp type c^.local_false, - return $ (op.1^.inst (lambdas [h] (app nh new_hyp.2)))^.close_constn (op.2 ++ new_hyp.1 ++ [nh])) + nh ← mk_local_def `nh $ imp type c.local_false, + return $ (op.1.inst (lambdas [h] (app nh new_hyp.2))).close_constn (op.2 ++ new_hyp.1 ++ [nh])) meta def on_first_right (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, [on_right_at c i f] +first $ do i ← list.range c.num_lits, [on_right_at c i f] meta def on_first_right' (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, [on_right_at' c i f] +first $ do i ← list.range c.num_lits, [on_right_at' c i f] meta def on_first_left (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, [on_left_at c i f] +first $ do i ← list.range c.num_lits, [on_left_at c i f] meta def on_first_left_dn (c : clause) (f : expr → tactic (list (list expr × expr))) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, [on_left_at_dn c i f] +first $ do i ← list.range c.num_lits, [on_left_at_dn c i f] end super diff --git a/library/tools/super/clausifier.lean b/library/tools/super/clausifier.lean index 770fce9604..2182561171 100644 --- a/library/tools/super/clausifier.lean +++ b/library/tools/super/clausifier.lean @@ -16,8 +16,8 @@ lift some tac <|> return none private meta def normalize : expr → tactic expr | e := do e' ← whnf e reducible, -args' ← monad.for e'^.get_app_args normalize, -return $ app_of_list e'^.get_app_fn args' +args' ← monad.for e'.get_app_args normalize, +return $ app_of_list e'.get_app_fn args' meta def inf_normalize_l (c : clause) : tactic (list clause) := on_first_left c $ λtype, do @@ -28,24 +28,24 @@ on_first_left c $ λtype, do meta def inf_normalize_r (c : clause) : tactic (list clause) := on_first_right c $ λha, do - a' ← normalize ha^.local_type, - guard $ a' ≠ ha^.local_type, - hna ← mk_local_def `hna (imp a' c^.local_false), + a' ← normalize ha.local_type, + guard $ a' ≠ ha.local_type, + hna ← mk_local_def `hna (imp a' c.local_false), return [([hna], app hna ha)] meta def inf_false_l (c : clause) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, - if c^.get_lit i = clause.literal.left ```(false) +first $ do i ← list.range c.num_lits, + if c.get_lit i = clause.literal.left ```(false) then [return []] else [] meta def inf_false_r (c : clause) : tactic (list clause) := on_first_right c $ λhf, - if hf^.local_type = c^.local_false + if hf.local_type = c.local_false then return [([], hf)] - else match hf^.local_type with + else match hf.local_type with | const ``false [] := do - pr ← mk_app ``false.rec [c^.local_false, hf], + pr ← mk_app ``false.rec [c.local_false, hf], return [([], pr)] | _ := failed end @@ -58,8 +58,8 @@ on_first_left c $ λt, end meta def inf_true_r (c : clause) : tactic (list clause) := -first $ do i ← list.range c^.num_lits, - if c^.get_lit i = clause.literal.right (const ``true []) +first $ do i ← list.range c.num_lits, + if c.get_lit i = clause.literal.right (const ``true []) then [return []] else [] @@ -74,9 +74,9 @@ on_first_left c $ λtype, meta def inf_not_r (c : clause) : tactic (list clause) := on_first_right c $ λhna, - match hna^.local_type with + match hna.local_type with | app (const ``not []) a := do - hnna ← mk_local_def `h ```((%%a → false) → %%c^.local_false), + hnna ← mk_local_def `h ```((%%a → false) → %%c.local_false), return [([hnna], app hnna hna)] | _ := failed end @@ -117,11 +117,11 @@ on_first_right' c $ λhyp, do meta def inf_or_r (c : clause) : tactic (list clause) := on_first_right c $ λhab, - match hab^.local_type with + match hab.local_type with | (app (app (const ``or []) a) b) := do - hna ← mk_local_def `l (imp a c^.local_false), - hnb ← mk_local_def `r (imp b c^.local_false), - proof ← mk_app ``or.elim [a, b, c^.local_false, hab, hna, hnb], + hna ← mk_local_def `l (imp a c.local_false), + hnb ← mk_local_def `r (imp b c.local_false), + proof ← mk_app ``or.elim [a, b, c.local_false, hab, hna, hnb], return [([hna, hnb], proof)] | _ := failed end @@ -140,7 +140,7 @@ on_first_left c $ λab, meta def inf_all_r (c : clause) : tactic (list clause) := on_first_right' c $ λhallb, - match hallb^.local_type with + match hallb.local_type with | (pi n bi a b) := do ha ← mk_local_def `x a, return [([ha], app hallb ha)] @@ -164,10 +164,10 @@ lemma imp_l_c {F : Prop} {a b} : ((a → b) → F) → ((a → F) → F) := meta def inf_imp_l (c : clause) : tactic (list clause) := on_first_left_dn c $ λhnab, - match hnab^.local_type with + match hnab.local_type with | (pi _ _ (pi _ _ a b) _) := - if b^.has_var then failed else do - hna ← mk_local_def `na (imp a c^.local_false), + if b.has_var then failed else do + hna ← mk_local_def `na (imp a c.local_false), pf ← first (do r ← [``super.imp_l, ``super.imp_l', ``super.imp_l_c], [mk_app r [hnab, hna]]), hb ← mk_local_def `b b, @@ -198,26 +198,26 @@ assume hab hnenb, meta def inf_all_l (c : clause) : tactic (list clause) := on_first_left_dn c $ λhnallb, - match hnallb^.local_type with + match hnallb.local_type with | pi _ _ (pi n bi a b) _ := do - enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c^.local_false)], - hnenb ← mk_local_def `h (imp enb c^.local_false), + enb ← mk_mapp ``Exists [none, some $ lam n binder_info.default a (imp b c.local_false)], + hnenb ← mk_local_def `h (imp enb c.local_false), pr ← mk_app ``super.demorgan' [hnallb, hnenb], return [([hnenb], pr)] | _ := failed end meta def inf_ex_r (c : clause) : tactic (list clause) := do -(qf, ctx) ← c^.open_constn c^.num_quants, +(qf, ctx) ← c.open_constn c.num_quants, skolemized ← on_first_right' qf $ λhexp, - match hexp^.local_type with + match hexp.local_type with | (app (app (const ``Exists [_]) d) p) := do sk_sym_name_pp ← get_unused_name `sk (some 1), inh_lc ← mk_local' `w binder_info.implicit d, sk_sym ← mk_local_def sk_sym_name_pp (pis (ctx ++ [inh_lc]) d), sk_p ← whnf_no_delta $ app p (app_of_list sk_sym (ctx ++ [inh_lc])), sk_ax ← mk_mapp ``Exists [some (local_type sk_sym), - some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp^.local_type sk_p)))], + some (lambdas [sk_sym] (pis (ctx ++ [inh_lc]) (imp hexp.local_type sk_p)))], sk_ax_name ← get_unused_name `sk_axiom (some 1), assert sk_ax_name sk_ax, nonempt_of_inh ← mk_mapp ``nonempty.intro [some d, some inh_lc], eps ← mk_mapp ``classical.epsilon [some d, some nonempt_of_inh, some p], @@ -229,7 +229,7 @@ skolemized ← on_first_right' qf $ λhexp, return [([inh_lc], app_of_list sk_ax' (ctx ++ [inh_lc, hexp]))] | _ := failed end, -return $ skolemized^.map (λs, s^.close_constn ctx) +return $ skolemized.map (λs, s.close_constn ctx) meta def first_some {a : Type} : list (tactic (option a)) → tactic (option a) | [] := return none @@ -239,7 +239,7 @@ private meta def get_clauses_core' (rules : list (clause → tactic (list clause : list clause → tactic (list clause) | cs := lift list.join $ do for cs $ λc, do first $ -rules^.map (λr, r c >>= get_clauses_core') ++ [return [c]] +rules.map (λr, r c >>= get_clauses_core') ++ [return [c]] meta def get_clauses_core (rules : list (clause → tactic (list clause))) (initial : list clause) : tactic (list clause) := do @@ -274,7 +274,7 @@ get_clauses_core clausification_rules_intuit meta def as_refutation : tactic unit := do repeat (do intro1, skip), tgt ← target, -if tgt^.is_constant || tgt^.is_local_constant then skip else do +if tgt.is_constant || tgt.is_local_constant then skip else do local_false_name ← get_unused_name `F none, tgt_type ← infer_type tgt, definev local_false_name tgt_type tgt, local_false ← get_local local_false_name, target_name ← get_unused_name `target none, @@ -287,20 +287,20 @@ l ← local_context, monad.for l (clause.of_proof local_false) meta def clausify_pre := preprocessing_rule $ take new, lift list.join $ for new $ λ dc, do -cs ← get_clauses_classical [dc^.c], -if cs^.length ≤ 1 then +cs ← get_clauses_classical [dc.c], +if cs.length ≤ 1 then return (for cs $ λ c, { dc with c := c }) else - for cs (λc, mk_derived c dc^.sc) + for cs (λc, mk_derived c dc.sc) -- @[super.inf] meta def clausification_inf : inf_decl := inf_decl.mk 0 $ λgiven, list.foldr orelse (return ()) $ do r ← clausification_rules_classical, - [do cs ← r given^.c, + [do cs ← r given.c, cs' ← get_clauses_classical cs, - for' cs' (λc, mk_derived c given^.sc^.sched_now >>= add_inferred), - remove_redundant given^.id []] + for' cs' (λc, mk_derived c given.sc.sched_now >>= add_inferred), + remove_redundant given.id []] end super diff --git a/library/tools/super/datatypes.lean b/library/tools/super/datatypes.lean index a30e44bfd3..0d5e215061 100644 --- a/library/tools/super/datatypes.lean +++ b/library/tools/super/datatypes.lean @@ -11,12 +11,12 @@ namespace super meta def has_diff_constr_eq_l (c : clause) : tactic bool := do env ← get_env, return $ list.bor $ do - l ← c^.get_lits, - guard l^.is_neg, - return $ match is_eq l^.formula with + l ← c.get_lits, + guard l.is_neg, + return $ match is_eq l.formula with | some (lhs, rhs) := - if env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs ∧ - lhs^.get_app_fn^.const_name ≠ rhs^.get_app_fn^.const_name then + if env.is_constructor_app lhs ∧ env.is_constructor_app rhs ∧ + lhs.get_app_fn.const_name ≠ rhs.get_app_fn.const_name then tt else ff @@ -24,16 +24,16 @@ return $ list.bor $ do end meta def diff_constr_eq_l_pre := preprocessing_rule $ -filter (λc, lift bnot $ has_diff_constr_eq_l c^.c) +filter (λc, lift bnot $ has_diff_constr_eq_l c.c) meta def try_no_confusion_eq_r (c : clause) (i : ℕ) : tactic (list clause) := on_right_at' c i $ λhyp, - match is_eq hyp^.local_type with + match is_eq hyp.local_type with | some (lhs, rhs) := do env ← get_env, lhs ← whnf lhs, rhs ← whnf rhs, - guard $ env^.is_constructor_app lhs ∧ env^.is_constructor_app rhs, - pr ← mk_app (lhs^.get_app_fn^.const_name^.get_prefix <.> "no_confusion") [```(false), lhs, rhs, hyp], + guard $ env.is_constructor_app lhs ∧ env.is_constructor_app rhs, + pr ← mk_app (lhs.get_app_fn.const_name.get_prefix <.> "no_confusion") [```(false), lhs, rhs, hyp], -- FIXME: change to local false ^^ ty ← infer_type pr, ty ← whnf ty, pr ← to_expr ``(@eq.mpr _ %%ty rfl %%pr), -- FIXME @@ -43,6 +43,6 @@ on_right_at' c i $ λhyp, @[super.inf] meta def datatype_infs : inf_decl := inf_decl.mk 10 $ take given, do -sequence' (do i ← list.range given^.c^.num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given^.c i]) +sequence' (do i ← list.range given.c.num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given.c i]) end super diff --git a/library/tools/super/defs.lean b/library/tools/super/defs.lean index 30d7e43c83..5363b9f3a1 100644 --- a/library/tools/super/defs.lean +++ b/library/tools/super/defs.lean @@ -19,8 +19,8 @@ on_left_at c i $ λt, do meta def try_unfold_def_right (c : clause) (i : ℕ) : tactic (list clause) := on_right_at c i $ λh, do - t' ← try_unfold_one_def h^.local_type, - hnt' ← mk_local_def `h (imp t' c^.local_false), + t' ← try_unfold_one_def h.local_type, + hnt' ← mk_local_def `h (imp t' c.local_false), return [([hnt'], app hnt' h)] @[super.inf] @@ -28,7 +28,7 @@ meta def unfold_def_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ d r ← [try_unfold_def_right, try_unfold_def_left], -- NOTE: we cannot restrict to selected literals here -- as this might prevent factoring, e.g. _n>0_ ∨ is_pos(0) -i ← list.range given^.c^.num_lits, -[inf_if_successful 3 given (r given^.c i)] +i ← list.range given.c.num_lits, +[inf_if_successful 3 given (r given.c i)] end super diff --git a/library/tools/super/demod.lean b/library/tools/super/demod.lean index 4d5f412507..1c8778392b 100644 --- a/library/tools/super/demod.lean +++ b/library/tools/super/demod.lean @@ -9,8 +9,8 @@ open tactic monad expr namespace super meta def is_demodulator (c : clause) : bool := -match c^.get_lits with -| [clause.literal.right eqn] := eqn^.is_eq^.is_some +match c.get_lits with +| [clause.literal.right eqn] := eqn.is_eq.is_some | _ := ff end @@ -18,41 +18,41 @@ variable gt : expr → expr → bool meta def demod' (cs1 : list derived_clause) : clause → list derived_clause → tactic (list derived_clause × clause) | c2 used_demods := (first $ do - i ← list.range c2^.num_lits, + i ← list.range c2.num_lits, pos ← rwr_positions c2 i, c1 ← cs1, (ltr, congr_ax) ← [(tt, ``super.sup_ltr), (ff, ``super.sup_rtl)], - [do c2' ← try_sup gt c1^.c c2 0 i pos ltr tt congr_ax, + [do c2' ← try_sup gt c1.c c2 0 i pos ltr tt congr_ax, demod' c2' (c1 :: used_demods)] ) <|> return (used_demods, c2) meta def demod (cs1 : list derived_clause) (c2 : clause) : tactic (list derived_clause × clause) := do -c2qf ← c2^.open_constn c2^.num_quants, +c2qf ← c2.open_constn c2.num_quants, (used_demods, c2qf') ← demod' gt cs1 c2qf.1 [], -if used_demods^.empty then return ([], c2) else -return (used_demods, c2qf'^.close_constn c2qf.2) +if used_demods.empty then return ([], c2) else +return (used_demods, c2qf'.close_constn c2qf.2) meta def demod_fwd_inf : inference := take given, do active ← get_active, -demods ← return (do ac ← active^.values, guard $ is_demodulator ac^.c, guard $ ac^.id ≠ given^.id, [ac]), -if demods^.empty then skip else do -(used_demods, given') ← demod gt demods given^.c, -if used_demods^.empty then skip else do -remove_redundant given^.id used_demods, -mk_derived given' given^.sc^.sched_now >>= add_inferred +demods ← return (do ac ← active.values, guard $ is_demodulator ac.c, guard $ ac.id ≠ given.id, [ac]), +if demods.empty then skip else do +(used_demods, given') ← demod gt demods given.c, +if used_demods.empty then skip else do +remove_redundant given.id used_demods, +mk_derived given' given.sc.sched_now >>= add_inferred meta def demod_back1 (given active : derived_clause) : prover unit := do -(used_demods, c') ← demod gt [given] active^.c, -if used_demods^.empty then skip else do -remove_redundant active^.id used_demods, -mk_derived c' active^.sc^.sched_now >>= add_inferred +(used_demods, c') ← demod gt [given] active.c, +if used_demods.empty then skip else do +remove_redundant active.id used_demods, +mk_derived c' active.sc.sched_now >>= add_inferred meta def demod_back_inf : inference := -take given, if ¬is_demodulator given^.c then skip else +take given, if ¬is_demodulator given.c then skip else do active ← get_active, sequence' $ do -ac ← active^.values, -guard $ ac^.id ≠ given^.id, +ac ← active.values, +guard $ ac.id ≠ given.id, [demod_back1 gt given ac] @[super.inf] diff --git a/library/tools/super/equality.lean b/library/tools/super/equality.lean index 554d282b67..f93fe50466 100644 --- a/library/tools/super/equality.lean +++ b/library/tools/super/equality.lean @@ -10,8 +10,8 @@ namespace super meta def try_unify_eq_l (c : clause) (i : nat) : tactic clause := do guard $ clause.literal.is_neg (clause.get_lit c i), -qf ← clause.open_metan c c^.num_quants, -match is_eq (qf.1^.get_lit i)^.formula with +qf ← clause.open_metan c c.num_quants, +match is_eq (qf.1.get_lit i).formula with | none := failed | some (lhs, rhs) := do unify lhs rhs, @@ -19,24 +19,24 @@ ty ← infer_type lhs, univ ← infer_univ ty, refl ← return $ app_of_list (const ``eq.refl [univ]) [ty, lhs], opened ← clause.open_constn qf.1 i, -clause.meta_closure qf.2 $ clause.close_constn (opened.1^.inst refl) opened.2 +clause.meta_closure qf.2 $ clause.close_constn (opened.1.inst refl) opened.2 end @[super.inf] meta def unify_eq_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do -i ← given^.selected, -[inf_if_successful 0 given (do u ← try_unify_eq_l given^.c i, return [u])] +i ← given.selected, +[inf_if_successful 0 given (do u ← try_unify_eq_l given.c i, return [u])] meta def has_refl_r (c : clause) : bool := list.bor $ do -literal ← c^.get_lits, -guard literal^.is_pos, -match is_eq literal^.formula with +literal ← c.get_lits, +guard literal.is_pos, +match is_eq literal.formula with | some (lhs, rhs) := [decidable.to_bool (lhs = rhs)] | none := [] end meta def refl_r_pre : prover unit := -preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c^.c) new +preprocessing_rule $ take new, return $ filter (λc, ¬has_refl_r c.c) new end super diff --git a/library/tools/super/factoring.lean b/library/tools/super/factoring.lean index ec7b1df1dd..7a66b96253 100644 --- a/library/tools/super/factoring.lean +++ b/library/tools/super/factoring.lean @@ -16,14 +16,14 @@ return $ clause.close_constn (clause.inst opened.1 e) opened.2 private meta def try_factor' (c : clause) (i j : nat) : tactic clause := do -- instantiate universal quantifiers using meta-variables -(qf, mvars) ← c^.open_metan c^.num_quants, +(qf, mvars) ← c.open_metan c.num_quants, -- unify the two literals -unify_lit (qf^.get_lit i) (qf^.get_lit j), +unify_lit (qf.get_lit i) (qf.get_lit j), -- check maximality condition -qfi ← qf^.inst_mvars, guard $ clause.is_maximal gt qfi i, +qfi ← qf.inst_mvars, guard $ clause.is_maximal gt qfi i, -- construct proof -(at_j, cs) ← qf^.open_constn j, hyp_i ← cs^.nth i, -let qf' := (at_j^.inst hyp_i)^.close_constn cs, +(at_j, cs) ← qf.open_constn j, hyp_i ← cs.nth i, +let qf' := (at_j.inst hyp_i).close_constn cs, -- instantiate meta-variables and replace remaining meta-variables by quantifiers clause.meta_closure mvars qf' @@ -31,25 +31,25 @@ meta def try_factor (c : clause) (i j : nat) : tactic clause := if i > j then try_factor' gt c j i else try_factor' gt c i j meta def try_infer_factor (c : derived_clause) (i j : nat) : prover unit := do -f ← try_factor gt c^.c i j, -ss ← does_subsume f c^.c, +f ← try_factor gt c.c i j, +ss ← does_subsume f c.c, if ss then do - f ← mk_derived f c^.sc^.sched_now, + f ← mk_derived f c.sc.sched_now, add_inferred f, - remove_redundant c^.id [f] + remove_redundant c.id [f] else do - inf_score 1 [c^.sc] >>= mk_derived f >>= add_inferred + inf_score 1 [c.sc] >>= mk_derived f >>= add_inferred @[super.inf] meta def factor_inf : inf_decl := inf_decl.mk 40 $ take given, do gt ← get_term_order, sequence' $ do - i ← given^.selected, - j ← list.range given^.c^.num_lits, + i ← given.selected, + j ← list.range given.c.num_lits, return $ try_infer_factor gt given i j <|> return () meta def factor_dup_lits_pre := preprocessing_rule $ take new, do for new $ λdc, do - dist ← dc^.c^.distinct, + dist ← dc.c.distinct, return { dc with c := dist } end super diff --git a/library/tools/super/inhabited.lean b/library/tools/super/inhabited.lean index 6a9af2fef9..4cb2346ef1 100644 --- a/library/tools/super/inhabited.lean +++ b/library/tools/super/inhabited.lean @@ -15,15 +15,15 @@ on_first_left c $ λtype, do meta def try_nonempty_lookup_left (c : clause) : tactic (list clause) := on_first_left_dn c $ λhnx, - match is_local_not c^.local_false hnx^.local_type with + match is_local_not c.local_false hnx.local_type with | some type := do univ ← infer_univ type, - lf_univ ← infer_univ c^.local_false, + lf_univ ← infer_univ c.local_false, guard $ lf_univ = level.zero, inst ← mk_instance (app (const ``nonempty [univ]) type), instt ← infer_type inst, return [([], app_of_list (const ``nonempty.elim [univ]) - [type, c^.local_false, inst, hnx])] + [type, c.local_false, inst, hnx])] | _ := failed end @@ -38,13 +38,13 @@ on_first_left c $ λprop, meta def try_nonempty_right (c : clause) : tactic (list clause) := on_first_right c $ λhnonempty, - match hnonempty^.local_type with + match hnonempty.local_type with | (app (const ``nonempty [u]) type) := do - lf_univ ← infer_univ c^.local_false, + lf_univ ← infer_univ c.local_false, guard $ lf_univ = level.zero, - hnx ← mk_local_def `nx (imp type c^.local_false), + hnx ← mk_local_def `nx (imp type c.local_false), return [([hnx], app_of_list (const ``nonempty.elim [u]) - [type, c^.local_false, hnonempty, hnx])] + [type, c.local_false, hnonempty, hnx])] | _ := failed end @@ -59,7 +59,7 @@ on_first_left c $ λprop, meta def try_inhabited_right (c : clause) : tactic (list clause) := on_first_right' c $ λhinh, - match hinh^.local_type with + match hinh.local_type with | (app (const ``inhabited [u]) type) := return [([], app_of_list (const ``inhabited.default [u]) [type, hinh])] | _ := failed @@ -71,6 +71,6 @@ for' [try_assumption_lookup_left, try_nonempty_lookup_left, try_nonempty_left, try_nonempty_right, try_inhabited_left, try_inhabited_right] $ λr, - simp_if_successful given (r given^.c) + simp_if_successful given (r given.c) end super diff --git a/library/tools/super/lpo.lean b/library/tools/super/lpo.lean index 544d591369..b36c76f73e 100644 --- a/library/tools/super/lpo.lean +++ b/library/tools/super/lpo.lean @@ -34,8 +34,8 @@ else if get_app_fn s = get_app_fn t then lex_ma lpo s t (get_app_args s) (get_ap else alpha lpo (get_app_args s) t meta def prec_gt_of_name_list (ns : list name) : expr → expr → bool := -let nis := rb_map.of_list ns^.zip_with_index in -λs t, match (nis^.find (name_of_funsym s), nis^.find (name_of_funsym t)) with +let nis := rb_map.of_list ns.zip_with_index in +λs t, match (nis.find (name_of_funsym s), nis.find (name_of_funsym t)) with | (some si, some ti) := si > ti | _ := ff end diff --git a/library/tools/super/misc_preprocessing.lean b/library/tools/super/misc_preprocessing.lean index 7ad7397272..176f276ed7 100644 --- a/library/tools/super/misc_preprocessing.lean +++ b/library/tools/super/misc_preprocessing.lean @@ -9,20 +9,20 @@ open expr list monad namespace super meta def is_taut (c : clause) : tactic bool := do -qf ← c^.open_constn c^.num_quants, +qf ← c.open_constn c.num_quants, return $ list.bor $ do - l1 ← qf^.1^.get_lits, guard l1^.is_neg, - l2 ← qf^.1^.get_lits, guard l2^.is_pos, - [decidable.to_bool $ l1^.formula = l2^.formula] + l1 ← qf.1.get_lits, guard l1.is_neg, + l2 ← qf.1.get_lits, guard l2.is_pos, + [decidable.to_bool $ l1.formula = l2.formula] meta def tautology_removal_pre : prover unit := -preprocessing_rule $ λnew, filter (λc, lift bnot $ is_taut c^.c) new +preprocessing_rule $ λnew, filter (λc, lift bnot $ is_taut c.c) new meta def remove_duplicates : list derived_clause → list derived_clause | [] := [] | (c :: cs) := - let (same_type, other_type) := partition (λc' : derived_clause, c'^.c^.type = c^.c^.type) cs in - { c with sc := foldl score.min c^.sc (same_type^.map $ λc, c^.sc) } :: remove_duplicates other_type + let (same_type, other_type) := partition (λc' : derived_clause, c'.c.type = c.c.type) cs in + { c with sc := foldl score.min c.sc (same_type.map $ λc, c.sc) } :: remove_duplicates other_type meta def remove_duplicates_pre : prover unit := preprocessing_rule $ λnew, @@ -30,6 +30,6 @@ return $ remove_duplicates new meta def clause_normalize_pre : prover unit := preprocessing_rule $ λnew, for new $ λdc, -do c' ← dc^.c^.normalize, return { dc with c := c' } +do c' ← dc.c.normalize, return { dc with c := c' } end super diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean index ccdc899bb8..2213e7a248 100644 --- a/library/tools/super/prover.lean +++ b/library/tools/super/prover.lean @@ -45,16 +45,16 @@ meta def run_prover_loop sequence' preprocessing_rules, new ← take_newly_derived, for' new register_as_passive, when (is_trace_enabled_for `super) $ for' new $ λn, - tactic.trace { n with c := { (n^.c) with proof := const (mk_simple_name "derived") [] } }, -needs_sat_run ← flip monad.lift state_t.read (λst, st^.needs_sat_run), + tactic.trace { n with c := { (n.c) with proof := const (mk_simple_name "derived") [] } }, +needs_sat_run ← flip monad.lift state_t.read (λst, st.needs_sat_run), if needs_sat_run then do res ← do_sat_run, match res with | some proof := return (some proof) | none := do - model ← flip monad.lift state_t.read (λst, st^.current_model), + model ← flip monad.lift state_t.read (λst, st.current_model), when (is_trace_enabled_for `super) (do - pp_model ← pp (model^.to_list^.map (λlit, if lit.2 = tt then lit.1 else ```(not %%lit.1))), + pp_model ← pp (model.to_list.map (λlit, if lit.2 = tt then lit.1 else ```(not %%lit.1))), trace $ to_fmt "sat model: " ++ pp_model), run_prover_loop i end @@ -115,7 +115,7 @@ open interactive.types meta def with_lemmas (ls : parse $ many ident) : tactic unit := monad.for' ls $ λl, do p ← mk_const l, t ← infer_type p, -n ← get_unused_name p^.get_app_fn^.const_name none, +n ← get_unused_name p.get_app_fn.const_name none, tactic.assertv n t p meta def super (extra_clause_names : parse $ many ident) diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean index 03b5e91d78..2cc19a84ed 100644 --- a/library/tools/super/prover_state.lean +++ b/library/tools/super/prover_state.lean @@ -22,27 +22,27 @@ def prio.never : ℕ := 2 def sched_default (sc : score) : score := { sc with priority := prio.default } def sched_now (sc : score) : score := { sc with priority := prio.immediate } -def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc^.cost + n } +def inc_cost (sc : score) (n : ℕ) : score := { sc with cost := sc.cost + n } def min (a b : score) : score := -{ priority := nat.min a^.priority b^.priority, - in_sos := a^.in_sos && b^.in_sos, - cost := nat.min a^.cost b^.cost, - age := nat.min a^.age b^.age } +{ priority := nat.min a.priority b.priority, + in_sos := a.in_sos && b.in_sos, + cost := nat.min a.cost b.cost, + age := nat.min a.age b.age } def combine (a b : score) : score := -{ priority := nat.max a^.priority b^.priority, - in_sos := a^.in_sos && b^.in_sos, - cost := a^.cost + b^.cost, - age := nat.max a^.age b^.age } +{ priority := nat.max a.priority b.priority, + in_sos := a.in_sos && b.in_sos, + cost := a.cost + b.cost, + age := nat.max a.age b.age } end score namespace score meta instance : has_to_string score := -⟨λe, "[" ++ to_string e^.priority ++ - "," ++ to_string e^.cost ++ - "," ++ to_string e^.age ++ - ",sos=" ++ to_string e^.in_sos ++ "]"⟩ +⟨λe, "[" ++ to_string e.priority ++ + "," ++ to_string e.cost ++ + "," ++ to_string e.age ++ + ",sos=" ++ to_string e.in_sos ++ "]"⟩ end score def clause_id := ℕ @@ -63,22 +63,22 @@ namespace derived_clause meta instance : has_to_tactic_format derived_clause := ⟨λc, do -prf_fmt ← pp c^.c^.proof, -c_fmt ← pp c^.c, -ass_fmt ← pp (c^.assertions^.map (λa, a^.local_type)), +prf_fmt ← pp c.c.proof, +c_fmt ← pp c.c, +ass_fmt ← pp (c.assertions.map (λa, a.local_type)), return $ -to_string c^.sc ++ " " ++ +to_string c.sc ++ " " ++ prf_fmt ++ " " ++ c_fmt ++ " <- " ++ ass_fmt ++ -" (selected: " ++ to_fmt c^.selected ++ +" (selected: " ++ to_fmt c.selected ++ ")" ⟩ meta def clause_with_assertions (ac : derived_clause) : clause := -ac^.c^.close_constn ac^.assertions +ac.c.close_constn ac.assertions meta def update_proof (dc : derived_clause) (p : expr) : derived_clause := -{ dc with c := { (dc^.c) with proof := p } } +{ dc with c := { (dc.c) with proof := p } } end derived_clause @@ -90,8 +90,8 @@ namespace locked_clause meta instance : has_to_tactic_format locked_clause := ⟨λc, do -c_fmt ← pp c^.dc, -reasons_fmt ← pp (c^.reasons^.map (λr, r^.for (λa, a^.local_type))), +c_fmt ← pp c.dc, +reasons_fmt ← pp (c.reasons.map (λr, r.for (λa, a.local_type))), return $ c_fmt ++ " (locked in case of: " ++ reasons_fmt ++ ")" ⟩ @@ -116,13 +116,13 @@ private meta def join_with_nl : list format → format := list.foldl (λx y, x ++ format.line ++ y) format.nil private meta def prover_state_tactic_fmt (s : prover_state) : tactic format := do -active_fmts ← mapm pp $ rb_map.values s^.active, -passive_fmts ← mapm pp $ rb_map.values s^.passive, -new_fmts ← mapm pp s^.newly_derived, -locked_fmts ← mapm pp s^.locked, -sat_fmts ← mapm pp s^.sat_solver^.clauses, -sat_model_fmts ← for s^.current_model^.to_list (λx, if x.2 = tt then pp x.1 else pp ```(not %%x.1)), -prec_fmts ← mapm pp s^.prec, +active_fmts ← mapm pp $ rb_map.values s.active, +passive_fmts ← mapm pp $ rb_map.values s.passive, +new_fmts ← mapm pp s.newly_derived, +locked_fmts ← mapm pp s.locked, +sat_fmts ← mapm pp s.sat_solver.clauses, +sat_model_fmts ← for s.current_model.to_list (λx, if x.2 = tt then pp x.1 else pp ```(not %%x.1)), +prec_fmts ← mapm pp s.prec, return (join_with_nl ([to_fmt "active:"] ++ map (append (to_fmt " ")) active_fmts ++ [to_fmt "passive:"] ++ map (append (to_fmt " ")) passive_fmts ++ @@ -163,21 +163,21 @@ end prover meta def selection_strategy := derived_clause → prover derived_clause meta def get_active : prover (rb_map clause_id derived_clause) := -do state ← state_t.read, return state^.active +do state ← state_t.read, return state.active meta def add_active (a : derived_clause) : prover unit := do state ← state_t.read, -state_t.write { state with active := state^.active^.insert a^.id a } +state_t.write { state with active := state.active.insert a.id a } meta def get_passive : prover (rb_map clause_id derived_clause) := lift passive state_t.read meta def get_precedence : prover (list expr) := -do state ← state_t.read, return state^.prec +do state ← state_t.read, return state.prec meta def get_term_order : prover (expr → expr → bool) := do state ← state_t.read, -return $ mk_lpo (map name_of_funsym state^.prec) +return $ mk_lpo (map name_of_funsym state.prec) private meta def set_precedence (new_prec : list expr) : prover unit := do state ← state_t.read, state_t.write { state with prec := new_prec } @@ -185,31 +185,31 @@ do state ← state_t.read, state_t.write { state with prec := new_prec } meta def register_consts_in_precedence (consts : list expr) := do p ← get_precedence, p_set ← return (rb_map.set_of_list (map name_of_funsym p)), -new_syms ← return $ list.filter (λc, ¬p_set^.contains (name_of_funsym c)) consts, +new_syms ← return $ list.filter (λc, ¬p_set.contains (name_of_funsym c)) consts, set_precedence (new_syms ++ p) meta def in_sat_solver {A} (cmd : cdcl.solver A) : prover A := do state ← state_t.read, -result ← cmd state^.sat_solver, +result ← cmd state.sat_solver, state_t.write { state with sat_solver := result.2 }, return result.1 meta def collect_ass_hyps (c : clause) : prover (list expr) := -let lcs := contained_lconsts c^.proof in +let lcs := contained_lconsts c.proof in do st ← state_t.read, return (do - hs ← st^.sat_hyps^.values, + hs ← st.sat_hyps.values, h ← [hs.1, hs.2], - guard $ lcs^.contains h^.local_uniq_name, + guard $ lcs.contains h.local_uniq_name, [h]) meta def get_clause_count : prover ℕ := -do s ← state_t.read, return s^.clause_counter +do s ← state_t.read, return s.clause_counter meta def get_new_cls_id : prover clause_id := do state ← state_t.read, -state_t.write { state with clause_counter := state^.clause_counter + 1 }, -return state^.clause_counter +state_t.write { state with clause_counter := state.clause_counter + 1 }, +return state.clause_counter meta def mk_derived (c : clause) (sc : score) : prover derived_clause := do ass ← collect_ass_hyps c, @@ -217,31 +217,31 @@ id ← get_new_cls_id, return { id := id, c := c, selected := [], assertions := ass, sc := sc } meta def add_inferred (c : derived_clause) : prover unit := do -c' ← c^.c^.normalize, c' ← return { c with c := c' }, -register_consts_in_precedence (contained_funsyms c'^.c^.type)^.values, +c' ← c.c.normalize, c' ← return { c with c := c' }, +register_consts_in_precedence (contained_funsyms c'.c.type).values, state ← state_t.read, -state_t.write { state with newly_derived := c' :: state^.newly_derived } +state_t.write { state with newly_derived := c' :: state.newly_derived } -- FIXME: what if we've seen the variable before, but with a weaker score? meta def mk_sat_var (v : expr) (suggested_ph : bool) (suggested_ev : score) : prover unit := -do st ← state_t.read, if st^.sat_hyps^.contains v then return () else do +do st ← state_t.read, if st.sat_hyps.contains v then return () else do hpv ← mk_local_def `h v, -hnv ← mk_local_def `hn $ imp v st^.local_false, -state_t.modify $ λst, { st with sat_hyps := st^.sat_hyps^.insert v (hpv, hnv) }, +hnv ← mk_local_def `hn $ imp v st.local_false, +state_t.modify $ λst, { st with sat_hyps := st.sat_hyps.insert v (hpv, hnv) }, in_sat_solver $ cdcl.mk_var_core v suggested_ph, match v with | (pi _ _ _ _) := do - c ← clause.of_proof st^.local_false hpv, + c ← clause.of_proof st.local_false hpv, mk_derived c suggested_ev >>= add_inferred -| _ := do cp ← clause.of_proof st^.local_false hpv, mk_derived cp suggested_ev >>= add_inferred, - cn ← clause.of_proof st^.local_false hnv, mk_derived cn suggested_ev >>= add_inferred +| _ := do cp ← clause.of_proof st.local_false hpv, mk_derived cp suggested_ev >>= add_inferred, + cn ← clause.of_proof st.local_false hnv, mk_derived cn suggested_ev >>= add_inferred end meta def get_sat_hyp_core (v : expr) (ph : bool) : prover (option expr) := flip monad.lift state_t.read $ λst, - match st^.sat_hyps^.find v with + match st.sat_hyps.find v with | some (hp, hn) := some $ if ph then hp else hn | none := none end @@ -250,30 +250,30 @@ meta def get_sat_hyp (v : expr) (ph : bool) : prover expr := do hyp_opt ← get_sat_hyp_core v ph, match hyp_opt with | some hyp := return hyp -| none := fail $ "unknown sat variable: " ++ v^.to_string +| none := fail $ "unknown sat variable: " ++ v.to_string end meta def add_sat_clause (c : clause) (suggested_ev : score) : prover unit := do -c ← c^.distinct, +c ← c.distinct, already_added ← flip monad.lift state_t.read $ λst, decidable.to_bool $ - c^.type ∈ st^.sat_solver^.clauses^.map (λd, d^.type), + c.type ∈ st.sat_solver.clauses.map (λd, d.type), if already_added then return () else do -for c^.get_lits $ λl, mk_sat_var l^.formula l^.is_neg suggested_ev, +for c.get_lits $ λl, mk_sat_var l.formula l.is_neg suggested_ev, in_sat_solver $ cdcl.mk_clause c, state_t.modify $ λst, { st with needs_sat_run := tt } meta def sat_eval_lit (v : expr) (pol : bool) : prover bool := -do v_st ← flip monad.lift state_t.read $ λst, st^.current_model^.find v, +do v_st ← flip monad.lift state_t.read $ λst, st.current_model.find v, match v_st with | some ph := return $ if pol then ph else bnot ph | none := return tt end meta def sat_eval_assertion (assertion : expr) : prover bool := -do lf ← flip monad.lift state_t.read $ λst, st^.local_false, -match is_local_not lf assertion^.local_type with +do lf ← flip monad.lift state_t.read $ λst, st.local_false, +match is_local_not lf assertion.local_type with | some v := sat_eval_lit v ff -| none := sat_eval_lit assertion^.local_type tt +| none := sat_eval_lit assertion.local_type tt end meta def sat_eval_assertions : list expr → prover bool @@ -285,33 +285,33 @@ return ff | [] := return tt private meta def intern_clause (c : derived_clause) : prover derived_clause := do -hyp_name ← get_unused_name (mk_simple_name $ "clause_" ++ to_string c^.id^.to_nat) none, -c' ← return $ c^.c^.close_constn c^.assertions, -assertv hyp_name c'^.type c'^.proof, +hyp_name ← get_unused_name (mk_simple_name $ "clause_" ++ to_string c.id.to_nat) none, +c' ← return $ c.c.close_constn c.assertions, +assertv hyp_name c'.type c'.proof, proof' ← get_local hyp_name, type ← infer_type proof', -- FIXME: otherwise "" -return $ c^.update_proof $ app_of_list proof' c^.assertions +return $ c.update_proof $ app_of_list proof' c.assertions meta def register_as_passive (c : derived_clause) : prover unit := do c ← intern_clause c, -ass_v ← sat_eval_assertions c^.assertions, -if c^.c^.num_quants = 0 ∧ c^.c^.num_lits = 0 then - add_sat_clause c^.clause_with_assertions c^.sc +ass_v ← sat_eval_assertions c.assertions, +if c.c.num_quants = 0 ∧ c.c.num_lits = 0 then + add_sat_clause c.clause_with_assertions c.sc else if ¬ass_v then do - state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st^.locked } + state_t.modify $ λst, { st with locked := ⟨c, []⟩ :: st.locked } else do - state_t.modify $ λst, { st with passive := st^.passive^.insert c^.id c } + state_t.modify $ λst, { st with passive := st.passive.insert c.id c } meta def remove_passive (id : clause_id) : prover unit := -do state ← state_t.read, state_t.write { state with passive := state^.passive^.erase id } +do state ← state_t.read, state_t.write { state with passive := state.passive.erase id } meta def move_locked_to_passive : prover unit := do -locked ← flip monad.lift state_t.read (λst, st^.locked), +locked ← flip monad.lift state_t.read (λst, st.locked), new_locked ← flip filter locked (λlc, do - reason_vals ← mapm sat_eval_assertions lc^.reasons, - c_val ← sat_eval_assertions lc^.dc^.assertions, - if reason_vals^.for_all (λr, r = ff) ∧ c_val then do - state_t.modify $ λst, { st with passive := st^.passive^.insert lc^.dc^.id lc^.dc }, + reason_vals ← mapm sat_eval_assertions lc.reasons, + c_val ← sat_eval_assertions lc.dc.assertions, + if reason_vals.for_all (λr, r = ff) ∧ c_val then do + state_t.modify $ λst, { st with passive := st.passive.insert lc.dc.id lc.dc }, return ff else return tt @@ -319,23 +319,23 @@ new_locked ← flip filter locked (λlc, do state_t.modify $ λst, { st with locked := new_locked } meta def move_active_to_locked : prover unit := -do active ← get_active, for' active^.values $ λac, do - c_val ← sat_eval_assertions ac^.assertions, +do active ← get_active, for' active.values $ λac, do + c_val ← sat_eval_assertions ac.assertions, if ¬c_val then do state_t.modify $ λst, { st with - active := st^.active^.erase ac^.id, - locked := ⟨ac, []⟩ :: st^.locked + active := st.active.erase ac.id, + locked := ⟨ac, []⟩ :: st.locked } else return () meta def move_passive_to_locked : prover unit := -do passive ← flip monad.lift state_t.read $ λst, st^.passive, for' passive^.to_list $ λpc, do - c_val ← sat_eval_assertions pc.2^.assertions, +do passive ← flip monad.lift state_t.read $ λst, st.passive, for' passive.to_list $ λpc, do + c_val ← sat_eval_assertions pc.2.assertions, if ¬c_val then do state_t.modify $ λst, { st with - passive := st^.passive^.erase pc.1, - locked := ⟨pc.2, []⟩ :: st^.locked + passive := st.passive.erase pc.1, + locked := ⟨pc.2, []⟩ :: st.locked } else return () @@ -360,21 +360,21 @@ end meta def take_newly_derived : prover (list derived_clause) := do state ← state_t.read, state_t.write { state with newly_derived := [] }, -return state^.newly_derived +return state.newly_derived meta def remove_redundant (id : clause_id) (parents : list derived_clause) : prover unit := do -when (not $ parents^.for_all $ λp, p^.id ≠ id) (fail "clause is redundant because of itself"), -red ← flip monad.lift state_t.read (λst, st^.active^.find id), +when (not $ parents.for_all $ λp, p.id ≠ id) (fail "clause is redundant because of itself"), +red ← flip monad.lift state_t.read (λst, st.active.find id), match red with | none := return () | some red := do -let reasons := parents^.map (λp, p^.assertions), -let assertion := red^.assertions, -if reasons^.for_all $ λr, r^.subset_of assertion then do - state_t.modify $ λst, { st with active := st^.active^.erase id } +let reasons := parents.map (λp, p.assertions), +let assertion := red.assertions, +if reasons.for_all $ λr, r.subset_of assertion then do + state_t.modify $ λst, { st with active := st.active.erase id } else do - state_t.modify $ λst, { st with active := st^.active^.erase id, - locked := ⟨red, reasons⟩ :: st^.locked } + state_t.modify $ λst, { st with active := st.active.erase id, + locked := ⟨red, reasons⟩ :: st.locked } end meta def inference := derived_clause → prover unit @@ -388,7 +388,7 @@ meta def seq_inferences : list inference → inference | (inf::infs) := λgiven, do inf given, now_active ← get_active, - if rb_map.contains now_active given^.id then + if rb_map.contains now_active given.id then seq_inferences infs given else return () @@ -397,15 +397,15 @@ meta def simp_inference (simpl : derived_clause → prover (option clause)) : in λgiven, do maybe_simpld ← simpl given, match maybe_simpld with | some simpld := do - derived_simpld ← mk_derived simpld given^.sc^.sched_now, + derived_simpld ← mk_derived simpld given.sc.sched_now, add_inferred derived_simpld, - remove_redundant given^.id [] + remove_redundant given.id [] | none := return () end meta def preprocessing_rule (f : list derived_clause → prover (list derived_clause)) : prover unit := do state ← state_t.read, -newly_derived' ← f state^.newly_derived, +newly_derived' ← f state.newly_derived, state' ← state_t.read, state_t.write { state' with newly_derived := newly_derived' } @@ -422,7 +422,7 @@ meta def empty (local_false : expr) : prover_state := meta def initial (local_false : expr) (clauses : list clause) : tactic prover_state := do after_setup ← for' clauses (λc, - let in_sos := ((contained_lconsts c^.proof)^.erase local_false^.local_uniq_name)^.size = 0 in + let in_sos := ((contained_lconsts c.proof).erase local_false.local_uniq_name).size = 0 in do mk_derived c { priority := score.prio.immediate, in_sos := in_sos, age := 0, cost := 0 } >>= add_inferred ) $ empty local_false, @@ -441,14 +441,14 @@ return $ list.foldl score.combine { priority := score.prio.default, meta def inf_if_successful (add_cost : ℕ) (parent : derived_clause) (tac : tactic (list clause)) : prover unit := (do inferred ← tac, for' inferred $ λc, - inf_score add_cost [parent^.sc] >>= mk_derived c >>= add_inferred) + inf_score add_cost [parent.sc] >>= mk_derived c >>= add_inferred) <|> return () meta def simp_if_successful (parent : derived_clause) (tac : tactic (list clause)) : prover unit := (do inferred ← tac, for' inferred $ λc, - mk_derived c parent^.sc^.sched_now >>= add_inferred, - remove_redundant parent^.id []) + mk_derived c parent.sc.sched_now >>= add_inferred, + remove_redundant parent.id []) <|> return () end super diff --git a/library/tools/super/resolution.lean b/library/tools/super/resolution.lean index d277912d6d..69fd1fc555 100644 --- a/library/tools/super/resolution.lean +++ b/library/tools/super/resolution.lean @@ -16,43 +16,43 @@ variables (i1 i2 : nat) -- c1 : ... → ¬a → ... -- c2 : ... → a → ... meta def try_resolve : tactic clause := do -qf1 ← c1^.open_metan c1^.num_quants, -qf2 ← c2^.open_metan c2^.num_quants, +qf1 ← c1.open_metan c1.num_quants, +qf2 ← c2.open_metan c2.num_quants, -- FIXME: using default transparency unifies m*n with (x*y*z)*w here ??? -unify (qf1.1^.get_lit i1)^.formula (qf2.1^.get_lit i2)^.formula transparency.reducible, -qf1i ← qf1.1^.inst_mvars, +unify (qf1.1.get_lit i1).formula (qf2.1.get_lit i2).formula transparency.reducible, +qf1i ← qf1.1.inst_mvars, guard $ clause.is_maximal gt qf1i i1, -op1 ← qf1.1^.open_constn i1, -op2 ← qf2.1^.open_constn c2^.num_lits, -a_in_op2 ← (op2.2^.nth i2)^.to_monad, +op1 ← qf1.1.open_constn i1, +op2 ← qf2.1.open_constn c2.num_lits, +a_in_op2 ← (op2.2.nth i2).to_monad, clause.meta_closure (qf1.2 ++ qf2.2) $ - (op1.1^.inst (op2.1^.close_const a_in_op2)^.proof)^.close_constn (op1.2 ++ op2.2^.remove_nth i2) + (op1.1.inst (op2.1.close_const a_in_op2).proof).close_constn (op1.2 ++ op2.2.remove_nth i2) meta def try_add_resolvent : prover unit := do -c' ← try_resolve gt ac1^.c ac2^.c i1 i2, -inf_score 1 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred +c' ← try_resolve gt ac1.c ac2.c i1 i2, +inf_score 1 [ac1.sc, ac2.sc] >>= mk_derived c' >>= add_inferred meta def maybe_add_resolvent : prover unit := try_add_resolvent gt ac1 ac2 i1 i2 <|> return () meta def resolution_left_inf : inference := take given, do active ← get_active, sequence' $ do - given_i ← given^.selected, - guard $ clause.literal.is_neg (given^.c^.get_lit given_i), + given_i ← given.selected, + guard $ clause.literal.is_neg (given.c.get_lit given_i), other ← rb_map.values active, - guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos, - other_i ← other^.selected, - guard $ clause.literal.is_pos (other^.c^.get_lit other_i), + guard $ ¬given.sc.in_sos ∨ ¬other.sc.in_sos, + other_i ← other.selected, + guard $ clause.literal.is_pos (other.c.get_lit other_i), [maybe_add_resolvent gt other given other_i given_i] meta def resolution_right_inf : inference := take given, do active ← get_active, sequence' $ do - given_i ← given^.selected, - guard $ clause.literal.is_pos (given^.c^.get_lit given_i), + given_i ← given.selected, + guard $ clause.literal.is_pos (given.c.get_lit given_i), other ← rb_map.values active, - guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos, - other_i ← other^.selected, - guard $ clause.literal.is_neg (other^.c^.get_lit other_i), + guard $ ¬given.sc.in_sos ∨ ¬other.sc.in_sos, + other_i ← other.selected, + guard $ clause.literal.is_neg (other.c.get_lit other_i), [maybe_add_resolvent gt given other given_i other_i] @[super.inf] diff --git a/library/tools/super/selection.lean b/library/tools/super/selection.lean index ba3819616e..d26c17b6c7 100644 --- a/library/tools/super/selection.lean +++ b/library/tools/super/selection.lean @@ -9,26 +9,26 @@ namespace super meta def simple_selection_strategy (f : (expr → expr → bool) → clause → list ℕ) : selection_strategy := take dc, do gt ← get_term_order, return $ - if dc^.selected^.empty ∧ dc^.c^.num_lits > 0 - then { dc with selected := f gt dc^.c } + if dc.selected.empty ∧ dc.c.num_lits > 0 + then { dc with selected := f gt dc.c } else dc meta def dumb_selection : selection_strategy := simple_selection_strategy $ λgt c, -match c^.lits_where clause.literal.is_neg with -| [] := list.range c^.num_lits +match c.lits_where clause.literal.is_neg with +| [] := list.range c.num_lits | neg_lit::_ := [neg_lit] end meta def selection21 : selection_strategy := simple_selection_strategy $ λgt c, let maximal_lits := list.filter_maximal (λi j, - gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits) in + gt (c.get_lit i).formula (c.get_lit j).formula) (list.range c.num_lits) in if list.length maximal_lits = 1 then maximal_lits else -let neg_lits := list.filter (λi, (c^.get_lit i)^.is_neg) (list.range c^.num_lits), +let neg_lits := list.filter (λi, (c.get_lit i).is_neg) (list.range c.num_lits), maximal_neg_lits := list.filter_maximal (λi j, - gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) neg_lits in -if ¬maximal_neg_lits^.empty then + gt (c.get_lit i).formula (c.get_lit j).formula) neg_lits in +if ¬maximal_neg_lits.empty then list.taken 1 maximal_neg_lits else maximal_lits @@ -36,20 +36,20 @@ else meta def selection22 : selection_strategy := simple_selection_strategy $ λgt c, let maximal_lits := list.filter_maximal (λi j, - gt (c^.get_lit i)^.formula (c^.get_lit j)^.formula) (list.range c^.num_lits), - maximal_lits_neg := list.filter (λi, (c^.get_lit i)^.is_neg) maximal_lits in -if ¬maximal_lits_neg^.empty then + gt (c.get_lit i).formula (c.get_lit j).formula) (list.range c.num_lits), + maximal_lits_neg := list.filter (λi, (c.get_lit i).is_neg) maximal_lits in +if ¬maximal_lits_neg.empty then list.taken 1 maximal_lits_neg else maximal_lits meta def clause_weight (c : derived_clause) : nat := -(c^.c^.get_lits^.for (λl, expr_size l^.formula + if l^.is_pos then 10 else 1))^.sum +(c.c.get_lits.for (λl, expr_size l.formula + if l.is_pos then 10 else 1)).sum meta def find_minimal_by (passive : rb_map clause_id derived_clause) {A} [has_ordering A] (f : derived_clause → A) : clause_id := -match rb_map.min $ rb_map.of_list $ passive^.values^.map $ λc, (f c, c^.id) with +match rb_map.min $ rb_map.of_list $ passive.values.map $ λc, (f c, c.id) with | some id := id | none := nat.zero end @@ -59,16 +59,16 @@ meta def age_of_clause_id : name → ℕ | _ := 0 meta def find_minimal_weight (passive : rb_map clause_id derived_clause) : clause_id := -find_minimal_by passive $ λc, (c^.sc^.priority, clause_weight c + c^.sc^.cost, c^.sc^.age, c^.id) +find_minimal_by passive $ λc, (c.sc.priority, clause_weight c + c.sc.cost, c.sc.age, c.id) meta def find_minimal_age (passive : rb_map clause_id derived_clause) : clause_id := -find_minimal_by passive $ λc, (c^.sc^.priority, c^.sc^.age, c^.id) +find_minimal_by passive $ λc, (c.sc.priority, c.sc.age, c.id) meta def weight_clause_selection : clause_selection_strategy := -take iter, do state ← state_t.read, return $ find_minimal_weight state^.passive +take iter, do state ← state_t.read, return $ find_minimal_weight state.passive meta def oldest_clause_selection : clause_selection_strategy := -take iter, do state ← state_t.read, return $ find_minimal_age state^.passive +take iter, do state ← state_t.read, return $ find_minimal_age state.passive meta def age_weight_clause_selection (thr mod : ℕ) : clause_selection_strategy := take iter, if iter % mod < thr then diff --git a/library/tools/super/simp.lean b/library/tools/super/simp.lean index ddaae27c38..9663d42f75 100644 --- a/library/tools/super/simp.lean +++ b/library/tools/super/simp.lean @@ -18,7 +18,7 @@ S ← simp_lemmas.mk_default, (type', heq) ← simplify S type, hyps ← return $ contained_lconsts type, hyps' ← return $ contained_lconsts_list [type', heq], -add_hyps ← return $ list.filter (λn : expr, ¬hyps^.contains n^.local_uniq_name) hyps'^.values, +add_hyps ← return $ list.filter (λn : expr, ¬hyps.contains n.local_uniq_name) hyps'.values, return (type', heq, add_hyps) meta def try_simplify_left (c : clause) (i : ℕ) : tactic (list clause) := @@ -30,7 +30,7 @@ on_left_at c i $ λtype, do meta def try_simplify_right (c : clause) (i : ℕ) : tactic (list clause) := on_right_at' c i $ λhyp, do - (type', heq, add_hyps) ← simplify_capturing_assumptions hyp^.local_type, + (type', heq, add_hyps) ← simplify_capturing_assumptions hyp.local_type, heqtype ← infer_type heq, heqsymm ← mk_eq_symm heq, prf ← mk_eq_mpr heqsymm hyp, @@ -38,7 +38,7 @@ on_right_at' c i $ λhyp, do meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do r ← [try_simplify_right, try_simplify_left], -i ← list.range given^.c^.num_lits, -[inf_if_successful 2 given (r given^.c i)] +i ← list.range given.c.num_lits, +[inf_if_successful 2 given (r given.c i)] end super diff --git a/library/tools/super/splitting.lean b/library/tools/super/splitting.lean index f30999fac1..6a781ed42a 100644 --- a/library/tools/super/splitting.lean +++ b/library/tools/super/splitting.lean @@ -11,57 +11,57 @@ namespace super private meta def find_components : list expr → list (list (expr × ℕ)) → list (list (expr × ℕ)) | (e::es) comps := let (contain_e, do_not_contain_e) := - partition (λc : list (expr × ℕ), c^.exists_ $ λf, - (abstract_local f.1 e^.local_uniq_name)^.has_var) comps in + partition (λc : list (expr × ℕ), c.exists_ $ λf, + (abstract_local f.1 e.local_uniq_name).has_var) comps in find_components es $ list.join contain_e :: do_not_contain_e | _ comps := comps meta def get_components (hs : list expr) : list (list expr) := -(find_components hs (hs^.zip_with_index^.map $ λh, [h]))^.map $ λc, -(sort_on (λh : expr × ℕ, h.2) c)^.map $ λh, h.1 +(find_components hs (hs.zip_with_index.map $ λh, [h])).map $ λc, +(sort_on (λh : expr × ℕ, h.2) c).map $ λh, h.1 meta def extract_assertions : clause → prover (clause × list expr) | c := -if c^.num_lits = 0 then return (c, []) -else if c^.num_quants ≠ 0 then do - qf ← c^.open_constn c^.num_quants, +if c.num_lits = 0 then return (c, []) +else if c.num_quants ≠ 0 then do + qf ← c.open_constn c.num_quants, qf_wo_as ← extract_assertions qf.1, - return (qf_wo_as.1^.close_constn qf.2, qf_wo_as.2) + return (qf_wo_as.1.close_constn qf.2, qf_wo_as.2) else do - hd ← return $ c^.get_lit 0, - hyp_opt ← get_sat_hyp_core hd^.formula hd^.is_neg, + hd ← return $ c.get_lit 0, + hyp_opt ← get_sat_hyp_core hd.formula hd.is_neg, match hyp_opt with | some h := do - wo_as ← extract_assertions (c^.inst h), + wo_as ← extract_assertions (c.inst h), return (wo_as.1, h :: wo_as.2) | _ := do - op ← c^.open_const, + op ← c.open_const, op_wo_as ← extract_assertions op.1, - return (op_wo_as.1^.close_const op.2, op_wo_as.2) + return (op_wo_as.1.close_const op.2, op_wo_as.2) end meta def mk_splitting_clause' (empty_clause : clause) : list (list expr) → tactic (list expr × expr) -| [] := return ([], empty_clause^.proof) +| [] := return ([], empty_clause.proof) | ([p] :: comps) := do p' ← mk_splitting_clause' comps, return (p::p'.1, p'.2) | (comp :: comps) := do (hs, p') ← mk_splitting_clause' comps, - hnc ← mk_local_def `hnc (imp (pis comp empty_clause^.local_false) empty_clause^.local_false), + hnc ← mk_local_def `hnc (imp (pis comp empty_clause.local_false) empty_clause.local_false), p'' ← return $ app hnc (lambdas comp p'), return (hnc::hs, p'') meta def mk_splitting_clause (empty_clause : clause) (comps : list (list expr)) : tactic clause := do (hs, p) ← mk_splitting_clause' empty_clause comps, -return $ { empty_clause with proof := p }^.close_constn hs +return $ { empty_clause with proof := p }.close_constn hs @[super.inf] meta def splitting_inf : inf_decl := inf_decl.mk 30 $ take given, do -lf ← flip monad.lift state_t.read $ λst, st^.local_false, -op ← given^.c^.open_constn given^.c^.num_binders, -if list.bor (given^.c^.get_lits^.map $ λl, (is_local_not lf l^.formula)^.is_some) then return () else +lf ← flip monad.lift state_t.read $ λst, st.local_false, +op ← given.c.open_constn given.c.num_binders, +if list.bor (given.c.get_lits.map $ λl, (is_local_not lf l.formula).is_some) then return () else let comps := get_components op.2 in -if comps^.length < 2 then return () else do +if comps.length < 2 then return () else do splitting_clause ← mk_splitting_clause op.1 comps, ass ← collect_ass_hyps splitting_clause, -add_sat_clause (splitting_clause^.close_constn ass) given^.sc^.sched_default, -remove_redundant given^.id [] +add_sat_clause (splitting_clause.close_constn ass) given.sc.sched_default, +remove_redundant given.id [] end super diff --git a/library/tools/super/subsumption.lean b/library/tools/super/subsumption.lean index 25e3ae3f6a..8aa23e7879 100644 --- a/library/tools/super/subsumption.lean +++ b/library/tools/super/subsumption.lean @@ -11,29 +11,29 @@ namespace super private meta def try_subsume_core : list clause.literal → list clause.literal → tactic unit | [] _ := skip | small large := first $ do - i ← small^.zip_with_index, j ← large^.zip_with_index, + i ← small.zip_with_index, j ← large.zip_with_index, return $ do unify_lit i.1 j.1, - try_subsume_core (small^.remove_nth i.2) (large^.remove_nth j.2) + try_subsume_core (small.remove_nth i.2) (large.remove_nth j.2) -- FIXME: this is incorrect if a quantifier is unused meta def try_subsume (small large : clause) : tactic unit := do small_open ← clause.open_metan small (clause.num_quants small), large_open ← clause.open_constn large (clause.num_quants large), -guard $ small^.num_lits ≤ large^.num_lits, -try_subsume_core small_open.1^.get_lits large_open.1^.get_lits +guard $ small.num_lits ≤ large.num_lits, +try_subsume_core small_open.1.get_lits large_open.1.get_lits meta def does_subsume (small large : clause) : tactic bool := (try_subsume small large >> return tt) <|> return ff meta def does_subsume_with_assertions (small large : derived_clause) : prover bool := do -if small^.assertions^.subset_of large^.assertions then do - does_subsume small^.c large^.c +if small.assertions.subset_of large.assertions then do + does_subsume small.c large.c else return ff meta def any_tt {m : Type → Type} [monad m] (active : rb_map clause_id derived_clause) (pred : derived_clause → m bool) : m bool := -active^.fold (return ff) $ λk a cont, do +active.fold (return ff) $ λk a cont, do v ← pred a, if v then return tt else cont meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : list A → m bool @@ -43,19 +43,19 @@ meta def any_tt_list {m : Type → Type} [monad m] {A} (pred : A → m bool) : l @[super.inf] meta def forward_subsumption : inf_decl := inf_decl.mk 20 $ take given, do active ← get_active, -sequence' $ do a ← active^.values, - guard $ a^.id ≠ given^.id, +sequence' $ do a ← active.values, + guard $ a.id ≠ given.id, return $ do - ss ← does_subsume a^.c given^.c, + ss ← does_subsume a.c given.c, if ss - then remove_redundant given^.id [a] + then remove_redundant given.id [a] else return () meta def forward_subsumption_pre : prover unit := preprocessing_rule $ λnew, do active ← get_active, filter (λn, do do ss ← any_tt active (λa, - if a^.assertions^.subset_of n^.assertions then do - does_subsume a^.c n^.c + if a.assertions.subset_of n.assertions then do + does_subsume a.c n.c else -- TODO: move to locked return ff), @@ -65,7 +65,7 @@ meta def subsumption_interreduction : list derived_clause → prover (list deriv | (c::cs) := do -- TODO: move to locked cs_that_subsume_c ← filter (λd, does_subsume_with_assertions d c) cs, - if ¬cs_that_subsume_c^.empty then + if ¬cs_that_subsume_c.empty then -- TODO: update score subsumption_interreduction cs else do @@ -76,7 +76,7 @@ meta def subsumption_interreduction : list derived_clause → prover (list deriv meta def subsumption_interreduction_pre : prover unit := preprocessing_rule $ λnew, -let new' := list.sort_on (λc : derived_clause, c^.c^.num_lits) new in +let new' := list.sort_on (λc : derived_clause, c.c.num_lits) new in subsumption_interreduction new' meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred : V → m bool) : m (list K) := @@ -86,7 +86,7 @@ meta def keys_where_tt {m} {K V : Type} [monad m] (active : rb_map K V) (pred : @[super.inf] meta def backward_subsumption : inf_decl := inf_decl.mk 20 $ λgiven, do active ← get_active, -ss ← keys_where_tt active (λa, does_subsume given^.c a^.c), -sequence' $ do id ← ss, guard (id ≠ given^.id), [remove_redundant id [given]] +ss ← keys_where_tt active (λa, does_subsume given.c a.c), +sequence' $ do id ← ss, guard (id ≠ given.id), [remove_redundant id [given]] end super diff --git a/library/tools/super/superposition.lean b/library/tools/super/superposition.lean index 81f27822a3..4c4280a31b 100644 --- a/library/tools/super/superposition.lean +++ b/library/tools/super/superposition.lean @@ -29,8 +29,8 @@ end meta def replace_position (v : expr) : expr → position → expr | (app a b) (p::ps) := let args := get_app_args (app a b) in -match args^.nth p with -| some arg := app_of_list a^.get_app_fn $ args^.update_nth p $ replace_position arg ps +match args.nth p with +| some arg := app_of_list a.get_app_fn $ args.update_nth p $ replace_position arg ps | none := app a b end | e [] := v @@ -46,7 +46,7 @@ variable lt_in_termorder : bool variable congr_ax : name lemma {u v w} sup_ltr (F : Sort u) (A : Sort v) (a1 a2) (f : A → Sort w) : (f a1 → F) → f a2 → a1 = a2 → F := -take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq^.symm) +take hnfa1 hfa2 he, hnfa1 (@eq.rec A a2 f hfa2 a1 he.symm) lemma {u v w} sup_rtl (F : Sort u) (A : Sort v) (a1 a2) (f : A → Sort w) : (f a1 → F) → f a2 → a2 = a1 → F := take hnfa1 hfa2 heq, hnfa1 (@eq.rec A a2 f hfa2 a1 heq) @@ -57,11 +57,11 @@ match is_eq e with end meta def try_sup : tactic clause := do -guard $ (c1^.get_lit i1)^.is_pos, -qf1 ← c1^.open_metan c1^.num_quants, -qf2 ← c2^.open_metan c2^.num_quants, -(rwr_from, rwr_to) ← (is_eq_dir (qf1.1^.get_lit i1)^.formula ltr)^.to_monad, -atom ← return (qf2.1^.get_lit i2)^.formula, +guard $ (c1.get_lit i1).is_pos, +qf1 ← c1.open_metan c1.num_quants, +qf2 ← c2.open_metan c2.num_quants, +(rwr_from, rwr_to) ← (is_eq_dir (qf1.1.get_lit i1).formula ltr).to_monad, +atom ← return (qf2.1.get_lit i2).formula, eq_type ← infer_type rwr_from, atom_at_pos ← return $ get_position atom pos, atom_at_pos_type ← infer_type atom_at_pos, @@ -75,52 +75,52 @@ if lt_in_termorder rwr_ctx_varn ← mk_fresh_name, abs_rwr_ctx ← return $ lam rwr_ctx_varn binder_info.default eq_type - (if (qf2.1^.get_lit i2)^.is_neg + (if (qf2.1.get_lit i2).is_neg then replace_position (mk_var 0) atom pos - else imp (replace_position (mk_var 0) atom pos) c2^.local_false), -lf_univ ← infer_univ c1^.local_false, + else imp (replace_position (mk_var 0) atom pos) c2.local_false), +lf_univ ← infer_univ c1.local_false, univ ← infer_univ eq_type, atom_univ ← infer_univ atom, -op1 ← qf1.1^.open_constn i1, -op2 ← qf2.1^.open_constn c2^.num_lits, -hi2 ← (op2.2^.nth i2)^.to_monad, +op1 ← qf1.1.open_constn i1, +op2 ← qf2.1.open_constn c2.num_lits, +hi2 ← (op2.2.nth i2).to_monad, new_atom ← whnf_no_delta $ app abs_rwr_ctx rwr_to', -new_hi2 ← return $ local_const hi2^.local_uniq_name `H binder_info.default new_atom, +new_hi2 ← return $ local_const hi2.local_uniq_name `H binder_info.default new_atom, new_fin_prf ← - return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1^.local_false, eq_type, rwr_from, rwr_to, - abs_rwr_ctx, (op2.1^.close_const hi2)^.proof, new_hi2], -clause.meta_closure (qf1.2 ++ qf2.2) $ (op1.1^.inst new_fin_prf)^.close_constn (op1.2 ++ op2.2^.update_nth i2 new_hi2) + return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1.local_false, eq_type, rwr_from, rwr_to, + abs_rwr_ctx, (op2.1.close_const hi2).proof, new_hi2], +clause.meta_closure (qf1.2 ++ qf2.2) $ (op1.1.inst new_fin_prf).close_constn (op1.2 ++ op2.2.update_nth i2 new_hi2) meta def rwr_positions (c : clause) (i : nat) : list (list ℕ) := -get_rwr_positions (c^.get_lit i)^.formula +get_rwr_positions (c.get_lit i).formula meta def try_add_sup : prover unit := -(do c' ← try_sup gt ac1^.c ac2^.c i1 i2 pos ltr ff congr_ax, - inf_score 2 [ac1^.sc, ac2^.sc] >>= mk_derived c' >>= add_inferred) +(do c' ← try_sup gt ac1.c ac2.c i1 i2 pos ltr ff congr_ax, + inf_score 2 [ac1.sc, ac2.sc] >>= mk_derived c' >>= add_inferred) <|> return () meta def superposition_back_inf : inference := take given, do active ← get_active, sequence' $ do - given_i ← given^.selected, - guard (given^.c^.get_lit given_i)^.is_pos, - option.to_monad $ is_eq (given^.c^.get_lit given_i)^.formula, + given_i ← given.selected, + guard (given.c.get_lit given_i).is_pos, + option.to_monad $ is_eq (given.c.get_lit given_i).formula, other ← rb_map.values active, - guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos, - other_i ← other^.selected, - pos ← rwr_positions other^.c other_i, + guard $ ¬given.sc.in_sos ∨ ¬other.sc.in_sos, + other_i ← other.selected, + pos ← rwr_positions other.c other_i, -- FIXME(gabriel): ``sup_ltr fails to resolve at runtime [do try_add_sup gt given other given_i other_i pos tt ``super.sup_ltr, try_add_sup gt given other given_i other_i pos ff ``super.sup_rtl] meta def superposition_fwd_inf : inference := take given, do active ← get_active, sequence' $ do - given_i ← given^.selected, + given_i ← given.selected, other ← rb_map.values active, - guard $ ¬given^.sc^.in_sos ∨ ¬other^.sc^.in_sos, - other_i ← other^.selected, - guard (other^.c^.get_lit other_i)^.is_pos, - option.to_monad $ is_eq (other^.c^.get_lit other_i)^.formula, - pos ← rwr_positions given^.c given_i, + guard $ ¬given.sc.in_sos ∨ ¬other.sc.in_sos, + other_i ← other.selected, + guard (other.c.get_lit other_i).is_pos, + option.to_monad $ is_eq (other.c.get_lit other_i).formula, + pos ← rwr_positions given.c given_i, [do try_add_sup gt other given other_i given_i pos tt ``super.sup_ltr, try_add_sup gt other given other_i given_i pos ff ``super.sup_rtl] diff --git a/library/tools/super/trim.lean b/library/tools/super/trim.lean index cad173ad48..69d0a6258a 100644 --- a/library/tools/super/trim.lean +++ b/library/tools/super/trim.lean @@ -11,7 +11,7 @@ namespace super -- TODO(gabriel): rewrite using conversions meta def trim : expr → tactic expr | (app (lam n m d b) arg) := - if ¬b^.has_var then + if ¬b.has_var then trim b else lift₂ app (trim (lam n m d b)) (trim arg) @@ -19,12 +19,12 @@ meta def trim : expr → tactic expr | (lam n m d b) := do x ← mk_local' `x m d, b' ← trim (instantiate_var b x), - return $ lam n m d (abstract_local b' x^.local_uniq_name) + return $ lam n m d (abstract_local b' x.local_uniq_name) | (elet n t v b) := if has_var b then do x ← mk_local_def `x t, b' ← trim (instantiate_var b x), - return $ elet n t v (abstract_local b' x^.local_uniq_name) + return $ elet n t v (abstract_local b' x.local_uniq_name) else trim b | e := return e diff --git a/library/tools/super/utils.lean b/library/tools/super/utils.lean index f453886427..7455e61973 100644 --- a/library/tools/super/utils.lean +++ b/library/tools/super/utils.lean @@ -60,10 +60,10 @@ def exists_ {A} (l : list A) (p : A → Prop) [decidable_pred p] : bool := list.any l (λx, to_bool (p x)) def subset_of {A} [decidable_eq A] (xs ys : list A) := -xs^.for_all (λx, x ∈ ys) +xs.for_all (λx, x ∈ ys) def filter_maximal {A} (gt : A → A → bool) (l : list A) : list A := -filter (λx, l^.for_all (λy, ¬gt y x)) l +filter (λx, l.for_all (λy, ¬gt y x)) l private def zip_with_index' {A} : ℕ → list A → list (A × ℕ) | _ nil := nil @@ -132,7 +132,7 @@ meta def contained_lconsts (e : expr) : rb_map name expr := contained_lconsts' e (rb_map.mk name expr) meta def contained_lconsts_list (es : list expr) : rb_map name expr := -es^.foldl (λlcs e, contained_lconsts' e lcs) (rb_map.mk name expr) +es.foldl (λlcs e, contained_lconsts' e lcs) (rb_map.mk name expr) namespace tactic diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index cb911b77ad..768da75b10 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -1046,47 +1046,10 @@ static expr parse_field(parser_state & p, unsigned, expr const * args, pos_info } } -static expr parse_field1(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 1), pos); -} -static expr parse_field2(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 2), pos); -} -static expr parse_field3(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 3), pos); -} -static expr parse_field4(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 4), pos); -} -static expr parse_field5(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 5), pos); -} -static expr parse_field6(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 6), pos); -} -static expr parse_field7(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 7), pos); -} -static expr parse_field8(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 8), pos); -} -static expr parse_field9(parser_state & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_field_notation(args[0], 9), pos); -} - parse_table init_led_table() { parse_table r(false); r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(1), Var(1))); r = r.add({transition("^.", mk_ext_action(parse_field))}, Var(0)); - r = r.add({transition(".1", mk_ext_action(parse_field1))}, Var(0)); - r = r.add({transition(".2", mk_ext_action(parse_field2))}, Var(0)); - r = r.add({transition(".3", mk_ext_action(parse_field3))}, Var(0)); - r = r.add({transition(".4", mk_ext_action(parse_field4))}, Var(0)); - r = r.add({transition(".5", mk_ext_action(parse_field5))}, Var(0)); - r = r.add({transition(".6", mk_ext_action(parse_field6))}, Var(0)); - r = r.add({transition(".7", mk_ext_action(parse_field7))}, Var(0)); - r = r.add({transition(".8", mk_ext_action(parse_field8))}, Var(0)); - r = r.add({transition(".9", mk_ext_action(parse_field9))}, Var(0)); return r; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 33da943a1a..e058a44043 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -612,7 +612,7 @@ unsigned parser::get_small_nat() { mpz val = get_num_val().get_numerator(); lean_assert(val >= 0); if (!val.is_unsigned_int()) - throw parser_error("invalid level expression, value does not fit in a machine integer", pos()); + throw parser_error("invalid numeral, value does not fit in a machine integer", pos()); return val.get_unsigned_int(); } @@ -1987,8 +1987,20 @@ expr parser::parse_led(expr left) { return copy_tag(left, update_sort(left, l)); } else { switch (curr()) { - case token_kind::Keyword: return parse_led_notation(left); - default: return mk_app(left, parse_expr(get_max_prec()), pos_of(left)); + case token_kind::Keyword: + return parse_led_notation(left); + case token_kind::FieldName: { + expr r = save_pos(mk_field_notation(left, get_name_val()), pos()); + next(); + return r; + } + case token_kind::FieldNum: { + expr r = save_pos(mk_field_notation(left, get_small_nat()), pos()); + next(); + return r; + } + default: + return mk_app(left, parse_expr(get_max_prec()), pos_of(left)); } } } @@ -2005,6 +2017,8 @@ unsigned parser::curr_lbp() const { case token_kind::Decimal: case token_kind::String: case token_kind::Char: return get_max_prec(); + case token_kind::FieldNum: case token_kind::FieldName: + return get_max_prec()+1; } lean_unreachable(); // LCOV_EXCL_LINE } @@ -2148,6 +2162,7 @@ void parser::reset_doc_string() { void parser::parse_imports(unsigned & fingerprint, std::vector & imports) { init_scanner(); + scanner::field_notation_scope scope(m_scanner, false); m_last_cmd_pos = pos(); bool prelude = false; if (curr_is_token(get_prelude_tk())) { diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 6b8a63b002..8a69fd9530 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -480,13 +480,59 @@ bool is_id_rest(char const * begin, char const * end) { static char const * g_error_key_msg = "unexpected token"; +void scanner::read_field_idx() { + lean_assert('0' <= curr() && curr() <= '9'); + mpz q(1); + char c = curr(); + next(); + m_num_val = c - '0'; + while (true) { + c = curr(); + if (auto r = try_digit_to_unsigned(10, c)) { + m_num_val = 10*m_num_val + *r; + next(); + } else { + break; + } + } +} + auto scanner::read_key_cmd_id() -> token_kind { buffer cs; next_utf_core(curr(), cs); unsigned num_utfs = 1; unsigned id_sz = 0; unsigned id_utf_sz = 0; - if (is_id_first(cs, 0)) { + if (m_field_notation && cs[0] == '.') { + next_utf(cs); + num_utfs++; + if (std::isdigit(curr())) { + /* field notation `.` */ + read_field_idx(); + return token_kind::FieldNum; + } else { + if (is_id_first(cs, 1) && cs[1] != '_') { + /* field notation `.` */ + num_utfs--; + cs[0] = cs[1]; + cs.pop_back(); + while (true) { + id_sz = cs.size(); + unsigned i = id_sz; + next_utf(cs); + num_utfs++; + if (!is_id_rest(&cs[i], cs.end())) { + break; + } + } + move_back(cs.size() - id_sz, num_utfs - 1); + cs.shrink(id_sz); + cs.push_back(0); + m_name_val = name(cs.data()); + return token_kind::FieldName; + } + } + } else if (is_id_first(cs, 0)) { id_sz = cs.size(); while (true) { id_sz = cs.size(); @@ -674,11 +720,11 @@ token::token(token_kind k, pos_info const & p, token_info const & info): } token::token(token_kind k, pos_info const & p, name const & v): m_kind(k), m_pos(p), m_name_val(new name(v)) { - lean_assert(m_kind == token_kind::QuotedSymbol || m_kind == token_kind::Identifier); + lean_assert(m_kind == token_kind::QuotedSymbol || m_kind == token_kind::Identifier || m_kind == token_kind::FieldName); } token::token(token_kind k, pos_info const & p, mpq const & v): m_kind(k), m_pos(p), m_num_val(new mpq (v)) { - lean_assert(m_kind == token_kind::Decimal || m_kind == token_kind::Numeral); + lean_assert(m_kind == token_kind::Decimal || m_kind == token_kind::Numeral || m_kind == token_kind::FieldNum); } token::token(token_kind k, pos_info const & p, std::string const & v): @@ -694,10 +740,10 @@ void token::dealloc() { case token_kind::Keyword: case token_kind::CommandKeyword: if (m_info != nullptr) delete m_info; return; - case token_kind::Identifier: case token_kind::QuotedSymbol: + case token_kind::Identifier: case token_kind::QuotedSymbol: case token_kind::FieldName: if (m_name_val != nullptr) delete m_name_val; return; - case token_kind::Numeral: case token_kind::Decimal: + case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum: if (m_num_val != nullptr) delete m_num_val; return; case token_kind::String: case token_kind::Char: @@ -716,10 +762,10 @@ void token::copy(token const & tk) { case token_kind::Keyword: case token_kind::CommandKeyword: m_info = new token_info(*tk.m_info); return; - case token_kind::Identifier: case token_kind::QuotedSymbol: + case token_kind::Identifier: case token_kind::QuotedSymbol: case token_kind::FieldName: m_name_val = new name(*tk.m_name_val); return; - case token_kind::Numeral: case token_kind::Decimal: + case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum: m_num_val = new mpq(*tk.m_num_val); return; case token_kind::String: case token_kind::Char: @@ -739,11 +785,11 @@ void token::steal(token && tk) { m_info = tk.m_info; tk.m_info = nullptr; return; - case token_kind::Identifier: case token_kind::QuotedSymbol: + case token_kind::Identifier: case token_kind::QuotedSymbol: case token_kind::FieldName: m_name_val = tk.m_name_val; tk.m_name_val = nullptr; return; - case token_kind::Numeral: case token_kind::Decimal: + case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum: m_num_val = tk.m_num_val; tk.m_num_val = nullptr; return; @@ -771,10 +817,10 @@ token read_tokens(environment & env, io_state const & ios, scanner & s, buffer { + public: + field_notation_scope(scanner & s, bool flag): + flet(s.m_field_notation, flag) {} + }; }; std::ostream & operator<<(std::ostream & out, token_kind k); bool is_id_rest(char const * begin, char const * end); @@ -116,8 +123,8 @@ class token { pos_info m_pos; union { token_info * m_info; /* Keyword, CommandKeyword */ - name * m_name_val; /* QuotedSymbol, Identifier */ - mpq * m_num_val; /* Decimal, Numeral */ + name * m_name_val; /* QuotedSymbol, Identifier, FieldName */ + mpq * m_num_val; /* Decimal, Numeral, FieldNum */ std::string * m_str_val; /* String, Char, DocBlock, ModDocBlock */ };