diff --git a/src/check/rules/clause/eqs.rs b/src/check/rules/clause/eqs.rs index 27f0090..bdecd74 100644 --- a/src/check/rules/clause/eqs.rs +++ b/src/check/rules/clause/eqs.rs @@ -15,7 +15,7 @@ use super::super::term::is_eta_var_borrow; /// 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 Equation { +pub(super) struct Equation { /// The pattern causes this problem. pub in_pat: AbsCopat, pub inst: Term, @@ -30,10 +30,10 @@ impl PatCommon for Equation { /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.Problem.html#AsBinding). #[derive(Debug, Clone)] -pub struct AsBind { - pub name: UID, - pub term: Term, - pub ty: Term, +pub(super) struct AsBind { + name: UID, + term: Term, + ty: Term, } impl From for Let { @@ -44,7 +44,7 @@ impl From for Let { } impl AsBind { - pub fn new(name: UID, term: Term, ty: Term) -> Self { + pub(super) fn new(name: UID, term: Term, ty: Term) -> Self { Self { name, term, ty } } } @@ -52,13 +52,13 @@ impl AsBind { /// Classified patterns, called `LeftoverPatterns` in Agda. /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.html#LeftoverPatterns). #[derive(Debug, Clone)] -pub struct PatClass { +pub(super) struct PatClass { /// Number of absurd patterns. - pub absurd_count: usize, - pub as_binds: Vec, - pub other_pats: Vec, + pub(super) absurd_count: usize, + pub(super) as_binds: Vec, + pub(super) other_pats: Vec, /// Supposed to be an `IntMap`. - pub pat_vars: PatVars, + pub(super) pat_vars: PatVars, } impl Add for PatClass { @@ -79,9 +79,9 @@ impl Add for PatClass { } } -pub type PatVars = HashMap>; +pub(super) type PatVars = HashMap>; -pub fn classify_eqs(mut tcs: TCS, eqs: Vec) -> TCMS { +pub(super) fn classify_eqs(mut tcs: TCS, eqs: Vec) -> TCMS { let mut pat_vars = PatVars::new(); let mut other_pats = Vec::with_capacity(eqs.len()); let mut as_binds = Vec::with_capacity(eqs.len()); diff --git a/src/check/rules/clause/lhs.rs b/src/check/rules/clause/lhs.rs index 5e444b1..2e5bc38 100644 --- a/src/check/rules/clause/lhs.rs +++ b/src/check/rules/clause/lhs.rs @@ -4,38 +4,37 @@ use std::rc::Rc; use voile_util::uid::{DBI, UID}; use crate::check::monad::{TCE, TCMS, TCS}; -use crate::check::rules::clause::{AsBind, PatVars}; -use crate::check::rules::term::is_eta_var_borrow; use crate::syntax::core::subst::{DeBruijn, RedEx, Subst}; use crate::syntax::core::{Pat as CorePat, Tele, TeleS, Term}; use crate::syntax::pat::{Copat, Pat, PatCommon}; +use super::super::term::is_eta_var_borrow; use super::super::ERROR_TAKE; -use super::{classify_eqs, LhsState}; +use super::{classify_eqs, AsBind, LhsState, PatVars}; /// Result of checking the LHS of a clause. /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.html#LHSResult). #[derive(Clone)] -pub struct Lhs { +pub(super) struct Lhs { /// $\Delta$: The types of the pattern variables, in internal dependency order. /// Corresponds to `clauseTel` (in Agda). - pub tele: Tele, + pub(super) tele: Tele, /// Whether the LHS has at least one absurd pattern. - pub has_absurd: bool, + pub(super) has_absurd: bool, /// The patterns in internal syntax. - pub pats: Vec, + pub(super) pats: Vec, /// The type of the body. Is $b~\sigma$ if $\Gamma$ is defined. - pub ty: Term, + pub(super) ty: Term, /// Substitution version of `pats`, only up to the first projection pattern. /// $\Delta \vdash \text{pat\_subst} : \Gamma$. /// Where $\Gamma$ is the argument telescope of the function. /// This is used to update inherited dot patterns in /// with-function clauses. - pub pat_sub: Rc, + pub(super) pat_sub: Rc, /// As-bindings from the left-hand side. /// Return instead of bound since we /// want them in where's and right-hand sides, but not in with-clauses - pub as_binds: Vec, + pub(super) as_binds: Vec, } /// Build a renaming for the internal patterns using variable names from @@ -49,7 +48,7 @@ pub struct Lhs { /// + `tele`: The telescope of pattern variables /// + `pat_vars`: The list of user names for each pattern variable /// -pub fn user_variable_names(tele: &TeleS, mut pat_vars: PatVars) -> (Vec>, Vec) { +fn user_variable_names(tele: &TeleS, mut pat_vars: PatVars) -> (Vec>, Vec) { let len_rng = 0..tele.len(); let mut as_binds = Vec::with_capacity(pat_vars.len()); let mut names = Vec::with_capacity(tele.len()); @@ -111,7 +110,7 @@ To compute $\Theta$ we can look at the arity of the with-function and compare it to numPats. This works since the with-function type is fully reduced. */ -pub fn final_check(tcs: TCS, mut lhs: LhsState) -> TCMS { +fn final_check(tcs: TCS, mut lhs: LhsState) -> TCMS { debug_assert!(lhs.problem.todo_pats.is_empty()); let len_pats = lhs.len_pats(); // It should be `len_pats - ctx.len()`, @@ -153,7 +152,7 @@ pub fn final_check(tcs: TCS, mut lhs: LhsState) -> TCMS { /// Checking a pattern matching lhs recursively. /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.html). -pub fn check_lhs(mut tcs: TCS, lhs: LhsState) -> TCMS { +pub(super) fn check_lhs(mut tcs: TCS, lhs: LhsState) -> TCMS { for split in (lhs.problem.equations.iter()).filter(|e| e.in_pat.is_split()) { use Copat::{App, Proj}; use Pat::{Absurd, Forced}; diff --git a/src/check/rules/clause/mod.rs b/src/check/rules/clause/mod.rs index e87ed39..8f0d7ab 100644 --- a/src/check/rules/clause/mod.rs +++ b/src/check/rules/clause/mod.rs @@ -4,16 +4,16 @@ use crate::syntax::core::{Clause, Tele, Term}; use super::term::{check, simplify, HasMeta}; -pub use self::eqs::*; -pub use self::lhs::*; -pub use self::state::*; +use self::eqs::*; +use self::lhs::*; +use self::state::*; mod eqs; mod lhs; mod state; /// Bind as patterns -pub fn bind_as_and_tele( +fn bind_as_and_tele( mut tcs: TCS, as_binds: Vec, mut tele: Tele, diff --git a/src/check/rules/clause/state.rs b/src/check/rules/clause/state.rs index 3e11c1f..a7f0b8e 100644 --- a/src/check/rules/clause/state.rs +++ b/src/check/rules/clause/state.rs @@ -9,36 +9,36 @@ use crate::syntax::pat::PatCommon; use super::Equation; #[derive(Debug, Clone)] -pub struct Problem { +pub(super) struct Problem { /// List of user patterns which could not yet be typed. - pub todo_pats: Vec, + pub(super) todo_pats: Vec, /// User patterns' unification problems. - pub equations: Vec, + pub(super) equations: Vec, } impl Problem { - pub fn is_all_solved(&self) -> bool { + pub(super) fn is_all_solved(&self) -> bool { self.todo_pats.is_empty() && self.equations.iter().all(|eq| eq.is_solved()) } } /// State worked on during lhs checking. #[derive(Clone)] -pub struct LhsState { +pub(super) struct LhsState { /// Pattern variables' types. - pub tele: Tele, + pub(super) tele: Tele, /// Patterns after splitting. /// Indices are positioned from right to left. - pub pats: Vec, + pub(super) pats: Vec, /// Yet solved pattern matching. - pub problem: Problem, + pub(super) problem: Problem, /// Type eliminated by `problem`. - pub target: Term, + pub(super) target: Term, } impl LhsState { /// Number of patterns. - pub fn len_pats(&self) -> usize { + pub(super) fn len_pats(&self) -> usize { self.pats.iter().take_while(|pat| !pat.is_proj()).count() } } @@ -47,7 +47,7 @@ impl LhsState { /// [this function](https://hackage.haskell.org/package/Agda-2.5.4/docs/src/Agda.TypeChecking.Rules.LHS.ProblemRest.html#initLHSState) /// is implemented via an /// [auxiliary function](https://hackage.haskell.org/package/Agda-2.5.4/docs/src/Agda.TypeChecking.Rules.LHS.ProblemRest.html#updateProblemRest). -pub fn init_lhs_state(pats: Vec, ty: Term) -> TCM { +pub(super) fn init_lhs_state(pats: Vec, ty: Term) -> TCM { let (tele, target) = ty.tele_view(); let mut pats_iter = pats.into_iter(); let tele_len = tele.len();