chore(library/vm,library/init/meta): remove vm_format, and some obsolete meta objects

library/init/data/option/instances.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.option.basic
-import init.meta.tactic
 
 universes u v
 

library/init/io.lean

@@ -3,10 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich
 -/
-
 prelude
 import init.control.state init.control.except init.data.string.basic init.control.coroutine
-import init.meta.tactic
 
 /-- Like https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
     Makes sure we never reorder `io` operations. -/
@@ -162,17 +160,6 @@ end proc
 -/
 end io
 
-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 {α : Type} [has_to_format α] (a : α) (o : options) : io unit :=
-format.print_using (to_fmt a) o
-
-meta definition pp {α : Type} [has_to_format α] (a : α) : io unit :=
-format.print (to_fmt a)
-
 /-
 /-- Run the external process specified by `args`.
 

library/init/meta/default.lean

@@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.name init.meta.options init.meta.format
-import init.meta.tactic
+import init.meta.name init.meta.options

library/init/meta/format.lean

@@ -1,156 +0,0 @@
-/-
-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.meta.options init.function init.data.to_string init.lean.format
-
-universes u v
-
-inductive format.color
-| red | green | orange | blue | pink | cyan | grey
-
-meta constant format : Type
-meta constant format.line            : format
-meta constant format.space           : format
-meta constant format.nil             : format
-meta constant format.compose         : format → format → format
-meta constant format.nest            : nat → format → format
-meta constant format.highlight       : format → color → format
-meta constant format.group           : format → format
-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  (f : format) (o : options := options.mk) : string
-meta constant format.of_options      : options → format
-meta constant format.is_nil          : format → bool
-meta constant trace_fmt {α : Type u} : format → (unit → α) → α
-
-meta instance : inhabited format :=
-⟨format.space⟩
-
-meta instance : has_append format :=
-⟨format.compose⟩
-
-meta instance : has_to_string format :=
-⟨λ f, f.to_string options.mk⟩
-
-meta class has_to_format (α : Type u) :=
-(to_format : α → format)
-
-meta instance : has_to_format format :=
-⟨id⟩
-
-meta def to_fmt {α : Type u} [has_to_format α] : α → format :=
-has_to_format.to_format
-
-meta instance nat_to_format : has_coe nat format :=
-⟨format.of_nat⟩
-
-meta instance string_to_format : has_coe string format :=
-⟨format.of_string⟩
-
-open format list
-
-meta def format.indent (f : format) (n : nat) : format :=
-nest n (line ++ f)
-
-meta def format.when {α : Type u} [has_to_format α] : bool → α → format
-| tt a := to_fmt a
-| ff a := nil
-
-meta def format.join (xs : list format) : format :=
-foldl compose (of_string "") xs
-
-meta instance : has_to_format options :=
-⟨λ o, format.of_options o⟩
-
-meta instance : has_to_format bool :=
-⟨λ b, if b then of_string "tt" else of_string "ff"⟩
-
-meta instance {p : Prop} : has_to_format (decidable p) :=
-⟨λ b : decidable p, @ite p b _ (of_string "tt") (of_string "ff")⟩
-
-meta instance : has_to_format string :=
-⟨λ s, format.of_string s⟩
-
-meta instance : has_to_format nat :=
-⟨λ n, format.of_nat n⟩
-
-meta instance : has_to_format uint32 :=
-⟨λ n, to_fmt n.to_nat⟩
-
-meta instance : has_to_format uint64 :=
-⟨λ n, to_fmt n.to_nat⟩
-
-meta instance : has_to_format char :=
-⟨λ c : char, format.of_string c.to_string⟩
-
-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 "]"
-
-meta instance {α : Type u} [has_to_format α] : has_to_format (list α) :=
-⟨list.to_format⟩
-
-attribute [instance] string.has_to_format
-
-meta instance : has_to_format name :=
-⟨λ n, to_fmt n.to_string⟩
-
-meta instance : has_to_format unit :=
-⟨λ u, to_fmt "()"⟩
-
-meta instance {α : Type u} [has_to_format α] : has_to_format (option α) :=
-⟨λ o, option.cases_on o
-  (to_fmt "none")
-  (λ a, to_fmt "(some " ++ nest 6 (to_fmt a) ++ to_fmt ")")⟩
-
-meta instance sum_has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] : has_to_format (sum α β) :=
-⟨λ s, sum.cases_on s
-  (λ a, to_fmt "(inl " ++ nest 5 (to_fmt a) ++ to_fmt ")")
-  (λ b, to_fmt "(inr " ++ nest 5 (to_fmt b) ++ to_fmt ")")⟩
-
-open prod
-
-meta instance {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] : has_to_format (prod α β) :=
-⟨λ ⟨a, b⟩, group (nest 1 (to_fmt "(" ++ to_fmt a ++ to_fmt "," ++ line ++ to_fmt b ++ to_fmt ")"))⟩
-
-open sigma
-
-meta instance {α : Type u} {β : α → Type v} [has_to_format α] [s : ∀ x, has_to_format (β x)]
-                                          : has_to_format (sigma β) :=
-⟨λ ⟨a, b⟩, group (nest 1 (to_fmt "⟨"  ++ to_fmt a ++ to_fmt "," ++ line ++ to_fmt b ++ to_fmt "⟩"))⟩
-
-open subtype
-
-meta instance {α : Type u} {p : α → Prop} [has_to_format α] : has_to_format (subtype p) :=
-⟨λ s, to_fmt (val s)⟩
-
-meta def format.bracket : string → string → format → format
-| o c f := to_fmt o ++ nest o.length f ++ to_fmt c
-
-meta def format.paren (f : format) : format :=
-format.bracket "(" ")" f
-
-meta def format.cbrace (f : format) : format :=
-format.bracket "{" "}" f
-
-meta def format.sbracket (f : format) : format :=
-format.bracket "[" "]" f
-
-meta def format.dcbrace (f : format) : format :=
-to_fmt "⦃" ++ nest 1 f ++ to_fmt "⦄"
-
-meta def format.from_lean_format : lean.format → format
-| (lean.format.nil) := format.nil
-| (lean.format.line) := format.line
-| (lean.format.text s) := s
-| (lean.format.nest n f) := (format.from_lean_format f).nest n
-| (lean.format.compose ff f₁ f₂) := format.compose (format.from_lean_format f₁) (format.from_lean_format f₂)
-| (lean.format.compose tt f₁ f₂) := (format.compose (format.from_lean_format f₁) (format.from_lean_format f₂)).group
-| (lean.format.choice f₁ f₂) := format.from_lean_format f₁ -- HACK
-
-meta instance has_to_format_of_lean_has_to_format {α} [lean.has_to_format α] : has_to_format α :=
-⟨format.from_lean_format ∘ lean.to_fmt⟩

