feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term
Replace `^.` with `.` in the stdlib
This commit is contained in:
Leonardo de Moura
parent
4fa3d31c95
commit
71685e4dd6
72 changed files with 840 additions and 810 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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₂)
|
||||
|
|
|
|||
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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') :=
|
||||
|
|
|
|||
|
|
@ -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 -/
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 β
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 -/
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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) :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <fn>' 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 <idx>' 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]
|
||||
|
|
|
|||
|
|
@ -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 "<position not available>"
|
||||
|
||||
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 :=
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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)) []
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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<module_name> & 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())) {
|
||||
|
|
|
|||
|
|
@ -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<char> 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 `.` <number> */
|
||||
read_field_idx();
|
||||
return token_kind::FieldNum;
|
||||
} else {
|
||||
if (is_id_first(cs, 1) && cs[1] != '_') {
|
||||
/* field notation `.` <atomic_id> */
|
||||
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<t
|
|||
else
|
||||
return token(k, s.get_pos_info(), s.get_token_info());
|
||||
break;
|
||||
case token_kind::Identifier: case token_kind::QuotedSymbol:
|
||||
case token_kind::Identifier: case token_kind::QuotedSymbol: case token_kind::FieldName:
|
||||
tk.push_back(token(k, s.get_pos_info(), s.get_name_val()));
|
||||
break;
|
||||
case token_kind::Numeral: case token_kind::Decimal:
|
||||
case token_kind::Numeral: case token_kind::Decimal: case token_kind::FieldNum:
|
||||
tk.push_back(token(k, s.get_pos_info(), s.get_num_val()));
|
||||
break;
|
||||
case token_kind::String: case token_kind::Char:
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ Author: Leonardo de Moura
|
|||
namespace lean {
|
||||
enum class token_kind {Keyword, CommandKeyword, Identifier, Numeral, Decimal,
|
||||
String, Char, QuotedSymbol,
|
||||
DocBlock, ModDocBlock, Eof};
|
||||
DocBlock, ModDocBlock, FieldNum, FieldName, Eof};
|
||||
/**
|
||||
\brief Scanner. The behavior of the scanner is controlled using a token set.
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ protected:
|
|||
std::string m_aux_buffer;
|
||||
|
||||
bool m_in_notation;
|
||||
|
||||
bool m_field_notation{true};
|
||||
|
||||
[[ noreturn ]] void throw_exception(char const * msg);
|
||||
void next();
|
||||
|
|
@ -76,6 +76,7 @@ protected:
|
|||
token_kind read_char();
|
||||
token_kind read_hex_number();
|
||||
token_kind read_number();
|
||||
void read_field_idx();
|
||||
token_kind read_key_cmd_id();
|
||||
token_kind read_quoted_symbol();
|
||||
void read_doc_block_core();
|
||||
|
|
@ -107,6 +108,12 @@ public:
|
|||
};
|
||||
|
||||
bool in_notation() const { return m_in_notation; }
|
||||
|
||||
class field_notation_scope : public flet<bool> {
|
||||
public:
|
||||
field_notation_scope(scanner & s, bool flag):
|
||||
flet<bool>(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 */
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue