/// Scope check + occurs check a solution candidate.
Scope check + occurs check a solution candidate.
Scope check + occurs check a solution candidate .
fn check_solution(
    env_size: var::Size,
    span: FileSpan,
    head: meta::Index,
    bound_levels: &im::Vector<var::Level>,
    rhs: &Rc<syntax::Term>,
) -> Result<(), Diagnostic<FileSpan>> {
    match rhs.as_ref() {
        // Scope check
        syntax::Term::Var(rhs_var_index) => {
            if bound_levels
                .iter()
                .any(|var_level| env_size.index(*var_level) == *rhs_var_index)
            {
                // FIXME: Better error message
                let message = format!("solution scope error: `?{}`", head.0);
                Err(Diagnostic::new_error(message).with_label(DiagnosticLabel::new_primary(span)))
            } else {
                Ok(())
            }
        },
        // Occurs check
        syntax::Term::Meta(rhs_meta_level) => {
            if *rhs_meta_level == head {
                // FIXME: Better error message
                let message = format!("occurs check: `?{}`", head.0);
                Err(Diagnostic::new_error(message).with_label(DiagnosticLabel::new_primary(span)))
            } else {
                Ok(())
            }
        },
        syntax::Term::Prim(_) => Ok(()),
        syntax::Term::Ann(term, term_ty) => {
            check_solution(env_size, span, head, bound_levels, term)?;
            check_solution(env_size, span, head, bound_levels, term_ty)?;
            Ok(())
        },
        syntax::Term::Let(_, _) => Err(Diagnostic::new_bug("attempted to unify let expressions")
            .with_label(DiagnosticLabel::new_primary(span))),
        syntax::Term::LiteralType(_) => Ok(()),
        syntax::Term::LiteralIntro(_) => Ok(()),
        syntax::Term::LiteralElim(scrutinee, clauses, default_clause) => {
            check_solution(env_size, span, head, bound_levels, scrutinee)?;
            for (_, body) in clauses.iter() {
                check_solution(env_size, span, head, bound_levels, body)?;
            }
            check_solution(env_size, span, head, bound_levels, default_clause)?;
            Ok(())
        },
        syntax::Term::FunType(_, _, param_ty, body_ty) => {
            check_solution(env_size, span, head, bound_levels, param_ty)?;
            check_solution(env_size + 1, span, head, bound_levels, body_ty)?;
            Ok(())
        },
        syntax::Term::FunIntro(_, _, body) => {
            check_solution(env_size + 1, span, head, bound_levels, body)?;
            Ok(())
        },
        syntax::Term::FunElim(fun, _, arg) => {
            check_solution(env_size, span, head, bound_levels, fun)?;
            check_solution(env_size, span, head, bound_levels, arg)?;
            Ok(())
        },
        syntax::Term::RecordType(ty_fields) => {
            for (i, (_, _, _, term)) in ty_fields.iter().enumerate() {
                check_solution(env_size + i as u32, span, head, bound_levels, term)?;
            }
            Ok(())
        },
        syntax::Term::RecordIntro(intro_fields) => {
            for (_, term) in intro_fields.iter() {
                check_solution(env_size, span, head, bound_levels, term)?;
            }
            Ok(())
        },
        syntax::Term::RecordElim(record, _) => {
            check_solution(env_size, span, head, bound_levels, record)
        },
        syntax::Term::Universe(_) => Ok(()),
    }
}
fn check_solution ( env_size : var :: Size , span : FileSpan , head : meta :: Index , bound_levels : & im :: Vector < var :: Level > , rhs : & Rc < syntax :: Term > , ) -> Result < ( ) , Diagnostic < FileSpan > > { match rhs . as_ref ( ) { // Scope check syntax :: Term :: Var ( rhs_var_index ) => { if bound_levels . iter ( ) . any ( | var_level | env_size . index ( * var_level ) == * rhs_var_index ) { // FIXME: Better error message let message = format ! ( " " head 0 ) ; Err ( Diagnostic :: new_error ( message ) . with_label ( DiagnosticLabel :: new_primary ( span ) ) ) } else { Ok ( ( ) ) } } , // Occurs check syntax :: Term :: Meta ( rhs_meta_level ) => { if * rhs_meta_level == head { // FIXME: Better error message let message = format ! ( " " head 0 ) ; Err ( Diagnostic :: new_error ( message ) . with_label ( DiagnosticLabel :: new_primary ( span ) ) ) } else { Ok ( ( ) ) } } , syntax :: Term :: Prim ( _ ) => Ok ( ( ) ) , syntax :: Term :: Ann ( term , term_ty ) => { check_solution ( env_size , span , head , bound_levels , term ) ? ; check_solution ( env_size , span , head , bound_levels , term_ty ) ? ; Ok ( ( ) ) } , syntax :: Term :: Let ( _ , _ ) => Err ( Diagnostic :: new_bug ( " " ) . with_label ( DiagnosticLabel :: new_primary ( span ) ) ) , syntax :: Term :: LiteralType ( _ ) => Ok ( ( ) ) , syntax :: Term :: LiteralIntro ( _ ) => Ok ( ( ) ) , syntax :: Term :: LiteralElim ( scrutinee , clauses , default_clause ) => { check_solution ( env_size , span , head , bound_levels , scrutinee ) ? ; for ( _ , body ) in clauses . iter ( ) { check_solution ( env_size , span , head , bound_levels , body ) ? ; } check_solution ( env_size , span , head , bound_levels , default_clause ) ? ; Ok ( ( ) ) } , syntax :: Term :: FunType ( _ , _ , param_ty , body_ty ) => { check_solution ( env_size , span , head , bound_levels , param_ty ) ? ; check_solution ( env_size + 1 , span , head , bound_levels , body_ty ) ? ; Ok ( ( ) ) } , syntax :: Term :: FunIntro ( _ , _ , body ) => { check_solution ( env_size + 1 , span , head , bound_levels , body ) ? ; Ok ( ( ) ) } , syntax :: Term :: FunElim ( fun , _ , arg ) => { check_solution ( env_size , span , head , bound_levels , fun ) ? ; check_solution ( env_size , span , head , bound_levels , arg ) ? ; Ok ( ( ) ) } , syntax :: Term :: RecordType ( ty_fields ) => { for ( i , ( _ , _ , _ , term ) ) in ty_fields . iter ( ) . enumerate ( ) { check_solution ( env_size + i as u32 , span , head , bound_levels , term ) ? ; } Ok ( ( ) ) } , syntax :: Term :: RecordIntro ( intro_fields ) => { for ( _ , term ) in intro_fields . iter ( ) { check_solution ( env_size , span , head , bound_levels , term ) ? ; } Ok ( ( ) ) } , syntax :: Term :: RecordElim ( record , _ ) => { check_solution ( env_size , span , head , bound_levels , record ) } , syntax :: Term :: Universe ( _ ) => Ok ( ( ) ) , } }
Scope check + occurs check a solution candidate.
Scope check + occurs check a solution candidate .
env_size
var::Size
span
FileSpan
head
meta::Index
bound_levels
&im::Vector<var::Level>
rhs
&Rc<syntax::Term>