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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
use crate::error::TypeError;
use crate::semantics::{type_with, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{Ctxt, ImportAlternativeId, ImportId, ToExprOptions};
/// Stores an alpha-normalized variable.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct AlphaVar {
idx: usize,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum HirKind<'cx> {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
/// A variable that couldn't be resolved. Detected during resolution, but causes an error during typeck.
MissingVar(V),
/// An import. It must have been resolved after resolution.
Import(ImportId<'cx>),
/// An import alternative. It must have been decided after resolution.
ImportAlternative(ImportAlternativeId<'cx>, Hir<'cx>, Hir<'cx>),
// Forbidden ExprKind variants: Var, Import, Completion
Expr(ExprKind<Hir<'cx>>),
}
// An expression with resolved variables and imports.
#[derive(Debug, Clone)]
pub struct Hir<'cx> {
kind: Box<HirKind<'cx>>,
span: Span,
}
impl AlphaVar {
pub fn new(idx: usize) -> Self {
AlphaVar { idx }
}
pub fn idx(self) -> usize {
self.idx
}
}
impl<'cx> Hir<'cx> {
pub fn new(kind: HirKind<'cx>, span: Span) -> Self {
Hir {
kind: Box::new(kind),
span,
}
}
pub fn kind(&self) -> &HirKind<'cx> {
&*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, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr {
hir_to_expr(cx, self, opts, &mut NameEnv::new())
}
/// Converts a closed Hir expr back to the corresponding AST expression.
pub fn to_expr_noopts(&self, cx: Ctxt<'cx>) -> Expr {
let opts = ToExprOptions { alpha: false };
self.to_expr(cx, opts)
}
pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr {
let opts = ToExprOptions { alpha: true };
self.to_expr(cx, opts)
}
pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
let opts = ToExprOptions { alpha: false };
let cx = env.cx();
let mut env = env.as_nameenv().clone();
hir_to_expr(cx, self, opts, &mut env)
}
/// Typecheck the Hir.
pub fn typecheck<'hir>(
&'hir self,
env: &TyEnv<'cx>,
) -> Result<Tir<'cx, 'hir>, TypeError> {
type_with(env, self, None)
}
pub fn typecheck_noenv<'hir>(
&'hir self,
cx: Ctxt<'cx>,
) -> Result<Tir<'cx, 'hir>, TypeError> {
typecheck(cx, self)
}
/// Eval the Hir. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
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, cx: Ctxt<'cx>) -> Nir<'cx> {
self.eval(NzEnv::new(cx))
}
}
fn hir_to_expr<'cx>(
cx: Ctxt<'cx>,
hir: &Hir<'cx>,
opts: ToExprOptions,
env: &mut NameEnv,
) -> Expr {
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::MissingVar(v) => ExprKind::Var(v.clone()),
HirKind::Import(import) => {
let typed = cx[import].unwrap_result();
return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new());
}
HirKind::ImportAlternative(alt, left, right) => {
let hir = if cx[alt].unwrap_selected() {
left
} else {
right
};
return hir_to_expr(cx, hir, opts, env);
}
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(cx, hir, opts, env);
if l.is_some() {
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<'cx> std::cmp::PartialEq for Hir<'cx> {
fn eq(&self, other: &Self) -> bool {
self.kind == other.kind
}
}
impl<'cx> std::cmp::Eq for Hir<'cx> {}
|
