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

chore(frontends/lean): remove some of the tactic support

Browse source
This commit is contained in:
Leonardo de Moura 2016-04-25 15:26:56 -07:00
parent de64750621
commit d88098f38d
33 changed files with 105 additions and 1127 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/order.lean
View file

@ -495,8 +495,8 @@ definition weak_order_dual {A : Type} (wo : weak_order A) : weak_order A :=
⦃ weak_order,
le := λx y, y ≤ x,
le_refl := le.refl,
le_trans := take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
le_antisymm := take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
le_trans := sorry, -- take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
le_antisymm := sorry ⦄ -- take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
lemma le_dual_eq_le {A : Type} (wo : weak_order A) (a b : A) :
@le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b =

32
library/data/list/comb.lean
View file

@ -31,9 +31,9 @@ definition map (f : A → B) : list A → list B
| [] := []
| (a :: l) := f a :: map l
theorem map_nil (f : A → B) : map f [] = []
theorem map_nil (f : A → B) : map f [] = [] := rfl
theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l
theorem map_cons (f : A → B) (a : A) (l : list A) : map f (a :: l) = f a :: map f l := rfl
lemma map_concat (f : A → B) (a : A) : Πl, map f (concat a l) = concat (f a) (map f l)
| nil := rfl
@ -140,7 +140,7 @@ definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
| [] := []
| (a::l) := if p a then a :: filter l else filter l
theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = []
theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = [] := rfl
theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
λ l pa, if_pos pa
@ -206,17 +206,17 @@ definition foldl (f : A → B → A) : A → list B → A
| a [] := a
| a (b :: l) := foldl (f a b) l
theorem foldl_nil [simp] (f : A → B → A) (a : A) : foldl f a [] = a
theorem foldl_nil [simp] (f : A → B → A) (a : A) : foldl f a [] = a := rfl
theorem foldl_cons [simp] (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l
theorem foldl_cons [simp] (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l := rfl
definition foldr (f : A → B → B) : B → list A → B
| b [] := b
| b (a :: l) := f a (foldr b l)
theorem foldr_nil [simp] (f : A → B → B) (b : B) : foldr f b [] = b
theorem foldr_nil [simp] (f : A → B → B) (b : B) : foldr f b [] = b := rfl
theorem foldr_cons [simp] (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l)
theorem foldr_cons [simp] (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l) := rfl
section foldl_eq_foldr
-- foldl and foldr coincide when f is commutative and associative
@ -269,11 +269,11 @@ foldr (λ a r, p a ∧ r) true l
definition any (l : list A) (p : A → Prop) : Prop :=
foldr (λ a r, p a ∨ r) false l
theorem all_nil_eq [simp] (p : A → Prop) : all [] p = true
theorem all_nil_eq [simp] (p : A → Prop) : all [] p = true := rfl
theorem all_nil (p : A → Prop) : all [] p := trivial
theorem all_cons_eq (p : A → Prop) (a : A) (l : list A) : all (a::l) p = (p a ∧ all l p)
theorem all_cons_eq (p : A → Prop) (a : A) (l : list A) : all (a::l) p = (p a ∧ all l p) := rfl
theorem all_cons {p : A → Prop} {a : A} {l : list A} (H1 : p a) (H2 : all l p) : all (a::l) p :=
and.intro H1 H2
@ -290,9 +290,9 @@ assume pa alllp, and.intro pa alllp
theorem all_implies {p q : A → Prop} : ∀ {l}, all l p → (∀ x, p x → q x) → all l q
| [] h₁ h₂ := trivial
| (a::l) h₁ h₂ :=
have all l q, from all_implies (all_of_all_cons h₁) h₂,
have h₃ : all l q, from all_implies (all_of_all_cons h₁) h₂,
have q a, from h₂ a (of_all_cons h₁),
all_cons_of_all this `all l q`
all_cons_of_all this h₃
theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p → p a
:= sorry
@ -312,9 +312,9 @@ theorem all_of_forall {p : A → Prop} : ∀ {l}, (∀a, a ∈ l → p a) → al
| (a::l) H := all_cons (H a !mem_cons)
(all_of_forall (λ a' H', H a' (mem_cons_of_mem _ H')))
theorem any_nil [simp] (p : A → Prop) : any [] p = false
theorem any_nil [simp] (p : A → Prop) : any [] p = false := rfl
theorem any_cons [simp] (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p)
theorem any_cons [simp] (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p) := rfl
theorem any_of_mem {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → p a → any l p
:= sorry
@ -374,7 +374,7 @@ definition unzip : list (A × B) → list A × list B
| (la, lb) := (a :: la, b :: lb)
end
theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], [])
theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], []) := rfl
theorem unzip_cons [simp] (a : A) (b : B) (l : list (A × B)) :
unzip ((a, b) :: l) = match unzip l with (la, lb) := (a :: la, b :: lb) end :=
@ -461,10 +461,10 @@ definition product : list A → list B → list (A × B)
| [] l₂ := []
| (a::l₁) l₂ := map (λ b, (a, b)) l₂ ++ product l₁ l₂
theorem nil_product (l : list B) : product (@nil A) l = []
theorem nil_product (l : list B) : product (@nil A) l = [] := rfl
theorem product_cons (a : A) (l₁ : list A) (l₂ : list B)
: product (a::l₁) l₂ = map (λ b, (a, b)) l₂ ++ product l₁ l₂
: product (a::l₁) l₂ = map (λ b, (a, b)) l₂ ++ product l₁ l₂ := rfl
theorem product_nil : ∀ (l : list A), product l (@nil B) = []
| [] := rfl

10
library/data/list/set.lean
View file

@ -360,7 +360,7 @@ definition erase_dup [decidable_eq A] : list A → list A
| [] := []
| (x :: xs) := if x ∈ xs then erase_dup xs else x :: erase_dup xs
theorem erase_dup_nil [decidable_eq A] : erase_dup [] = ([] : list A)
theorem erase_dup_nil [decidable_eq A] : erase_dup [] = ([] : list A) := rfl
theorem erase_dup_cons_of_mem [decidable_eq A] {a : A} {l : list A} : a ∈ l → erase_dup (a::l) = erase_dup l :=
assume ainl, calc
@ -507,9 +507,9 @@ definition upto : nat → list nat
| 0 := []
| (n+1) := n :: upto n
theorem upto_nil : upto 0 = nil
theorem upto_nil : upto 0 = nil := rfl
theorem upto_succ (n : nat) : upto (succ n) = n :: upto n
theorem upto_succ (n : nat) : upto (succ n) = n :: upto n := rfl
theorem length_upto : ∀ n, length (upto n) = n
:= sorry
@ -575,7 +575,7 @@ definition union : list A → list A → list A
| [] l₂ := l₂
| (a::l₁) l₂ := if a ∈ l₂ then union l₁ l₂ else a :: union l₁ l₂
theorem nil_union (l : list A) : union [] l = l
theorem nil_union (l : list A) : union [] l = l := rfl
theorem union_cons_of_mem {a : A} {l₂} : ∀ (l₁), a ∈ l₂ → union (a::l₁) l₂ = union l₁ l₂ :=
take l₁, assume ainl₂, calc
@ -806,7 +806,7 @@ definition inter : list A → list A → list A
| [] l₂ := []
| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
theorem inter_nil (l : list A) : inter [] l = []
theorem inter_nil (l : list A) : inter [] l = [] := rfl
theorem inter_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → inter (a::l₁) l₂ = a :: inter l₁ l₂ :=
assume i, if_pos i

