voile/syntax/abs/
trans.rs

1use std::collections::BTreeMap;
2
3use voile_util::loc::*;
4use voile_util::meta::MI;
5use voile_util::tags::{PiSig::*, *};
6use voile_util::uid::*;
7
8use crate::check::monad::{TCE, TCM};
9use crate::syntax::surf::{Decl, DeclKind, Expr, Param};
10
11use super::ast::*;
12
13/// Key: global declaration name; Value: global declaration index.
14type GlobCtx = BTreeMap<String, GI>;
15
16/// Key: local declaration name; Value: de-bruijn indices.
17type LocalCtx = BTreeMap<String, (DBI, Plicit)>;
18
19pub fn trans_decls(decls: Vec<Decl>) -> TCM<Vec<AbsDecl>> {
20    trans_decls_contextual(Default::default(), decls).map(|tcs| tcs.decls)
21}
22
23pub fn trans_decls_contextual(tcs: TransState, decls: Vec<Decl>) -> TCM<TransState> {
24    decls.into_iter().try_fold(tcs, trans_one_decl)
25}
26
27/// Translation state.
28#[derive(Debug, Clone, Default)]
29pub struct TransState {
30    pub decls: Vec<AbsDecl>,
31    /// The index of the $n_{th}$ valid declaration
32    /// (`Impl`s are not counted as valid declarations because they're just
33    /// attachments to existing declarations).
34    pub signature_indices: Vec<DBI>,
35    pub context_mapping: GlobCtx,
36    pub decl_count: GI,
37    pub meta_count: MI,
38}
39
40fn trans_one_decl(mut tcs: TransState, decl: Decl) -> TCM<TransState> {
41    let abs = trans_expr(
42        decl.body,
43        &tcs.decls,
44        &mut tcs.meta_count,
45        &tcs.context_mapping,
46    )?;
47
48    let decl_total = tcs.decl_count;
49    let dbi = *tcs
50        .context_mapping
51        .entry(decl.name.text.clone())
52        .or_insert_with(|| decl_total);
53    let original = if decl_total > dbi {
54        Some(&tcs.decls[tcs.signature_indices[dbi.0].0])
55    } else {
56        None
57    };
58    let modified = match (decl.kind, original) {
59        (DeclKind::Sign, None) => {
60            let abs = AbsDecl::Sign(abs, tcs.decl_count);
61            tcs.signature_indices.push(DBI(tcs.decls.len()));
62            tcs.decl_count += 1;
63            abs
64        }
65        // Re-type-signaturing something, should give error
66        (DeclKind::Sign, Some(thing)) => {
67            return Err(TCE::ReDefine(decl.name.loc, thing.loc()));
68        }
69        // Re-defining something, should give error
70        (_, Some(AbsDecl::Impl(thing, ..))) | (_, Some(AbsDecl::Decl(thing))) => {
71            return Err(TCE::ReDefine(decl.name.loc, thing.loc()));
72        }
73        (DeclKind::Impl, None) => {
74            tcs.decl_count += 1;
75            tcs.signature_indices.push(DBI(tcs.decls.len()));
76            AbsDecl::Decl(abs)
77        }
78        (DeclKind::Impl, Some(AbsDecl::Sign(_, dbi))) => AbsDecl::Impl(abs, *dbi),
79    };
80    tcs.decls.push(modified);
81    Ok(tcs)
82}
83
84pub fn trans_expr(expr: Expr, env: &[AbsDecl], meta_count: &mut MI, map: &GlobCtx) -> TCM<Abs> {
85    trans_expr_inner(expr, meta_count, env, map, &[], &Default::default())
86}
87
88fn trans_expr_inner(
89    expr: Expr,
90    meta_count: &mut MI,
91    env: &[AbsDecl],
92    global_map: &GlobCtx,
93    local_env: &[UID],
94    local_map: &LocalCtx,
95) -> TCM<Abs> {
96    let mut recursion =
97        |e: Expr| trans_expr_inner(e, meta_count, env, global_map, local_env, local_map);
98    let map_labels =
99        |Labelled { expr, label }| recursion(expr).map(|expr| Labelled { label, expr });
100    match expr {
101        Expr::Type(syntax, level) => Ok(Abs::Type(syntax, level)),
102        Expr::Var(ident) => {
103            let name = &ident.text;
104            if local_map.contains_key(name) {
105                let (dbi, _) = local_map[name];
106                Ok(Abs::Var(ident.clone(), local_env[dbi.0], dbi))
107            } else if global_map.contains_key(name) {
108                Ok(Abs::Ref(ident.clone(), global_map[name]))
109            } else {
110                Err(TCE::LookUpFailed(ident.clone()))
111            }
112        }
113        Expr::App(app_vec) => Ok(app_vec.try_map(recursion)?.fold1(|result: Abs, abs: Abs| {
114            Abs::app(merge_info(&result, &abs), result, Plicit::Ex, abs)
115        })),
116        // I really hope I can reuse the code with `App` here :(
117        Expr::Pipe(pipe_vec) => Ok(pipe_vec
118            .try_map(recursion)?
119            .rev_fold1(|result, abs| Abs::app(merge_info(&result, &abs), result, Plicit::Ex, abs))),
120        Expr::Meta(ident) => {
121            let ret = Ok(Abs::Meta(ident.clone(), *meta_count));
122            *meta_count += 1;
123            ret
124        }
125        Expr::Cons(ident) => Ok(Abs::Cons(ident.clone())),
126        // TODO: check uniqueness?
127        Expr::RowKind(info, kind, labels) => Ok(Abs::RowKind(info, kind, labels)),
128        Expr::Proj(expr, projections) => Ok(projections.fold(recursion(*expr)?, |abs, label| {
129            Abs::proj(merge_info(&abs, &label), abs, label)
130        })),
131        Expr::RowPoly(info, kind, labels, rest) => {
132            let labels: Result<_, _> = labels.into_iter().map(map_labels).collect();
133            let rest = rest.map(|e| recursion(*e)).transpose()?;
134            Ok(Abs::row_polymorphic_type(info, kind, labels?, rest))
135        }
136        Expr::Rec(info, fields, rest) => {
137            let labels: Result<_, _> = fields.into_iter().map(map_labels).collect();
138            let rest = rest.map(|e| recursion(*e)).transpose()?;
139            Ok(Abs::record(info, labels?, rest))
140        }
141        Expr::Tup(tup_vec) => Ok(tup_vec
142            .try_map(recursion)?
143            .fold1(|pair, abs| Abs::pair(abs.loc(), pair, abs))),
144        Expr::Sig(initial, last) => trans_dependent_type(
145            meta_count, env, global_map, local_env, local_map, initial, *last, Sigma,
146        ),
147        Expr::Cases(label, binding, body, or) => {
148            let or = trans_expr_inner(*or, meta_count, env, global_map, local_env, local_map)?;
149            let mut local = local_env.to_vec();
150            local.reserve_exact(local.len() + 1);
151            let mut local_map = local_map.clone();
152            let mut names = Vec::with_capacity(1);
153            introduce_abstractions(&[binding.clone()], &mut local, &mut local_map, &mut names);
154            let body = trans_expr_inner(*body, meta_count, env, global_map, &local, &local_map)?;
155            Ok(Abs::case_or(label, binding, names[0], body, or))
156        }
157        Expr::Whatever(info) => Ok(Abs::Whatever(info)),
158        Expr::Lam(info, params, body) => {
159            let mut local = local_env.to_vec();
160            local.reserve_exact(local.len() + params.len() + 1);
161            let mut local_map = local_map.clone();
162            let mut names = Vec::with_capacity(params.len());
163            introduce_abstractions(&params, &mut local, &mut local_map, &mut names);
164            let body = trans_expr_inner(*body, meta_count, env, global_map, &local, &local_map)?;
165            Ok(params.into_iter().rev().fold(body, |lam_abs, param| {
166                let pop_empty = "The stack `names` is empty. Please report this as a bug.";
167                let name = names.pop().expect(pop_empty);
168                Abs::lam(info.clone(), param.clone(), name, lam_abs)
169            }))
170        }
171        Expr::Pi(params, result) => trans_dependent_type(
172            meta_count, env, global_map, local_env, local_map, params, *result, Pi,
173        ),
174        Expr::Lift(info, levels, inner) => Ok(Abs::lift(info, levels, recursion(*inner)?)),
175    }
176}
177
178fn introduce_abstractions(
179    params: &[Ident],
180    local_env: &mut Vec<UID>,
181    local_map: &mut LocalCtx,
182    names: &mut Vec<UID>,
183) {
184    for param in params {
185        let shadowing = local_map.get(&param.text).cloned().map(|(dbi, _)| dbi);
186        for (_name, (dbi, _)) in local_map.iter_mut() {
187            let dbi_value = *dbi;
188            *dbi += 1;
189            if shadowing == Some(dbi_value) {
190                local_env.remove(dbi_value.0);
191            }
192        }
193        local_map.insert(param.text.clone(), (Default::default(), Plicit::Ex));
194        let new_name = unsafe { next_uid() };
195        local_env.insert(0, new_name);
196        names.push(new_name);
197    }
198}
199
200fn trans_dependent_type(
201    meta_count: &mut MI,
202    env: &[AbsDecl],
203    global_map: &GlobCtx,
204    local_env: &[UID],
205    local_map: &LocalCtx,
206    params: Vec<Param>,
207    result: Expr,
208    kind: PiSig,
209) -> TCM<Abs> {
210    let mut pi_env = local_env.to_vec();
211    let mut pi_map = local_map.clone();
212    let mut names = Vec::with_capacity(params.len());
213    let pi_initial = Vec::with_capacity(params.len());
214    let pi_vec: Vec<(Abs, Plicit)> = params.into_iter().try_fold(pi_initial, |pi_vec, param| {
215        introduce_telescope(
216            meta_count,
217            env,
218            global_map,
219            &mut pi_env,
220            &mut pi_map,
221            &mut names,
222            pi_vec,
223            param,
224        )
225    })?;
226
227    Ok(pi_vec.into_iter().rev().fold(
228        trans_expr_inner(result, meta_count, env, global_map, &pi_env, &pi_map)?,
229        |pi_abs, (param, plicit)| {
230            let info = param.loc() + pi_abs.loc();
231            let pop_empty = "The stack `names` is empty. Please report this as a bug.";
232            Abs::dependent_type(
233                info,
234                kind,
235                names.pop().expect(pop_empty),
236                plicit,
237                param,
238                pi_abs,
239            )
240        },
241    ))
242}
243
244fn introduce_telescope(
245    meta_count: &mut MI,
246    env: &[AbsDecl],
247    global_map: &GlobCtx,
248    dt_env: &mut Vec<UID>,
249    dt_map: &mut LocalCtx,
250    names: &mut Vec<UID>,
251    mut dt_vec: Vec<(Abs, Plicit)>,
252    param: Param,
253) -> TCM<Vec<(Abs, Plicit)>> {
254    let param_ty = trans_expr_inner(param.ty, meta_count, env, global_map, &dt_env, &dt_map)?;
255    for name in &param.names {
256        let param_name = name.text.clone();
257        // These two are actually our assumption. Hope they're correct.
258        assert_eq!(dt_env.len(), dt_map.len());
259        // let shadowing = dt_map.get(&param_name).cloned();
260        dt_map.iter_mut().for_each(|(_name, (dbi, _))| *dbi += 1);
261        /*
262        let dbi_value = *dbi;
263        if shadowing == Some(dbi_value) {
264            // just remove the DBI map, for there still need to be a place holder in `Vec`
265            dt_env.remove(dbi_value);
266            // this is not necessary for dt_map will be updated below
267            // *dbi = 0;
268        }
269        */
270        dt_map.insert(param_name, (Default::default(), param.plicit));
271        let new_name = unsafe { next_uid() };
272        dt_env.insert(0, new_name);
273        names.push(new_name);
274        dt_vec.push((param_ty.clone(), param.plicit));
275    }
276    if param.names.is_empty() {
277        let new_name = unsafe { next_uid() };
278        dt_map.iter_mut().for_each(|(_name, (dbi, _))| *dbi += 1);
279        dt_env.insert(0, new_name);
280        names.push(new_name);
281        dt_vec.push((param_ty, param.plicit));
282    }
283
284    Ok(dt_vec)
285}
voile/syntax/abs/trans.rs

voile/syntax/abs/
trans.rs