library/init/meta/interaction_monad.lean

@@ -1,98 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
--/
-prelude
-import init.function init.data.option.basic init.util
-import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
-import init.data.nat.div init.meta.format
-import init.data.repr init.data.string.basic init.data.to_string init.meta.pos
-
-universes u v
-
-meta inductive interaction_monad.result (state : Type) (α : Type u)
-| success      : α → state → interaction_monad.result
-| exception {} : option (unit → format) → option pos → state → interaction_monad.result
-
-open interaction_monad.result
-
-section
-variables {state : Type} {α : Type u}
-variables [has_to_string α]
-
-meta def interaction_monad.result_to_string : result state α → string
-| (success a s)              := to_string a
-| (exception (some t) ref s) := "Exception: " ++ to_string (t ())
-| (exception none ref s)     := "[silent exception]"
-
-meta instance interaction_monad.result_has_string : has_to_string (result state α) :=
-⟨interaction_monad.result_to_string⟩
-end
-
-meta def interaction_monad.result.clamp_pos {state : Type} {α : Type u} (line0 line col : ℕ) : result state α → result state α
-| (success a s)              := success a s
-| (exception msg (some p) s) := exception msg (some $ if p.line < line0 then ⟨line, col⟩ else p) s
-| (exception msg none s)     := exception msg (some ⟨line, col⟩) s
-
-@[reducible] meta def interaction_monad (state : Type) (α : Type u) :=
-state → result state α
-
-section
-variables {state : Type} {α : Type u} {β : Type v}
-local notation `m` := interaction_monad state
-
-@[inline] meta def interaction_monad_fmap (f : α → β) (t : m α) : m β :=
-λ s, interaction_monad.result.cases_on (t s)
-  (λ a s', success (f a) s')
-  (λ e s', exception e s')
-
-@[inline] meta def interaction_monad_bind (t₁ : m α) (t₂ : α → m β) : m β :=
-λ s,  interaction_monad.result.cases_on (t₁ s)
-  (λ a s', t₂ a s')
-  (λ e s', exception e s')
-
-@[inline] meta def interaction_monad_return (a : α) : m α :=
-λ s, success a s
-
-meta def interaction_monad_orelse {α : Type u} (t₁ t₂ : m α) : m α :=
-λ s, interaction_monad.result.cases_on (t₁ s)
-  success
-  (λ e₁ ref₁ s', interaction_monad.result.cases_on (t₂ s)
-     success
-     exception)
-
-@[inline] meta def interaction_monad_seq (t₁ : m α) (t₂ : m β) : m β :=
-interaction_monad_bind t₁ (λ a, t₂)
-
-meta instance interaction_monad.monad : monad m :=
-{map := @interaction_monad_fmap _, pure := @interaction_monad_return _, bind := @interaction_monad_bind _}
-
-meta def interaction_monad.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (s : state) : result state α :=
-exception (some (λ _, to_fmt msg)) none s
-
-meta def interaction_monad.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : m α :=
-λ s, interaction_monad.mk_exception msg s
-
-meta def interaction_monad.silent_fail {α : Type u} : m α :=
-λ s, exception none none s
-
-meta def interaction_monad.failed {α : Type u} : m α :=
-interaction_monad.fail "failed"
-
-/- Alternative orelse operator that allows to select which exception should be used.
-   The default is to use the first exception since the standard `orelse` uses the second. -/
-meta def interaction_monad.orelse' {α : Type u} (t₁ t₂ : m α) (use_first_ex := tt) : m α :=
-λ s, interaction_monad.result.cases_on (t₁ s)
-  success
-  (λ e₁ ref₁ s₁', interaction_monad.result.cases_on (t₂ s)
-     success
-     (λ e₂ ref₂ s₂', if use_first_ex then (exception e₁ ref₁ s₁') else (exception e₂ ref₂ s₂')))
-
-meta instance interaction_monad.monad_fail : monad_fail m :=
-{ fail := λ α s, interaction_monad.fail (to_fmt s), ..interaction_monad.monad }
-
--- TODO: unify `parser` and `tactic` behavior?
--- meta instance interaction_monad.alternative : alternative m :=
--- ⟨@interaction_monad_fmap, (λ α a s, success a s), (@fapp _ _), @interaction_monad.failed, @interaction_monad_orelse⟩
-end

library/init/meta/ref.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.meta.tactic
-universes u v
-
-namespace tactic
-meta constant ref (α : Type u) : Type u
-/-- Create a new reference `r` with initial value `a`, execute `t r`, and then delete `r`. -/
-meta constant using_new_ref {α : Type u} {β : Type v} (a : α) (t : ref α → tactic β) : tactic β
-/-- Read the value stored in the given reference. -/
-meta constant read_ref {α : Type u} : ref α → tactic α
-/-- Update the value stored in the given reference. -/
-meta constant write_ref {α : Type u} : ref α → α → tactic unit
-end tactic

library/init/meta/tactic.lean

@@ -1,81 +0,0 @@
-/-
-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.function init.data.option.basic init.util
-import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
-import init.data.nat.div init.meta.format
-import init.data.repr init.data.string.basic init.meta.interaction_monad
-
-meta constant tactic_state : Type
-
-universes u v
-
-namespace tactic_state
-end tactic_state
-
-
-@[reducible] meta def tactic := interaction_monad tactic_state
-@[reducible] meta def tactic_result := interaction_monad.result tactic_state
-
-namespace tactic
-  export interaction_monad (hiding failed fail)
-  meta def failed {α : Type} : tactic α := interaction_monad.failed
-  meta def fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : tactic α :=
-  interaction_monad.fail msg
-end tactic
-
-namespace tactic_result
-  export interaction_monad.result
-end tactic_result
-
-open tactic
-open tactic_result
-
-infixl ` >>=[tactic] `:2 := interaction_monad_bind
-infixl ` >>[tactic] `:2  := interaction_monad_seq
-
-meta instance : alternative tactic :=
-{ failure := @interaction_monad.failed _,
-  orelse  := @interaction_monad_orelse _,
-  ..interaction_monad.monad }
-
-namespace tactic
-variables {α : Type u}
-
-@[inline] meta def write (s' : tactic_state) : tactic unit :=
-λ s, success () s'
-
-@[inline] meta def read : tactic tactic_state :=
-λ s, success s s
-
-end tactic
-
-meta class has_to_tactic_format (α : Type u) :=
-(to_tactic_format : α → tactic format)
-
-meta def tactic.pp {α : Type u} [has_to_tactic_format α] : α → tactic format :=
-has_to_tactic_format.to_tactic_format
-
-open tactic format
-
-@[priority 10] meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α :=
-⟨(λ x, pure x) ∘ to_fmt⟩
-
-namespace tactic
-open tactic_state
-
-meta def trace {α : Type u} [has_to_tactic_format α] (a : α) : tactic unit :=
-do fmt ← pp a,
-   pure $ _root_.trace_fmt fmt (λ u, ())
-
-end tactic
-
-notation [parsing_only] `command`:max := tactic unit
-
-meta def monad_from_pure_bind {m : Type u → Type v}
-  (pure : Π {α : Type u}, α → m α)
-  (bind : Π {α β : Type u}, m α → (α → m β) → m β) : monad m :=
-{pure := @pure, bind := @bind}

library/init/util.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.format
+import init.core init.data.string.basic
 universes u
 
 /-- This function has a native implementation that tracks time. -/
@@ -15,9 +15,6 @@ f.get
 def trace {α : Type u} (s : string) (f : thunk α) : α :=
 f.get
 
-meta def trace_val {α : Type u} [has_to_format α] (f : α) : α :=
-trace (to_fmt f).to_string f
-
 /-- This function has a native implementation that shows the VM call stack. -/
 def trace_call_stack {α : Type u} (f : thunk α) : α :=
 f.get

src/library/vm/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
-  vm_options.cpp vm_format.cpp vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)
+  vm_options.cpp vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)

src/library/vm/init_module.cpp

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/vm/vm_io.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_options.h"
-#include "library/vm/vm_format.h"
 #include "library/vm/vm_array.h"
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_platform.h"
@@ -25,7 +24,6 @@ void initialize_vm_core_module() {
     initialize_vm_io();
     initialize_vm_name();
     initialize_vm_options();
-    initialize_vm_format();
     initialize_vm_array();
     initialize_vm_string();
     initialize_vm_platform();
@@ -35,7 +33,6 @@ void finalize_vm_core_module() {
     finalize_vm_platform();
     finalize_vm_string();
     finalize_vm_array();
-    finalize_vm_format();
     finalize_vm_options();
     finalize_vm_name();
     finalize_vm_io();
@@ -47,7 +44,6 @@ void finalize_vm_core_module() {
 
 void initialize_vm_module() {
     initialize_vm();
-    initialize_vm_format_builtin_idxs();
     initialize_vm_array_builtin_idxs();
 }
 void finalize_vm_module() {

src/library/vm/vm_format.cpp

@@ -1,196 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <iostream>
-#include "util/sexpr/format.h"
-#include "library/trace.h"
-#include "library/parray.h"
-#include "library/scope_pos_info_provider.h"
-#include "library/vm/vm.h"
-#include "library/vm/vm_array.h"
-#include "library/vm/vm_io.h"
-#include "library/vm/vm_nat.h"
-#include "library/vm/vm_string.h"
-#include "library/vm/vm_options.h"
-
-namespace lean {
-struct vm_format : public vm_external {
-    format m_val;
-    vm_format(format const & v):m_val(v) {}
-    virtual ~vm_format() {}
-    virtual void dealloc() override { delete this; }
-    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_format(m_val); }
-    virtual vm_external * clone(vm_clone_fn const &) override { return new vm_format(m_val); }
-};
-
-bool is_format(vm_obj const & o) {
-    return is_external(o) && dynamic_cast<vm_format*>(to_external(o));
-}
-
-format const & to_format(vm_obj const & o) {
-    lean_vm_check(dynamic_cast<vm_format*>(to_external(o)));
-    return static_cast<vm_format*>(to_external(o))->m_val;
-}
-
-vm_obj to_obj(format const & n) {
-    return mk_vm_external(new vm_format(n));
-}
-
-vm_obj format_line() {
-    return to_obj(line());
-}
-
-vm_obj format_space() {
-    return to_obj(space());
-}
-
-vm_obj format_nil() {
-    return to_obj(format());
-}
-
-vm_obj format_compose(vm_obj const & fmt1, vm_obj const & fmt2) {
-    return to_obj(compose(to_format(fmt1), to_format(fmt2)));
-}
-
-vm_obj format_nest(vm_obj const & i, vm_obj const & fmt) {
-    return to_obj(nest(to_unsigned(i), to_format(fmt)));
-}
-
-vm_obj format_highlight(vm_obj const & fmt, vm_obj const & c) {
-    return to_obj(highlight(to_format(fmt), static_cast<format::format_color>(cidx(c))));
-}
-
-vm_obj format_group(vm_obj const & fmt) {
-    return to_obj(group(to_format(fmt)));
-}
-
-vm_obj format_of_string(vm_obj const & s) {
-    return to_obj(format(to_string(s)));
-}
-
-vm_obj format_of_nat(vm_obj const & n) {
-    if (is_simple(n))
-        return to_obj(format(cidx(n)));
-    else
-        return to_obj(format(to_mpz(n).to_string()));
-}
-
-vm_obj format_flatten(vm_obj const & fmt) {
-    return to_obj(flatten(to_format(fmt)));
-}
-
-vm_obj format_to_string(vm_obj const & fmt, vm_obj const & opts) {
-    std::ostringstream out;
-    out << mk_pair(to_format(fmt), to_options(opts));
-    return to_obj(out.str());
-}
-
-/* TODO(jroesch): unify with IO */
-static vm_obj mk_buffer(parray<vm_obj> const & a) {
-    return mk_vm_pair(mk_vm_nat(a.size()), to_obj(a));
-}
-
-vm_obj format_to_buffer(vm_obj const & fmt, vm_obj const & opts) {
-    std::ostringstream out;
-    out << mk_pair(to_format(fmt), to_options(opts));
-
-    // TODO(jroesch): make this more performant?
-    auto fmt_string = out.str();
-    parray<vm_obj> buffer;
-
-    for (auto c : out.str()) {
-        buffer.push_back(mk_vm_simple(c));
-    }
-
-    return mk_buffer(buffer);
-}
-
-vm_obj format_print_using(vm_obj const & fmt, vm_obj const & opts, vm_obj const & /* state */) {
-    get_global_ios().get_regular_stream() << mk_pair(to_format(fmt), to_options(opts));
-    return mk_io_result(mk_vm_unit());
-}
-
-vm_obj format_of_options(vm_obj const & opts) {
-    return to_obj(pp(to_options(opts)));
-}
-
-vm_obj format_is_nil(vm_obj const & fmt) {
-    return mk_vm_bool(to_format(fmt).is_nil_fmt());
-}
-
-vm_obj trace_fmt(vm_obj const &, vm_obj const & fmt, vm_obj const & fn) {
-    tout() << to_format(fmt) << "\n";
-    return invoke(fn, mk_vm_unit());
-}
-
-vm_obj scope_trace(vm_obj const &, vm_obj const & line, vm_obj const & col, vm_obj const & fn) {
-    pos_info_provider * pip = get_pos_info_provider();
-    if (pip) {
-        scope_traces_as_messages traces_as_messages(pip->get_file_name(), pos_info(force_to_unsigned(line), force_to_unsigned(col)));
-        return invoke(fn, mk_vm_unit());
-    } else {
-        return invoke(fn, mk_vm_unit());
-    }
-}
-
-struct vm_format_thunk : public vm_external {
-    std::function<format()> m_val;
-    vm_format_thunk(std::function<format()> const & fn):m_val(fn) {}
-    virtual ~vm_format_thunk() {}
-    virtual void dealloc() override { delete this; }
-    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_format_thunk(m_val); }
-    virtual vm_external * clone(vm_clone_fn const &) override { return new vm_format_thunk(m_val); }
-};
-
-std::function<format()> const & to_format_thunk(vm_obj const & o) {
-    lean_vm_check(dynamic_cast<vm_format_thunk*>(to_external(o)));
-    return static_cast<vm_format_thunk*>(to_external(o))->m_val;
-}
-
-vm_obj to_obj(std::function<format()> const & fn) {
-    return mk_vm_external(new vm_format_thunk(fn));
-}
-
-static unsigned g_apply_format_thunk_idx = -1;
-
-vm_obj mk_vm_format_thunk(std::function<format()> const & fn) {
-    vm_obj t = to_obj(fn);
-    return mk_vm_closure(g_apply_format_thunk_idx, 1, &t);
-}
-
-vm_obj apply_format_thunk(vm_obj const & t, vm_obj const & /* u */) {
-    format f = to_format_thunk(t)();
-    return to_obj(f);
-}
-
-void initialize_vm_format() {
-    DECLARE_VM_BUILTIN(name({"format", "line"}),             format_line);
-    DECLARE_VM_BUILTIN(name({"format", "space"}),            format_space);
-    DECLARE_VM_BUILTIN(name({"format", "nil"}),              format_nil);
-    DECLARE_VM_BUILTIN(name({"format", "compose"}),          format_compose);
-    DECLARE_VM_BUILTIN(name({"format", "nest"}),             format_nest);
-    DECLARE_VM_BUILTIN(name({"format", "highlight"}),        format_highlight);
-    DECLARE_VM_BUILTIN(name({"format", "group"}),            format_group);
-    DECLARE_VM_BUILTIN(name({"format", "of_string"}),        format_of_string);
-    DECLARE_VM_BUILTIN(name({"format", "of_nat"}),           format_of_nat);
-    DECLARE_VM_BUILTIN(name({"format", "flatten"}),          format_flatten);
-    DECLARE_VM_BUILTIN(name({"format", "to_string"}),        format_to_string);
-    DECLARE_VM_BUILTIN(name({"format", "to_buffer"}),        format_to_buffer);
-    DECLARE_VM_BUILTIN(name({"format", "print_using"}),      format_print_using);
-    DECLARE_VM_BUILTIN(name({"format", "of_options"}),       format_of_options);
-    DECLARE_VM_BUILTIN(name({"format", "is_nil"}),           format_is_nil);
-    DECLARE_VM_BUILTIN(name("trace_fmt"),                    trace_fmt);
-    DECLARE_VM_BUILTIN(name("scope_trace"),                  scope_trace);
-    DECLARE_VM_BUILTIN("_apply_format_thunk", apply_format_thunk);
-}
-
-void finalize_vm_format() {
-}
-
-void initialize_vm_format_builtin_idxs() {
-    g_apply_format_thunk_idx = *get_vm_builtin_idx(name("_apply_format_thunk"));
-}
-}

src/library/vm/vm_format.h

@@ -1,22 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/sexpr/format.h"
-#include "library/vm/vm.h"
-
-namespace lean {
-bool is_format(vm_obj const & o);
-format const & to_format(vm_obj const & o);
-vm_obj to_obj(format const & fmt);
-
-/* Return an object of type (unit -> format) */
-vm_obj mk_vm_format_thunk(std::function<format()> const & fn);
-
-void initialize_vm_format();
-void finalize_vm_format();
-void initialize_vm_format_builtin_idxs();
-}