2
library/data/list/sort.lean
View file

@ -193,7 +193,7 @@ lemma strongly_sorted_sort_aux : ∀ {n : nat} {l : list A} (h : length l = n),
suppose x ∈ sort_aux R n (erase m l) leq,
have x ∈ erase m l, from mem_perm (sort_aux_perm R leq) this,
have x ∈ l, from mem_of_mem_erase this,
show R m x, from of_mem_of_all this `all l (R m)`),
show R m x, from of_mem_of_all this sorry), -- `all l (R m)`),
strongly_sorted.step hall ss
variable {R}

16
library/data/list/sorted.lean
View file

@ -33,10 +33,10 @@ sorry -- begin intros a l h, cases h, split, repeat assumption end
lemma sorted.rect_on {P : list A → Type} : ∀ {l}, sorted R l → P [] → (∀ a l, sorted R l → P l → hd_rel R a l → P (a::l)) → P l
| [] s h₁ h₂ := h₁
| (a::l) s h₁ h₂ :=
have hd_rel R a l, from and.left (sorted_inv s),
have sorted R l, from and.right (sorted_inv s),
have P l, from sorted.rect_on this h₁ h₂,
h₂ a l `sorted R l` `P l` `hd_rel R a l`
have aux₁ : hd_rel R a l, from and.left (sorted_inv s),
have aux₂ : sorted R l, from and.right (sorted_inv s),
have aux₃ : P l, from sorted.rect_on aux₂ h₁ h₂,
h₂ a l aux₂ aux₃ aux₁
lemma sorted_singleton (a : A) : sorted R [a] :=
sorted.step !hd_rel.base !sorted.base
@ -70,9 +70,9 @@ lemma sorted_of_strongly_sorted : ∀ {l}, strongly_sorted R l → sorted R l
| [] h := !sorted.base
| [a] h := !sorted_singleton
| (a::b::l) (strongly_sorted.step h₁ h₂) :=
have hd_rel R a (b::l), from hd_rel.step _ (of_all_cons h₁),
have aux : hd_rel R a (b::l), from hd_rel.step _ (of_all_cons h₁),
have sorted R (b::l), from sorted_of_strongly_sorted h₂,
sorted.step `hd_rel R a (b::l)` `sorted R (b::l)`
sorted.step aux this
lemma sorted_extends (trans : transitive R) : ∀ {a l}, sorted R (a::l) → all l (R a)
:= sorry
@ -94,9 +94,9 @@ theorem strongly_sorted_of_sorted_of_transitive (trans : transitive R) : ∀ {l}
| [] h := !strongly_sorted.base
| (a::l) h :=
have sorted R l, from and.right (sorted_inv h),
have strongly_sorted R l, from strongly_sorted_of_sorted_of_transitive this,
have aux : strongly_sorted R l, from strongly_sorted_of_sorted_of_transitive this,
have all l (R a), from sorted_extends trans h,
strongly_sorted.step `all l (R a)` `strongly_sorted R l`
strongly_sorted.step this aux
open perm

6
library/data/nat/find.lean
View file

