haskell: report value evaluation errors
This commit is contained in:
parent
312e9e2d79
commit
ec45a765d7
2 changed files with 110 additions and 60 deletions
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue