From 7e6a10bd1bc9bbbf81e53190839b40d3f1856ddf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Feb 2017 11:21:02 -0800 Subject: [PATCH] chore(tests/lean): fix tests, and environment.decl_pos --- library/init/meta/environment.lean | 2 +- tests/lean/interactive/my_tac_class.lean | 4 ++-- tests/lean/interactive/rb_map_ts.lean | 4 ++-- tests/lean/run/basic_monitor2.lean | 8 ++++---- tests/lean/run/basic_monitor3.lean | 6 +++--- tests/lean/run/decl_olean.lean | 4 ++-- tests/lean/run/eval_attr_cache.lean | 2 +- tests/lean/run/fingerprint.lean | 2 +- tests/lean/run/my_tac_class.lean | 4 ++-- tests/lean/run/run_tactic1.lean | 2 +- 10 files changed, 19 insertions(+), 19 deletions(-) diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index 63b5afbd01..fe3e128e37 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -79,7 +79,7 @@ meta constant trans_for : environment → name → option name The result is none if d was not defined in an imported file. -/ meta constant decl_olean : environment → name → option string /- (decl_pos env d) returns the source location of d if available. -/ -meta constant decl_pos_info : environment → name → option pos +meta constant decl_pos : environment → name → option pos open expr meta constant unfold_untrusted_macros : environment → expr → expr diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean index 057712882f..e07297042b 100644 --- a/tests/lean/interactive/my_tac_class.lean +++ b/tests/lean/interactive/my_tac_class.lean @@ -25,10 +25,10 @@ meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit meta def execute (tac : mytac unit) : tactic unit := tac 0 >> return () -meta def save_info (line col : nat) : mytac unit := +meta def save_info (p : pos) : mytac unit := do v ← state_t.read, s ← tactic.read, - tactic.save_info_thunk line col + tactic.save_info_thunk p (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++ tactic_state.to_format s) diff --git a/tests/lean/interactive/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean index 886afae221..6bbb46a5c7 100644 --- a/tests/lean/interactive/rb_map_ts.lean +++ b/tests/lean/interactive/rb_map_ts.lean @@ -25,10 +25,10 @@ meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit meta def execute (tac : mytac unit) : tactic unit := tac (name_map.mk nat) >> return () -meta def save_info (line col : nat) : mytac unit := +meta def save_info (p : pos) : mytac unit := do v ← state_t.read, s ← tactic.read, - tactic.save_info_thunk line col + tactic.save_info_thunk p (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++ tactic_state.to_format s) diff --git a/tests/lean/run/basic_monitor2.lean b/tests/lean/run/basic_monitor2.lean index 47a7056413..c0d29bbadf 100644 --- a/tests/lean/run/basic_monitor2.lean +++ b/tests/lean/run/basic_monitor2.lean @@ -9,10 +9,10 @@ return (to_fmt "") meta def pos_info (fn : name) : vm format := do { - d ← vm.get_decl fn, - some (line, col) ← return (vm_decl.pos d) | failure, - file ← get_file fn, - return (file ++ ":" ++ line ++ ":" ++ col) + d ← vm.get_decl fn, + some pos ← return (vm_decl.pos d) | failure, + file ← get_file fn, + return (file ++ ":" ++ pos.1 ++ ":" ++ pos.2) } <|> return (to_fmt "") diff --git a/tests/lean/run/basic_monitor3.lean b/tests/lean/run/basic_monitor3.lean index 1efcab3ae6..53962421b5 100644 --- a/tests/lean/run/basic_monitor3.lean +++ b/tests/lean/run/basic_monitor3.lean @@ -9,10 +9,10 @@ return (to_fmt "") meta def pos_info (fn : name) : vm format := do { - d ← vm.get_decl fn, - some (line, col) ← return (vm_decl.pos d) | failure, + d ← vm.get_decl fn, + some pos ← return (vm_decl.pos d) | failure, file ← get_file fn, - return (file ++ ":" ++ line ++ ":" ++ col) + return (file ++ ":" ++ pos.1 ++ ":" ++ pos.2) } <|> return (to_fmt "") diff --git a/tests/lean/run/decl_olean.lean b/tests/lean/run/decl_olean.lean index 60ee7f6a1e..d47e7f1dc4 100644 --- a/tests/lean/run/decl_olean.lean +++ b/tests/lean/run/decl_olean.lean @@ -5,9 +5,9 @@ def g : nat → nat := meta def show_pos (n : name) : command := do env ← get_env, - pos ← returnopt (env^.decl_pos_info n), + pos ← returnopt (env^.decl_pos n), olean ← returnopt (env^.decl_olean n) <|> return "current file", - trace $ to_string n ++ " was defined at " ++ olean ++ " : " ++ to_string pos + trace $ to_string n ++ " was defined at " ++ olean ++ " : " ++ to_string pos.1 ++ ":" ++ to_string pos.2 run_command show_pos `add run_command show_pos `nat.succ diff --git a/tests/lean/run/eval_attr_cache.lean b/tests/lean/run/eval_attr_cache.lean index 1f968ecdc5..aaf02f48a8 100644 --- a/tests/lean/run/eval_attr_cache.lean +++ b/tests/lean/run/eval_attr_cache.lean @@ -1,5 +1,5 @@ open tactic - +meta def list_name.to_expr (n : list name) : tactic expr := to_expr (quote n) meta def my_attr : caching_user_attribute (name → bool) := { name := "my_attr", descr := "my attr", diff --git a/tests/lean/run/fingerprint.lean b/tests/lean/run/fingerprint.lean index 218bb7a8f2..7d613f90d5 100644 --- a/tests/lean/run/fingerprint.lean +++ b/tests/lean/run/fingerprint.lean @@ -1,5 +1,5 @@ open tactic - +meta def nat.to_expr (n : nat) : tactic expr := to_expr (quote n) run_command attribute.fingerprint `reducible >>= trace definition ex0 : nat := diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean index 222bb1eacc..f20974ca5e 100644 --- a/tests/lean/run/my_tac_class.lean +++ b/tests/lean/run/my_tac_class.lean @@ -29,10 +29,10 @@ meta def rstep {α : Type} (line : nat) (col : nat) (t : mytac α) : mytac unit meta def execute (tac : mytac unit) : tactic unit := tac 0 >> return () -meta def save_info (line col : nat) : mytac unit := +meta def save_info (p : pos) : mytac unit := do v ← state_t.read, s ← tactic.read, - tactic.save_info_thunk line col + tactic.save_info_thunk p (λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++ tactic_state.to_format s) diff --git a/tests/lean/run/run_tactic1.lean b/tests/lean/run/run_tactic1.lean index 75fd8e4f2e..28ce9885da 100644 --- a/tests/lean/run/run_tactic1.lean +++ b/tests/lean/run/run_tactic1.lean @@ -15,7 +15,7 @@ meta definition mk_defs : nat → command | 0 := skip | (n+1) := do N ← to_expr `(nat), - v ← n^.to_expr, + v ← to_expr (quote n), add_decl (declaration.defn (name.append_after `val n) [] N v reducibility_hints.opaque tt), mk_defs n