@ -100,9 +100,9 @@ match x with
| 0 := λ f l0, by_cases
(λ p0 : p 0, tag 0 p0)
(suppose ¬ p 0,
have lbp 1, from lbp_succ l0 this,
have 1 ≺ 0, from and.intro (lt.base 0) `lbp 1`,
f 1 `1 ≺ 0` `lbp 1`)
have h₁ : lbp 1, from lbp_succ l0 this,
have 1 ≺ 0, from and.intro (lt.base 0) h₁,
f 1 this h₁)
| (succ n) := λ f lsn, by_cases
(suppose p (succ n), tag (succ n) this)
(suppose ¬ p (succ n),

26
library/data/num.lean
View file

@ -10,9 +10,9 @@ namespace pos_num
theorem succ_not_is_one (a : pos_num) : is_one (succ a) = ff :=
pos_num.induction_on a rfl (take n iH, rfl) (take n iH, rfl)
theorem succ_one : succ one = bit0 one
theorem succ_bit1 (a : pos_num) : succ (bit1 a) = bit0 (succ a)
theorem succ_bit0 (a : pos_num) : succ (bit0 a) = bit1 a
theorem succ_one : succ one = bit0 one := rfl
theorem succ_bit1 (a : pos_num) : succ (bit1 a) = bit0 (succ a) := rfl
theorem succ_bit0 (a : pos_num) : succ (bit0 a) = bit1 a := rfl
theorem ne_of_bit0_ne_bit0 {a b : pos_num} (H₁ : bit0 a ≠ bit0 b) : a ≠ b :=
suppose a = b,
@ -35,16 +35,16 @@ namespace pos_num
section
variables (a b : pos_num)
theorem one_add_one : one + one = bit0 one
theorem one_add_bit0 : one + (bit0 a) = bit1 a
theorem one_add_bit1 : one + (bit1 a) = succ (bit1 a)
theorem bit0_add_one : (bit0 a) + one = bit1 a
theorem bit1_add_one : (bit1 a) + one = succ (bit1 a)
theorem bit0_add_bit0 : (bit0 a) + (bit0 b) = bit0 (a + b)
theorem bit0_add_bit1 : (bit0 a) + (bit1 b) = bit1 (a + b)
theorem bit1_add_bit0 : (bit1 a) + (bit0 b) = bit1 (a + b)
theorem bit1_add_bit1 : (bit1 a) + (bit1 b) = succ (bit1 (a + b))
theorem one_mul : one * a = a
theorem one_add_one : one + one = bit0 one := rfl
theorem one_add_bit0 : one + (bit0 a) = bit1 a := rfl
theorem one_add_bit1 : one + (bit1 a) = succ (bit1 a) := rfl
theorem bit0_add_one : (bit0 a) + one = bit1 a := rfl
theorem bit1_add_one : (bit1 a) + one = succ (bit1 a) := rfl
theorem bit0_add_bit0 : (bit0 a) + (bit0 b) = bit0 (a + b) := rfl
theorem bit0_add_bit1 : (bit0 a) + (bit1 b) = bit1 (a + b) := rfl
theorem bit1_add_bit0 : (bit1 a) + (bit0 b) = bit1 (a + b) := rfl
theorem bit1_add_bit1 : (bit1 a) + (bit1 b) = succ (bit1 (a + b)) := rfl
theorem one_mul : one * a = a := rfl
end
theorem mul_one : ∀ a, a * one = a

8
library/init/tactic.lean
View file

@ -104,6 +104,7 @@ definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
-- with_options_tac is just a marker for the builtin 'with_attributes' notation
definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : tactic := builtin
/-
definition simp : tactic := #tactic with_options [blast.strategy "simp"] blast
definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
definition simp_topdown : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
@ -112,6 +113,7 @@ definition rec_simp : tactic := #tactic with_options [blast.strategy "rec_s
definition rec_inst_simp : tactic := #tactic with_options [blast.strategy "rec_ematch_simp"] blast
definition grind : tactic := #tactic with_options [blast.strategy "grind"] blast
definition grind_simp : tactic := #tactic with_options [blast.strategy "grind_simp"] blast
-/
definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
@ -151,11 +153,11 @@ definition try (t : tactic) : tactic := or_else t id
definition repeat1 (t : tactic) : tactic := and_then t (repeat t)
definition focus (t : tactic) : tactic := focus_at t 0
definition determ (t : tactic) : tactic := at_most t 1
definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
-- definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
definition do (n : num) (t : tactic) : tactic :=
nat.rec id (λn t', and_then t t') (nat.of_num n)
end tactic
tactic_infixl `;`:15 := tactic.and_then
tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
-- tactic_infixl `;`:15 := tactic.and_then
-- tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
--tactic_notation `replace` s `with` t := tactic.replace_tac s t

4
library/tools/helper_tactics.lean
View file

@ -12,6 +12,6 @@ import logic.eq
open tactic
namespace helper_tactics
definition apply_refl := apply eq.refl
tactic_hint apply_refl
-- definition apply_refl := apply eq.refl
-- tactic_hint apply_refl
end helper_tactics

14
src/frontends/lean/CMakeLists.txt
View file

@ -3,15 +3,19 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
inductive_cmd.cpp dependencies.cpp
begin_end_annotation.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
pp.cpp theorem_queue.cpp
structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
coercion_elaborator.cpp info_tactic.cpp
coercion_elaborator.cpp
init_module.cpp
parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
type_util.cpp elaborator_exception.cpp local_ref_info.cpp
obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
parse_with_options_tactic.cpp opt_cmd.cpp prenum.cpp
parse_with_attributes_tactic.cpp print_cmd.cpp elaborator_context.cpp elaborator.cpp
opt_cmd.cpp prenum.cpp
print_cmd.cpp elaborator_context.cpp elaborator.cpp
# LEGACY
old_elaborator.cpp
# begin_end_annotation.cpp tactic_hint.cpp
# info_tactic.cpp
# parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
# parse_with_options_tactic.cpp
#parse_with_attributes_tactic.cpp
)

30
src/frontends/lean/begin_end_annotation.cpp
View file

@ -1,30 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "library/annotation.h"
namespace lean {
static name * g_begin_end = nullptr;
static name * g_begin_end_element = nullptr;
expr mk_begin_end_annotation(expr const & e) { return mk_annotation(*g_begin_end, e, nulltag); }
expr mk_begin_end_element_annotation(expr const & e) { return mk_annotation(*g_begin_end_element, e, nulltag); }
bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_end); }
bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
void initialize_begin_end_annotation() {
g_begin_end = new name("begin_end");
g_begin_end_element = new name("begin_end_element");
register_annotation(*g_begin_end);
register_annotation(*g_begin_end_element);
}
void finalize_begin_end_annotation() {
delete g_begin_end;
delete g_begin_end_element;
}
}

19
src/frontends/lean/begin_end_annotation.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
#include "frontends/lean/cmd_table.h"
namespace lean {
expr mk_begin_end_annotation(expr const & e);
expr mk_begin_end_element_annotation(expr const & e);
bool is_begin_end_annotation(expr const & e);
bool is_begin_end_element_annotation(expr const & e);
void initialize_begin_end_annotation();
void finalize_begin_end_annotation();
}

6
src/frontends/lean/builtin_cmds.cpp
View file

@ -42,9 +42,9 @@ Author: Leonardo de Moura
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/print_cmd.h"
#include "frontends/lean/find_cmd.h"
#include "frontends/lean/begin_end_annotation.h"
// #include "frontends/lean/begin_end_annotation.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/tactic_hint.h"
// #include "frontends/lean/tactic_hint.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parse_table.h"
@ -695,7 +695,7 @@ void init_cmd_table(cmd_table & r) {
register_inductive_cmd(r);
register_structure_cmd(r);
register_notation_cmds(r);
register_tactic_hint_cmd(r);
// register_tactic_hint_cmd(r);
}
static cmd_table * g_cmds = nullptr;

4
src/frontends/lean/builtin_exprs.cpp
View file

@ -27,11 +27,11 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/calc.h"
#include "frontends/lean/begin_end_annotation.h"
// #include "frontends/lean/begin_end_annotation.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/info_tactic.h"
// #include "frontends/lean/info_tactic.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/obtain_expr.h"

139
src/frontends/lean/builtin_tactics.cpp
View file

@ -1,139 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <library/let.h>
#include <library/constants.h>
#include "library/tactic/note_tactic.h"
#include "library/tactic/generalize_tactic.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/parse_rewrite_tactic.h"
#include "frontends/lean/parse_with_options_tactic.h"
#include "frontends/lean/parse_with_attributes_tactic.h"
namespace lean {
namespace notation {
static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_rewrite_tactic(p), pos);
}
static expr parse_xrewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_xrewrite_tactic(p), pos);
}
static expr parse_krewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_krewrite_tactic(p), pos);
}
static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_esimp_tactic(p), pos);
}
static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_unfold_tactic(p), pos);
}
static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_fold_tactic(p), pos);
}
static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const &) {
return args[0];
}
static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
auto id_pos = p.pos();
name id = p.check_atomic_id_next("invalid 'let' tactic, identifier expected");
p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected");
expr value = p.parse_tactic_expr_arg();
// Register value as expandable local expr. Identical to let term parsing, but without surrounding mk_let.
value = p.save_pos(mk_let_value(value), id_pos);
p.add_local_expr(id, value);
// nothing to do, so return the id tactic
return p.save_pos(mk_constant(get_tactic_id_name()), pos);
}
static expr parse_note_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
name id = p.check_atomic_id_next("invalid 'note' tactic, identifier expected");
p.check_token_next(get_assign_tk(), "invalid 'note' tactic, ':=' expected");
expr value = p.parse_tactic_expr_arg();
return p.save_pos(mk_note_tactic_expr(id, value), pos);
}
static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_with_options_tactic(p), pos);
}
static expr parse_with_attributes_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_with_attributes_tactic(p), pos);
}
static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
expr e = p.parse_tactic_expr_arg();
name id;
if (p.curr_is_token(get_as_tk())) {
p.next();
id = p.check_atomic_id_next("invalid 'generalize' tactic, identifier expected");
} else {
if (is_constant(e))
id = const_name(e);
else if (is_local(e))
id = local_pp_name(e);
else
id = name("x");
}
return p.save_pos(mk_generalize_tactic_expr(e, id), pos);
}
parse_table init_tactic_nud_table() {
action Expr(mk_expr_action());
expr x0 = mk_var(0);
parse_table r;
r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
r = r.add({transition("krewrite", mk_ext_action(parse_krewrite_tactic_expr))}, x0);
r = r.add({transition("xrewrite", mk_ext_action(parse_xrewrite_tactic_expr))}, x0);
r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0);
r = r.add({transition("generalize", mk_ext_action(parse_generalize_tactic))}, x0);
r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0);
r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0);
r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0);
r = r.add({transition("note", mk_ext_action(parse_note_tactic))}, x0);
r = r.add({transition("with_options", mk_ext_action(parse_with_options_tactic_expr))}, x0);
r = r.add({transition("with_attributes", mk_ext_action(parse_with_attributes_tactic_expr))}, x0);
r = r.add({transition("with_attrs", mk_ext_action(parse_with_attributes_tactic_expr))}, x0);
return r;
}
parse_table init_tactic_led_table() {
parse_table r(false);
return r;
}
}
static parse_table * g_nud_table = nullptr;
static parse_table * g_led_table = nullptr;
parse_table get_builtin_tactic_nud_table() {
return *g_nud_table;
}
parse_table get_builtin_tactic_led_table() {
return *g_led_table;
}
void initialize_builtin_tactics() {
g_nud_table = new parse_table();
*g_nud_table = notation::init_tactic_nud_table();
g_led_table = new parse_table();
*g_led_table = notation::init_tactic_led_table();
}
void finalize_builtin_tactics() {
delete g_led_table;
delete g_nud_table;
}
}

14
src/frontends/lean/builtin_tactics.h
View file

@ -1,14 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "frontends/lean/parse_table.h"
namespace lean {
parse_table get_builtin_tactic_nud_table();
parse_table get_builtin_tactic_led_table();
void initialize_builtin_tactics();
void finalize_builtin_tactics();
}

3
src/frontends/lean/calc.cpp
View file

