logicaffeine_kernel/dag/sem/
types.rs

1//! The types of values, for the parts of conversion and reduction that look at types — proof
2//! irrelevance, η, struct-η, unit-like types, K — and for projections. Values reaching here are
3//! well-typed, so this is inference without checking: a head's type followed along the spine.
4
5use super::value::{CtxId, Head, Sp, Val, V};
6use super::{reject, Sem};
7use crate::dag::error::KResult;
8use crate::dag::level::{LevelId, LevelsId};
9use crate::dag::name::NameId;
10use crate::dag::relevance::{Signature, MAX_TRACKED};
11
12impl Sem<'_> {
13    /// The type of `v`.
14    pub fn type_of(&mut self, v: V) -> KResult<V> {
15        if let Some(t) = self.st.arena.type_memo(v) {
16            return Ok(t);
17        }
18        self.enter()?;
19        let r = self.type_of_uncached(v);
20        self.leave();
21        let r = r?;
22        self.st.arena.set_type_memo(v, r);
23        Ok(r)
24    }
25
26    fn type_of_uncached(&mut self, v: V) -> KResult<V> {
27        match self.st.arena.get(v) {
28            Val::Sort(l) => {
29                let sl = self.k.s.levels.succ(l);
30                Ok(self.st.arena.sort(sl))
31            }
32            Val::Nat(_) => self.const0(self.k.wk.nat),
33            Val::Str(_) => self.const0(self.k.wk.string),
34            Val::Neu { head, spine, .. } => {
35                let mut ty = match self.st.arena.head(head) {
36                    Head::Local { ty, .. } => ty,
37                    Head::Const { name, levels } => self.const_type(name, levels)?,
38                    Head::Proj { s, idx, x } => {
39                        let xt = self.type_of(x)?;
40                        self.proj_type(s, idx, x, xt, false)?
41                    }
42                };
43                for a in self.st.arena.args(spine) {
44                    let w = self.whnf(ty)?;
45                    ty = self.instantiate(w, a)?;
46                }
47                Ok(ty)
48            }
49            Val::Lam { env, body, .. } => {
50                let d = self.lam_domain(v)?;
51                Ok(self.st.arena.pi_lam(d, env, CtxId::EMPTY, body))
52            }
53            Val::Pi { dom, .. } | Val::PiLam { dom, .. } => {
54                let ld = self.sort_level(dom)?;
55                let lb = self.under(dom, |s, x| {
56                    let cod = s.instantiate(v, x)?;
57                    s.sort_level(cod)
58                })?;
59                let l = self.k.s.levels.imax(ld, lb);
60                Ok(self.st.arena.sort(l))
61            }
62        }
63    }
64
65    /// The universe level of a type.
66    pub(crate) fn sort_level(&mut self, ty: V) -> KResult<LevelId> {
67        let tt = self.type_of(ty)?;
68        match self.sort_of(tt)? {
69            Some(l) => Ok(l),
70            None => Err(reject(format!("type expected, found {}", self.show(ty)))),
71        }
72    }
73
74    /// Whether the type `ty` lives in `Prop`.
75    pub fn is_prop(&mut self, ty: V) -> KResult<bool> {
76        let l = self.sort_level(ty)?;
77        Ok(self.k.s.levels.is_always_zero(l))
78    }
79
80    /// Whether `v` is a proof (its type is a proposition): decided by its shape or its head's
81    /// [`Signature`] where they decide it, by inferring its type otherwise, and remembered on the
82    /// value.
83    pub(crate) fn is_proof(&mut self, v: V) -> KResult<bool> {
84        if let Some(p) = self.st.arena.proof_memo(v) {
85            return Ok(p);
86        }
87        let p = match self.static_proof(v)? {
88            Some(p) => p,
89            None => {
90                self.st.counters.proof_probes += 1;
91                let t = self.type_of(v)?;
92                self.is_prop(t)?
93            }
94        };
95        self.st.arena.set_proof_memo(v, p);
96        Ok(p)
97    }
98
99    fn static_proof(&mut self, v: V) -> KResult<Option<bool>> {
100        Ok(match self.st.arena.get(v) {
101            Val::Sort(_) | Val::Pi { .. } | Val::PiLam { .. } | Val::Nat(_) | Val::Str(_) => {
102                Some(false)
103            }
104            Val::Lam { .. } => None,
105            Val::Neu { head, spine, .. } => match self.st.arena.head(head) {
106                Head::Const { name, levels } => {
107                    let k = self.st.arena.spine_len(spine) as usize;
108                    self.signature(name, levels)?.and_then(|s| s.is_proof(k))
109                }
110                Head::Local { ty, .. } if spine == Sp::NIL => self.static_proposition(ty)?,
111                _ => None,
112            },
113        })
114    }
115
116    /// Whether the type `ty` is a proposition, where its shape or its head's signature decides it.
117    fn static_proposition(&mut self, ty: V) -> KResult<Option<bool>> {
118        Ok(match self.st.arena.get(ty) {
119            Val::Sort(_) => Some(false),
120            Val::Neu { head, spine, .. } => match self.st.arena.head(head) {
121                Head::Const { name, levels } => {
122                    let k = self.st.arena.spine_len(spine) as usize;
123                    self.signature(name, levels)?
124                        .and_then(|s| s.is_proposition(k))
125                }
126                _ => None,
127            },
128            _ => None,
129        })
130    }
131
132    /// The [`Signature`] of `c.{ls}`, computed once per settled constant and instantiation and
133    /// shared by every later declaration; `None` for a constant only provisionally in the
134    /// environment, or one given the wrong number of universes, whose applications' types must be
135    /// inferred.
136    pub fn signature(&mut self, c: NameId, ls: LevelsId) -> KResult<Option<Signature>> {
137        if let Some(s) = self.k.known_signature(c, ls) {
138            return Ok(Some(s));
139        }
140        if !self.k.env.is_settled(c) {
141            return Ok(None);
142        }
143        match self.k.env.get(c) {
144            Some(k) if k.lparams.len() == self.k.s.levels.get_list(ls).len() => {}
145            _ => return Ok(None),
146        }
147        if !self.k.relevance.computing.insert((c, ls)) {
148            return Ok(None);
149        }
150        let r = self
151            .const_type(c, ls)
152            .and_then(|ty| self.telescope_signature(ty));
153        self.k.relevance.computing.remove(&(c, ls));
154        let s = r?;
155        self.k.note_signature(c, ls, s);
156        Ok(Some(s))
157    }
158
159    /// The signature of the type `ty`: its telescope walked under fresh variables, each binder
160    /// type's universe tested for `Prop`, and the result's universe deciding every partial
161    /// application (see [`Signature`]).
162    pub(crate) fn telescope_signature(&mut self, ty: V) -> KResult<Signature> {
163        let mut proof_args = 0u64;
164        let mut bound = 0usize;
165        let r = (|| -> KResult<Signature> {
166            let mut cur = ty;
167            let result = loop {
168                let w = self.whnf(cur)?;
169                let dom = match self.st.arena.get(w) {
170                    Val::Pi { dom, .. } | Val::PiLam { dom, .. } => dom,
171                    _ => break w,
172                };
173                if bound == MAX_TRACKED {
174                    return Ok(Signature::new(proof_args, 0, 0, None));
175                }
176                let l = self.sort_level(dom)?;
177                if self.k.s.levels.is_always_zero(l) {
178                    proof_args |= 1 << bound;
179                }
180                let x = self.bind(dom);
181                bound += 1;
182                cur = self.instantiate(w, x)?;
183            };
184            let n = bound;
185            if n >= MAX_TRACKED {
186                return Ok(Signature::new(proof_args, 0, 0, None));
187            }
188            let proposition = match self.st.arena.get(result) {
189                Val::Sort(l) => Some(self.k.s.levels.is_always_zero(l)),
190                _ => None,
191            };
192            let known = u64::MAX >> (MAX_TRACKED - 1 - n);
193            let level = self.sort_level(result)?;
194            let proofs = if self.k.s.levels.is_always_zero(level) {
195                known
196            } else {
197                0
198            };
199            Ok(Signature::new(
200                proof_args,
201                proofs,
202                known,
203                Some((n as u32, proposition)),
204            ))
205        })();
206        for _ in 0..bound {
207            self.unbind();
208        }
209        r
210    }
211
212    /// The type of field `idx` of the structure value `x : xt` (Lean's `inferProj`). With `check`,
213    /// the projection's side conditions are enforced: a structure in `Prop` may only be projected
214    /// to its proof fields (and past a data field only if nothing later depends on it).
215    pub(crate) fn proj_type(
216        &mut self,
217        sname: NameId,
218        idx: u32,
219        x: V,
220        xt: V,
221        check: bool,
222    ) -> KResult<V> {
223        let fail = |s: &mut Sem| {
224            reject(format!(
225                "invalid projection .{} of '{}'",
226                idx + 1,
227                s.k.s.names.display(sname)
228            ))
229        };
230        let ty = self.whnf(xt)?;
231        let Some((iname, ils, _, tsp)) = self.const_app(ty) else {
232            return Err(fail(self));
233        };
234        if iname != sname {
235            return Err(fail(self));
236        }
237        let Some(ind) = self.k.env.inductive(iname).cloned() else {
238            return Err(fail(self));
239        };
240        let targs = self.st.arena.args(tsp);
241        if ind.ctors.len() != 1 || targs.len() != (ind.num_params + ind.num_indices) as usize {
242            return Err(fail(self));
243        }
244        let mut r = self.const_type(ind.ctors[0], ils)?;
245        for arg in targs.iter().take(ind.num_params as usize) {
246            let w = self.whnf(r)?;
247            if !matches!(self.st.arena.get(w), Val::Pi { .. } | Val::PiLam { .. }) {
248                return Err(fail(self));
249            }
250            r = self.instantiate(w, *arg)?;
251        }
252        let maybe_prop = if check {
253            let sl = self.sort_level(ty)?;
254            !self.k.s.levels.is_never_zero(sl)
255        } else {
256            false
257        };
258        for i in 0..idx {
259            let w = self.whnf(r)?;
260            let (dom, body) = match self.st.arena.get(w) {
261                Val::Pi { dom, body, .. } | Val::PiLam { dom, body, .. } => (dom, body),
262                _ => return Err(fail(self)),
263            };
264            let depends = self.k.s.loose_bvar_mask(body).is_none_or(|m| m & 1 == 1);
265            if maybe_prop && depends && !self.is_prop(dom)? {
266                return Err(fail(self));
267            }
268            let p = self.proj(iname, i, x)?;
269            r = self.instantiate(w, p)?;
270        }
271        let w = self.whnf(r)?;
272        let dom = match self.st.arena.get(w) {
273            Val::Pi { dom, .. } | Val::PiLam { dom, .. } => dom,
274            _ => return Err(fail(self)),
275        };
276        if maybe_prop && !self.is_prop(dom)? {
277            return Err(fail(self));
278        }
279        Ok(dom)
280    }
281}
logicaffeine_kernel/dag/sem/types.rs

logicaffeine_kernel/dag/sem/
types.rs
