nar/syntax/core/subst/
redex.rs

1use std::rc::Rc;
2
3use voile_util::{meta::MetaSolution, uid::DBI};
4
5use crate::syntax::{
6    common::{Bind, Let},
7    core::{
8        subst::{def_app, PrimSubst, Subst},
9        Closure, Elim, Term, Val, ValData,
10    },
11    pat::{Copat, Pat},
12};
13
14/// Reducible expressions.
15/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Substitute.Class.html#Subst).
16pub trait RedEx<T: Sized = Self, A = Term>: Sized {
17    /// Apply a substitution to a redex.
18    fn reduce_dbi(self, subst: Rc<PrimSubst<A>>) -> T;
19}
20
21impl RedEx for Term {
22    fn reduce_dbi(self, subst: Rc<Subst>) -> Term {
23        match self {
24            Term::Whnf(n) => n.reduce_dbi(subst),
25            Term::Redex(f, id, args) => def_app(f, id, vec![], args.reduce_dbi(subst)),
26        }
27    }
28}
29
30impl RedEx for Elim {
31    fn reduce_dbi(self, subst: Rc<Subst>) -> Elim {
32        match self {
33            Elim::App(term) => Elim::app(term.reduce_dbi(subst)),
34            e => e,
35        }
36    }
37}
38
39impl<R, T: RedEx<R>> RedEx<MetaSolution<R>> for MetaSolution<T> {
40    fn reduce_dbi(self, subst: Rc<Subst>) -> MetaSolution<R> {
41        use MetaSolution::*;
42        match self {
43            Solved(t) => Solved(Box::new(t.reduce_dbi(subst))),
44            Inlined => Inlined,
45            Unsolved => Unsolved,
46        }
47    }
48}
49
50impl<R, T: RedEx<R>> RedEx<Bind<R>> for Bind<T> {
51    fn reduce_dbi(self, subst: Rc<Subst>) -> Bind<R> {
52        self.map_term(|t| t.reduce_dbi(subst))
53    }
54}
55
56impl<R, T: RedEx<R>> RedEx<Let<R>> for Let<T> {
57    fn reduce_dbi(self, subst: Rc<Subst>) -> Let<R> {
58        let bind = self.bind.reduce_dbi(subst.clone());
59        Let::new(bind, self.val.reduce_dbi(subst))
60    }
61}
62
63impl RedEx for ValData {
64    fn reduce_dbi(self, subst: Rc<Subst>) -> Self {
65        ValData::new(self.kind, self.def, self.args.reduce_dbi(subst))
66    }
67}
68
69impl RedEx<Term> for Val {
70    fn reduce_dbi(self, subst: Rc<Subst>) -> Term {
71        match self {
72            Val::Pi(arg, closure) => Term::pi2(
73                arg.unboxed().reduce_dbi(subst.clone()).boxed(),
74                closure.reduce_dbi(subst),
75            ),
76            Val::Cons(name, a) => Term::cons(name, a.reduce_dbi(subst)),
77            Val::Type(n) => Term::universe(n),
78            Val::Data(info) => Term::data(info.reduce_dbi(subst)),
79            Val::Meta(m, a) => Term::meta(m, a.reduce_dbi(subst)),
80            Val::Var(f, args) => subst.lookup(f).apply_elim(args.reduce_dbi(subst)),
81            Val::Axiom(a) => Term::Whnf(Val::Axiom(a)),
82            Val::Refl => Term::reflexivity(),
83            Val::Id(ty, a, b) => Term::identity(
84                ty.reduce_dbi(subst.clone()),
85                a.reduce_dbi(subst.clone()),
86                b.reduce_dbi(subst),
87            ),
88        }
89    }
90}
91
92impl RedEx for Closure {
93    fn reduce_dbi(self, subst: Rc<Subst>) -> Self {
94        match self {
95            Closure::Plain(body) => Self::plain(body.reduce_dbi(subst.lift_by(DBI(1)))),
96        }
97    }
98}
99
100/// For `Tele`.
101impl<R, T: RedEx<R>> RedEx<Vec<R>> for Vec<T> {
102    fn reduce_dbi(self, subst: Rc<Subst>) -> Vec<R> {
103        self.into_iter()
104            .map(|e| e.reduce_dbi(subst.clone()))
105            .collect()
106    }
107}
108
109impl<A, B, X: RedEx<A>, Y: RedEx<B>> RedEx<(A, B)> for (X, Y) {
110    fn reduce_dbi(self, subst: Rc<Subst>) -> (A, B) {
111        let (x, y) = self;
112        (x.reduce_dbi(subst.clone()), y.reduce_dbi(subst))
113    }
114}
115
116impl<Ix, R, T: RedEx<R>> RedEx<Copat<Ix, R>> for Copat<Ix, T> {
117    fn reduce_dbi(self, subst: Rc<Subst>) -> Copat<Ix, R> {
118        match self {
119            Copat::App(a) => Copat::App(a.reduce_dbi(subst)),
120            Copat::Proj(p) => Copat::Proj(p),
121        }
122    }
123}
124
125impl<Ix, R, T: RedEx<R>> RedEx<Pat<Ix, R>> for Pat<Ix, T> {
126    fn reduce_dbi(self, subst: Rc<Subst>) -> Pat<Ix, R> {
127        match self {
128            Pat::Refl => Pat::Refl,
129            Pat::Absurd => Pat::Absurd,
130            Pat::Var(v) => Pat::Var(v),
131            Pat::Cons(f, c, pats) => Pat::Cons(f, c, pats.reduce_dbi(subst)),
132            Pat::Forced(t) => Pat::Forced(t.reduce_dbi(subst)),
133        }
134    }
135}
nar/syntax/core/subst/redex.rs

nar/syntax/core/subst/
redex.rs