@ -28,14 +28,13 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/begin_end_annotation.h"
namespace lean {
static name * g_calc_name = nullptr;
static expr mk_calc_annotation_core(expr const & e) { return mk_annotation(*g_calc_name, e); }
static expr mk_calc_annotation(expr const & pr) {
if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
if (is_by(pr) || /* is_begin_end_annotation(pr) || */ is_sorry(pr)) {
return pr;
} else {
return mk_calc_annotation_core(pr);

58
src/frontends/lean/info_tactic.cpp
View file

@ -1,58 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
LEAN_THREAD_PTR(proof_state const, g_info_proof_state);
optional<proof_state> get_info_tactic_proof_state() {
if (g_info_proof_state) {
return some_proof_state(*g_info_proof_state);
} else {
return none_proof_state();
}
}
void set_info_tactic_proof_state(proof_state const * ps) {
g_info_proof_state = ps;
}
struct scoped_info_tactic_proof_state {
scoped_info_tactic_proof_state(proof_state const & s) {
set_info_tactic_proof_state(&s);
}
~scoped_info_tactic_proof_state() {
set_info_tactic_proof_state(nullptr);
}
};
tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
return tactic1([=](environment const &, io_state const & ios, proof_state const & ps) -> proof_state {
// create dummy variable just to communicate position to the elaborator
expr dummy = mk_sort(mk_level_zero(), e.get_tag());
scoped_info_tactic_proof_state scope(ps);
fn(goal(), ios.get_options(), dummy, none_expr(), substitution(), false);
return ps;
});
}
#define INFO_TAC_NAME name({"tactic", "info"})
expr mk_info_tactic_expr() {
return mk_constant(INFO_TAC_NAME);
}
void initialize_info_tactic() {
register_tac(INFO_TAC_NAME,
[](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
return mk_info_tactic(fn, e);
});
}
void finalize_info_tactic() {
}
}

19
src/frontends/lean/info_tactic.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/proof_state.h"
namespace lean {
expr mk_info_tactic_expr();
/** \brief The tactic framework does not have access to the info manager.
Thus, it cannot store the proof_state there. The info tactic accomplishes
that by (temporarily) saving the proof state in a thread-local storage
that is accessed by the elaborator using this function. */
optional<proof_state> get_info_tactic_proof_state();
void initialize_info_tactic();
void finalize_info_tactic();
}

30
src/frontends/lean/init_module.cpp
View file

@ -9,19 +9,19 @@ Author: Leonardo de Moura
#include "frontends/lean/old_elaborator.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/tactic_hint.h"
// #include "frontends/lean/tactic_hint.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/calc.h"
#include "frontends/lean/begin_end_annotation.h"
// #include "frontends/lean/begin_end_annotation.h"
#include "frontends/lean/builtin_cmds.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/builtin_tactics.h"
// #include "frontends/lean/builtin_tactics.h"
#include "frontends/lean/inductive_cmd.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/parse_table.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/info_tactic.h"
// #include "frontends/lean/info_tactic.h"
#include "frontends/lean/find_cmd.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/pp.h"
@ -31,7 +31,7 @@ Author: Leonardo de Moura
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/nested_declaration.h"
#include "frontends/lean/prenum.h"
#include "frontends/lean/parse_with_attributes_tactic.h"
// #include "frontends/lean/parse_with_attributes_tactic.h"
namespace lean {
void initialize_frontend_lean_module() {
@ -42,19 +42,19 @@ void initialize_frontend_lean_module() {
initialize_parse_table();
initialize_builtin_cmds();
initialize_builtin_exprs();
initialize_builtin_tactics();
// initialize_builtin_tactics();
initialize_elaborator_context();
initialize_old_elaborator();
initialize_scanner();
initialize_parser();
initialize_tactic_hint();
// initialize_tactic_hint();
initialize_parser_config();
initialize_calc();
initialize_begin_end_annotation();
// initialize_begin_end_annotation();
initialize_inductive_cmd();
initialize_structure_cmd();
initialize_info_manager();
initialize_info_tactic();
// initialize_info_tactic();
initialize_pp();
initialize_server();
initialize_find_cmd();
@ -62,10 +62,10 @@ void initialize_frontend_lean_module() {
initialize_obtain_expr();
initialize_decl_cmds();
initialize_nested_declaration();
initialize_with_attributes_tactic();
// initialize_with_attributes_tactic();
}
void finalize_frontend_lean_module() {
finalize_with_attributes_tactic();
// finalize_with_attributes_tactic();
finalize_nested_declaration();
finalize_decl_cmds();
finalize_obtain_expr();
@ -73,19 +73,19 @@ void finalize_frontend_lean_module() {
finalize_find_cmd();
finalize_server();
finalize_pp();
finalize_info_tactic();
// finalize_info_tactic();
finalize_info_manager();
finalize_structure_cmd();
finalize_inductive_cmd();
finalize_begin_end_annotation();
// finalize_begin_end_annotation();
finalize_calc();
finalize_parser_config();
finalize_tactic_hint();
// finalize_tactic_hint();
finalize_parser();
finalize_scanner();
finalize_old_elaborator();
finalize_elaborator_context();
finalize_builtin_tactics();
// finalize_builtin_tactics();
finalize_builtin_exprs();
finalize_builtin_cmds();
finalize_parse_table();

109
src/frontends/lean/old_elaborator.cpp
View file

@ -48,12 +48,11 @@ Author: Leonardo de Moura
#include "library/definitional/equations.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/old_elaborator.h"
#include "frontends/lean/info_tactic.h"
#include "frontends/lean/begin_end_annotation.h"
// #include "frontends/lean/info_tactic.h"
// #include "frontends/lean/begin_end_annotation.h"
#include "frontends/lean/elaborator_exception.h"
#include "frontends/lean/nested_declaration.h"
#include "frontends/lean/calc.h"
@ -740,7 +739,9 @@ expr old_elaborator::visit_app(expr const & e, constraint_seq & cs) {
}
constraint_seq a_cs;
expr d_type = binding_domain(f_type);
if (d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() ||
if (false) {
/*
d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type() ||
d_type == get_tactic_using_expr_type() || d_type == get_tactic_location_type() ||
d_type == get_tactic_with_expr_type()) {
expr const & a = app_arg(e);
@ -755,6 +756,8 @@ expr old_elaborator::visit_app(expr const & e, constraint_seq & cs) {
}
cs += f_cs + a_cs;
return r;
*/
lean_unreachable();
} else {
expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs);
expr a_type = infer_type(a, a_cs);
@ -1976,24 +1979,6 @@ bool old_elaborator::try_using(substitution & subst, expr const & mvar, proof_st
}
}
static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq) {
if (is_begin_end_element_annotation(pre_tac)) {
pre_tac_seq.push_back(get_annotation_arg(pre_tac));
} else if (is_begin_end_annotation(pre_tac)) {
// nested begin-end block
pre_tac_seq.push_back(pre_tac);
} else {
buffer<expr> args;
if (get_app_args(pre_tac, args) == get_and_then_tac_fn()) {
for (expr const & arg : args) {
extract_begin_end_tactics(arg, pre_tac_seq);
}
} else {
throw exception("internal error, invalid begin-end tactic");
}
}
}
void old_elaborator::show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr) {
unsigned line, col;
if (!m_ctx.has_show_goal_at(line, col))
@ -2017,81 +2002,6 @@ void old_elaborator::show_goal(proof_state const & ps, expr const & start, expr
print_lean_info_footer(out.get_stream());
}
bool old_elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
lean_assert(is_begin_end_annotation(pre_tac));
expr end_expr = pre_tac;
expr start_expr = get_annotation_arg(pre_tac);
buffer<expr> pre_tac_seq;
extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
for (expr ptac : pre_tac_seq) {
if (is_begin_end_annotation(ptac)) {
goals gs = ps.get_goals();
if (!gs)
throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac);
goal g = head(gs);
expr mvar = g.get_mvar();
proof_state focus_ps(ps, goals(g));
if (!try_using_begin_end(subst, mvar, focus_ps, ptac))
return false;
ps = proof_state(ps, tail(gs), subst);
} else {
show_goal(ps, start_expr, end_expr, ptac);
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {
try {
ps = ps.update_report_failure(true);
proof_state_seq seq = (*tac)(env(), ios(), ps);
auto r = seq.pull();
if (!r) {
// tactic failed to produce any result
display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
return false;
}
if (m_ctx.m_flycheck_goals) {
if (auto p = pip()->get_pos_info(ptac)) {
auto out = regular(env(), ios(), m_tc->get_type_context());
flycheck_information info(ios());
if (info.enabled()) {
display_information_pos(out, pip()->get_file_name(), p->first, p->second);
out << " proof state:\n" << ps.pp(out.get_formatter()) << "\n";
}
}
}
ps = r->first;
} catch (tactic_exception & ex) {
display_tactic_exception(ex, ps, ptac);
return false;
} catch (exception &) {
throw;
} catch (throwable & ex) {
auto out = regular(env(), ios(), m_tc->get_type_context());
flycheck_error err(ios());
if (!err.enabled() || save_error(pip(), ptac)) {
display_error_pos(out, pip(), ptac);
out << ex.what() << "\nproof state:\n";
out << ps.pp(out.get_formatter()) << "\n";
}
return false;
}
} else {
return false;
}
}
}
show_goal(ps, start_expr, end_expr, end_expr);
if (!empty(ps.get_goals())) {
display_unsolved_subgoals(mvar, ps, pre_tac);
return false;
} else {
subst = ps.get_subst();
lean_assert(subst.is_assigned(mvar));
expr v = subst.instantiate(mvar);
subst.assign(mlocal_name(mvar), v);
return true;
}
}
// The parameters univs_fixed is true if the elaborator has instantiated the universe metavariables with universe parameters.
// See issue #771
void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta) {
@ -2110,6 +2020,7 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name
throw_elaborator_exception("failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) "
"(solution: provide type explicitly)", mvar);
}
/*
proof_state ps = to_proof_state(*meta, type, subst);
if (auto pre_tac = get_pre_tactic_for(mvar)) {
if (is_begin_end_annotation(*pre_tac)) {
@ -2134,6 +2045,8 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name
}
}
}
*/
return;
}
/** \brief Execute \c fn on every metavariable occurring in \c e.
@ -2408,9 +2321,11 @@ elaborate_result old_elaborator::elaborate_nested(list<expr> const & ctx, option
expr const & n, bool use_tactic_hints,
substitution const & subst, bool report_unassigned) {
if (infom()) {
/*
if (auto ps = get_info_tactic_proof_state()) {
save_proof_state_info(*ps, n);
}
*/
}
expr e = translate(env(), ctx, n);
metavar_closure cls;

226
src/frontends/lean/parse_rewrite_tactic.cpp
View file

