[ lhs ] Restrict visibility

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<AsBind> for Let {
@@ -44,21 +44,21 @@ impl From<AsBind> 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 }
     }
 }
 
 /// 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<AsBind>,
-    pub other_pats: Vec<AbsCopat>,
+    pub(super) absurd_count: usize,
+    pub(super) as_binds: Vec<AsBind>,
+    pub(super) other_pats: Vec<AbsCopat>,
     /// 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<DBI, Vec<UID>>;
+pub(super) type PatVars = HashMap<DBI, Vec<UID>>;
 
-pub fn classify_eqs(mut tcs: TCS, eqs: Vec<Equation>) -> TCMS<PatClass> {
+pub(super) fn classify_eqs(mut tcs: TCS, eqs: Vec<Equation>) -> TCMS<PatClass> {
     let mut pat_vars = PatVars::new();
     let mut other_pats = Vec::with_capacity(eqs.len());
     let mut as_binds = Vec::with_capacity(eqs.len());

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<CorePat>,
+    pub(super) pats: Vec<CorePat>,
     /// 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<Subst>,
+    pub(super) pat_sub: Rc<Subst>,
     /// 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<AsBind>,
+    pub(super) as_binds: Vec<AsBind>,
 }
 
 /// 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<Option<UID>>, Vec<AsBind>) {
+fn user_variable_names(tele: &TeleS, mut pat_vars: PatVars) -> (Vec<Option<UID>>, Vec<AsBind>) {
     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<Lhs> {
+fn final_check(tcs: TCS, mut lhs: LhsState) -> TCMS<Lhs> {
     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<Lhs> {
 
 /// 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<Lhs> {
+pub(super) fn check_lhs(mut tcs: TCS, lhs: LhsState) -> TCMS<Lhs> {
     for split in (lhs.problem.equations.iter()).filter(|e| e.in_pat.is_split()) {
         use Copat::{App, Proj};
         use Pat::{Absurd, Forced};

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<T>(
+fn bind_as_and_tele<T>(
     mut tcs: TCS,
     as_binds: Vec<AsBind>,
     mut tele: Tele,

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<AbsCopat>,
+    pub(super) todo_pats: Vec<AbsCopat>,
     /// User patterns' unification problems.
-    pub equations: Vec<Equation>,
+    pub(super) equations: Vec<Equation>,
 }
 
 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<Pat>,
+    pub(super) pats: Vec<Pat>,
     /// 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<AbsCopat>, ty: Term) -> TCM<LhsState> {
+pub(super) fn init_lhs_state(pats: Vec<AbsCopat>, ty: Term) -> TCM<LhsState> {
     let (tele, target) = ty.tele_view();
     let mut pats_iter = pats.into_iter();
     let tele_len = tele.len();