/// Check the given items and add them to the context.
Check the given items and add them to the context.
Check the given items and add them to the context .
fn check_items(context: &mut Context, metas: &meta::Env, items: &[Item]) -> Result<(), TypeError> {
    // Declarations that may be waiting to be defined
    let mut forward_declarations = im::HashMap::new();
    for item in items {
        use im::hashmap::Entry;
        match item {
            Item::Declaration(_, label, term_ty) => {
                log::trace!("checking declaration:\t{}\t= {:?}", label, term_ty);
                match forward_declarations.entry(&label.0) {
                    // No previous declaration for this name was seen, so we can
                    // go-ahead and type check, elaborate, and then add it to
                    // the context
                    Entry::Vacant(entry) => {
                        synth_universe(&context, metas, &term_ty)?;
                        // Ensure that we evaluate the forward declaration in
                        // the current context - if we wait until later more
                        // definitions might have come in to scope!
                        let term_ty = context.eval_term(metas, &term_ty)?;
                        entry.insert(Some(term_ty));
                    },
                    // There's a declaration for this name already pending - we
                    // can't add a new one!
                    Entry::Occupied(_) => return Err(TypeError::AlreadyDeclared(label.clone())),
                }
                log::trace!("validated declaration:\t{}", label);
            },
            Item::Definition(_, label, term) => {
                log::trace!("checking definition:\t{}\t= {:?}", label, term);
                let (term, ty) = match forward_declarations.entry(&label.0) {
                    // No prior declaration was found, so we'll try synthesizing
                    // its type instead
                    Entry::Vacant(entry) => {
                        let term_ty = synth_term(&context, metas, term)?;
                        entry.insert(None);
                        (term, term_ty)
                    },
                    // Something has happened with this declaration, let's
                    // 'take' a look!
                    Entry::Occupied(mut entry) => match entry.get_mut().take() {
                        // We found a prior declaration, so we'll use it as a
                        // basis for checking the definition
                        Some(term_ty) => {
                            check_term(&context, metas, term, &term_ty)?;
                            (term, term_ty)
                        },
                        // This declaration was already given a definition, so
                        // this is an error!
                        //
                        // NOTE: Some languages (eg. Haskell, Agda, Idris, and
                        // Erlang) turn duplicate definitions into case matches.
                        // Languages like Elm don't. What should we do here?
                        None => return Err(TypeError::AlreadyDefined(label.clone())),
                    },
                };
                log::trace!("validated definition:\t{}", label);
                let value = context.eval_term(metas, &term)?;
                context.add_defn(value, ty);
            },
        }
    }
    Ok(())
}
fn check_items ( context : & mut Context , metas : & meta :: Env , items : & [ Item ] ) -> Result < ( ) , TypeError > { // Declarations that may be waiting to be defined let mut forward_declarations = im :: HashMap :: new ( ) ; for item in items { use im :: hashmap :: Entry ; match item { Item :: Declaration ( _ , label , term_ty ) => { log :: trace ! ( " \t \t " label term_ty ) ; match forward_declarations . entry ( & label . 0 ) { // No previous declaration for this name was seen, so we can // go-ahead and type check, elaborate, and then add it to // the context Entry :: Vacant ( entry ) => { synth_universe ( & context , metas , & term_ty ) ? ; // Ensure that we evaluate the forward declaration in // the current context - if we wait until later more // definitions might have come in to scope! let term_ty = context . eval_term ( metas , & term_ty ) ? ; entry . insert ( Some ( term_ty ) ) ; } , // There's a declaration for this name already pending - we // can't add a new one! Entry :: Occupied ( _ ) => return Err ( TypeError :: AlreadyDeclared ( label . clone ( ) ) ) , } log :: trace ! ( " \t " label ) ; } , Item :: Definition ( _ , label , term ) => { log :: trace ! ( " \t \t " label term ) ; let ( term , ty ) = match forward_declarations . entry ( & label . 0 ) { // No prior declaration was found, so we'll try synthesizing // its type instead Entry :: Vacant ( entry ) => { let term_ty = synth_term ( & context , metas , term ) ? ; entry . insert ( None ) ; ( term , term_ty ) } , // Something has happened with this declaration, let's // 'take' a look! Entry :: Occupied ( mut entry ) => match entry . get_mut ( ) . take ( ) { // We found a prior declaration, so we'll use it as a // basis for checking the definition Some ( term_ty ) => { check_term ( & context , metas , term , & term_ty ) ? ; ( term , term_ty ) } , // This declaration was already given a definition, so // this is an error! // // NOTE: Some languages (eg. Haskell, Agda, Idris, and // Erlang) turn duplicate definitions into case matches. // Languages like Elm don't. What should we do here? None => return Err ( TypeError :: AlreadyDefined ( label . clone ( ) ) ) , } , } ; log :: trace ! ( " \t " label ) ; let value = context . eval_term ( metas , & term ) ? ; context . add_defn ( value , ty ) ; } , } } Ok ( ( ) ) }
Check the given items and add them to the context.
Check the given items and add them to the context .
context
&mut Context
metas
&meta::Env
items
&[Item]