voile/check/
decl.rs

1use std::mem::swap;
2
3use voile_util::loc::ToLoc;
4
5use crate::syntax::abs::AbsDecl;
6use crate::syntax::core::{Neutral, TraverseNeutral, Val, ValInfo, TYPE_OMEGA};
7
8use super::monad::{ValTCM, TCE, TCM, TCS};
9
10/// Checking a list of declarations.
11pub fn check_decls(tcs: TCS, decls: Vec<AbsDecl>) -> TCM {
12    decls.into_iter().try_fold(tcs, check_decl)
13}
14
15fn require_local_emptiness(tcs: &TCS) {
16    debug_assert!(tcs.local_env.is_empty());
17    debug_assert!(tcs.local_gamma.is_empty());
18}
19
20fn unimplemented_to_glob(v: &mut [ValInfo], i: usize) {
21    let mut placeholder = Default::default();
22    swap(&mut v[i], &mut placeholder);
23    placeholder = placeholder.map_ast(|ast| ast.unimplemented_to_glob());
24    swap(&mut placeholder, &mut v[i]);
25}
26
27pub fn inline_metas(mut tcs: TCS, val: ValInfo) -> ValTCM {
28    use Neutral::*;
29    let info = val.loc;
30    let val = val.ast.try_map_neutral(&mut |neut| match neut {
31        Meta(mi) => tcs
32            .meta_context
33            .take_meta(mi)
34            .ok_or_else(|| TCE::MetaUnsolved(mi)),
35        e => Ok(Val::Neut(e)),
36    })?;
37    Ok((val.into_info(info), tcs))
38}
39
40/**
41Checking one declaration.
42$$
43\newcommand{\cdecl}[2]{#1 \vdash_\texttt{d} #2 \ \textbf{ok}}
44\newcommand{\Gcdecl}[1]{\cdecl{\Gamma}{#1}}
45\newcommand{\infer}[3]{#1 \vdash_\texttt{i} #2 \Leftarrow #3}
46\newcommand{\xx}[0]{\texttt{x}}
47\newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4}
48\newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}}
49\newcommand{\ty}[0]{\tau}
50\newcommand{\cA}[0]{\mathcal A}
51\newcommand{\cB}[0]{\mathcal B}
52\cfrac{}{\cdecl{}{}}
53\quad
54\cfrac{}{
55  \infer{
56    \Gamma, \textbf{val } \xx' : \cA
57  }{\xx'}{\cA}
58}
59\quad
60\cfrac{
61  \Gtyck{A}{\ty}{\cA} \quad
62  \cdecl{
63    \Gamma, \textbf{val } \xx' : \cA
64  }{D}
65}{
66  \Gcdecl{\textbf{val } \xx' : A; D}
67}
68\\\\ \space \\\\
69\cfrac{
70  \tyck{
71    \Gamma, \xx' : \cA
72  }{a}{\cA}{\alpha}
73  \quad
74  \cdecl{
75    \Gamma,
76    \textbf{val } \xx' : \cA,
77    \textbf{let } \xx' = \alpha
78  }{D}
79}{
80  \cdecl{
81    \Gamma, \textbf{val } \xx' : \cA
82  }{\textbf{let } \xx' = a; D}
83}
84$$
85*/
86fn check_decl(tcs: TCS, decl: AbsDecl) -> TCM {
87    debug_assert_eq!(tcs.gamma.len(), tcs.env.len());
88    let tcs = match decl {
89        AbsDecl::Impl(impl_abs, sign_dbi) => {
90            let sign = tcs.glob_type(sign_dbi);
91            let sign_cloned = sign.ast.clone();
92            let (val_fake, tcs) = tcs.check(&impl_abs, &sign_cloned)?;
93            // We generate axioms for lambda parameters during type-checking.
94            // Now it's time to change them back to `var` references.
95            let val = val_fake.map_ast(|ast| ast.generated_to_var());
96            let (val, mut tcs) = inline_metas(tcs, val)?;
97
98            tcs.env[sign_dbi.0] = val;
99
100            // Every references to me are now actually valid (they were axioms before),
101            // replace them with a global reference.
102            for i in sign_dbi.0..tcs.glob_len() {
103                unimplemented_to_glob(&mut tcs.env, i);
104            }
105            for i in sign_dbi.0 + 1..tcs.glob_len() {
106                unimplemented_to_glob(&mut tcs.gamma, i);
107            }
108
109            // Err(TCE::DbiOverflow(tcs.env.len(), new_dbi))
110            tcs
111        }
112        AbsDecl::Sign(sign_abs, self_index) => {
113            let loc = sign_abs.loc();
114            let (sign_fake, tcs) = tcs.check(&sign_abs, &TYPE_OMEGA)?;
115            let (sign_fake, mut tcs) = inline_metas(tcs, sign_fake)?;
116            let sign = sign_fake.map_ast(|ast| ast.generated_to_var());
117            let val_info = Val::fresh_unimplemented(self_index).into_info(loc);
118            tcs.env.push(val_info);
119            tcs.gamma.push(sign);
120
121            // Give warning on axiom?
122            tcs
123        }
124        AbsDecl::Decl(impl_abs) => {
125            let (inferred, tcs) = tcs.infer(&impl_abs)?;
126            let (inferred, tcs) = inline_metas(tcs, inferred)?;
127            let (compiled, tcs) = tcs.evaluate(impl_abs);
128            let (compiled, mut tcs) = inline_metas(tcs, compiled)?;
129            let compiled = compiled.map_ast(|ast| ast.generated_to_var());
130            let inferred = inferred.map_ast(|ast| ast.generated_to_var());
131            tcs.env.push(compiled);
132            tcs.gamma.push(inferred);
133
134            tcs
135        }
136    };
137
138    require_local_emptiness(&tcs);
139    Ok(tcs)
140}
141
142impl TCS {
143    #[inline]
144    pub fn check_decls(self, decls: Vec<AbsDecl>) -> TCM {
145        check_decls(self, decls)
146    }
147}
voile/check/decl.rs

voile/check/
decl.rs
