/// Read a value back into the core syntax, normalizing as required.
Read a value back into the core syntax, normalizing as required.
Read a value back into the core syntax normalizing as required .
pub fn read_back_value(
    prims: &prim::Env,
    metas: &meta::Env,
    size: var::Size,
    term: &Rc<Value>,
) -> Result<Rc<Term>, String> {
    match term.as_ref() {
        Value::Neutral(head, spine) => read_back_neutral(prims, metas, size, head, spine),
        // Literals
        Value::LiteralType(literal_ty) => Ok(Rc::from(Term::literal_ty(literal_ty.clone()))),
        Value::LiteralIntro(literal_intro) => {
            Ok(Rc::from(Term::literal_intro(literal_intro.clone())))
        },
        // Functions
        Value::FunType(app_mode, name_hint, param_ty, body_ty) => {
            let app_mode = app_mode.clone();
            let name_hint = name_hint.clone();
            let body_ty = inst_closure(prims, metas, size, body_ty)?;
            let param_ty = read_back_value(prims, metas, size, param_ty)?;
            let body_ty = read_back_value(prims, metas, size + 1, &body_ty)?;
            Ok(Rc::from(Term::FunType(
                app_mode, name_hint, param_ty, body_ty,
            )))
        },
        Value::FunIntro(app_mode, name_hint, body) => {
            let app_mode = app_mode.clone();
            let name_hint = name_hint.clone();
            let body = inst_closure(prims, metas, size, body)?;
            let body = read_back_value(prims, metas, size + 1, &body)?;
            Ok(Rc::from(Term::FunIntro(app_mode, name_hint, body)))
        },
        // Records
        Value::RecordTypeExtend(doc, label, name_hint, term_ty, rest_ty) => {
            let mut size = size;
            let term_ty = read_back_value(prims, metas, size, term_ty)?;
            let mut rest_ty = inst_closure(prims, metas, size, rest_ty)?;
            let mut field_tys = vec![(doc.clone(), label.clone(), name_hint.clone(), term_ty)];
            while let Value::RecordTypeExtend(doc, label, name_hint, next_term_ty, next_rest_ty) =
                rest_ty.as_ref()
            {
                size += 1;
                let next_term_ty = read_back_value(prims, metas, size, next_term_ty)?;
                field_tys.push((doc.clone(), label.clone(), name_hint.clone(), next_term_ty));
                rest_ty = inst_closure(prims, metas, size, next_rest_ty)?;
            }
            Ok(Rc::from(Term::RecordType(field_tys)))
        },
        Value::RecordTypeEmpty => Ok(Rc::from(Term::RecordType(Vec::new()))),
        Value::RecordIntro(fields) => {
            let fields = fields
                .iter()
                .map(|(label, term)| {
                    Ok((label.clone(), read_back_value(prims, metas, size, term)?))
                })
                .collect::<Result<_, String>>()?;
            Ok(Rc::from(Term::RecordIntro(fields)))
        },
        // Universes
        Value::Universe(level) => Ok(Rc::from(Term::universe(*level))),
    }
}
pub fn read_back_value ( prims : & prim :: Env , metas : & meta :: Env , size : var :: Size , term : & Rc < Value > , ) -> Result < Rc < Term > , String > { match term . as_ref ( ) { Value :: Neutral ( head , spine ) => read_back_neutral ( prims , metas , size , head , spine ) , // Literals Value :: LiteralType ( literal_ty ) => Ok ( Rc :: from ( Term :: literal_ty ( literal_ty . clone ( ) ) ) ) , Value :: LiteralIntro ( literal_intro ) => { Ok ( Rc :: from ( Term :: literal_intro ( literal_intro . clone ( ) ) ) ) } , // Functions Value :: FunType ( app_mode , name_hint , param_ty , body_ty ) => { let app_mode = app_mode . clone ( ) ; let name_hint = name_hint . clone ( ) ; let body_ty = inst_closure ( prims , metas , size , body_ty ) ? ; let param_ty = read_back_value ( prims , metas , size , param_ty ) ? ; let body_ty = read_back_value ( prims , metas , size + 1 , & body_ty ) ? ; Ok ( Rc :: from ( Term :: FunType ( app_mode , name_hint , param_ty , body_ty , ) ) ) } , Value :: FunIntro ( app_mode , name_hint , body ) => { let app_mode = app_mode . clone ( ) ; let name_hint = name_hint . clone ( ) ; let body = inst_closure ( prims , metas , size , body ) ? ; let body = read_back_value ( prims , metas , size + 1 , & body ) ? ; Ok ( Rc :: from ( Term :: FunIntro ( app_mode , name_hint , body ) ) ) } , // Records Value :: RecordTypeExtend ( doc , label , name_hint , term_ty , rest_ty ) => { let mut size = size ; let term_ty = read_back_value ( prims , metas , size , term_ty ) ? ; let mut rest_ty = inst_closure ( prims , metas , size , rest_ty ) ? ; let mut field_tys = vec ! [ ( doc clone ( ) label clone ( ) name_hint clone ( ) term_ty ) ] ; while let Value :: RecordTypeExtend ( doc , label , name_hint , next_term_ty , next_rest_ty ) = rest_ty . as_ref ( ) { size += 1 ; let next_term_ty = read_back_value ( prims , metas , size , next_term_ty ) ? ; field_tys . push ( ( doc . clone ( ) , label . clone ( ) , name_hint . clone ( ) , next_term_ty ) ) ; rest_ty = inst_closure ( prims , metas , size , next_rest_ty ) ? ; } Ok ( Rc :: from ( Term :: RecordType ( field_tys ) ) ) } , Value :: RecordTypeEmpty => Ok ( Rc :: from ( Term :: RecordType ( Vec :: new ( ) ) ) ) , Value :: RecordIntro ( fields ) => { let fields = fields . iter ( ) . map ( | ( label , term ) | { Ok ( ( label . clone ( ) , read_back_value ( prims , metas , size , term ) ? ) ) } ) . collect :: < Result < _ , String > > ( ) ? ; Ok ( Rc :: from ( Term :: RecordIntro ( fields ) ) ) } , // Universes Value :: Universe ( level ) => Ok ( Rc :: from ( Term :: universe ( * level ) ) ) , } }
Read a value back into the core syntax, normalizing as required.
Read a value back into the core syntax normalizing as required .
prims
&prim::Env
metas
&meta::Env
size
var::Size
term
&Rc<Value>