/// Check that a term conforms to a given type.
Check that a term conforms to a given type.
Check that a term conforms to a given type .
pub fn check_term(
    context: &Context,
    metas: &meta::Env,
    term: &Rc<Term>,
    expected_ty: &Rc<Type>,
) -> Result<(), TypeError> {
    log::trace!("checking term:\t\t{:?}", term);
    match term.as_ref() {
        Term::Prim(prim_name) => match context.prims().lookup_entry(prim_name) {
            None => Err(TypeError::UnknownPrim(prim_name.clone())),
            Some(_) => Ok(()),
        },
        Term::Let(items, body) => {
            let mut context = context.clone();
            check_items(&mut context, metas, items)?;
            check_term(&context, metas, body, expected_ty)
        },
        Term::LiteralElim(scrutinee, clauses, default_body) => {
            let scrutinee_ty = synth_term(context, metas, scrutinee)?;
            // Check that the clauses are sorted by patterns and that patterns aren't duplicated
            // TODO: use `Iterator::is_sorted_by` when it is stable
            if clauses
                .iter()
                .tuple_windows()
                // FIXME: Floating point equality?
                .any(|((l1, _), (l2, _))| l1 >= l2)
            {
                return Err(TypeError::BadLiteralPatterns(
                    clauses.iter().map(|(l, _)| l.clone()).collect(),
                ));
            }
            for (literal_intro, body) in clauses.iter() {
                check_literal(context, metas, literal_intro, &scrutinee_ty)?;
                check_term(context, metas, body, &expected_ty)?;
            }
            check_term(context, metas, default_body, expected_ty)
        },
        Term::FunIntro(intro_app_mode, _, body) => match expected_ty.as_ref() {
            Value::FunType(ty_app_mode, _, param_ty, body_ty) if intro_app_mode == ty_app_mode => {
                let mut body_context = context.clone();
                let param = body_context.add_param(param_ty.clone());
                let body_ty = context.app_closure(metas, body_ty, param)?;
                check_term(&body_context, metas, body, &body_ty)
            },
            Value::FunType(ty_app_mode, _, _, _) => Err(TypeError::UnexpectedAppMode {
                found: intro_app_mode.clone(),
                expected: ty_app_mode.clone(),
            }),
            _ => Err(TypeError::ExpectedFunType {
                found: expected_ty.clone(),
            }),
        },
        Term::RecordIntro(intro_fields) => {
            let mut context = context.clone();
            let mut expected_ty = expected_ty.clone();
            for (label, term) in intro_fields {
                if let Value::RecordTypeExtend(_, expected_label, _, expected_term_ty, rest) =
                    expected_ty.as_ref()
                {
                    if label != expected_label {
                        return Err(TypeError::UnexpectedField {
                            found: label.clone(),
                            expected: expected_label.clone(),
                        });
                    }
                    check_term(&context, metas, term, expected_term_ty)?;
                    let term_value = context.eval_term(metas, term)?;
                    context.add_defn(term_value.clone(), expected_term_ty.clone());
                    expected_ty = context.app_closure(metas, &rest, term_value)?;
                } else {
                    return Err(TypeError::TooManyFieldsFound);
                }
            }
            if let Value::RecordTypeEmpty = expected_ty.as_ref() {
                Ok(())
            } else {
                Err(TypeError::NotEnoughFieldsProvided)
            }
        },
        _ => {
            let synth_ty = synth_term(context, metas, term)?;
            context.check_subtype(metas, &synth_ty, expected_ty)
        },
    }
}
pub fn check_term ( context : & Context , metas : & meta :: Env , term : & Rc < Term > , expected_ty : & Rc < Type > , ) -> Result < ( ) , TypeError > { log :: trace ! ( " \t \t " term ) ; match term . as_ref ( ) { Term :: Prim ( prim_name ) => match context . prims ( ) . lookup_entry ( prim_name ) { None => Err ( TypeError :: UnknownPrim ( prim_name . clone ( ) ) ) , Some ( _ ) => Ok ( ( ) ) , } , Term :: Let ( items , body ) => { let mut context = context . clone ( ) ; check_items ( & mut context , metas , items ) ? ; check_term ( & context , metas , body , expected_ty ) } , Term :: LiteralElim ( scrutinee , clauses , default_body ) => { let scrutinee_ty = synth_term ( context , metas , scrutinee ) ? ; // Check that the clauses are sorted by patterns and that patterns aren't duplicated // TODO: use `Iterator::is_sorted_by` when it is stable if clauses . iter ( ) . tuple_windows ( ) // FIXME: Floating point equality? . any ( | ( ( l1 , _ ) , ( l2 , _ ) ) | l1 >= l2 ) { return Err ( TypeError :: BadLiteralPatterns ( clauses . iter ( ) . map ( | ( l , _ ) | l . clone ( ) ) . collect ( ) , ) ) ; } for ( literal_intro , body ) in clauses . iter ( ) { check_literal ( context , metas , literal_intro , & scrutinee_ty ) ? ; check_term ( context , metas , body , & expected_ty ) ? ; } check_term ( context , metas , default_body , expected_ty ) } , Term :: FunIntro ( intro_app_mode , _ , body ) => match expected_ty . as_ref ( ) { Value :: FunType ( ty_app_mode , _ , param_ty , body_ty ) if intro_app_mode == ty_app_mode => { let mut body_context = context . clone ( ) ; let param = body_context . add_param ( param_ty . clone ( ) ) ; let body_ty = context . app_closure ( metas , body_ty , param ) ? ; check_term ( & body_context , metas , body , & body_ty ) } , Value :: FunType ( ty_app_mode , _ , _ , _ ) => Err ( TypeError :: UnexpectedAppMode { found : intro_app_mode . clone ( ) , expected : ty_app_mode . clone ( ) , } ) , _ => Err ( TypeError :: ExpectedFunType { found : expected_ty . clone ( ) , } ) , } , Term :: RecordIntro ( intro_fields ) => { let mut context = context . clone ( ) ; let mut expected_ty = expected_ty . clone ( ) ; for ( label , term ) in intro_fields { if let Value :: RecordTypeExtend ( _ , expected_label , _ , expected_term_ty , rest ) = expected_ty . as_ref ( ) { if label != expected_label { return Err ( TypeError :: UnexpectedField { found : label . clone ( ) , expected : expected_label . clone ( ) , } ) ; } check_term ( & context , metas , term , expected_term_ty ) ? ; let term_value = context . eval_term ( metas , term ) ? ; context . add_defn ( term_value . clone ( ) , expected_term_ty . clone ( ) ) ; expected_ty = context . app_closure ( metas , & rest , term_value ) ? ; } else { return Err ( TypeError :: TooManyFieldsFound ) ; } } if let Value :: RecordTypeEmpty = expected_ty . as_ref ( ) { Ok ( ( ) ) } else { Err ( TypeError :: NotEnoughFieldsProvided ) } } , _ => { let synth_ty = synth_term ( context , metas , term ) ? ; context . check_subtype ( metas , & synth_ty , expected_ty ) } , } }
Check that a term conforms to a given type.
Check that a term conforms to a given type .
context
&Context
metas
&meta::Env
term
&Rc<Term>
expected_ty
&Rc<Type>