@ -1,226 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/tactic/rewrite_tactic.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parse_tactic_location.h"
namespace lean {
static optional<expr> parse_pattern(parser & p) {
if (p.curr_is_token(get_lcurly_tk())) {
p.next();
expr r = p.parse_tactic_expr_arg();
p.check_token_next(get_rcurly_tk(), "invalid rewrite pattern, '}' expected");
return some_expr(r);
} else {
return none_expr();
}
}
static expr parse_rule(parser & p, bool use_paren) {
if (use_paren) {
if (p.curr_is_token(get_lparen_tk())) {
p.next();
expr r = p.parse_tactic_expr_arg();
p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ')' expected");
return r;
} else {
return p.parse_tactic_id_arg();
}
} else {
return p.parse_tactic_expr_arg();
}
}
static void check_not_in_theorem_queue(parser & p, name const & n, pos_info const & pos) {
if (p.in_theorem_queue(n)) {
throw parser_error(sstream() << "invalid 'rewrite' tactic, cannot unfold '" << n << "' "
<< "which is still in the theorem queue. Use command 'reveal " << n << "' "
<< "to access its definition.", pos);
}
}
static expr parse_rewrite_unfold_core(parser & p, bool force_unfold) {
buffer<name> to_unfold;
if (p.curr_is_token(get_lbracket_tk())) {
p.next();
while (true) {
auto pos = p.pos();
to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
check_not_in_theorem_queue(p, to_unfold.back(), pos);
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid unfold rewrite step, ',' or ']' expected");
} else {
auto pos = p.pos();
to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '[' expected"));
check_not_in_theorem_queue(p, to_unfold.back(), pos);
}
location loc = parse_tactic_location(p);
return mk_rewrite_unfold(to_list(to_unfold), force_unfold, loc);
}
static expr parse_rewrite_unfold(parser & p, bool force_unfold) {
lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()));
p.next();
return parse_rewrite_unfold_core(p, force_unfold);
}
// If use_paren is true, then lemmas must be identifiers or be wrapped with parenthesis
static expr parse_rewrite_element(parser & p, bool use_paren) {
if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
bool force_unfold = true;
return parse_rewrite_unfold(p, force_unfold);
}
if (p.curr_is_token(get_down_tk())) {
p.next();
expr e = p.parse_tactic_expr_arg();
location loc = parse_tactic_location(p);
return mk_rewrite_fold(e, loc);
}
bool symm = false;
if (p.curr_is_token(get_sub_tk())) {
p.next();
symm = true;
}
if (p.curr_is_numeral()) {
unsigned n = p.parse_small_nat();
if (p.curr_is_token(get_greater_tk())) {
p.next();
optional<expr> pat = parse_pattern(p);
expr H = parse_rule(p, use_paren);
location loc = parse_tactic_location(p);
return mk_rewrite_at_most_n(pat, H, symm, n, loc);
} else {
optional<expr> pat = parse_pattern(p);
expr H = parse_rule(p, use_paren);
location loc = parse_tactic_location(p);
return mk_rewrite_exactly_n(pat, H, symm, n, loc);
}
} else if (p.curr_is_token(get_star_tk())) {
p.next();
optional<expr> pat = parse_pattern(p);
expr H = parse_rule(p, use_paren);
location loc = parse_tactic_location(p);
return mk_rewrite_zero_or_more(pat, H, symm, loc);
} else if (p.curr_is_token(get_plus_tk())) {
p.next();
optional<expr> pat = parse_pattern(p);
expr H = parse_rule(p, use_paren);
location loc = parse_tactic_location(p);
return mk_rewrite_one_or_more(pat, H, symm, loc);
} else if (p.curr_is_token(get_triangle_tk()) || p.curr_is_token(get_greater_tk())) {
p.next();
if (p.curr_is_token(get_star_tk())) {
p.next();
location loc = parse_tactic_location(p);
return mk_rewrite_reduce(loc);
} else {
expr e = p.parse_tactic_expr_arg();
location loc = parse_tactic_location(p);
return mk_rewrite_reduce_to(e, loc);
}
} else {
optional<expr> pat = parse_pattern(p);
expr H = parse_rule(p, use_paren);
location loc = parse_tactic_location(p);
return mk_rewrite_once(pat, H, symm, loc);
}
}
void parse_rewrite_tactic_elems(parser & p, buffer<expr> & elems) {
if (p.curr_is_token(get_lbracket_tk())) {
p.next();
while (!p.curr_is_token(get_rbracket_tk())) {
auto pos = p.pos();
elems.push_back(p.save_pos(parse_rewrite_element(p, false), pos));
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.next();
} else {
auto pos = p.pos();
elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos));
}
}
expr parse_rewrite_tactic(parser & p) {
buffer<expr> elems;
parse_rewrite_tactic_elems(p, elems);
return mk_rewrite_tactic_expr(elems);
}
expr parse_xrewrite_tactic(parser & p) {
buffer<expr> elems;
parse_rewrite_tactic_elems(p, elems);
return mk_xrewrite_tactic_expr(elems);
}
expr parse_krewrite_tactic(parser & p) {
buffer<expr> elems;
parse_rewrite_tactic_elems(p, elems);
return mk_krewrite_tactic_expr(elems);
}
expr parse_esimp_tactic(parser & p) {
buffer<expr> elems;
auto pos = p.pos();
bool force_unfold = false;
if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
elems.push_back(p.save_pos(parse_rewrite_unfold(p, force_unfold), pos));
} else if (p.curr_is_token(get_lbracket_tk())) {
elems.push_back(p.save_pos(parse_rewrite_unfold_core(p, force_unfold), pos));
} else {
location loc = parse_tactic_location(p);
elems.push_back(p.save_pos(mk_rewrite_reduce(loc), pos));
}
return mk_rewrite_tactic_expr(elems);
}
expr parse_unfold_tactic(parser & p) {
buffer<expr> elems;
auto pos = p.pos();
bool force_unfold = true;
if (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid unfold tactic, identifier expected");
check_not_in_theorem_queue(p, c, pos);
location loc = parse_tactic_location(p);
elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), force_unfold, loc), pos));
} else if (p.curr_is_token(get_lbracket_tk())) {
elems.push_back(p.save_pos(parse_rewrite_unfold_core(p, force_unfold), pos));
} else {
throw parser_error("invalid unfold tactic, identifier or `[` expected", pos);
}
return mk_rewrite_tactic_expr(elems);
}
expr parse_fold_tactic(parser & p) {
buffer<expr> elems;
auto pos = p.pos();
if (p.curr_is_token(get_lbracket_tk())) {
p.next();
while (true) {
auto pos = p.pos();
expr e = p.parse_tactic_expr_arg();
location loc = parse_tactic_location(p);
elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid 'fold' tactic, ',' or ']' expected");
} else {
expr e = p.parse_tactic_expr_arg();
location loc = parse_tactic_location(p);
elems.push_back(p.save_pos(mk_rewrite_fold(e, loc), pos));;
}
return mk_rewrite_tactic_expr(elems);
}
}

