/// Check that a given term conforms to an expected type.
///
/// Returns the elaborated term.
Check that a given term conforms to an expected type.
Returns the elaborated term.
Check that a given term conforms to an expected type . Returns the elaborated term .
pub fn check_term(
    context: &Context,
    metas: &mut meta::Env,
    concrete_term: &Term<'_>,
    expected_ty: &Rc<domain::Type>,
) -> Result<Rc<syntax::Term>, Diagnostic<FileSpan>> {
    log::trace!("checking term:\t\t{}", concrete_term);
    match concrete_term {
        Term::Prim(_, name) => {
            let prim_name = prim::Name(literal::parse_string(name)?);
            match context.prims().lookup_entry(&prim_name) {
                None => Err(Diagnostic::new_error("unknown primitive")
                    .with_label(DiagnosticLabel::new_primary(name.span()))),
                Some(_) => Ok(Rc::from(syntax::Term::prim(prim_name))),
            }
        },
        Term::Hole(span) => Ok(context.new_meta(metas, *span, expected_ty.clone())),
        Term::Parens(_, concrete_term) => check_term(context, metas, concrete_term, expected_ty),
        Term::Let(_, concrete_items, concrete_body) => {
            let mut context = context.clone();
            let items = check_items(&mut context, metas, concrete_items)?;
            let body = check_term(&context, metas, concrete_body, expected_ty)?;
            Ok(Rc::from(syntax::Term::Let(items, body)))
        },
        Term::If(_, condition, consequent, alternative) => {
            let bool_ty = Rc::from(domain::Value::literal_ty(LiteralType::Bool));
            let condition = check_term(context, metas, condition, &bool_ty)?;
            let consequent = check_term(context, metas, consequent, expected_ty)?;
            let alternative = check_term(context, metas, alternative, expected_ty)?;
            Ok(Rc::from(syntax::Term::LiteralElim(
                condition,
                Rc::from(vec![(LiteralIntro::Bool(true), consequent)]),
                alternative,
            )))
        },
        Term::Case(span, scrutinee, clauses) => {
            let clauses = clauses
                .iter()
                .map(|(pattern, body)| CaseClause::new(pattern, body))
                .collect();
            clause::check_case(context, metas, *span, scrutinee, clauses, expected_ty)
        },
        Term::LiteralIntro(kind, literal) => {
            let literal_intro = literal::check(context, metas, *kind, literal, expected_ty)?;
            Ok(Rc::from(syntax::Term::literal_intro(literal_intro)))
        },
        Term::FunIntro(_, concrete_params, concrete_body) => {
            let clause = Clause::new(concrete_params, None, concrete_body);
            clause::check_clause(context, metas, clause, expected_ty)
        },
        Term::RecordIntro(span, concrete_intro_fields) => {
            let mut context = context.clone();
            let mut fields = Vec::new();
            let mut expected_ty = expected_ty.clone();
            for concrete_intro_field in concrete_intro_fields {
                let (expected_label, expected_term_ty, rest) = match expected_ty.as_ref() {
                    domain::Value::RecordTypeExtend(_, label, _, ty, rest) => Ok((label, ty, rest)),
                    _ => Err(Diagnostic::new_error("too many fields found")
                        .with_label(DiagnosticLabel::new_primary(*span))),
                }?;
                let (found_label, params, body_ty, body) = concrete_intro_field.desugar();
                if found_label.slice == expected_label.0 {
                    let clause = Clause::new(params, body_ty, &body);
                    let term = clause::check_clause(&context, metas, clause, expected_term_ty)?;
                    let term_value = context.eval_term(metas, body.span(), &term)?;
                    let term_ty = expected_term_ty.clone();
                    fields.push((expected_label.clone(), term));
                    context.add_defn(found_label, term_value.clone(), term_ty);
                    expected_ty = context.app_closure(metas, &rest, term_value)?;
                } else {
                    return Err(Diagnostic::new_error("field not found").with_label(
                        DiagnosticLabel::new_primary(found_label.span()).with_message(format!(
                            "expected `{}`, but found `{}`",
                            found_label, expected_label,
                        )),
                    ));
                }
            }
            if let domain::Value::RecordTypeEmpty = expected_ty.as_ref() {
                Ok(Rc::from(syntax::Term::RecordIntro(fields)))
            } else {
                Err(Diagnostic::new_error("not enough fields provided")
                    .with_label(DiagnosticLabel::new_primary(*span)))
            }
        },
        _ => {
            let (synth, synth_ty) = synth_term(MetaInsertion::Yes, context, metas, concrete_term)?;
            context.unify_values(metas, concrete_term.span(), &synth_ty, expected_ty)?;
            Ok(synth)
        },
    }
}
pub fn check_term ( context : & Context , metas : & mut meta :: Env , concrete_term : & Term < ' _ > , expected_ty : & Rc < domain :: Type > , ) -> Result < Rc < syntax :: Term > , Diagnostic < FileSpan > > { log :: trace ! ( " \t \t " concrete_term ) ; match concrete_term { Term :: Prim ( _ , name ) => { let prim_name = prim :: Name ( literal :: parse_string ( name ) ? ) ; match context . prims ( ) . lookup_entry ( & prim_name ) { None => Err ( Diagnostic :: new_error ( " " ) . with_label ( DiagnosticLabel :: new_primary ( name . span ( ) ) ) ) , Some ( _ ) => Ok ( Rc :: from ( syntax :: Term :: prim ( prim_name ) ) ) , } } , Term :: Hole ( span ) => Ok ( context . new_meta ( metas , * span , expected_ty . clone ( ) ) ) , Term :: Parens ( _ , concrete_term ) => check_term ( context , metas , concrete_term , expected_ty ) , Term :: Let ( _ , concrete_items , concrete_body ) => { let mut context = context . clone ( ) ; let items = check_items ( & mut context , metas , concrete_items ) ? ; let body = check_term ( & context , metas , concrete_body , expected_ty ) ? ; Ok ( Rc :: from ( syntax :: Term :: Let ( items , body ) ) ) } , Term :: If ( _ , condition , consequent , alternative ) => { let bool_ty = Rc :: from ( domain :: Value :: literal_ty ( LiteralType :: Bool ) ) ; let condition = check_term ( context , metas , condition , & bool_ty ) ? ; let consequent = check_term ( context , metas , consequent , expected_ty ) ? ; let alternative = check_term ( context , metas , alternative , expected_ty ) ? ; Ok ( Rc :: from ( syntax :: Term :: LiteralElim ( condition , Rc :: from ( vec ! [ ( LiteralIntro Bool ( true ) consequent ) ] ) , alternative , ) ) ) } , Term :: Case ( span , scrutinee , clauses ) => { let clauses = clauses . iter ( ) . map ( | ( pattern , body ) | CaseClause :: new ( pattern , body ) ) . collect ( ) ; clause :: check_case ( context , metas , * span , scrutinee , clauses , expected_ty ) } , Term :: LiteralIntro ( kind , literal ) => { let literal_intro = literal :: check ( context , metas , * kind , literal , expected_ty ) ? ; Ok ( Rc :: from ( syntax :: Term :: literal_intro ( literal_intro ) ) ) } , Term :: FunIntro ( _ , concrete_params , concrete_body ) => { let clause = Clause :: new ( concrete_params , None , concrete_body ) ; clause :: check_clause ( context , metas , clause , expected_ty ) } , Term :: RecordIntro ( span , concrete_intro_fields ) => { let mut context = context . clone ( ) ; let mut fields = Vec :: new ( ) ; let mut expected_ty = expected_ty . clone ( ) ; for concrete_intro_field in concrete_intro_fields { let ( expected_label , expected_term_ty , rest ) = match expected_ty . as_ref ( ) { domain :: Value :: RecordTypeExtend ( _ , label , _ , ty , rest ) => Ok ( ( label , ty , rest ) ) , _ => Err ( Diagnostic :: new_error ( " " ) . with_label ( DiagnosticLabel :: new_primary ( * span ) ) ) , } ? ; let ( found_label , params , body_ty , body ) = concrete_intro_field . desugar ( ) ; if found_label . slice == expected_label . 0 { let clause = Clause :: new ( params , body_ty , & body ) ; let term = clause :: check_clause ( & context , metas , clause , expected_term_ty ) ? ; let term_value = context . eval_term ( metas , body . span ( ) , & term ) ? ; let term_ty = expected_term_ty . clone ( ) ; fields . push ( ( expected_label . clone ( ) , term ) ) ; context . add_defn ( found_label , term_value . clone ( ) , term_ty ) ; expected_ty = context . app_closure ( metas , & rest , term_value ) ? ; } else { return Err ( Diagnostic :: new_error ( " " ) . with_label ( DiagnosticLabel :: new_primary ( found_label . span ( ) ) . with_message ( format ! ( " " found_label expected_label ) ) , ) ) ; } } if let domain :: Value :: RecordTypeEmpty = expected_ty . as_ref ( ) { Ok ( Rc :: from ( syntax :: Term :: RecordIntro ( fields ) ) ) } else { Err ( Diagnostic :: new_error ( " " ) . with_label ( DiagnosticLabel :: new_primary ( * span ) ) ) } } , _ => { let ( synth , synth_ty ) = synth_term ( MetaInsertion :: Yes , context , metas , concrete_term ) ? ; context . unify_values ( metas , concrete_term . span ( ) , & synth_ty , expected_ty ) ? ; Ok ( synth ) } , } }
Check that a given term conforms to an expected type.
Check that a given term conforms to an expected type .
context
&Context
metas
&mut meta::Env
concrete_term
&Term<'_>
expected_ty
&Rc<domain::Type>