-
Notifications
You must be signed in to change notification settings - Fork 4
/
clause.rs
49 lines (44 loc) · 1.6 KB
/
clause.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
use crate::check::monad::{TCM, TCS};
use crate::syntax::abs::{AbsClause, AbsCopat};
use crate::syntax::core::{Clause, Pat, Tele, Term, Val};
/// A user pattern and a core term that they should equal
/// after splitting is complete.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#ProblemEq).
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct ProblemEq {
/// The pattern causes this problem.
in_pat: AbsCopat,
inst: Term,
ty: Term,
}
/// User patterns we still have to split on.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.Problem.html#Problem).
#[derive(Debug, Clone)]
pub struct Problem {
/// User patterns.
eqs: Vec<ProblemEq>,
/// List of user patterns which could not yet be typed.
rest_pats: Vec<AbsCopat>,
}
/// State worked on during lhs checking.
#[derive(Debug, Clone)]
pub struct LhsState {
/// Pattern variables' types.
tele: Tele,
/// Patterns after splitting. Indices are positioned from right to left.
pats: Vec<Pat>,
/// User patterns' unification problems.
problem: Problem,
/// Type eliminated by `problem.rest_pats`.
target: Term,
// TODO: what is `_lhsPartialSplit`?
}
pub fn init_lhs_state(tele: Tele) -> TCM<LhsState> {
unimplemented!()
}
/// Checking an abstract clause.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.Def.html#checkClause).
pub fn clause(tcs: TCS, cls: AbsClause, against: &Val) -> TCM<Clause> {
// Expand pattern synonyms here once we support it.
unimplemented!()
}