18
src/frontends/lean/parse_rewrite_tactic.h
View file

@ -1,18 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
class parser;
expr parse_rewrite_tactic(parser & p);
expr parse_krewrite_tactic(parser & p);
expr parse_xrewrite_tactic(parser & p);
expr parse_esimp_tactic(parser & p);
expr parse_unfold_tactic(parser & p);
expr parse_fold_tactic(parser & p);
}

96
src/frontends/lean/parse_tactic_location.cpp
View file

@ -1,96 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/tactic/location.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parse_tactic_location.h"
namespace lean {
static occurrence parse_occurrence(parser & p) {
bool is_pos = true;
if (p.curr_is_token(get_sub_tk())) {
p.next();
is_pos = false;
if (!p.curr_is_token(get_lcurly_tk()))
throw parser_error("invalid tactic location, '{' expected", p.pos());
}
if (p.curr_is_token(get_lcurly_tk())) {
p.next();
buffer<unsigned> occs;
while (true) {
auto pos = p.pos();
unsigned i = p.parse_small_nat();
if (i == 0)
throw parser_error("invalid tactic location, first occurrence is 1", pos);
occs.push_back(i);
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rcurly_tk(), "invalid tactic location, '}' or ',' expected");
if (is_pos)
return occurrence::mk_occurrences(occs);
else
return occurrence::mk_except_occurrences(occs);
} else {
return occurrence();
}
}
location parse_tactic_location(parser & p) {
if (p.curr_is_token(get_at_tk())) {
p.next();
if (p.curr_is_token(get_star_tk())) {
p.next();
if (p.curr_is_token(get_turnstile_tk())) {
p.next();
if (p.curr_is_token(get_star_tk())) {
// at * |- *
return location::mk_everywhere();
} else {
// at * |-
return location::mk_all_hypotheses();
}
} else {
// at *
return location::mk_everywhere();
}
} else if (p.curr_is_token(get_lparen_tk())) {
p.next();
buffer<name> hyps;
buffer<occurrence> hyp_occs;
while (true) {
hyps.push_back(p.get_name_val());
p.next();
hyp_occs.push_back(parse_occurrence(p));
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rparen_tk(), "invalid tactic location, ')' expected");
if (p.curr_is_token(get_turnstile_tk())) {
p.next();
occurrence goal_occ = parse_occurrence(p);
return location::mk_at(goal_occ, hyps, hyp_occs);
} else {
return location::mk_hypotheses_at(hyps, hyp_occs);
}
} else if (p.curr_is_token(get_lcurly_tk()) || p.curr_is_token(get_sub_tk())) {
occurrence o = parse_occurrence(p);
return location::mk_goal_at(o);
} else {
buffer<name> hyps;
buffer<occurrence> hyp_occs;
hyps.push_back(p.check_id_next("invalid tactic location, identifier expected"));
hyp_occs.push_back(parse_occurrence(p));
return location::mk_hypotheses_at(hyps, hyp_occs);
}
} else {
return location::mk_goal_only();
}
}
}

13
src/frontends/lean/parse_tactic_location.h
View file

@ -1,13 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/location.h"
namespace lean {
class parser;
location parse_tactic_location(parser & p);
}

120
src/frontends/lean/parse_with_attributes_tactic.cpp
View file

@ -1,120 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "library/constants.h"
#include "library/scoped_ext.h"
#include "library/kernel_serializer.h"
#include "library/tactic/expr_to_tactic.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/decl_attributes.h"
namespace lean {
static name * g_name = nullptr;
static std::string * g_opcode = nullptr;
// Auxiliary macro for wrapping decl_attributes object as an expression
class attributes_macro_cell : public macro_definition_cell {
decl_attributes m_decl;
public:
attributes_macro_cell(decl_attributes const & decl):m_decl(decl) {}
virtual name get_name() const { return *g_name; }
virtual void write(serializer & s) const { s << *g_opcode; m_decl.write(s); }
virtual expr check_type(expr const &, abstract_type_context &, bool) const {
return mk_constant(get_tactic_expr_name());
}
virtual optional<expr> expand(expr const &, abstract_type_context &) const {
return some_expr(mk_constant(get_tactic_expr_builtin_name()));
}
virtual bool operator==(macro_definition_cell const & other) const {
if (auto o = dynamic_cast<attributes_macro_cell const *>(&other))
return m_decl == o->m_decl;
return false;
}
decl_attributes const & get_attrs() const { return m_decl; }
};
expr mk_attributes_expr(decl_attributes const & d) {
macro_definition def(new attributes_macro_cell(d));
return mk_macro(def);
}
bool is_attributes_expr(expr const & e) {
return is_macro(e) && macro_def(e).get_name() == *g_name;
}
decl_attributes const & get_attributes_expr_attributes(expr const & e) {
lean_assert(is_attributes_expr(e));
return static_cast<attributes_macro_cell const*>(macro_def(e).raw())->get_attrs();
}
static expr * g_with_attributes_tac = nullptr;
expr mk_with_attributes_tactic_expr(decl_attributes const & a, buffer<name> const & cs, expr const & t) {
return mk_app(*g_with_attributes_tac, mk_attributes_expr(a), ids_to_tactic_expr(cs), t);
}
tactic with_attributes(decl_attributes const & d, list<name> const & cs, tactic const & t) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
environment new_env = env;
for (name const & c : cs)
new_env = d.apply(new_env, ios, c, get_namespace(new_env));
return t(new_env, ios, s);
});
}
expr parse_with_attributes_tactic(parser & p) {
buffer<name> cs;
bool persistent = false;
bool abbrev = false;
decl_attributes attributes(abbrev, persistent);
name c = p.check_constant_next("invalid 'with_attributes' tactical, constant expected");
cs.push_back(c);
while (p.curr_is_identifier()) {
cs.push_back(p.check_constant_next("invalid 'with_attributes' tactical, constant expected"));
}
attributes.parse(p);
expr t = p.parse_tactic(get_max_prec());
return mk_with_attributes_tactic_expr(attributes, cs, t);
}
void initialize_with_attributes_tactic() {
g_name = new name("attributes");
g_opcode = new std::string("ATTRS");
register_macro_deserializer(*g_opcode,
[](deserializer & d, unsigned num, expr const *) {
if (num > 0)
throw corrupted_stream_exception();
decl_attributes attrs;
attrs.read(d);
return mk_attributes_expr(attrs);
});
name with_attributes_tac_name{"tactic", "with_attributes_tac"};
g_with_attributes_tac = new expr(Const(with_attributes_tac_name));
register_tac(with_attributes_tac_name,
[=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 3)
throw expr_to_tactic_exception(e, "invalid 'with_attributes' tactical, it must have two arguments");
check_tactic_expr(args[0], "invalid 'with_attributes' tactical, invalid argument");
expr attrs = get_tactic_expr_expr(args[0]);
if (!is_attributes_expr(attrs))
throw expr_to_tactic_exception(args[0], "invalid 'with_attributes' tactical, invalid argument");
buffer<name> cs;
get_tactic_id_list_elements(args[1], cs, "invalid 'with_attributes' tactical, invalid argument");
tactic t = expr_to_tactic(tc, fn, args[2], p);
return with_attributes(get_attributes_expr_attributes(attrs), to_list(cs), t);
});
}
void finalize_with_attributes_tactic() {
delete g_name;
delete g_opcode;
delete g_with_attributes_tac;
}
}

