logicaffeine_kernel/dag/
logos.rs

1//! LOGOS's own terms in the core's store: [`lower`] takes a [`Term`] of LOGOS's Calculus of
2//! Inductive Constructions to an [`ExprId`], and [`lift`] takes it back.
3//!
4//! Named variables become de Bruijn indices, a global becomes a constant (one name component, as
5//! written), and LOGOS's universes become levels: `Prop` is `0`, `Type n` is `n + 1`, `SProp` is
6//! [`super::level::LevelNode::SProp`]. `match`, `fix` and mutual `fix` are their
7//! own nodes, and the literals keep their LOGOS meaning (`Nat` and `Text` as the core's `Nat` and
8//! string literals, the rest as [`Lit`]). An annotation is transparent and is not kept; a hole is
9//! not a kernel term and is refused.
10//!
11//! `lift` names a variable after the depth of its binder (`v0` outermost), so a lifted term is
12//! α-equivalent to the term that was lowered, and lowering it again gives the same id. It names the
13//! kernel's local `i` `fvar{i}`, which [`lower_open`] takes back to that local.
14
15use super::expr::{ExprId, Lit, Node, Store};
16use super::level::{LevelId, LevelNode, LevelsId};
17use super::name::{NameId, NameNode};
18use super::nat::Nat;
19use crate::term::{Literal, Term, Universe};
20
21/// Why a term has no image in the core.
22#[derive(Clone, Debug, PartialEq)]
23pub enum LowerError {
24    /// A variable no enclosing binder binds.
25    Unbound(String),
26    /// An unelaborated metavariable.
27    Hole,
28}
29
30/// The core expression for a closed LOGOS term.
31pub fn lower(store: &mut Store, t: &Term) -> Result<ExprId, LowerError> {
32    Lowering {
33        store,
34        scope: Vec::new(),
35        open: false,
36    }
37    .term(t)
38}
39
40/// The core expression for a LOGOS term over the kernel's locals, named as [`lift`] names them.
41pub fn lower_open(store: &mut Store, t: &Term) -> Result<ExprId, LowerError> {
42    Lowering {
43        store,
44        scope: Vec::new(),
45        open: true,
46    }
47    .term(t)
48}
49
50/// The local `lift` names `v`, if it names one.
51fn local_named(v: &str) -> Option<u32> {
52    let i: u32 = v.strip_prefix("fvar")?.parse().ok()?;
53    (local_name(i) == v).then_some(i)
54}
55
56fn local_name(i: u32) -> String {
57    format!("fvar{i}")
58}
59
60/// The core level for a LOGOS universe.
61pub fn lower_universe(store: &mut Store, u: &Universe) -> LevelId {
62    match u {
63        Universe::SProp => store.levels.sprop(),
64        Universe::Prop => LevelId::ZERO,
65        Universe::Type(n) => store.levels.of_nat(*n as u64 + 1),
66        Universe::Var(v) => {
67            let n = store.names.str(NameId::ANON, v);
68            store.levels.param(n)
69        }
70        Universe::Succ(a) => {
71            let a = lower_universe(store, a);
72            store.levels.succ(a)
73        }
74        Universe::Max(a, b) => {
75            let (a, b) = (lower_universe(store, a), lower_universe(store, b));
76            store.levels.max_raw(a, b)
77        }
78        Universe::IMax(a, b) => {
79            let (a, b) = (lower_universe(store, a), lower_universe(store, b));
80            store.levels.imax_raw(a, b)
81        }
82    }
83}
84
85struct Lowering<'s> {
86    store: &'s mut Store,
87    /// The binder names in scope, innermost last.
88    scope: Vec<String>,
89    /// Whether a free variable may name one of the kernel's locals.
90    open: bool,
91}
92
93impl Lowering<'_> {
94    fn under<T>(&mut self, names: &[&String], f: impl FnOnce(&mut Self) -> T) -> T {
95        self.scope.extend(names.iter().map(|n| (*n).clone()));
96        let r = f(self);
97        self.scope.truncate(self.scope.len() - names.len());
98        r
99    }
100
101    fn global(&mut self, name: &str, levels: &[Universe]) -> ExprId {
102        let n = self.store.names.str(NameId::ANON, name);
103        let ls: Vec<LevelId> = levels
104            .iter()
105            .map(|u| lower_universe(self.store, u))
106            .collect();
107        self.store.cnst_levels(n, &ls)
108    }
109
110    fn term(&mut self, t: &Term) -> Result<ExprId, LowerError> {
111        Ok(match t {
112            Term::Sort(u) => {
113                let l = lower_universe(self.store, u);
114                self.store.sort(l)
115            }
116            Term::Var(v) => match self.scope.iter().rposition(|n| n == v) {
117                Some(i) => self.store.bvar((self.scope.len() - 1 - i) as u32),
118                None => match local_named(v).filter(|_| self.open) {
119                    Some(i) => self.store.fvar(i),
120                    None => return Err(LowerError::Unbound(v.clone())),
121                },
122            },
123            Term::Global(n) => self.global(n, &[]),
124            Term::Const { name, levels } => self.global(name, levels),
125            Term::Pi {
126                param,
127                param_type,
128                body_type,
129            } => {
130                let a = self.term(param_type)?;
131                let b = self.under(&[param], |l| l.term(body_type))?;
132                self.store.pi(a, b)
133            }
134            Term::Lambda {
135                param,
136                param_type,
137                body,
138            } => {
139                let a = self.term(param_type)?;
140                let b = self.under(&[param], |l| l.term(body))?;
141                self.store.lam(a, b)
142            }
143            Term::App(f, a) => {
144                let (f, a) = (self.term(f)?, self.term(a)?);
145                self.store.app(f, a)
146            }
147            Term::Match {
148                discriminant,
149                motive,
150                cases,
151            } => {
152                let d = self.term(discriminant)?;
153                let m = self.term(motive)?;
154                let cs = cases
155                    .iter()
156                    .map(|c| self.term(c))
157                    .collect::<Result<Vec<_>, _>>()?;
158                self.store.match_(d, m, &cs)
159            }
160            Term::Fix { name, body } => {
161                let b = self.under(&[name], |l| l.term(body))?;
162                self.store.fix(b)
163            }
164            Term::MutualFix { defs, index } => {
165                let names: Vec<&String> = defs.iter().map(|(n, _)| n).collect();
166                let bodies = self.under(&names, |l| {
167                    defs.iter()
168                        .map(|(_, b)| l.term(b))
169                        .collect::<Result<Vec<_>, _>>()
170                })?;
171                self.store.mutual_fix(&bodies, *index as u32)
172            }
173            Term::Let {
174                name,
175                ty,
176                value,
177                body,
178            } => {
179                let (ty, value) = (self.term(ty)?, self.term(value)?);
180                let body = self.under(&[name], |l| l.term(body))?;
181                self.store.let_(ty, value, body)
182            }
183            Term::Lit(lit) => match lit {
184                Literal::Int(i) => self.store.lit(Lit::Int(*i)),
185                Literal::BigInt(b) => self.store.lit(Lit::BigInt(b.clone())),
186                Literal::Nat(n) => self.store.nat_lit(Nat::from_bigint(n)),
187                Literal::Float(f) => self.store.lit(Lit::Float(f.to_bits())),
188                Literal::Text(s) => self.store.str_lit(s),
189                Literal::Duration(d) => self.store.lit(Lit::Duration(*d)),
190                Literal::Date(d) => self.store.lit(Lit::Date(*d)),
191                Literal::Moment(m) => self.store.lit(Lit::Moment(*m)),
192            },
193            Term::Annotated { term, .. } => self.term(term)?,
194            Term::Hole => return Err(LowerError::Hole),
195        })
196    }
197}
198
199/// The LOGOS term for a closed core expression.
200pub fn lift(store: &Store, e: ExprId) -> Term {
201    lift_at(store, e, 0)
202}
203
204/// The LOGOS universe for a core level.
205pub fn lift_level(store: &Store, l: LevelId) -> Universe {
206    let ls = &store.levels;
207    if let Some(n) = concrete(store, l) {
208        return if n == 0 {
209            Universe::Prop
210        } else {
211            Universe::Type((n - 1) as u32)
212        };
213    }
214    match ls.node(l) {
215        LevelNode::SProp => Universe::SProp,
216        LevelNode::Zero => Universe::Prop,
217        LevelNode::Succ(a) => Universe::Succ(Box::new(lift_level(store, a))),
218        LevelNode::Max(a, b) => Universe::Max(
219            Box::new(lift_level(store, a)),
220            Box::new(lift_level(store, b)),
221        ),
222        LevelNode::IMax(a, b) => Universe::IMax(
223            Box::new(lift_level(store, a)),
224            Box::new(lift_level(store, b)),
225        ),
226        LevelNode::Param(n) => Universe::Var(component(store, n)),
227    }
228}
229
230/// `succ` applied `n` times to `0`.
231fn concrete(store: &Store, mut l: LevelId) -> Option<u64> {
232    let mut n = 0u64;
233    loop {
234        match store.levels.node(l) {
235            LevelNode::Zero => return Some(n),
236            LevelNode::Succ(a) => {
237                n += 1;
238                l = a;
239            }
240            _ => return None,
241        }
242    }
243}
244
245/// A core name as the `Term` kernel spells it.
246pub(super) fn component(store: &Store, n: NameId) -> String {
247    match store.names.node(n) {
248        NameNode::Str(p, s) if *p == NameId::ANON => store.names.component(*s).to_string(),
249        _ => store.names.display(n),
250    }
251}
252
253fn var(level: u32) -> String {
254    format!("v{level}")
255}
256
257fn lift_at(store: &Store, e: ExprId, depth: u32) -> Term {
258    let bx = |t: Term| Box::new(t);
259    match store.node(e) {
260        Node::BVar(i) => Term::Var(var(depth - 1 - i)),
261        Node::FVar(i) => Term::Var(local_name(i)),
262        Node::Sort(l) => Term::Sort(lift_level(store, l)),
263        Node::Const(n, ls) => {
264            let levels: Vec<Universe> = store
265                .levels
266                .get_list(ls)
267                .iter()
268                .map(|l| lift_level(store, *l))
269                .collect();
270            if ls == LevelsId::EMPTY {
271                Term::Global(component(store, n))
272            } else {
273                Term::Const {
274                    name: component(store, n),
275                    levels,
276                }
277            }
278        }
279        Node::App(f, a) => Term::App(bx(lift_at(store, f, depth)), bx(lift_at(store, a, depth))),
280        Node::Lam(t, b) => Term::Lambda {
281            param: var(depth),
282            param_type: bx(lift_at(store, t, depth)),
283            body: bx(lift_at(store, b, depth + 1)),
284        },
285        Node::Pi(t, b) => Term::Pi {
286            param: var(depth),
287            param_type: bx(lift_at(store, t, depth)),
288            body_type: bx(lift_at(store, b, depth + 1)),
289        },
290        Node::Let(t, v, b) => Term::Let {
291            name: var(depth),
292            ty: bx(lift_at(store, t, depth)),
293            value: bx(lift_at(store, v, depth)),
294            body: bx(lift_at(store, b, depth + 1)),
295        },
296        Node::NatLit(n) => Term::Lit(Literal::Nat(store.nat(n).to_bigint())),
297        Node::StrLit(s) => Term::Lit(Literal::Text(store.string(s).to_string())),
298        Node::Lit(l) => Term::Lit(match store.lit_value(l) {
299            Lit::Int(i) => Literal::Int(*i),
300            Lit::BigInt(b) => Literal::BigInt(b.clone()),
301            Lit::Float(bits) => Literal::Float(f64::from_bits(*bits)),
302            Lit::Duration(d) => Literal::Duration(*d),
303            Lit::Date(d) => Literal::Date(*d),
304            Lit::Moment(m) => Literal::Moment(*m),
305        }),
306        Node::Match(d, m, cs) => Term::Match {
307            discriminant: bx(lift_at(store, d, depth)),
308            motive: bx(lift_at(store, m, depth)),
309            cases: store
310                .seq_items(cs)
311                .iter()
312                .map(|c| lift_at(store, *c, depth))
313                .collect(),
314        },
315        Node::Fix(b) => Term::Fix {
316            name: var(depth),
317            body: bx(lift_at(store, b, depth + 1)),
318        },
319        Node::MutualFix(ds, index) => {
320            let bodies = store.seq_items(ds);
321            let n = bodies.len() as u32;
322            Term::MutualFix {
323                defs: bodies
324                    .iter()
325                    .enumerate()
326                    .map(|(i, b)| (var(depth + i as u32), lift_at(store, *b, depth + n)))
327                    .collect(),
328                index: index as usize,
329            }
330        }
331        Node::Proj(..) => {
332            unreachable!("LOGOS has no projection node: a Lean projection is not a LOGOS term")
333        }
334        Node::Seq(..) | Node::Nil => unreachable!("a sequence is lifted by the node that holds it"),
335    }
336}
337
338/// The levels the `Term` kernel's application rule infers for a bare reference to a
339/// universe-polymorphic declaration (`type_checker::implicit_levels_for_head`), written out. The
340/// declaration's level parameters become metavariables; left to right, each argument whose domain
341/// mentions one solves it from the argument's type; a head whose every level is solved becomes
342/// `Const` at those levels. A head left with an unsolved level stays a bare reference, which the
343/// core refuses rather than guesses at.
344///
345/// This is elaboration, outside the trusted core: the core checks the explicit term it produces,
346/// so a level chosen wrongly here can only make a declaration fail, never let one through.
347pub fn explicit_levels(ctx: &crate::Context, t: &Term) -> Term {
348    let bx = |t: Term| Box::new(t);
349    match t {
350        Term::App(..) => {
351            let mut args = Vec::new();
352            let mut head = t;
353            while let Term::App(f, a) = head {
354                args.push(a.as_ref());
355                head = f;
356            }
357            args.reverse();
358            let args: Vec<Term> = args.iter().map(|a| explicit_levels(ctx, a)).collect();
359            let head = match head {
360                Term::Global(n) => solve_levels(ctx, n, &args).unwrap_or_else(|| head.clone()),
361                other => explicit_levels(ctx, other),
362            };
363            args.into_iter().fold(head, |f, a| Term::App(bx(f), bx(a)))
364        }
365        Term::Pi {
366            param,
367            param_type,
368            body_type,
369        } => {
370            let a = explicit_levels(ctx, param_type);
371            let inner = ctx.extend(param, a.clone());
372            Term::Pi {
373                param: param.clone(),
374                param_type: bx(a),
375                body_type: bx(explicit_levels(&inner, body_type)),
376            }
377        }
378        Term::Lambda {
379            param,
380            param_type,
381            body,
382        } => {
383            let a = explicit_levels(ctx, param_type);
384            let inner = ctx.extend(param, a.clone());
385            Term::Lambda {
386                param: param.clone(),
387                param_type: bx(a),
388                body: bx(explicit_levels(&inner, body)),
389            }
390        }
391        Term::Let {
392            name,
393            ty,
394            value,
395            body,
396        } => {
397            let ty2 = explicit_levels(ctx, ty);
398            let value2 = explicit_levels(ctx, value);
399            let inner = ctx.extend(name, ty2.clone());
400            Term::Let {
401                name: name.clone(),
402                ty: bx(ty2),
403                value: bx(value2),
404                body: bx(explicit_levels(&inner, body)),
405            }
406        }
407        Term::Match {
408            discriminant,
409            motive,
410            cases,
411        } => Term::Match {
412            discriminant: bx(explicit_levels(ctx, discriminant)),
413            motive: bx(explicit_levels(ctx, motive)),
414            cases: cases.iter().map(|c| explicit_levels(ctx, c)).collect(),
415        },
416        Term::Fix { name, body } => {
417            let inner = match crate::type_checker::infer_type(ctx, t) {
418                Ok(ty) => ctx.extend(name, ty),
419                Err(_) => return t.clone(),
420            };
421            Term::Fix {
422                name: name.clone(),
423                body: bx(explicit_levels(&inner, body)),
424            }
425        }
426        Term::MutualFix { defs, index } => {
427            let mut inner = ctx.clone();
428            for (i, (name, _)) in defs.iter().enumerate() {
429                let member = Term::MutualFix {
430                    defs: defs.clone(),
431                    index: i,
432                };
433                match crate::type_checker::infer_type(ctx, &member) {
434                    Ok(ty) => inner = inner.extend(name, ty),
435                    Err(_) => return t.clone(),
436                }
437            }
438            Term::MutualFix {
439                defs: defs
440                    .iter()
441                    .map(|(n, b)| (n.clone(), explicit_levels(&inner, b)))
442                    .collect(),
443                index: *index,
444            }
445        }
446        Term::Annotated { term, .. } => explicit_levels(ctx, term),
447        other => other.clone(),
448    }
449}
450
451/// The explicit reference `name.{levels}` the application rule solves from `args`, if it solves
452/// every level.
453fn solve_levels(ctx: &crate::Context, name: &str, args: &[Term]) -> Option<Term> {
454    let (params, ty) = level_telescope(ctx, name)?;
455    if params.is_empty() {
456        return None;
457    }
458    let metas = crate::term::fresh_level_metas(name, &params);
459    let mut cur = crate::term::instantiate_universes(&ty, &metas);
460    let mut solved = std::collections::HashMap::new();
461    for a in args {
462        if !matches!(cur, Term::Pi { .. }) {
463            cur = crate::reduction::normalize(ctx, &cur);
464        }
465        let Term::Pi {
466            param_type,
467            body_type,
468            ..
469        } = &cur
470        else {
471            break;
472        };
473        if crate::term::mentions_level_meta(param_type) {
474            if let Ok(at) = crate::type_checker::infer_type(ctx, a) {
475                let at = if matches!(at, Term::Sort(_)) {
476                    at
477                } else {
478                    crate::reduction::normalize(ctx, &at)
479                };
480                let mut step = std::collections::HashMap::new();
481                crate::term::unify_levels(param_type, &at, &mut step);
482                for (k, v) in step {
483                    solved.entry(k).or_insert(v);
484                }
485            }
486        }
487        cur = crate::term::instantiate_universes(body_type, &solved);
488    }
489    let levels: Vec<Universe> = params
490        .iter()
491        .map(|p| metas[p].substitute(&solved))
492        .collect();
493    let unsolved = levels
494        .iter()
495        .any(|u| crate::term::universe_mentions(u, &crate::term::is_level_meta));
496    (!unsolved).then(|| Term::Const {
497        name: name.to_string(),
498        levels,
499    })
500}
501
502/// A global's universe parameters and type: its explicit level telescope, or else the level
503/// variables its type mentions, which the `Term` kernel reads as bound by the declaration.
504pub fn level_telescope(ctx: &crate::Context, name: &str) -> Option<(Vec<String>, Term)> {
505    if let Some((ps, ty)) = ctx.poly_declaration(name) {
506        return Some((ps.to_vec(), ty.clone()));
507    }
508    let ty = ctx.get_global(name)?;
509    Some((crate::term::free_level_vars(ty), ty.clone()))
510}
logicaffeine_kernel/dag/logos.rs

logicaffeine_kernel/dag/
logos.rs
