From 2281fb30c8eb05f1bd15ef4ea55c713c733c6f35 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Nov 2014 19:08:37 -0800 Subject: [PATCH] refactor(library): use "symbolic" precedences in the standard library --- library/data/sigma/decl.lean | 8 ++++---- library/hott/trunc.lean | 4 ++-- library/hott/types/sigma.lean | 4 ++-- src/frontends/lean/class.cpp | 11 +++-------- src/frontends/lean/notation_cmd.cpp | 12 ++++-------- src/frontends/lean/util.cpp | 21 +++++++++++++++++++++ src/frontends/lean/util.h | 7 +++++++ 7 files changed, 43 insertions(+), 24 deletions(-) diff --git a/library/data/sigma/decl.lean b/library/data/sigma/decl.lean index 5abf408dd..75af80744 100644 --- a/library/data/sigma/decl.lean +++ b/library/data/sigma/decl.lean @@ -1,7 +1,7 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -import logic.eq logic.heq data.unit +import logic.eq logic.heq data.unit data.num.ops structure sigma {A : Type} (B : A → Type) := dpair :: (dpr1 : A) (dpr2 : B dpr1) @@ -14,8 +14,8 @@ namespace sigma notation `dpr₂` := dpr2 namespace ops - postfix `.1`:10000 := dpr1 - postfix `.2`:10000 := dpr2 - notation `⟨` t:(foldr `,`:0 (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \> + postfix `.1`:(max+1) := dpr1 + postfix `.2`:(max+1) := dpr2 + notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \> end ops end sigma diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index e984e777d..6dc07a6d9 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -22,8 +22,8 @@ namespace truncation minus_two : trunc_index, trunc_S : trunc_index → trunc_index - postfix `.+1`:10000 := trunc_index.trunc_S - postfix `.+2`:10000 := λn, (n .+1 .+1) + postfix `.+1`:(max+1) := trunc_index.trunc_S + postfix `.+2`:(max+1) := λn, (n .+1 .+1) notation `-2` := trunc_index.minus_two notation `-1` := (-2.+1) diff --git a/library/hott/types/sigma.lean b/library/hott/types/sigma.lean index 656eabad1..b0b02f8f3 100644 --- a/library/hott/types/sigma.lean +++ b/library/hott/types/sigma.lean @@ -39,14 +39,14 @@ namespace sigma definition pr1_path (p : u ≈ v) : u.1 ≈ v.1 := ap dpr1 p - postfix `..1`:10000 := pr1_path + postfix `..1`:(max+1) := pr1_path definition pr2_path (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 := path.rec_on p idp --Coq uses the following proof, which only computes if u,v are dpairs AND p is idp --(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p - postfix `..2`:10000 := pr2_path + postfix `..2`:(max+1) := pr2_path definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : dpair (path_sigma p q)..1 (path_sigma p q)..2 ≈ ⟨p, q⟩ := diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 0a9782cdf..574689f90 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/reducible.h" #include "library/num.h" +#include "library/normalize.h" #include "library/aliases.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" @@ -181,20 +182,14 @@ list get_class_instances(environment const & env, name const & c) { return ptr_to_list(s.m_instances.find(c)); } -static environment open_priority_namespace(parser & p) { - name prio("std", "priority"); - environment env = using_namespace(p.env(), p.ios(), prio); - return overwrite_aliases(env, prio, name()); -} - optional parse_instance_priority(parser & p) { if (p.curr_is_token(get_priority_tk())) { p.next(); auto pos = p.pos(); - environment env = open_priority_namespace(p); + environment env = open_priority_aliases(open_num_notation(p.env())); parser::local_scope scope(p, env); expr val = p.parse_expr(); - val = type_checker(p.env()).whnf(val).first; + val = normalize(p.env(), val); if (optional mpz_val = to_num(val)) { if (!mpz_val->is_unsigned_int()) throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index e1d9e5b38..cb635e638 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -14,9 +14,11 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/explicit.h" #include "library/num.h" +#include "library/normalize.h" #include "library/aliases.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" +#include "frontends/lean/util.h" namespace lean { static std::string parse_symbol(parser & p, char const * msg) { @@ -32,21 +34,15 @@ static std::string parse_symbol(parser & p, char const * msg) { return n.to_string(); } -static environment open_prec_namespace(parser & p) { - name prec("std", "prec"); - environment env = using_namespace(p.env(), p.ios(), prec); - return overwrite_aliases(env, prec, name()); -} - static unsigned parse_precedence_core(parser & p) { auto pos = p.pos(); if (p.curr_is_numeral()) { return p.parse_small_nat(); } else { - environment env = open_prec_namespace(p); + environment env = open_prec_aliases(open_num_notation(p.env())); parser::local_scope scope(p, env); expr val = p.parse_expr(get_max_prec()); - val = type_checker(p.env()).whnf(val).first; + val = normalize(p.env(), val); if (optional mpz_val = to_num(val)) { if (!mpz_val->is_unsigned_int()) throw parser_error("invalid 'precedence', argument does not fit in a machine integer", pos); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 11da6fa57..28a88ac8a 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -415,4 +415,25 @@ name get_decl_short_name(name const & d, environment const & env) { else return d; } + +environment open_num_notation(environment const & env) { + name num("num"); + try { + environment new_env = overwrite_notation(env, num); + return overwrite_aliases(new_env, num, name()); + } catch (exception &) { + // num namespace is not available, then use only the aliases + return overwrite_aliases(env, num, name()); + } +} + +environment open_prec_aliases(environment const & env) { + name prec("std", "prec"); + return overwrite_aliases(env, prec, name()); +} + +environment open_priority_aliases(environment const & env) { + name prio("std", "priority"); + return overwrite_aliases(env, prio, name()); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 0f56c6f60..87c1a1625 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -107,4 +107,11 @@ optional is_uniquely_aliased(environment const & env, name const & n); /** \brief Get declaration 'short-name' that can uniquely identify it. */ name get_decl_short_name(name const & d, environment const & env); + +/** \brief Open 'num' notation and aliases. */ +environment open_num_notation(environment const & env); +/** \brief Open 'std.prec' aliases */ +environment open_prec_aliases(environment const & env); +/** \brief Open 'std.priority' aliases */ +environment open_priority_aliases(environment const & env); }