From a3a8d76e965249db9bc286a69700b0183a3f7ed2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 27 Jan 2021 14:16:12 +0100 Subject: [PATCH] chore: move pp_options.cpp to Lean --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 137 ++++++- src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 3 - src/library/pp_options.cpp | 344 ------------------ src/library/pp_options.h | 55 --- src/library/util.cpp | 1 - tests/compiler/partial.lean | 2 +- tests/elabissues/zmod.lean | 2 +- tests/lean/run/CoeNew.lean | 2 +- tests/lean/run/meta2.lean | 2 - tests/lean/run/new_compiler.lean | 4 +- tests/lean/run/newfrontend5.lean | 2 +- tests/lean/run/rc_tests.lean | 4 +- 13 files changed, 131 insertions(+), 429 deletions(-) delete mode 100644 src/library/pp_options.cpp delete mode 100644 src/library/pp_options.h diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 79582987a2..01f6b0a265 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -33,6 +33,123 @@ import Lean.Elab.Term namespace Lean +register_builtin_option pp.all : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, " ++ + "and disable beta reduction and notations during pretty printing" +} +register_builtin_option pp.notation : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)" +} +register_builtin_option pp.coercions : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) display coercionss" +} +register_builtin_option pp.universes : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display universes" +} +register_builtin_option pp.full_names : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display fully qualified names" +} +register_builtin_option pp.private_names : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display internal names assigned to private declarations" +} +register_builtin_option pp.binder_types : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display types of lambda and Pi parameters" +} +register_builtin_option pp.structure_instances : Bool := { + defValue := true + group := "pp" + -- TODO: implement second part + descr := "(pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation " ++ + "or '⟨fieldValue, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute" +} +register_builtin_option pp.structure_projections : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) display structure projections using field notation" +} +register_builtin_option pp.explicit : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display implicit arguments" +} +register_builtin_option pp.structure_instance_type : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display type of structure instances" +} +register_builtin_option pp.safe_shadowing : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) allow variable shadowing if there is no collision" +} +-- TODO: +/- +register_builtin_option g_pp_max_depth : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum expression depth, after that it will use ellipsis" +} +register_builtin_option g_pp_max_steps : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis" +} +register_builtin_option g_pp_proofs : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function" +} +register_builtin_option g_pp_locals_full_names : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) show full names of locals" +} +register_builtin_option g_pp_beta : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) apply beta-reduction when pretty printing" +} +register_builtin_option g_pp_goal_compact : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) try to display goal in a single line when possible" +} +register_builtin_option g_pp_goal_max_hyps : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum number of hypotheses to be displayed" +} +register_builtin_option g_pp_instantiate_mvars : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals" +} +register_builtin_option g_pp_annotations : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display internal annotations (for debugging purposes only)" +} +register_builtin_option g_pp_compact_let : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) minimal indentation at `let`-declarations" +} +-/ + def getPPAll (o : Options) : Bool := o.get `pp.all false def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types (!getPPAll o) def getPPCoercions (o : Options) : Bool := o.get `pp.coercions (!getPPAll o) @@ -44,17 +161,9 @@ def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_insta def getPPUniverses (o : Options) : Bool := o.get `pp.universes (getPPAll o) def getPPFullNames (o : Options) : Bool := o.get `pp.full_names (getPPAll o) def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names (getPPAll o) -def getPPUnicode (o : Options) : Bool := o.get `pp.unicode (!getPPAll o) +def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true -builtin_initialize - registerOption `pp.explicit { defValue := false, group := "pp", descr := "(pretty printer) display implicit arguments" } - registerOption `pp.structure_instance_type { defValue := false, group := "pp", descr := "(pretty printer) display type of structure instances" } - registerOption `pp.safe_shadowing { defValue := true, group := "pp", descr := "(pretty printer) allow variable shadowing if there is no collision" } - -- TODO: register other options when old pretty printer is removed - --registerOption `pp.universes { defValue := false, group := "pp", descr := "(pretty printer) display universes" } - - /-- Associate pretty printer options to a specific subterm using a synthetic position. -/ abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b) @@ -104,7 +213,7 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) := KeyedDeclsAttribute.init { builtinName := `builtinDelab, name := `delab, - descr := "Register a delaborator. + descr := "Register a delaborator. [delab k] registers a declaration of type `Lean.PrettyPrinter.Delaborator.Delab` for the `Lean.Expr` constructor `k`. Multiple delaborators for a single constructor are tried in turn until @@ -142,13 +251,11 @@ def getExprKind : DelabM Name := do | _ => `mdata | Expr.proj _ _ _ _ => `proj -/-- Evaluate option accessor, using subterm-specific options if set. Default to `true` if `pp.all` is set. -/ +/-- Evaluate option accessor, using subterm-specific options if set. -/ def getPPOption (opt : Options → Bool) : DelabM Bool := do let ctx ← read - let val := opt ctx.defaultOptions - match ctx.optionsPerPos.find? ctx.pos with - | some opts => pure $ opt opts - | none => pure val + let opts ← ctx.optionsPerPos.find? ctx.pos |>.getD ctx.defaultOptions + return opt opts def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do let b ← getPPOption opt diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index bb9805c5f7..f2dcefcf23 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -3,7 +3,7 @@ add_library(library OBJECT expr_lt.cpp module.cpp sorry.cpp replace_visitor.cpp num.cpp class.cpp util.cpp print.cpp annotation.cpp protected.cpp reducible.cpp init_module.cpp - pp_options.cpp projection.cpp + projection.cpp aux_recursors.cpp trace.cpp profiling.cpp time_task.cpp formatter.cpp) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 6f9a95d3f8..d4678e5b54 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/print.h" #include "library/util.h" -#include "library/pp_options.h" #include "library/profiling.h" #include "library/time_task.h" #include "library/formatter.h" @@ -38,13 +37,11 @@ void initialize_library_module() { initialize_annotation(); initialize_class(); initialize_library_util(); - initialize_pp_options(); initialize_time_task(); } void finalize_library_module() { finalize_time_task(); - finalize_pp_options(); finalize_library_util(); finalize_class(); finalize_annotation(); diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp deleted file mode 100644 index 2d57dbf6b2..0000000000 --- a/src/library/pp_options.cpp +++ /dev/null @@ -1,344 +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 "util/option_declarations.h" -#include "library/pp_options.h" - -#ifndef LEAN_DEFAULT_PP_MAX_DEPTH -#define LEAN_DEFAULT_PP_MAX_DEPTH 64 -#endif - -#ifndef LEAN_DEFAULT_PP_MAX_STEPS -#define LEAN_DEFAULT_PP_MAX_STEPS 5000 -#endif - -#ifndef LEAN_DEFAULT_PP_NOTATION -#define LEAN_DEFAULT_PP_NOTATION true -#endif - -#ifndef LEAN_DEFAULT_PP_IMPLICIT -#define LEAN_DEFAULT_PP_IMPLICIT false -#endif - -#ifndef LEAN_DEFAULT_PP_PROOFS -#define LEAN_DEFAULT_PP_PROOFS true -#endif - -#ifndef LEAN_DEFAULT_PP_COERCIONS -#define LEAN_DEFAULT_PP_COERCIONS true -#endif - -#ifndef LEAN_DEFAULT_PP_UNIVERSES -#define LEAN_DEFAULT_PP_UNIVERSES false -#endif - -#ifndef LEAN_DEFAULT_PP_FULL_NAMES -#define LEAN_DEFAULT_PP_FULL_NAMES false -#endif - -#ifndef LEAN_DEFAULT_PP_PRIVATE_NAMES -#define LEAN_DEFAULT_PP_PRIVATE_NAMES false -#endif - -#ifndef LEAN_DEFAULT_PP_PURIFY_METAVARS -#define LEAN_DEFAULT_PP_PURIFY_METAVARS true -#endif - -#ifndef LEAN_DEFAULT_PP_PURIFY_LOCALS -#define LEAN_DEFAULT_PP_PURIFY_LOCALS true -#endif - -#ifndef LEAN_DEFAULT_PP_LOCALS_FULL_NAMES -#define LEAN_DEFAULT_PP_LOCALS_FULL_NAMES false -#endif - -#ifndef LEAN_DEFAULT_PP_BETA -#define LEAN_DEFAULT_PP_BETA false -#endif - -#ifndef LEAN_DEFAULT_PP_NUMERALS -#define LEAN_DEFAULT_PP_NUMERALS true -#endif - -#ifndef LEAN_DEFAULT_PP_STRINGSS -#define LEAN_DEFAULT_PP_STRINGS true -#endif - -#ifndef LEAN_DEFAULT_PP_PRETERM -#define LEAN_DEFAULT_PP_PRETERM false -#endif - -#ifndef LEAN_DEFAULT_PP_GOAL_COMPACT -#define LEAN_DEFAULT_PP_GOAL_COMPACT false -#endif - -#ifndef LEAN_DEFAULT_PP_GOAL_MAX_HYPS -#define LEAN_DEFAULT_PP_GOAL_MAX_HYPS 200 -#endif - -#ifndef LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT -#define LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT true -#endif - -#ifndef LEAN_DEFAULT_PP_BINDER_TYPES -#define LEAN_DEFAULT_PP_BINDER_TYPES true -#endif - -#ifndef LEAN_DEFAULT_PP_ALL -#define LEAN_DEFAULT_PP_ALL false -#endif - -#ifndef LEAN_DEFAULT_PP_STRUCTURE_INSTANCES -#define LEAN_DEFAULT_PP_STRUCTURE_INSTANCES true -#endif - -#ifndef LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER -#define LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER false -#endif - -#ifndef LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS -#define LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS true -#endif - -#ifndef LEAN_DEFAULT_PP_INSTANTIATE_MVARS -#define LEAN_DEFAULT_PP_INSTANTIATE_MVARS true -#endif - -#ifndef LEAN_DEFAULT_PP_ANNOTATIONS -#define LEAN_DEFAULT_PP_ANNOTATIONS false -#endif - -namespace lean { -static name * g_pp_max_depth = nullptr; -static name * g_pp_max_steps = nullptr; -static name * g_pp_notation = nullptr; -static name * g_pp_implicit = nullptr; -static name * g_pp_proofs = nullptr; -static name * g_pp_coercions = nullptr; -static name * g_pp_universes = nullptr; -static name * g_pp_full_names = nullptr; -static name * g_pp_private_names = nullptr; -static name * g_pp_purify_metavars = nullptr; -static name * g_pp_purify_locals = nullptr; -static name * g_pp_locals_full_names = nullptr; -static name * g_pp_beta = nullptr; -static name * g_pp_numerals = nullptr; -static name * g_pp_strings = nullptr; -static name * g_pp_preterm = nullptr; -static name * g_pp_goal_compact = nullptr; -static name * g_pp_goal_max_hyps = nullptr; -static name * g_pp_binder_types = nullptr; -static name * g_pp_hide_comp_irrel = nullptr; -static name * g_pp_structure_instances = nullptr; -static name * g_pp_structure_instances_qualifier = nullptr; -static name * g_pp_structure_projections = nullptr; -static name * g_pp_instantiate_mvars = nullptr; -static name * g_pp_annotations = nullptr; -static name * g_pp_compact_let = nullptr; -static name * g_pp_all = nullptr; - -void initialize_pp_options() { - g_pp_max_depth = new name{"pp", "max_depth"}; - mark_persistent(g_pp_max_depth->raw()); - g_pp_max_steps = new name{"pp", "max_steps"}; - mark_persistent(g_pp_max_steps->raw()); - g_pp_notation = new name{"pp", "notation"}; - mark_persistent(g_pp_notation->raw()); - g_pp_implicit = new name{"pp", "implicit"}; - mark_persistent(g_pp_implicit->raw()); - g_pp_proofs = new name{"pp", "proofs"}; - mark_persistent(g_pp_proofs->raw()); - g_pp_coercions = new name{"pp", "coercions"}; - mark_persistent(g_pp_coercions->raw()); - g_pp_universes = new name{"pp", "universes"}; - mark_persistent(g_pp_universes->raw()); - g_pp_full_names = new name{"pp", "full_names"}; - mark_persistent(g_pp_full_names->raw()); - g_pp_private_names = new name{"pp", "private_names"}; - mark_persistent(g_pp_private_names->raw()); - g_pp_purify_metavars = new name{"pp", "purify_metavars"}; - mark_persistent(g_pp_purify_metavars->raw()); - g_pp_purify_locals = new name{"pp", "purify_locals"}; - mark_persistent(g_pp_purify_locals->raw()); - g_pp_locals_full_names = new name{"pp", "locals_full_names"}; - mark_persistent(g_pp_locals_full_names->raw()); - g_pp_beta = new name{"pp", "beta"}; - mark_persistent(g_pp_beta->raw()); - g_pp_numerals = new name{"pp", "numerals"}; - mark_persistent(g_pp_numerals->raw()); - g_pp_strings = new name{"pp", "strings"}; - mark_persistent(g_pp_strings->raw()); - g_pp_preterm = new name{"pp", "preterm"}; - mark_persistent(g_pp_preterm->raw()); - g_pp_binder_types = new name{"pp", "binder_types"}; - mark_persistent(g_pp_binder_types->raw()); - g_pp_hide_comp_irrel = new name{"pp", "hide_comp_irrelevant"}; - mark_persistent(g_pp_hide_comp_irrel->raw()); - g_pp_all = new name{"pp", "all"}; - mark_persistent(g_pp_all->raw()); - g_pp_goal_compact = new name{"pp", "goal", "compact"}; - mark_persistent(g_pp_goal_compact->raw()); - g_pp_compact_let = new name{"pp", "compact_let"}; - mark_persistent(g_pp_compact_let->raw()); - g_pp_goal_max_hyps = new name{"pp", "goal", "max_hypotheses"}; - mark_persistent(g_pp_goal_max_hyps->raw()); - g_pp_structure_instances = new name{"pp", "structure_instances"}; - mark_persistent(g_pp_structure_instances->raw()); - g_pp_structure_instances_qualifier = new name{"pp", "structure_instances_qualifier"}; - mark_persistent(g_pp_structure_instances_qualifier->raw()); - g_pp_structure_projections = new name{"pp", "structure_projections"}; - mark_persistent(g_pp_structure_projections->raw()); - g_pp_instantiate_mvars = new name{"pp", "instantiate_mvars"}; - mark_persistent(g_pp_instantiate_mvars->raw()); - g_pp_annotations = new name{"pp", "annotations"}; - mark_persistent(g_pp_annotations->raw()); - - register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, - "(pretty printer) maximum expression depth, after that it will use ellipsis"); - register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, - "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"); - register_bool_option(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION, - "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); - register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, - "(pretty printer) display implicit parameters"); - register_bool_option(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS, - "(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function"); - register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS, - "(pretty printer) display coercionss"); - register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES, - "(pretty printer) display universes"); - register_bool_option(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES, - "(pretty printer) display fully qualified names"); - register_bool_option(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES, - "(pretty printer) display internal names assigned to private declarations"); - register_bool_option(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS, - "(pretty printer) rename internal metavariable names (with \"user-friendly\" ones) " - "before pretty printing"); - register_bool_option(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS, - "(pretty printer) rename local names to avoid name capture, " - "before pretty printing"); - register_bool_option(*g_pp_locals_full_names, LEAN_DEFAULT_PP_LOCALS_FULL_NAMES, - "(pretty printer) show full names of locals"); - register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA, - "(pretty printer) apply beta-reduction when pretty printing"); - register_bool_option(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS, - "(pretty printer) display nat/num numerals in decimal notation"); - register_bool_option(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS, - "(pretty printer) pretty print string and character literals"); - register_bool_option(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM, - "(pretty printer) assume the term is a preterm (i.e., a term before elaboration)"); - register_bool_option(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT, - "(pretty printer) try to display goal in a single line when possible"); - register_unsigned_option(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS, - "(pretty printer) maximum number of hypotheses to be displayed"); - register_bool_option(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT, - "(pretty printer) hide terms marked as computationally irrelevant, these marks are introduced by the code generator"); - register_bool_option(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES, - "(pretty printer) display types of lambda and Pi parameters"); - register_bool_option(*g_pp_structure_instances, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES, - "(pretty printer) display structure instances using the '{ field_name := field_value, ... }' notation " - "or '⟨field_value, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute"); - register_bool_option(*g_pp_structure_instances_qualifier, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER, - "(pretty printer) include qualifier 'struct_name .' " - "when displaying structure instances using the '{ struct_name . field_name := field_value, ... }' notation, " - "this option is ignored when pp.structure_instances is false"); - register_bool_option(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS, - "(pretty printer) display structure projections using field notation"); - register_bool_option(*g_pp_all, LEAN_DEFAULT_PP_ALL, - "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, " - "and disable beta reduction and notation during pretty printing"); - register_bool_option(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS, - "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals"); - register_bool_option(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS, - "(pretty printer) display internal annotations (for debugging purposes only)"); - register_bool_option(*g_pp_compact_let, false, - "(pretty printer) minimal indentation at `let`-declarations"); - - options universes_true(*g_pp_universes, true); - options full_names_true(*g_pp_full_names, true); - options implicit_true(*g_pp_implicit, true); - options proofs_true(*g_pp_proofs, true); - options coercions_true(*g_pp_coercions, true); - options notation_false(*g_pp_notation, false); - options binder_types_true(*g_pp_binder_types, true); - options implicit_coercions = join(coercions_true, implicit_true); - options implicit_notation = join(notation_false, implicit_true); - options all = universes_true + implicit_true + proofs_true + coercions_true + notation_false + full_names_true + binder_types_true; -} - -void finalize_pp_options() { - delete g_pp_compact_let; - delete g_pp_preterm; - delete g_pp_numerals; - delete g_pp_strings; - delete g_pp_max_depth; - delete g_pp_max_steps; - delete g_pp_notation; - delete g_pp_implicit; - delete g_pp_proofs; - delete g_pp_coercions; - delete g_pp_universes; - delete g_pp_full_names; - delete g_pp_private_names; - delete g_pp_purify_metavars; - delete g_pp_purify_locals; - delete g_pp_locals_full_names; - delete g_pp_beta; - delete g_pp_goal_compact; - delete g_pp_goal_max_hyps; - delete g_pp_binder_types; - delete g_pp_hide_comp_irrel; - delete g_pp_structure_instances; - delete g_pp_structure_instances_qualifier; - delete g_pp_structure_projections; - delete g_pp_all; - delete g_pp_instantiate_mvars; - delete g_pp_annotations; -} - -name const & get_pp_implicit_name() { return *g_pp_implicit; } -name const & get_pp_proofs_name() { return *g_pp_proofs; } -name const & get_pp_coercions_name() { return *g_pp_coercions; } -name const & get_pp_full_names_name() { return *g_pp_full_names; } -name const & get_pp_universes_name() { return *g_pp_universes; } -name const & get_pp_notation_name() { return *g_pp_notation; } -name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; } -name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; } -name const & get_pp_locals_full_names_name() { return *g_pp_locals_full_names; } -name const & get_pp_beta_name() { return *g_pp_beta; } -name const & get_pp_preterm_name() { return *g_pp_preterm; } -name const & get_pp_numerals_name() { return *g_pp_numerals; } -name const & get_pp_strings_name() { return *g_pp_strings; } -name const & get_pp_binder_types_name() { return *g_pp_binder_types; } - -unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } -unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } -bool get_pp_notation(options const & opts) { return opts.get_bool(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } -bool get_pp_implicit(options const & opts) { return opts.get_bool(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } -bool get_pp_proofs(options const & opts) { return opts.get_bool(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS); } -bool get_pp_coercions(options const & opts) { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); } -bool get_pp_universes(options const & opts) { return opts.get_bool(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); } -bool get_pp_full_names(options const & opts) { return opts.get_bool(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); } -bool get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } -bool get_pp_purify_metavars(options const & opts) { return opts.get_bool(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS); } -bool get_pp_purify_locals(options const & opts) { return opts.get_bool(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS); } -bool get_pp_locals_full_names(options const & opts) { return opts.get_bool(*g_pp_locals_full_names, LEAN_DEFAULT_PP_LOCALS_FULL_NAMES); } -bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } -bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } -bool get_pp_strings(options const & opts) { return opts.get_bool(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS); } -bool get_pp_preterm(options const & opts) { return opts.get_bool(*g_pp_preterm, LEAN_DEFAULT_PP_PRETERM); } -bool get_pp_goal_compact(options const & opts) { return opts.get_bool(*g_pp_goal_compact, LEAN_DEFAULT_PP_GOAL_COMPACT); } -unsigned get_pp_goal_max_hyps(options const & opts) { return opts.get_unsigned(*g_pp_goal_max_hyps, LEAN_DEFAULT_PP_GOAL_MAX_HYPS); } -bool get_pp_binder_types(options const & opts) { return opts.get_bool(*g_pp_binder_types, LEAN_DEFAULT_PP_BINDER_TYPES); } -bool get_pp_hide_comp_irrel(options const & opts) { return opts.get_bool(*g_pp_hide_comp_irrel, LEAN_DEFAULT_PP_HIDE_COMP_IRRELEVANT); } -bool get_pp_structure_instances(options const & opts) { return opts.get_bool(*g_pp_structure_instances, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES); } -bool get_pp_structure_instances_qualifier(options const & opts) { return opts.get_bool(*g_pp_structure_instances_qualifier, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER); } -bool get_pp_structure_projections(options const & opts) { return opts.get_bool(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS); } -bool get_pp_instantiate_mvars(options const & o) { return o.get_bool(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS); } -bool get_pp_annotations(options const & o) { return o.get_bool(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS); } -bool get_pp_compact_let(options const & opts) { return opts.get_bool(*g_pp_compact_let, false); } -bool get_pp_all(options const & opts) { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); } -} diff --git a/src/library/pp_options.h b/src/library/pp_options.h deleted file mode 100644 index a6f95c2c49..0000000000 --- a/src/library/pp_options.h +++ /dev/null @@ -1,55 +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 "util/options.h" -namespace lean { -name const & get_pp_implicit_name(); -name const & get_pp_proofs_name(); -name const & get_pp_coercions_name(); -name const & get_pp_full_names_name(); -name const & get_pp_universes_name(); -name const & get_pp_notation_name(); -name const & get_pp_purify_metavars_name(); -name const & get_pp_purify_locals_name(); -name const & get_pp_locals_full_names_name(); -name const & get_pp_beta_name(); -name const & get_pp_preterm_name(); -name const & get_pp_numerals_name(); -name const & get_pp_strings_name(); -name const & get_pp_binder_types_name(); - -unsigned get_pp_max_depth(options const & opts); -unsigned get_pp_max_steps(options const & opts); -bool get_pp_notation(options const & opts); -bool get_pp_implicit(options const & opts); -bool get_pp_proofs(options const & opts); -bool get_pp_coercions(options const & opts); -bool get_pp_universes(options const & opts); -bool get_pp_full_names(options const & opts); -bool get_pp_private_names(options const & opts); -bool get_pp_beta(options const & opts); -bool get_pp_purify_metavars(options const & opts); -bool get_pp_purify_locals(options const & opts); -bool get_pp_locals_full_names(options const & opts); -bool get_pp_numerals(options const & opts); -bool get_pp_strings(options const & opts); -bool get_pp_preterm(options const & opts); -bool get_pp_goal_compact(options const & opts); -unsigned get_pp_goal_max_hyps(options const & opts); -bool get_pp_binder_types(options const & opts); -bool get_pp_hide_comp_irrel(options const & opts); -bool get_pp_structure_instances(options const & opts); -bool get_pp_structure_instances_qualifier(options const & opts); -bool get_pp_structure_projections(options const & opts); -bool get_pp_instantiate_mvars(options const & o); -bool get_pp_annotations(options const & o); -bool get_pp_compact_let(options const & opts); -bool get_pp_all(options const & opts); - -void initialize_pp_options(); -void finalize_pp_options(); -} diff --git a/src/library/util.cpp b/src/library/util.cpp index ef05a6a4fe..720ce120d8 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/suffixes.h" #include "library/annotation.h" #include "library/constants.h" -#include "library/pp_options.h" #include "library/projection.h" #include "library/replace_visitor.h" #include "library/num.h" diff --git a/tests/compiler/partial.lean b/tests/compiler/partial.lean index aeef0db262..d52201249d 100644 --- a/tests/compiler/partial.lean +++ b/tests/compiler/partial.lean @@ -1,5 +1,5 @@ -set_option pp.implicit true +set_option pp.explicit true set_option pp.binder_types false -- set_option trace.compiler.boxed true diff --git a/tests/elabissues/zmod.lean b/tests/elabissues/zmod.lean index a3d07ca4b2..f0da804643 100644 --- a/tests/elabissues/zmod.lean +++ b/tests/elabissues/zmod.lean @@ -30,7 +30,7 @@ instance zmodIsRing {n : Nat} : Ring (Zmod n) := /- After the instance above, Zmod already has `+`, `*` notations, but not `/` -/ -set_option pp.implicit true +set_option pp.explicit true set_option pp.notation false #check fun (a b : Zmod 10) => a * b -- works diff --git a/tests/lean/run/CoeNew.lean b/tests/lean/run/CoeNew.lean index 032140f73d..140b09d767 100644 --- a/tests/lean/run/CoeNew.lean +++ b/tests/lean/run/CoeNew.lean @@ -17,7 +17,7 @@ structure ConstantFunction (α β : Type) := instance constantFunctionCoe {α β : Type} : CoeFun (ConstantFunction α β) (fun _ => α → β) := { coe := fun c => c.f } -set_option pp.implicit true +set_option pp.explicit true #synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Nat #synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Bool diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index acdc95ffda..cf6b1f6c3a 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -1,4 +1,3 @@ -#lang lean4 import Lean.Meta open Lean open Lean.Meta @@ -533,7 +532,6 @@ withLocalDeclD `α type $ fun α => do print t; pure () -set_option pp.purify_metavars false #eval tst34 def tst35 : MetaM Unit := do diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean index 0fa118a081..377e6f7239 100644 --- a/tests/lean/run/new_compiler.lean +++ b/tests/lean/run/new_compiler.lean @@ -3,9 +3,9 @@ universes u v w r s set_option trace.compiler.stage1 true --- setOption pp.implicit True +-- set_option pp.explicit true set_option pp.binder_types false -set_option pp.proofs true +-- set_option pp.proofs true def foo (n : Nat) : Nat := let x := Nat.zero; diff --git a/tests/lean/run/newfrontend5.lean b/tests/lean/run/newfrontend5.lean index 61f60d6977..eeb26ce32e 100644 --- a/tests/lean/run/newfrontend5.lean +++ b/tests/lean/run/newfrontend5.lean @@ -52,7 +52,7 @@ set_option pp.all true -- #check let x := (fun (f : {α : Type} → α → α) => (f, f)) @id; (x.1 [], x.2 true) -- we need constApprox := true for this one set_option pp.all false -set_option pp.implicit true +set_option pp.explicit true def h (x := 10) (y := 20) : Nat := x + y #check h -- h 10 20 : Nat diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean index 3c30d96767..32474d3a1e 100644 --- a/tests/lean/run/rc_tests.lean +++ b/tests/lean/run/rc_tests.lean @@ -1,8 +1,8 @@ universes u v --- setOption pp.binderTypes False -set_option pp.implicit true +-- set_option pp.binder_types false +set_option pp.explicit true set_option trace.compiler.llnf true -- set_option trace.compiler.boxed true