1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
use crate::semantics::core::value::Value;
use crate::semantics::core::value_kind::ValueKind;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::NormalizedExpr;
use crate::syntax;
use crate::syntax::{Builtin, ExprF};
#[derive(Copy, Clone)]
/// Controls conversion from `Value` to `Expr`
pub(crate) struct ToExprOptions {
/// Whether to convert all variables to `_`
pub(crate) alpha: bool,
/// Whether to normalize before converting
pub(crate) normalize: bool,
}
/// Converts a value back to the corresponding AST expression.
pub(crate) fn value_to_expr(
val: &Value,
opts: ToExprOptions,
) -> NormalizedExpr {
if opts.normalize {
val.normalize_whnf();
}
val.as_kind().to_expr(opts)
}
/// Converts a value back to the corresponding AST expression.
pub(crate) fn kind_to_expr(
kind: &ValueKind,
opts: ToExprOptions,
) -> NormalizedExpr {
match kind {
ValueKind::Lam(x, t, e) => rc(ExprF::Lam(
x.to_label_maybe_alpha(opts.alpha),
t.to_expr(opts),
e.to_expr(opts),
)),
ValueKind::AppliedBuiltin(b, args) => args
.iter()
.map(|v| v.to_expr(opts))
.fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
ValueKind::Pi(x, t, e) => rc(ExprF::Pi(
x.to_label_maybe_alpha(opts.alpha),
t.to_expr(opts),
e.to_expr(opts),
)),
ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
ValueKind::Const(c) => rc(ExprF::Const(*c)),
ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)),
ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
ValueKind::EmptyOptionalLit(n) => rc(ExprF::App(
rc(ExprF::Builtin(Builtin::OptionalNone)),
n.to_expr(opts),
)),
ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
rc(ExprF::Builtin(Builtin::List)),
n.to_expr(opts),
)))),
ValueKind::NEListLit(elts) => rc(ExprF::NEListLit(
elts.iter().map(|n| n.to_expr(opts)).collect(),
)),
ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit(
kvs.iter()
.map(|(k, v)| (k.clone(), v.to_expr(opts)))
.collect(),
)),
ValueKind::RecordType(kts) => rc(ExprF::RecordType(
kts.iter()
.map(|(k, v)| (k.clone(), v.to_expr(opts)))
.collect(),
)),
ValueKind::UnionType(kts) => rc(ExprF::UnionType(
kts.iter()
.map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts))))
.collect(),
)),
ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field(
ValueKind::UnionType(kts.clone()).to_expr(opts),
l.clone(),
)),
ValueKind::UnionLit(l, v, kts) => rc(ExprF::App(
ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
v.to_expr(opts),
)),
ValueKind::TextLit(elts) => rc(ExprF::TextLit(
elts.iter()
.map(|contents| contents.map_ref(|e| e.to_expr(opts)))
.collect(),
)),
ValueKind::Equivalence(x, y) => rc(ExprF::BinOp(
syntax::BinOp::Equivalence,
x.to_expr(opts),
y.to_expr(opts),
)),
ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
}
}
|
