/// Synthesize the type of the term.
Synthesize the type of the term.
Synthesize the type of the term .
pub fn synth_term(
    context: &Context,
    metas: &meta::Env,
    term: &Rc<Term>,
) -> Result<Rc<Type>, TypeError> {
    use std::cmp;
    log::trace!("synthesizing term:\t{:?}", term);
    match term.as_ref() {
        Term::Var(var_index) => match context.lookup_ty(*var_index) {
            None => Err(TypeError::UnboundVariable(*var_index)),
            Some(var_ty) => Ok(var_ty.clone()),
        },
        Term::Meta(meta_level) => match metas.lookup_solution(*meta_level) {
            Some((_, meta::Solution::Solved(_value), meta_ty)) => Ok(meta_ty.clone()),
            Some((_, meta::Solution::Unsolved, _)) => Err(TypeError::UnsolvedMeta(*meta_level)),
            None => Err(TypeError::UnboundMeta(*meta_level)),
        },
        Term::Prim(prim_name) => match context.prims().lookup_entry(prim_name) {
            None => Err(TypeError::UnknownPrim(prim_name.clone())),
            Some(_) => Err(TypeError::AmbiguousTerm(term.clone())),
        },
        Term::Ann(term, term_ty) => {
            synth_universe(context, metas, term_ty)?;
            let term_ty = context.eval_term(metas, &term_ty)?;
            check_term(context, metas, term, &term_ty)?;
            Ok(term_ty)
        },
        Term::Let(items, body) => {
            let mut context = context.clone();
            check_items(&mut context, metas, items)?;
            synth_term(&context, metas, body)
        },
        Term::LiteralType(_) => Ok(Rc::from(Value::universe(0))),
        Term::LiteralIntro(literal_intro) => Ok(synth_literal(literal_intro)),
        Term::LiteralElim(_, _, _) => Err(TypeError::AmbiguousTerm(term.clone())),
        Term::FunType(_app_mode, _, param_ty, body_ty) => {
            let param_level = synth_universe(context, metas, param_ty)?;
            let param_ty_value = context.eval_term(metas, param_ty)?;
            let mut body_ty_context = context.clone();
            body_ty_context.add_param(param_ty_value);
            let body_level = synth_universe(&body_ty_context, metas, body_ty)?;
            Ok(Rc::from(Value::universe(cmp::max(param_level, body_level))))
        },
        Term::FunIntro(_, _, _) => Err(TypeError::AmbiguousTerm(term.clone())),
        Term::FunElim(fun, arg_app_mode, arg) => {
            let fun_ty = synth_term(context, metas, fun)?;
            match fun_ty.as_ref() {
                Value::FunType(ty_app_mode, _, arg_ty, body_ty) if arg_app_mode == ty_app_mode => {
                    check_term(context, metas, arg, arg_ty)?;
                    let arg_value = context.eval_term(metas, arg)?;
                    Ok(context.app_closure(metas, body_ty, arg_value)?)
                },
                Value::FunType(ty_app_mode, _, _, _) => Err(TypeError::UnexpectedAppMode {
                    found: arg_app_mode.clone(),
                    expected: ty_app_mode.clone(),
                }),
                _ => Err(TypeError::ExpectedFunType {
                    found: fun_ty.clone(),
                }),
            }
        },
        Term::RecordType(ty_fields) => {
            let mut context = context.clone();
            let mut max_level = UniverseLevel(0);
            for (_, _, _, ty) in ty_fields {
                let ty_level = synth_universe(&context, metas, &ty)?;
                context.add_param(context.eval_term(metas, &ty)?);
                max_level = cmp::max(max_level, ty_level);
            }
            Ok(Rc::from(Value::universe(max_level)))
        },
        Term::RecordIntro(intro_fields) => {
            if intro_fields.is_empty() {
                Ok(Rc::from(Value::RecordTypeEmpty))
            } else {
                Err(TypeError::AmbiguousTerm(term.clone()))
            }
        },
        Term::RecordElim(record, label) => {
            let mut record_ty = synth_term(context, metas, record)?;
            while let Value::RecordTypeExtend(_, current_label, _, current_ty, rest) =
                record_ty.as_ref()
            {
                if label == current_label {
                    return Ok(current_ty.clone());
                } else {
                    let label = current_label.clone();
                    let expr = Rc::from(Term::RecordElim(record.clone(), label));
                    record_ty =
                        context.app_closure(metas, rest, context.eval_term(metas, &expr)?)?;
                }
            }
            Err(TypeError::NoFieldInType(label.clone()))
        },
        Term::Universe(level) => match level.shift(1) {
            None => Err(TypeError::OverflowingUniverseLevel),
            Some(level) => Ok(Rc::from(Value::universe(level))),
        },
    }
}
pub fn synth_term ( context : & Context , metas : & meta :: Env , term : & Rc < Term > , ) -> Result < Rc < Type > , TypeError > { use std :: cmp ; log :: trace ! ( " \t " term ) ; match term . as_ref ( ) { Term :: Var ( var_index ) => match context . lookup_ty ( * var_index ) { None => Err ( TypeError :: UnboundVariable ( * var_index ) ) , Some ( var_ty ) => Ok ( var_ty . clone ( ) ) , } , Term :: Meta ( meta_level ) => match metas . lookup_solution ( * meta_level ) { Some ( ( _ , meta :: Solution :: Solved ( _value ) , meta_ty ) ) => Ok ( meta_ty . clone ( ) ) , Some ( ( _ , meta :: Solution :: Unsolved , _ ) ) => Err ( TypeError :: UnsolvedMeta ( * meta_level ) ) , None => Err ( TypeError :: UnboundMeta ( * meta_level ) ) , } , Term :: Prim ( prim_name ) => match context . prims ( ) . lookup_entry ( prim_name ) { None => Err ( TypeError :: UnknownPrim ( prim_name . clone ( ) ) ) , Some ( _ ) => Err ( TypeError :: AmbiguousTerm ( term . clone ( ) ) ) , } , Term :: Ann ( term , term_ty ) => { synth_universe ( context , metas , term_ty ) ? ; let term_ty = context . eval_term ( metas , & term_ty ) ? ; check_term ( context , metas , term , & term_ty ) ? ; Ok ( term_ty ) } , Term :: Let ( items , body ) => { let mut context = context . clone ( ) ; check_items ( & mut context , metas , items ) ? ; synth_term ( & context , metas , body ) } , Term :: LiteralType ( _ ) => Ok ( Rc :: from ( Value :: universe ( 0 ) ) ) , Term :: LiteralIntro ( literal_intro ) => Ok ( synth_literal ( literal_intro ) ) , Term :: LiteralElim ( _ , _ , _ ) => Err ( TypeError :: AmbiguousTerm ( term . clone ( ) ) ) , Term :: FunType ( _app_mode , _ , param_ty , body_ty ) => { let param_level = synth_universe ( context , metas , param_ty ) ? ; let param_ty_value = context . eval_term ( metas , param_ty ) ? ; let mut body_ty_context = context . clone ( ) ; body_ty_context . add_param ( param_ty_value ) ; let body_level = synth_universe ( & body_ty_context , metas , body_ty ) ? ; Ok ( Rc :: from ( Value :: universe ( cmp :: max ( param_level , body_level ) ) ) ) } , Term :: FunIntro ( _ , _ , _ ) => Err ( TypeError :: AmbiguousTerm ( term . clone ( ) ) ) , Term :: FunElim ( fun , arg_app_mode , arg ) => { let fun_ty = synth_term ( context , metas , fun ) ? ; match fun_ty . as_ref ( ) { Value :: FunType ( ty_app_mode , _ , arg_ty , body_ty ) if arg_app_mode == ty_app_mode => { check_term ( context , metas , arg , arg_ty ) ? ; let arg_value = context . eval_term ( metas , arg ) ? ; Ok ( context . app_closure ( metas , body_ty , arg_value ) ? ) } , Value :: FunType ( ty_app_mode , _ , _ , _ ) => Err ( TypeError :: UnexpectedAppMode { found : arg_app_mode . clone ( ) , expected : ty_app_mode . clone ( ) , } ) , _ => Err ( TypeError :: ExpectedFunType { found : fun_ty . clone ( ) , } ) , } } , Term :: RecordType ( ty_fields ) => { let mut context = context . clone ( ) ; let mut max_level = UniverseLevel ( 0 ) ; for ( _ , _ , _ , ty ) in ty_fields { let ty_level = synth_universe ( & context , metas , & ty ) ? ; context . add_param ( context . eval_term ( metas , & ty ) ? ) ; max_level = cmp :: max ( max_level , ty_level ) ; } Ok ( Rc :: from ( Value :: universe ( max_level ) ) ) } , Term :: RecordIntro ( intro_fields ) => { if intro_fields . is_empty ( ) { Ok ( Rc :: from ( Value :: RecordTypeEmpty ) ) } else { Err ( TypeError :: AmbiguousTerm ( term . clone ( ) ) ) } } , Term :: RecordElim ( record , label ) => { let mut record_ty = synth_term ( context , metas , record ) ? ; while let Value :: RecordTypeExtend ( _ , current_label , _ , current_ty , rest ) = record_ty . as_ref ( ) { if label == current_label { return Ok ( current_ty . clone ( ) ) ; } else { let label = current_label . clone ( ) ; let expr = Rc :: from ( Term :: RecordElim ( record . clone ( ) , label ) ) ; record_ty = context . app_closure ( metas , rest , context . eval_term ( metas , & expr ) ? ) ? ; } } Err ( TypeError :: NoFieldInType ( label . clone ( ) ) ) } , Term :: Universe ( level ) => match level . shift ( 1 ) { None => Err ( TypeError :: OverflowingUniverseLevel ) , Some ( level ) => Ok ( Rc :: from ( Value :: universe ( level ) ) ) , } , } }
Synthesize the type of the term.
Synthesize the type of the term .
context
&Context
metas
&meta::Env
term
&Rc<Term>