c4718a87ab
this is a first step towards porting the code `constructions.cpp` to Lean: It leaves the construction of the `Declaration` untouched, but moves adding the declarations to the environment, and setting various attributes, to the Lean world. This allows the remaining logic (the construction of the `Declaration`) to be implemented in Lean separately and easily compared to the C++ implementation, before we replace that too. To that end, `Declaraion` gains an `BEq` instance. --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com> Co-authored-by: Arthur Adjedj <arthur.adjedj@ens-paris-saclay.fr>
85 lines
2.5 KiB
C++
85 lines
2.5 KiB
C++
/*
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include "util/name_generator.h"
|
|
#include "kernel/type_checker.h"
|
|
#include "library/util.h"
|
|
#include "library/constants.h"
|
|
|
|
namespace lean {
|
|
static name * g_constructions_fresh = nullptr;
|
|
|
|
static level get_level(type_checker & ctx, expr const & A) {
|
|
expr S = ctx.whnf(ctx.infer(A));
|
|
if (!is_sort(S))
|
|
throw exception("invalid expression, sort expected");
|
|
return sort_level(S);
|
|
}
|
|
|
|
expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) {
|
|
return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
|
|
}
|
|
|
|
expr mk_and_left(type_checker &, expr const & H) {
|
|
return mk_proj(get_and_name(), nat(0), H);
|
|
}
|
|
|
|
expr mk_and_right(type_checker &, expr const & H) {
|
|
return mk_proj(get_and_name(), nat(1), H);
|
|
}
|
|
|
|
expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) {
|
|
level l1 = get_level(ctx, A);
|
|
level l2 = get_level(ctx, B);
|
|
return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
|
|
}
|
|
|
|
expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) {
|
|
expr A = ctx.infer(a);
|
|
expr B = ctx.infer(b);
|
|
level l1 = get_level(ctx, A);
|
|
level l2 = get_level(ctx, B);
|
|
return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
|
|
}
|
|
|
|
expr mk_pprod_fst(type_checker &, expr const & p) {
|
|
return mk_proj(get_pprod_name(), nat(0), p);
|
|
}
|
|
|
|
expr mk_pprod_snd(type_checker &, expr const & p) {
|
|
return mk_proj(get_pprod_name(), nat(1), p);
|
|
}
|
|
|
|
expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) {
|
|
return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
|
|
}
|
|
|
|
expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop) {
|
|
return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
|
|
}
|
|
|
|
expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop) {
|
|
return prop ? mk_and_left(ctx, p) : mk_pprod_fst(ctx, p);
|
|
}
|
|
|
|
expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop) {
|
|
return prop ? mk_and_right(ctx, p) : mk_pprod_snd(ctx, p);
|
|
}
|
|
|
|
name_generator mk_constructions_name_generator() {
|
|
return name_generator(*g_constructions_fresh);
|
|
}
|
|
|
|
void initialize_constructions_util() {
|
|
g_constructions_fresh = new name("_cnstr_fresh");
|
|
mark_persistent(g_constructions_fresh->raw());
|
|
register_name_generator_prefix(*g_constructions_fresh);
|
|
}
|
|
|
|
void finalize_constructions_util() {
|
|
delete g_constructions_fresh;
|
|
}
|
|
}
|