~jojo/kapreolo

ff31d0cbff741667fdd8788680f2a06715f80c5c — JoJo 2 months ago b845ed8
subst all tvars in expr tree when done checking def
3 files changed, 39 insertions(+), 12 deletions(-)

M src/check.rs
M src/main.rs
M src/prelude.rs
M src/check.rs => src/check.rs +14 -4
@@ 29,12 29,14 @@ pub struct Def {
    pub root: ExprRef,
}

#[derive(Debug)]
enum TVar {
    Univ,  // Bound in a universal quantification
    Exist, // Existential type. As of yet unknown.
    Subst(Type),
}

#[derive(Debug)]
struct Checker<'c, 'r> {
    cache: &'c mut Cache,
    exprs: &'r Arena<ExprRef, Expr>,


@@ 89,10 91,18 @@ impl<'c, 'r> Checker<'c, 'r> {
        };
        checker.infer(def.root)?;
        assert_eq!(checker.exprs.len(), checker.expr_types.len());

        let t_root = checker.expr_types.get(def.root).unwrap().clone();
        let t_root = checker.subst_type(&t_root);
        let Checker { explicit_tvars, hole_locs, tvars, expr_types, .. } = checker;
        let expr_types = {
            let mut v = Vec::with_capacity(expr_types.len() as usize);
            for i in 0..expr_types.len() {
                let t = &expr_types.get(ExprRef::from_u32(i)).unwrap();
                let tsubst = subst_type_rec(&|tvref| &tvars[tvref], t);
                v.push(tsubst)
            }
            Arena::<ExprRef, _>::from(v)
        };

        let t_root = expr_types[def.root].clone();
        let annotated = def.expr_annots.get(def.root).is_some();
        for tv in free_tvars(&t_root) {
            match (annotated, &tvars[tv]) {


@@ 104,7 114,7 @@ impl<'c, 'r> Checker<'c, 'r> {
                (_, TVar::Subst(_)) => panic!("ice: TVar::Subst after subst_type in inferred type of def root"),
            }
        }
        Ok(expr_types.to_continuous())
        Ok(expr_types)
    }

    fn infer(&mut self, eref: ExprRef) -> Result<&Type> {

M src/main.rs => src/main.rs +21 -0
@@ 451,4 451,25 @@ mod test {
        ";
        assert_matches!(run_tmp(src), Ok(Operand::Const(Const::Int(55))))
    }

    #[test]
    fn test_match() {
        let src = "
            (def main (base2pow 5))
            (def base2pow
                 (fun [x]
                      (match x
                             [0   1]
                             [1   2]
                             [2   4]
                             [3   8]
                             [4  16]
                             [5  32]
                             [6  64]
                             [7 128]
                             [8 256]
                             [x  -1])))
        ";
        assert_matches!(run_tmp(src), Ok(Operand::Const(Const::Int(32))))
    }
}

M src/prelude.rs => src/prelude.rs +4 -8
@@ 23,6 23,10 @@ impl<K: ArenaElemRef, V> Arena<K, V> {
        Self(vec![], PhantomData)
    }

    pub fn from(v: Vec<V>) -> Self {
        Self(v, PhantomData)
    }

    pub fn len(&self) -> u32 {
        self.0.len() as u32
    }


@@ 100,14 104,6 @@ impl<K: ArenaElemRef, V> SparseOutOfBand<K, V> {
    pub fn get(&self, elem_ref: K) -> Option<&V> {
        self.0.get(&elem_ref.to_u32())
    }

    pub fn to_continuous(mut self) -> OutOfBand<K, V> {
        let mut v = Vec::with_capacity(self.0.len());
        for i in 0..self.0.len() {
            v.push(self.0.remove(&(i as u32)).unwrap())
        }
        Arena(v, self.1)
    }
}

impl<K: ArenaElemRef, V: Default> SparseOutOfBand<K, V> {