/// Check that the body of the given clause conforms to they expected type, and
/// elaborate it.
Check that the body of the given clause conforms to they expected type, and
elaborate it.
Check that the body of the given clause conforms to they expected type and elaborate it .
fn check_clause_body(
    context: &Context,
    metas: &mut meta::Env,
    clause: &Clause<'_>,
    expected_body_ty: &Rc<domain::Type>,
) -> Result<Rc<syntax::Term>, Diagnostic<FileSpan>> {
    match clause.body_ty {
        None => check_term(&context, metas, clause.body, &expected_body_ty),
        Some(body_ty) => {
            let body_ty_span = body_ty.span();
            let (body_ty, _) = synth_universe(&context, metas, body_ty)?;
            let body_ty_value = context.eval_term(metas, body_ty_span, &body_ty)?;
            let body = check_term(&context, metas, clause.body, &body_ty_value)?;
            // TODO: Ensure that this is respecting variance correctly!
            context.unify_values(metas, clause.body.span(), &body_ty_value, &expected_body_ty)?;
            Ok(Rc::from(syntax::Term::ann(body, body_ty)))
        },
    }
}
fn check_clause_body ( context : & Context , metas : & mut meta :: Env , clause : & Clause < ' _ > , expected_body_ty : & Rc < domain :: Type > , ) -> Result < Rc < syntax :: Term > , Diagnostic < FileSpan > > { match clause . body_ty { None => check_term ( & context , metas , clause . body , & expected_body_ty ) , Some ( body_ty ) => { let body_ty_span = body_ty . span ( ) ; let ( body_ty , _ ) = synth_universe ( & context , metas , body_ty ) ? ; let body_ty_value = context . eval_term ( metas , body_ty_span , & body_ty ) ? ; let body = check_term ( & context , metas , clause . body , & body_ty_value ) ? ; // TODO: Ensure that this is respecting variance correctly! context . unify_values ( metas , clause . body . span ( ) , & body_ty_value , & expected_body_ty ) ? ; Ok ( Rc :: from ( syntax :: Term :: ann ( body , body_ty ) ) ) } , } }
Check that the body of the given clause conforms to they expected type, and
elaborate it.
Check that the body of the given clause conforms to they expected type and elaborate it .
context
&Context
metas
&mut meta::Env
clause
&Clause<'_>
expected_body_ty
&Rc<domain::Type>