Commit 1bf173b5 authored by Kai-Oliver Prott's avatar Kai-Oliver Prott
Browse files

Add MonadFail support in TypeCheck and desugaring

parent fd0f8c4b
......@@ -1283,7 +1283,9 @@ tcStmt _ ps mTy (StmtDecl spi ds) = do
(ps', ds') <- tcDecls ds
return ((ps `Set.union` ps', mTy), StmtDecl spi ds')
tcStmt p ps mTy st@(StmtBind spi t e) = do
(ps', ty) <- maybe freshMonadType (return . (,) emptyPredSet) mTy
failable <- checkFailableBind t
let freshMType = if failable then freshMonadFailType else freshMonadType
(ps', ty) <- maybe freshMType (return . (,) emptyPredSet) mTy
alpha <- freshTypeVar
(ps'', e') <-
tcArg p "statement" (ppStmt st) (ps `Set.union` ps') (applyType ty [alpha]) e
......@@ -1291,6 +1293,42 @@ tcStmt p ps mTy st@(StmtBind spi t e) = do
(ps''', t') <- tcPatternArg p "statement" (ppStmt st) ps'' alpha t
return ((ps''', Just ty), StmtBind spi t' e')
checkFailableBind :: Pattern a -> TCM Bool
checkFailableBind (ConstructorPattern _ _ idt ps ) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> or <$> mapM checkFailableBind ps -- or [] == False
[DataType _ _ cs]
| length cs == 1 -> or <$> mapM checkFailableBind ps
| otherwise -> return True
_ -> return True
checkFailableBind (InfixPattern _ _ p1 idt p2) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> (||) <$> checkFailableBind p1
<*> checkFailableBind p2
[DataType _ _ cs]
| length cs == 1 -> (||) <$> checkFailableBind p1
<*> checkFailableBind p2
| otherwise -> return True
_ -> return True
checkFailableBind (RecordPattern _ _ idt fs ) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> or <$> mapM (checkFailableBind . fieldContent) fs
[DataType _ _ cs]
| length cs == 1 -> or <$> mapM (checkFailableBind . fieldContent) fs
| otherwise -> return True
_ -> return True
where fieldContent (Field _ _ c) = c
checkFailableBind (TuplePattern _ ps ) =
or <$> mapM checkFailableBind ps
checkFailableBind (AsPattern _ _ p ) = checkFailableBind p
checkFailableBind (ParenPattern _ p ) = checkFailableBind p
checkFailableBind (LazyPattern _ _ ) = return False
checkFailableBind (VariablePattern _ _ _ ) = return False
checkFailableBind _ = return True
tcInfixOp :: InfixOp a -> TCM (PredSet, Type, InfixOp PredType)
tcInfixOp (InfixOp _ op) = do
m <- getModuleIdent
......@@ -1586,6 +1624,9 @@ freshFractionalType = freshPredType [qFractionalId]
freshMonadType :: TCM (PredSet, Type)
freshMonadType = freshPredType [qMonadId]
freshMonadFailType :: TCM (PredSet, Type)
freshMonadFailType = freshPredType [qMonadFailId]
freshConstrained :: [Type] -> TCM Type
freshConstrained = freshVar . TypeConstrained
......
......@@ -839,18 +839,56 @@ dsStmt (StmtExpr _ e1) e' =
return $ apply (prelBind_ (typeOf e1) (typeOf e')) [e1, e']
dsStmt (StmtBind _ t e1) e' = do
v <- freshVar "_#var" t
failable <- checkFailableBind t
let func = Lambda NoSpanInfo [uncurry (VariablePattern NoSpanInfo) v] $
Case NoSpanInfo Rigid (uncurry mkVar v)
[ caseAlt NoSpanInfo t e'
, caseAlt NoSpanInfo (uncurry (VariablePattern NoSpanInfo) v)
(failedPatternMatch $ typeOf e')
]
Case NoSpanInfo Rigid (uncurry mkVar v) $
caseAlt NoSpanInfo t e' :
if failable
then [caseAlt NoSpanInfo
(uncurry (VariablePattern NoSpanInfo) v)
(failedPatternMatch $ typeOf e')]
else []
return $ apply (prelBind (typeOf e1) (typeOf t) (typeOf e')) [e1, func]
where failedPatternMatch ty =
apply (prelFail ty)
[Literal NoSpanInfo predStringType $ String "Pattern match failed!"]
dsStmt (StmtDecl _ ds) e' = return $ Let NoSpanInfo ds e'
checkFailableBind :: Pattern a -> DsM Bool
checkFailableBind (ConstructorPattern _ _ idt ps ) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> or <$> mapM checkFailableBind ps -- or [] == False
[DataType _ _ cs]
| length cs == 1 -> or <$> mapM checkFailableBind ps
| otherwise -> return True
_ -> return True
checkFailableBind (InfixPattern _ _ p1 idt p2) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> (||) <$> checkFailableBind p1
<*> checkFailableBind p2
[DataType _ _ cs]
| length cs == 1 -> (||) <$> checkFailableBind p1
<*> checkFailableBind p2
| otherwise -> return True
_ -> return True
checkFailableBind (RecordPattern _ _ idt fs ) = do
tcEnv <- getTyConsEnv
case qualLookupTypeInfo idt tcEnv of
[RenamingType _ _ _ ] -> or <$> mapM (checkFailableBind . fieldContent) fs
[DataType _ _ cs]
| length cs == 1 -> or <$> mapM (checkFailableBind . fieldContent) fs
| otherwise -> return True
_ -> return True
where fieldContent (Field _ _ c) = c
checkFailableBind (TuplePattern _ ps ) =
or <$> mapM checkFailableBind ps
checkFailableBind (AsPattern _ _ p ) = checkFailableBind p
checkFailableBind (ParenPattern _ p ) = checkFailableBind p
checkFailableBind (LazyPattern _ _ ) = return False
checkFailableBind (VariablePattern _ _ _ ) = return False
checkFailableBind _ = return True
-- -----------------------------------------------------------------------------
-- Desugaring of List Comprehensions
-- -----------------------------------------------------------------------------
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment