{"header":{"message":"feat(Syntax.Abstract): add unification and type checking","description":null,"timestamp":"2024-08-26T23:29:23.768470484Z","authors":[{}]},"hash":"JSZSXPHKKMTLHV4CXCYAKHU32USXDBSZH7HSH7V662TZ7JA3VA6QC","authors":[{"login":"fogti","key":"ZFnYYAXSF9fgPaXKyrt5a2oor75nLVcpU8T8fEnRqwm"}],"deps":{"hashes":[["JSZSXPHKKMTLHV4CXCYAKHU32USXDBSZH7HSH7V662TZ7JA3VA6QC","feat(Syntax.Abstract): add unification and type checking"],["AA",null],["QXX6KTFXDUOBY3WATDAZ4XIRLHSRKXLSDQSSD7OP7CDLRUHGJELAC","Syntax.Abstract: implement eval"],["JDF4JUMSZJ6JD4Y27R2G5JC6LFT6SNCP52UDVCGKQ4QAGMGUDMJAC","some attempts at abstract syntax"],["EFHQIYTCATMP3PQNVAUSK75EDA5E3QCOB737TTJWURPFCUO7VSXQC","add Literal from yanais"]],"deps":["QXX6KTFXDUOBY3WATDAZ4XIRLHSRKXLSDQSSD7OP7CDLRUHGJELAC"],"known":["JDF4JUMSZJ6JD4Y27R2G5JC6LFT6SNCP52UDVCGKQ4QAGMGUDMJAC"]},"hunks":[{"Edit":{"inode":{"change":5,"pos":55},"path":"core/lib/GardGround/Syntax/Literal.hs","line":9,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":205}],"down_context":[{"change":5,"pos":205}],"flag":"BLOCK","start":0,"end":15,"inode":{"change":5,"pos":55}}},"contents":[{"Add":" litTypeOf,"}]}},{"Edit":{"inode":{"change":5,"pos":55},"path":"core/lib/GardGround/Syntax/Literal.hs","line":38,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":1019}],"down_context":[],"flag":"BLOCK","start":16,"end":176,"inode":{"change":5,"pos":55}}},"contents":[{"Add":""},{"Add":"-- | compute type of literal"},{"Add":"litTypeOf :: Literal -> PrimTy"},{"Add":"litTypeOf (LNat _) = PtUnsInt PIsize"},{"Add":"litTypeOf (LIntSz _) = PtIntSz"},{"Add":"litTypeOf (LPrimTy _) = PtType"}]}},{"Edit":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":11,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":171}],"down_context":[{"change":2,"pos":78}],"flag":"BLOCK","start":177,"end":186,"inode":{"change":3,"pos":36}}},"contents":[{"Add":" unify,"}]}},{"Edit":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":13,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":86}],"down_context":[{"change":3,"pos":171}],"flag":"BLOCK","start":187,"end":209,"inode":{"change":3,"pos":36}}},"contents":[{"Add":" typeInf,"},{"Add":" typeChk,"}]}},{"Replacement":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":21,"ins":{"up_context":[{"change":3,"pos":310}],"down_context":[{"change":3,"pos":353}],"flag":"BLOCK","start":210,"end":294,"inode":{"change":3,"pos":36}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":310},"to":{"change":2,"start":87,"end":144},"introduced_by":2}],"inode":{"change":3,"pos":36}},"ins_contents":[{"Add":"import GardGround.Syntax.Literal (Literal(..), PrimTy(..), lookupBinder, litTypeOf)"}],"del_contents":[{"Del":"import GardGround.Syntax.Literal (Literal, lookupBinder)\n"}]}},{"Edit":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":43,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1055}],"down_context":[{"change":3,"pos":1055}],"flag":"BLOCK","start":295,"end":320,"inode":{"change":3,"pos":36}}},"contents":[{"Add":" | VEInvalidLamTy Value"}]}},{"Edit":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":46,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":175}],"down_context":[{"change":3,"pos":1085}],"flag":"BLOCK","start":321,"end":395,"inode":{"change":3,"pos":36}}},"contents":[{"Add":" | VEInferGlobal Ident"},{"Add":" | VEInferLam Expr"},{"Add":" | VEUnifyFailed Value Value"}]}},{"Edit":{"inode":{"change":3,"pos":36},"path":"core/lib/GardGround/Syntax/Abstract.hs","line":117,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":729}],"down_context":[],"flag":"BLOCK","start":396,"end":3222,"inode":{"change":3,"pos":36}}},"contents":[{"Add":""},{"Add":"unify :: Natural -> Value -> Value -> Either ValueError ()"},{"Add":"unify i l r ="},{"Add":" let vf = vfree $ Quote i in"},{"Add":" case (l, r) of"},{"Add":" (VLam f, VLam f') -> do"},{"Add":" v <- f vf"},{"Add":" v' <- f' vf"},{"Add":" unify (i + 1) v v'"},{"Add":" (VPi a f, VPi a' f') -> do"},{"Add":" unify i a a'"},{"Add":" v <- f vf"},{"Add":" v' <- f' vf"},{"Add":" unify (i + 1) v v'"},{"Add":" (VNeutral (Neutral nr xs), VNeutral (Neutral nr' xs')) -> do"},{"Add":" lres <- unifyList xs xs'"},{"Add":" if (nr /= nr') || (not lres) then (Left $ VEUnifyFailed (VNeutral $ Neutral nr xs) (VNeutral $ Neutral nr' xs')) else pure ()"},{"Add":" _ -> Left $ VEUnifyFailed l r"},{"Add":""},{"Add":" where"},{"Add":" unifyList :: [Value] -> [Value] -> Either ValueError Bool"},{"Add":" unifyList [] [] = Right True"},{"Add":" unifyList [] (_:_) = Right False"},{"Add":" unifyList (_:_) [] = Right False"},{"Add":" unifyList (x:xs) (y:ys) = unify i x y >> unifyList xs ys"},{"Add":""},{"Add":"evalTenv :: [(Value, Value)] -> Expr -> EvalResult"},{"Add":"evalTenv tenv e = eval e $ fmap (\\(x, _) -> x) tenv"},{"Add":"{-# INLINE evalTenv #-}"},{"Add":""},{"Add":"tenvLen :: [(Value, Value)] -> Natural"},{"Add":"tenvLen tenv = toEnum $ length tenv"},{"Add":"{-# INLINE tenvLen #-}"},{"Add":""},{"Add":"-- | Try to infer the type of an expression with a given context of (values, types) on stack"},{"Add":"typeInf :: [(Value, Value)] -> Expr -> EvalResult"},{"Add":"typeInf tenv kind = case kind of"},{"Add":" ENeutralRoot (Local x) -> case lookupBinder tenv x of"},{"Add":" Nothing -> Left . VEOutOfRangeLocal $ x - (tenvLen tenv)"},{"Add":" Just (_, y) -> Right y"},{"Add":" ENeutralRoot (NrLiteral lit) -> Right . VNeutral $ Neutral (NrLiteral . LPrimTy $ litTypeOf lit) mempty"},{"Add":" ENeutralRoot (Global g) -> Left $ VEInferGlobal g"},{"Add":" ENeutralRoot (Quote q) -> Left $ VEOutOfRangeQuote q"},{"Add":""},{"Add":" EAnnot e e' -> do"},{"Add":" v' <- evalTenv tenv e'"},{"Add":" typeChk tenv e v'"},{"Add":" Right v'"},{"Add":""},{"Add":" EApply (ELam e) e' -> do"},{"Add":" t' <- typeInf tenv e'"},{"Add":" v' <- evalTenv tenv e'"},{"Add":" -- here, we don't have to unify the argument"},{"Add":" typeInf ((v', t'):tenv) e"},{"Add":""},{"Add":" EApply e e' -> do"},{"Add":" t <- typeInf tenv e"},{"Add":" case t of"},{"Add":" VPi arg resf -> do"},{"Add":" t' <- typeInf tenv e'"},{"Add":" unify 0 arg t'"},{"Add":" v' <- evalTenv tenv e'"},{"Add":" resf v'"},{"Add":" _ -> Left $ VEInvalidLamTy t"},{"Add":""},{"Add":" EPi e e' -> do"},{"Add":" let vstar = VNeutral $ Neutral (NrLiteral $ LPrimTy PtType) mempty"},{"Add":" typeChk tenv e vstar"},{"Add":" v <- evalTenv tenv e"},{"Add":" let tenv' = (VNeutral $ Neutral (Local $ tenvLen tenv) mempty, v):tenv"},{"Add":" v' <- evalTenv tenv' e'"},{"Add":" q' <- quote 0 v'"},{"Add":" typeChk tenv' q' vstar"},{"Add":" pure vstar"},{"Add":""},{"Add":" ELam f -> Left $ VEInferLam f"},{"Add":""},{"Add":"-- | Check if an expression matches the expected type"},{"Add":"typeChk :: [(Value, Value)] -> Expr -> Value -> Either ValueError ()"},{"Add":"typeChk tenv kind xty = case (kind, xty) of"},{"Add":" (ELam f, VPi arg res) -> do"},{"Add":" let llte = VNeutral $ Neutral (Local $ tenvLen tenv) mempty"},{"Add":" let tenv' = (llte, arg):tenv"},{"Add":" v <- evalTenv tenv' f"},{"Add":" rv <- res llte"},{"Add":" q <- quote 0 v"},{"Add":" typeChk tenv' q rv"},{"Add":""},{"Add":" _ -> do"},{"Add":" k' <- typeInf tenv kind"},{"Add":" unify 0 k' xty"}]}}],"owner":"fogti","repo":"gardground","token":"cXOGBaq6IxqJ/fkyD076k92o4lrecBHWSqzWe9qYZFo=","login":null}

…

Dependencies

Change contents