<commit_before>/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include "util/sexpr/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 false
#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_METAVAR_ARGS
#define LEAN_DEFAULT_PP_METAVAR_ARGS 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_BETA
#define LEAN_DEFAULT_PP_BETA true
#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_ABBREVIATIONS
#define LEAN_DEFAULT_PP_ABBREVIATIONS 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 false
#endif

#ifndef LEAN_DEFAULT_PP_LAZY_ABSTRACTION
#define LEAN_DEFAULT_PP_LAZY_ABSTRACTION false
#endif

#ifndef LEAN_DEFAULT_PP_ALL
#define LEAN_DEFAULT_PP_ALL 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_metavar_args      = nullptr;
static name * g_pp_purify_metavars   = nullptr;
static name * g_pp_purify_locals     = nullptr;
static name * g_pp_beta              = nullptr;
static name * g_pp_numerals          = nullptr;
static name * g_pp_strings           = nullptr;
static name * g_pp_abbreviations     = 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_lazy_abstraction  = nullptr;
static name * g_pp_all               = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;

void initialize_pp_options() {
    g_pp_max_depth         = new name{"pp", "max_depth"};
    g_pp_max_steps         = new name{"pp", "max_steps"};
    g_pp_notation          = new name{"pp", "notation"};
    g_pp_implicit          = new name{"pp", "implicit"};
    g_pp_proofs            = new name{"pp", "proofs"};
    g_pp_coercions         = new name{"pp", "coercions"};
    g_pp_universes         = new name{"pp", "universes"};
    g_pp_full_names        = new name{"pp", "full_names"};
    g_pp_private_names     = new name{"pp", "private_names"};
    g_pp_metavar_args      = new name{"pp", "metavar_args"};
    g_pp_purify_metavars   = new name{"pp", "purify_metavars"};
    g_pp_purify_locals     = new name{"pp", "purify_locals"};
    g_pp_beta              = new name{"pp", "beta"};
    g_pp_numerals          = new name{"pp", "numerals"};
    g_pp_strings           = new name{"pp", "strings"};
    g_pp_abbreviations     = new name{"pp", "abbreviations"};
    g_pp_preterm           = new name{"pp", "preterm"};
    g_pp_binder_types      = new name{"pp", "binder_types"};
    g_pp_hide_comp_irrel   = new name{"pp", "hide_comp_irrelevant"};
    g_pp_all               = new name{"pp", "all"};
    g_pp_lazy_abstraction  = new name{"pp", "lazy_abstraction"};
    g_pp_goal_compact      = new name{"pp", "goal", "compact"};
    g_pp_goal_max_hyps     = new name{"pp", "goal", "max_hypotheses"};

    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) display proof terms");
    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");<commit_msg>doc(src/library/pp_options): improve description of pp.proofs option<commit_after>/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include "util/sexpr/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 false
#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_METAVAR_ARGS
#define LEAN_DEFAULT_PP_METAVAR_ARGS 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_BETA
#define LEAN_DEFAULT_PP_BETA true
#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_ABBREVIATIONS
#define LEAN_DEFAULT_PP_ABBREVIATIONS 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 false
#endif

#ifndef LEAN_DEFAULT_PP_LAZY_ABSTRACTION
#define LEAN_DEFAULT_PP_LAZY_ABSTRACTION false
#endif

#ifndef LEAN_DEFAULT_PP_ALL
#define LEAN_DEFAULT_PP_ALL 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_metavar_args      = nullptr;
static name * g_pp_purify_metavars   = nullptr;
static name * g_pp_purify_locals     = nullptr;
static name * g_pp_beta              = nullptr;
static name * g_pp_numerals          = nullptr;
static name * g_pp_strings           = nullptr;
static name * g_pp_abbreviations     = 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_lazy_abstraction  = nullptr;
static name * g_pp_all               = nullptr;
static list<options> * g_distinguishing_pp_options = nullptr;

void initialize_pp_options() {
    g_pp_max_depth         = new name{"pp", "max_depth"};
    g_pp_max_steps         = new name{"pp", "max_steps"};
    g_pp_notation          = new name{"pp", "notation"};
    g_pp_implicit          = new name{"pp", "implicit"};
    g_pp_proofs            = new name{"pp", "proofs"};
    g_pp_coercions         = new name{"pp", "coercions"};
    g_pp_universes         = new name{"pp", "universes"};
    g_pp_full_names        = new name{"pp", "full_names"};
    g_pp_private_names     = new name{"pp", "private_names"};
    g_pp_metavar_args      = new name{"pp", "metavar_args"};
    g_pp_purify_metavars   = new name{"pp", "purify_metavars"};
    g_pp_purify_locals     = new name{"pp", "purify_locals"};
    g_pp_beta              = new name{"pp", "beta"};
    g_pp_numerals          = new name{"pp", "numerals"};
    g_pp_strings           = new name{"pp", "strings"};
    g_pp_abbreviations     = new name{"pp", "abbreviations"};
    g_pp_preterm           = new name{"pp", "preterm"};
    g_pp_binder_types      = new name{"pp", "binder_types"};
    g_pp_hide_comp_irrel   = new name{"pp", "hide_comp_irrelevant"};
    g_pp_all               = new name{"pp", "all"};
    g_pp_lazy_abstraction  = new name{"pp", "lazy_abstraction"};
    g_pp_goal_compact      = new name{"pp", "goal", "compact"};
    g_pp_goal_max_hyps     = new name{"pp", "goal", "max_hypotheses"};

    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");
{'fraction_non_alphanumeric': 0.07834101382488479, 'fraction_numerical': 0.0025136154168412233, 'mean_word_length': 4.055484963998306, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4302689', 'n_tokens_mistral': 4269, 'n_tokens_neox': 4108, 'n_words': 874}