From 8d47d2a0263efee744bedeb82ef7e83aa7a9162a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Oct 2018 11:20:19 -0700 Subject: [PATCH] chore(library/vm,library/init/meta): remove `vm_format`, and some obsolete meta objects --- library/init/data/option/instances.lean | 1 - library/init/io.lean | 13 -- library/init/meta/default.lean | 3 +- library/init/meta/format.lean | 156 ------------------ library/init/meta/interaction_monad.lean | 98 ------------ library/init/meta/ref.lean | 18 --- library/init/meta/tactic.lean | 81 ---------- library/init/util.lean | 5 +- src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 4 - src/library/vm/vm_format.cpp | 196 ----------------------- src/library/vm/vm_format.h | 22 --- 12 files changed, 3 insertions(+), 596 deletions(-) delete mode 100644 library/init/meta/format.lean delete mode 100644 library/init/meta/interaction_monad.lean delete mode 100644 library/init/meta/ref.lean delete mode 100644 library/init/meta/tactic.lean delete mode 100644 src/library/vm/vm_format.cpp delete mode 100644 src/library/vm/vm_format.h diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index 9a28e34616..724810261a 100644 --- a/library/init/data/option/instances.lean +++ b/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 diff --git a/library/init/io.lean b/library/init/io.lean index 382a3ca227..8e226afb2e 100644 --- a/library/init/io.lean +++ b/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`. diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 837eed3edd..87ccbcc8cd 100644 --- a/library/init/meta/default.lean +++ b/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 diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean deleted file mode 100644 index e934cc501b..0000000000 --- a/library/init/meta/format.lean +++ /dev/null @@ -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⟩ diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean deleted file mode 100644 index f858763be7..0000000000 --- a/library/init/meta/interaction_monad.lean +++ /dev/null @@ -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 diff --git a/library/init/meta/ref.lean b/library/init/meta/ref.lean deleted file mode 100644 index 5981ece7ec..0000000000 --- a/library/init/meta/ref.lean +++ /dev/null @@ -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 diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean deleted file mode 100644 index eb5cb1f6e1..0000000000 --- a/library/init/meta/tactic.lean +++ /dev/null @@ -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} diff --git a/library/init/util.lean b/library/init/util.lean index 0e6f81fc95..7d2c739308 100644 --- a/library/init/util.lean +++ b/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 diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 11668177b5..0f5cbdb7a4 100644 --- a/src/library/vm/CMakeLists.txt +++ b/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) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 22ed23a8e6..86d4cad571 100644 --- a/src/library/vm/init_module.cpp +++ b/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() { diff --git a/src/library/vm/vm_format.cpp b/src/library/vm/vm_format.cpp deleted file mode 100644 index 9a59143b90..0000000000 --- a/src/library/vm/vm_format.cpp +++ /dev/null @@ -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 -#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(to_external(o)); -} - -format const & to_format(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(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(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 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 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 m_val; - vm_format_thunk(std::function 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 const & to_format_thunk(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_val; -} - -vm_obj to_obj(std::function 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 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")); -} -} diff --git a/src/library/vm/vm_format.h b/src/library/vm/vm_format.h deleted file mode 100644 index 678709cb24..0000000000 --- a/src/library/vm/vm_format.h +++ /dev/null @@ -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 const & fn); - -void initialize_vm_format(); -void finalize_vm_format(); -void initialize_vm_format_builtin_idxs(); -}