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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
use crate::error::TypeError;
use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{NormalizedExpr, ToExprOptions};
/// Stores an alpha-normalized variable.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct AlphaVar {
idx: usize,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum HirKind {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
/// Result of resolving an import.
Import(Hir, Type),
// Forbidden ExprKind variants: Var, Import, Completion
Expr(ExprKind<Hir>),
}
// An expression with resolved variables and imports.
#[derive(Debug, Clone)]
pub(crate) struct Hir {
kind: Box<HirKind>,
span: Span,
}
impl AlphaVar {
pub(crate) fn new(idx: usize) -> Self {
AlphaVar { idx }
}
pub(crate) fn idx(&self) -> usize {
self.idx
}
}
impl Hir {
pub fn new(kind: HirKind, span: Span) -> Self {
Hir {
kind: Box::new(kind),
span,
}
}
pub fn kind(&self) -> &HirKind {
&*self.kind
}
pub fn span(&self) -> Span {
self.span.clone()
}
/// Converts a closed Hir expr back to the corresponding AST expression.
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
hir_to_expr(self, opts, &mut NameEnv::new())
}
/// Converts a closed Hir expr back to the corresponding AST expression.
pub fn to_expr_noopts(&self) -> NormalizedExpr {
let opts = ToExprOptions { alpha: false };
self.to_expr(opts)
}
pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
let opts = ToExprOptions { alpha: false };
let mut env = env.as_nameenv().clone();
hir_to_expr(self, opts, &mut env)
}
/// Typecheck the Hir.
pub fn typecheck<'hir>(
&'hir self,
env: &TyEnv,
) -> Result<Tir<'hir>, TypeError> {
type_with(env, self, None)
}
/// Eval the Hir. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
Nir::new_thunk(env.into(), self.clone())
}
/// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
pub fn eval_closed_expr(&self) -> Nir {
self.eval(NzEnv::new())
}
/// Eval a closed Hir fully and recursively;
pub fn rec_eval_closed_expr(&self) -> Nir {
let val = self.eval_closed_expr();
val.normalize();
val
}
}
fn hir_to_expr(
hir: &Hir,
opts: ToExprOptions,
env: &mut NameEnv,
) -> NormalizedExpr {
let kind = match hir.kind() {
HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
HirKind::Import(hir, _) => {
return hir_to_expr(hir, opts, &mut NameEnv::new())
}
HirKind::Expr(e) => {
let e = e.map_ref_maybe_binder(|l, hir| {
if let Some(l) = l {
env.insert_mut(l);
}
let e = hir_to_expr(hir, opts, env);
if let Some(_) = l {
env.remove_mut();
}
e
});
match e {
ExprKind::Lam(_, t, e) if opts.alpha => {
ExprKind::Lam("_".into(), t, e)
}
ExprKind::Pi(_, t, e) if opts.alpha => {
ExprKind::Pi("_".into(), t, e)
}
e => e,
}
}
};
Expr::new(kind, hir.span())
}
impl std::cmp::PartialEq for Hir {
fn eq(&self, other: &Self) -> bool {
self.kind == other.kind
}
}
impl std::cmp::Eq for Hir {}
|