15
src/frontends/lean/parse_with_attributes_tactic.h
View file

@ -1,15 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
class parser;
expr parse_with_attributes_tactic(parser & p);
void initialize_with_attributes_tactic();
void finalize_with_attributes_tactic();
}

49
src/frontends/lean/parse_with_options_tactic.cpp
View file

@ -1,49 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "library/tactic/with_options_tactic.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/util.h"
namespace lean {
expr parse_with_options_tactic(parser & p) {
options o;
p.check_token_next(get_lbracket_tk(), "invalid 'with_options' tactical, '[' expected");
while (true) {
auto id_kind = parse_option_name(p, "invalid 'with_options' tactical, identifier (i.e., option name) expected");
name id = id_kind.first;
option_kind k = id_kind.second;
if (k == BoolOption) {
if (p.curr_is_token_or_id(get_true_tk()))
o = o.update(id, true);
else if (p.curr_is_token_or_id(get_false_tk()))
o = o.update(id, false);
else
throw parser_error("invalid Boolean option value, 'true' or 'false' expected", p.pos());
p.next();
} else if (k == StringOption) {
if (!p.curr_is_string())
throw parser_error("invalid option value, given option is not a string", p.pos());
o = o.update(id, p.get_str_val());
p.next();
} else if (k == DoubleOption) {
o = o.update(id, p.parse_double());
} else if (k == UnsignedOption || k == IntOption) {
o = o.update(id, p.parse_small_nat());
} else {
throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos());
}
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid 'with_options' tactical, ']' expected");
expr t = p.parse_tactic(get_max_prec());
return mk_with_options_tactic_expr(o, t);
}
}

13
src/frontends/lean/parse_with_options_tactic.h
View file

@ -1,13 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
class parser;
expr parse_with_options_tactic(parser & p);
}

6
src/frontends/lean/parser.cpp
View file

@ -49,8 +49,8 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
#include "frontends/lean/notation_cmd.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/parse_rewrite_tactic.h"
#include "frontends/lean/parse_tactic_location.h"
// #include "frontends/lean/parse_rewrite_tactic.h"
// #include "frontends/lean/parse_tactic_location.h"
#include "frontends/lean/update_environment_exception.h"
#include "frontends/lean/local_ref_info.h"
#include "frontends/lean/opt_cmd.h"
@ -2004,9 +2004,11 @@ expr parser::parse_tactic_nud() {
check_token_next(get_with_tk(), "invalid tactic expression, 'with' expected");
expr e = parse_expr();
r = mk_app(r, e, id_pos);
/*
} else if (is_tactic_location_type(d)) {
location l = parse_tactic_location(*this);
r = mk_app(r, mk_location_expr(l), id_pos);
*/
} else {
unsigned rbp;
if ((arity == 1) ||

8
src/frontends/lean/parser_config.cpp
View file

@ -11,7 +11,6 @@ Author: Leonardo de Moura
#include "library/kernel_serializer.h"
#include "frontends/lean/parser_config.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/builtin_tactics.h"
#include "frontends/lean/builtin_cmds.h"
namespace lean {
@ -227,9 +226,10 @@ struct notation_state {
m_nud(get_builtin_nud_table()),
m_led(get_builtin_led_table()),
m_reserved_nud(true),
m_reserved_led(false),
m_tactic_nud(get_builtin_tactic_nud_table()),
m_tactic_led(get_builtin_tactic_led_table()) {
m_reserved_led(false)
{
// m_tactic_nud(get_builtin_tactic_nud_table()),
// m_tactic_led(get_builtin_tactic_led_table()) {
}
parse_table & nud(notation_entry_group g) {

96
src/frontends/lean/tactic_hint.cpp
View file

@ -1,96 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "util/sstream.h"
#include "kernel/type_checker.h"
#include "library/scoped_ext.h"
#include "library/constants.h"
#include "library/kernel_serializer.h"
#include "library/tactic/tactic.h"
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/cmd_table.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
namespace lean {
typedef list<expr> tactic_hints;
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
struct tactic_hint_config {
typedef tactic_hints state;
typedef expr entry;
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
s = cons(e, filter(s, [&](expr const & e1) { return e1 != e; }));
}
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e;
}
static entry read_entry(deserializer & d) {
entry e;
d >> e;
return e;
}
static optional<unsigned> get_fingerprint(entry const & e) {
return some(e.hash());
}
};
template class scoped_ext<tactic_hint_config>;
typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
void initialize_tactic_hint() {
g_class_name = new name("tactic");
g_key = new std::string("TACHINT");
tactic_hint_ext::initialize();
}
void finalize_tactic_hint() {
tactic_hint_ext::finalize();
delete g_key;
delete g_class_name;
}
list<expr> const & get_tactic_hints(environment const & env) {
return tactic_hint_ext::get_state(env);
}
expr parse_tactic_name(parser & p) {
auto pos = p.pos();
name pre_tac = p.check_constant_next("invalid tactic name, constant expected");
auto decl = p.env().get(pre_tac);
expr pre_tac_type = decl.get_type();
if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != get_tactic_name())
throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos);
buffer<level> ls;
for (auto const & n : decl.get_univ_params())
ls.push_back(mk_meta_univ(n));
return mk_constant(pre_tac, to_list(ls.begin(), ls.end()));
}
environment tactic_hint_cmd(parser & p) {
expr pre_tac = parse_tactic_name(p);
return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), pre_tac, get_namespace(p.env()), true);
}
void register_tactic_hint_cmd(cmd_table & r) {
add_cmd(r, cmd_info("tactic_hint", "add a new tactic hint", tactic_hint_cmd));
}
}

19
src/frontends/lean/tactic_hint.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/tactic.h"
#include "frontends/lean/cmd_table.h"
namespace lean {
list<expr> const & get_tactic_hints(environment const & env);
class parser;
expr parse_tactic_name(parser & p);
void register_tactic_hint_cmd(cmd_table & r);
void initialize_tactic_hint();
void finalize_tactic_hint();
}