refactor(library): move 'meta' to 'init' folder

Motivation: tactic framework should be always available.

library/init/default.lean

@@ -5,8 +5,10 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.datatypes init.reserved_notation init.logic
-import init.relation init.wf init.nat init.wf_k init.prod
+import init.relation init.nat init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.fin init.list init.char init.string init.to_string init.timeit
 import init.unsigned
+import init.meta
+import init.wf init.wf_k

library/init/meta/base_tactic.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.format
+prelude
+import init.monad init.meta.format
 /-
 Remark: we use a thunk that produces a format object as the exception information.
 Motivation: the formatting object may be big.

library/init/meta/cmp_result.lean

@@ -3,6 +3,9 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
+import init.to_string init.prod
+
 inductive cmp_result :=
 | lt | eq | gt
 

library/init/meta/default.lean

@@ -3,5 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name meta.options meta.format meta.rb_map
-import meta.level meta.expr
+prelude
+import init.meta.name init.meta.options init.meta.format init.meta.rb_map
+import init.meta.level init.meta.expr init.meta.base_tactic

library/init/meta/expr.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.level
+prelude
+import init.meta.level
 
 inductive binder_info :=
 | default | implicit | strict_implicit | inst_implicit | other

library/init/meta/format.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import system.IO meta.options
+prelude
+import init.meta.options
 
 inductive format.color :=
 | red | green | orange | blue | pink | cyan | grey
@@ -19,12 +20,8 @@ meta_constant format.of_string   : string → format
 meta_constant format.of_nat      : nat → format
 meta_constant format.flatten     : format → format
 meta_constant format.to_string   : format → options → string
-meta_constant format.print_using : format → options → IO unit
 meta_constant format.of_options  : options → format
 
-meta_definition format.print (fmt : format) : IO unit :=
-format.print_using fmt options.mk
-
 meta_definition format_has_add [instance] : has_add format :=
 has_add.mk format.compose
 
@@ -37,12 +34,6 @@ structure has_to_format [class] (A : Type) :=
 meta_definition to_fmt {A : Type} [has_to_format A] : A → format :=
 has_to_format.to_format
 
-meta_definition pp_using {A : Type} [has_to_format A] (a : A) (o : options) : IO unit :=
-format.print_using (to_fmt a) o
-
-meta_definition pp {A : Type} [has_to_format A] (a : A) : IO unit :=
-format.print (to_fmt a)
-
 namespace format
 attribute [coercion] of_string of_nat
 end format

library/init/meta/level.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name meta.format
+prelude
+import init.meta.name init.meta.format
 
 /- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
 inductive level :=

library/init/meta/name.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.cmp_result
+prelude
+import init.meta.cmp_result
 
 /- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/
 inductive name :=

library/init/meta/options.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name
+prelude
+import init.meta.name
 
 meta_constant options                  : Type₁
 meta_constant options.size             : options → nat

library/init/meta/rb_map.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.cmp_result meta.name meta.format
+prelude
+import init.meta.cmp_result init.meta.name init.meta.format
 
 meta_constant rb_map.{l₁ l₂} : Type.{l₁} → Type.{l₂} → Type.{max l₁ l₂ 1}
 

library/system/IO.lean

@@ -12,3 +12,14 @@ attribute [instance] functorIO monadIO
 constant put_str : string → IO unit
 constant put_nat : nat → IO unit
 constant get_line : IO string
+
+meta_constant format.print_using : format → options → IO unit
+
+meta_definition format.print (fmt : format) : IO unit :=
+format.print_using fmt options.mk
+
+meta_definition pp_using {A : Type} [has_to_format A] (a : A) (o : options) : IO unit :=
+format.print_using (to_fmt a) o
+
+meta_definition pp {A : Type} [has_to_format A] (a : A) : IO unit :=
+format.print (to_fmt a)

tests/lean/run/base_tac1.lean

@@ -1,4 +1,3 @@
-import meta.base_tactic
 open tactic
 
 meta_definition tac [reducible] := base_tactic string

tests/lean/run/format.lean

@@ -1,4 +1,4 @@
-import meta
+import system.IO
 open list
 
 vm_eval pp ([["aaa", "bbb", "ccc", "dddd", "eeeeee", "ffffff"], ["aaa", "bbb", "ccc", "dddd", "eeeeee", "ffffff"],

tests/lean/run/meta_expr1.lean

@@ -1,4 +1,3 @@
-import meta
 open unsigned list
 
 meta_definition e1 := expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" [])

tests/lean/run/meta_level1.lean

@@ -1,4 +1,4 @@
-import meta
+import system.IO
 
 vm_eval do pp (level.max (level.succ level.zero) (level.param "foo")), put_str "\n"
 

tests/lean/run/opt1.lean

@@ -1,5 +1,3 @@
-import meta
-
 vm_eval options.get_string options.mk "opt1" "<empty>"
 vm_eval options.get_string (options.set_string options.mk "opt1" "val1") "opt1" "<empty>"
 vm_eval if (options.mk = options.mk) then bool.tt else bool.ff

tests/lean/run/rb_map1.lean

@@ -1,4 +1,4 @@
-import meta
+import system.IO
 
 section
 open nat_map