From ec45a765d7ce277dc54e60906d89fc513b8982df Mon Sep 17 00:00:00 2001 From: Alain Zscheile Date: Sat, 28 Oct 2023 13:28:12 +0200 Subject: [PATCH] haskell: report value evaluation errors --- .../lib/Language/Yanais/Nfker7h/Ast.hs | 120 ++++++++++++------ .../lib/Language/Yanais/Nfker7h/Typeck.hs | 50 +++++--- 2 files changed, 110 insertions(+), 60 deletions(-) diff --git a/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Ast.hs b/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Ast.hs index 7a62144..ca0b606 100644 --- a/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Ast.hs +++ b/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Ast.hs @@ -12,10 +12,13 @@ module Language.Yanais.Nfker7h.Ast ( ExprChk(..), Deque, Neutral(..), + ValueError(..), Value(..), ValueInf(..), Eval(..), + binderLookup, + unpackVB, unpackVP, quoteInf, @@ -25,7 +28,6 @@ module Language.Yanais.Nfker7h.Ast ( ) where import qualified Deque.Strict as Deq -import qualified Data.List as List import Data.Hashable (Hashable) import Data.Void (Void, absurd) import Generic.Data (Generic) @@ -72,14 +74,19 @@ data Binder tyinf = Binder { bdpat :: Pattern Void, bdtyp :: tyinf } data ExprInfKind info = EBound Natural | EFree NeutralRoot + + -- the following can't be the result of quoting | EAnnot (ExprChk info) (ExprChk info) | EApply (ExprInf info) (ExprChk info) + -- lambdas | EILambda (Binder (ExprChk info)) (ExprInf info) | EITyLambda (Binder (ExprChk info)) (ExprChk info) + -- references | ERefOf (ExprInf info) | ERefOfTy (ExprChk info) + deriving (Eq, Functor, Show) -- | checkable expressions (inferrable expressions prefixed by untyped lambda binders) @@ -91,20 +98,32 @@ type Deque a = Deq.Deque a -- | neutral values (a root, to which might be some values applied) data Neutral = Neutral NeutralRoot (Deque Value) -data Value = VLam (Value -> Value) | VInf ValueInf +-- | errors during evaluation to values +data ValueError = + VEInvalidApply ValueInf Value + | VELambdaNonInf (Value -> Either ValueError Value) + | VEOutOfRange Natural -data ValueInf = VPi Value (Value -> Value) +data Value = VLam (Value -> Either ValueError Value) | VInf ValueInf + +data ValueInf = VPi Value (Value -> Either ValueError Value) | VNeutral Neutral | VRefOf ValueInf | VRefOfTy Value -vapp :: Value -> Value -> Value -vapp (VLam f) v = f v -vapp (VInf f) v = VInf $ vappInf f v +binderLookup :: [a] -> Natural -> Maybe a +binderLookup = foldr ffun (const Nothing) + where + ffun x _ 0 = Just x + ffun _ r k = r (k-1) -vappInf :: ValueInf -> Value -> ValueInf -vappInf (VNeutral (Neutral nam xs)) v = VNeutral . (Neutral nam) $ Deq.snoc v xs -vappInf _ _ = error "tried to apply something which can't do that" +vapp :: Value -> Value -> Either ValueError Value +vapp (VLam f) v = f v +vapp (VInf f) v = fmap VInf $ vappInf f v + +vappInf :: ValueInf -> Value -> Either ValueError ValueInf +vappInf (VNeutral (Neutral nam xs)) v = Right . VNeutral . (Neutral nam) $ Deq.snoc v xs +vappInf l r = Left $ VEInvalidApply l r type EvalEnv = [Value] @@ -119,33 +138,44 @@ unpackVP val bindpat env = case bindpat of PatNameAnon -> val:env PatName nam -> if nullIdent nam then env else val:env -killNonInf :: Value -> ValueInf -killNonInf (VLam _) = error "lambda is not inferrable" -killNonInf (VInf v) = v +killNonInf :: Value -> Either ValueError ValueInf +killNonInf (VLam l) = Left . VELambdaNonInf $ l +killNonInf (VInf v) = Right v class Eval a where - eval :: a b -> EvalEnv -> Value + eval :: a b -> EvalEnv -> Either ValueError Value subst :: Natural -> ExprInf b -> a b -> a b -evalInf :: ExprInfKind info -> EvalEnv -> ValueInf +evalInf :: ExprInfKind info -> EvalEnv -> Either ValueError ValueInf evalInf kind env = case kind of - EBound b -> killNonInf $ List.genericIndex env b - EAnnot e _ -> killNonInf $ eval e env - EApply e e' -> killNonInf $ vapp (eval e env) (eval e' env) - EILambda b e' -> killNonInf $ VLam $ \y -> eval e' $ unpackVB y b env + EBound b -> case binderLookup env b of + Nothing -> Left . VEOutOfRange $ b + Just y -> killNonInf y + EAnnot e _ -> eval e env >>= killNonInf + EApply e e' -> do + v <- eval e env + v' <- eval e' env + vapp v v' >>= killNonInf + + EILambda b e' -> killNonInf (VLam $ \y -> eval e' $ unpackVB y b env) -- the cases above also need to be handled by normal `eval` - EFree x -> VNeutral $ Neutral x mempty - EITyLambda b e' -> VPi (eval (bdtyp b) env) $ \y -> eval e' $ unpackVB y b env - ERefOf (ExprInf _ e) -> VRefOf $ evalInf e env - ERefOfTy e -> VRefOfTy $ eval e env + EFree x -> Right. VNeutral $ Neutral x mempty + EITyLambda b e' -> fmap (\res -> VPi res $ \y -> eval e' $ unpackVB y b env) $ eval (bdtyp b) env + ERefOf (ExprInf _ e) -> fmap VRefOf $ evalInf e env + ERefOfTy e -> fmap VRefOfTy $ eval e env instance Eval ExprInf where eval (ExprInf _ kind) env = case kind of - EBound b -> List.genericIndex env b + EBound b -> case binderLookup env b of + Nothing -> Left . VEOutOfRange $ b + Just y -> Right y EAnnot e _ -> eval e env - EApply e e' -> vapp (eval e env) (eval e' env) - EILambda b e' -> VLam $ \y -> eval e' $ unpackVB y b env - _ -> VInf $ evalInf kind env + EApply e e' -> do + v <- eval e env + v' <- eval e' env + vapp v v' + EILambda b e' -> Right . VLam $ \y -> eval e' $ unpackVB y b env + _ -> fmap VInf $ evalInf kind env subst i r (ExprInf info kind) = case kind of EBound b -> if i == b then r else (ExprInf info $ EBound b) @@ -160,34 +190,42 @@ instance Eval ExprInf where instance Eval ExprChk where eval (ExprChk xs' inf) env = case xs' of [] -> eval inf env - x:xs -> VLam $ \y -> eval (ExprChk xs inf) $ unpackVP y x env + x:xs -> Right . VLam $ \y -> eval (ExprChk xs inf) $ unpackVP y x env subst i r (ExprChk xs inf) = ExprChk xs $ subst (i + (fromInteger . toInteger $ length xs)) r inf valQuote :: Natural -> Value valQuote i = VInf . VNeutral $ Neutral (Quote i) mempty -quoteInf :: Natural -> ValueInf -> ExprInf () -quoteInf i (VPi v f) = ExprInf () $ EITyLambda (anonBind $ quote i v) (quote (i + 1) (f $ valQuote i)) +quoteInf :: Natural -> ValueInf -> Either ValueError (ExprInf ()) +quoteInf i (VPi v f) = do + fr <- f $ valQuote i + bdty' <- quote i v + frq <- quote (i + 1) fr + pure $ ExprInf () $ EITyLambda (anonBind bdty') frq where anonBind ty = Binder { bdpat = PatNameAnon, bdtyp = ty } -quoteInf i (VRefOf v) = ExprInf () $ ERefOf $ quoteInf i v -quoteInf i (VRefOfTy v) = ExprInf () $ ERefOfTy $ quote i v +quoteInf i (VRefOf v) = fmap ((ExprInf ()) . ERefOf) $ quoteInf i v +quoteInf i (VRefOfTy v) = fmap ((ExprInf ()) . ERefOfTy) $ quote i v quoteInf i (VNeutral n) = nQuote i n where - nQuote :: Natural -> Neutral -> ExprInf () - nQuote i' (Neutral root dq) = ExprInf () $ case Deq.unsnoc dq of + nQuote :: Natural -> Neutral -> Either ValueError (ExprInf ()) + nQuote i' (Neutral root dq) = fmap (ExprInf ()) $ case Deq.unsnoc dq of Nothing -> case root of - Quote k -> EBound $ i' - k - 1 - x' -> EFree x' - Just (v, dq2) -> EApply (nQuote i' $ Neutral root dq2) (quote i' v) + Quote k -> Right . EBound $ i' - k - 1 + x' -> Right $ EFree x' + Just (v, dq2) -> do + lam <- nQuote i' $ Neutral root dq2 + arg <- quote i' v + pure $ EApply lam arg -quote :: Natural -> Value -> ExprChk () +quote :: Natural -> Value -> Either ValueError (ExprChk ()) -quote i (VLam f) = - let (ExprChk binders f2) = quote (i + 1) (f $ valQuote i) - in ExprChk (PatNameAnon : binders) f2 +quote i (VLam f) = do + faq <- f $ valQuote i + (ExprChk binders f2) <- quote (i + 1) faq + pure $ ExprChk (PatNameAnon : binders) f2 -quote i (VInf x) = ExprChk [] $ quoteInf i x +quote i (VInf x) = fmap (ExprChk []) $ quoteInf i x diff --git a/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Typeck.hs b/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Typeck.hs index 1132ae7..ac3b9a9 100644 --- a/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Typeck.hs +++ b/haskell/nfker7h/lib/Language/Yanais/Nfker7h/Typeck.hs @@ -25,26 +25,28 @@ type Type = Value data TypeError = TETypesNotEq (ExprChk ()) (ExprChk ()) | TENotOfType (ExprChk ()) Type - | TEOutOfRange Natural | TENotFound NeutralRoot | TEIllegalApply Value + | TEValueError ValueError type TyckMonad a = ReaderT TyckEnv (Either TypeError) a -binderLookup :: TyckEnv -> Natural -> Maybe Value -binderLookup env = foldr ffun (const Nothing) (binders env) - where - ffun x _ 0 = Just x - ffun _ r k = r (k-1) - binderLookup' :: Natural -> TyckMonad Value -binderLookup' n = ReaderT $ \env -> case binderLookup env n of - Nothing -> Left $ TEOutOfRange n +binderLookup' n = ReaderT $ \env -> case binderLookup (binders env) n of + Nothing -> Left . TEValueError $ VEOutOfRange n Just x -> Right x litToVal :: Literal -> Value litToVal l = VInf . VNeutral $ Neutral (NrLiteral l) mempty +liftValueEval :: Either ValueError v -> TyckMonad v +liftValueEval res = ReaderT $ \_ -> case res of + Left err -> Left $ TEValueError err + Right x -> Right x + +eval' :: Eval a => a b -> [Value] -> TyckMonad Value +eval' x env = liftValueEval $ eval x env + typeChkIsTy :: ExprChk () -> TyckMonad () typeChkIsTy e = typeChk e $ litToVal $ LPrimTy PtType @@ -68,35 +70,45 @@ typeInf (ExprInf _ kind) = case kind of EAnnot e ety -> do typeChkIsTy ety -- what if the term depends on the env ??? - let tau = eval ety [] + tau <- eval' ety [] typeChk e tau return tau EApply e e' -> typeInf e >>= \sigm -> case sigm of - VInf (VPi tau tau') -> typeChk e' tau >> return (tau' $ eval e' []) + VInf (VPi tau tau') -> do + typeChk e' tau + eres <- eval' e' [] + liftValueEval $ tau' eres _ -> throwError $ TEIllegalApply sigm -- this is not correct, but I don't know how to do it correctly... -- we would need a way to replace a value in a value... - EILambda b e' -> typeChkBinder b (\bty -> fmap (\res -> VInf $ VPi bty (\_ -> res)) $ typeInf e') + EILambda b e' -> typeChkBinder b (\bty -> fmap (\res -> VInf $ VPi bty (\_ -> Right res)) $ typeInf e') EITyLambda b e' -> typeChkBinder b (\_ -> typeChkIsTy e') >> (pure . litToVal $ LPrimTy PtType) -- this is nasty - ERefOf e -> fmap (VInf . VRefOf . killNonInf) (typeInf e) + ERefOf e -> do + ety <- typeInf e + ety' <- liftValueEval $ killNonInf ety + pure . VInf . VRefOf $ ety' + ERefOfTy e -> fmap (VInf . VRefOfTy) (typeChkIsTy e >> (pure . litToVal $ LPrimTy PtType)) typeChk :: ExprChk () -> Type -> TyckMonad () typeChk (ExprChk [] inf) v = do v' <- typeInf inf - let q = quote 0 v - let q' = quote 0 v' + q <- liftValueEval $ quote 0 v + q' <- liftValueEval $ quote 0 v' if (q == q') then pure () else throwError $ TETypesNotEq q q' -typeChk (ExprChk (b:xs) inf) (VInf (VPi tau tau')) = - let inner = (asks $ binderCount) >>= \len -> typeChk (ExprChk xs inf) (tau' $ VInf . VNeutral $ Neutral (Local len) mempty) - in typeChkPattern b tau inner +typeChk (ExprChk (b:xs) inf) (VInf (VPi tau tau')) = typeChkPattern b tau inner + where + inner = do + len <- asks binderCount + tauev <- liftValueEval $ tau' $ VInf . VNeutral $ Neutral (Local len) mempty + typeChk (ExprChk xs inf) tauev typeChk a b = throwError $ TENotOfType a b @@ -106,7 +118,7 @@ typeChkBinder b inner = do let bdt = bdtyp b typeChkIsTy bdt -- what if the term depends on the env ??? - let bdt' = eval bdt [] + bdt' <- liftValueEval $ eval bdt [] typeChkPattern (bdpat b) bdt' (inner bdt') typeChkPattern :: Pattern Void -> Type -> TyckMonad a -> TyckMonad a