anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-05 22:46:08 +03:00
Code Issues Projects Releases Wiki Activity

fix checking for constructors apps in patterns

Browse Source
This commit is contained in:
Jan Mas Rovira 2022-03-29 10:04:10 +02:00
parent 153ebe36a2
commit b685af034d
1 changed files with 34 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
View File

@ -103,6 +103,39 @@ unfoldFunType t = case t of
TypeIden {} -> ([], t) TypeIden {} -> ([], t)
TypeFunction (Function l r) -> first (l:) (unfoldFunType r) TypeFunction (Function l r) -> first (l:) (unfoldFunType r)
checkFunctionClause :: forall r. Members '[Reader InfoTable, Error Err] r =>
FunctionInfo -> FunctionClause -> Sem r FunctionClause
checkFunctionClause info FunctionClause{..} = do
let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
(patTys, restTys) = splitAt (length _clausePatterns) argTys
bodyTy = foldFunType restTys rty
when (length patTys /= length _clausePatterns) (throwErr "too many patterns")
locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
return FunctionClause {
_clauseBody = clauseBody',
..
}
checkPattern :: forall r. Members '[Reader InfoTable, Error Err] r =>
Type -> Pattern -> Sem r LocalVars
checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
where
go :: Type -> Pattern -> Sem r [(VarName, Type)]
go ty p = case p of
PatternWildcard -> return []
PatternVariable v -> return [(v, ty)]
PatternConstructorApp a -> do
info <- lookupConstructor (a ^. constrAppConstructor)
when (TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) /= ty) (throwErr "wrong type for constructor")
goConstr a
where
goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
goConstr (ConstructorApp c ps) = do
tys <- (^. constructorInfoArgs) <$> lookupConstructor c
when (length tys /= length ps) (throwErr "wrong number of arguments in constructor app")
concat <$> zipWithM go tys ps
throwErr :: Members '[Error Err] r => Err -> Sem r a throwErr :: Members '[Error Err] r => Err -> Sem r a
throwErr = throw throwErr = throw
@ -140,33 +173,3 @@ inferExpression' e = case e of
getFunctionType t = case t of getFunctionType t = case t of
TypeFunction f -> return f TypeFunction f -> return f
_ -> throwErr "expected function type" _ -> throwErr "expected function type"
checkFunctionClause :: forall r. Members '[Reader InfoTable, Error Err] r =>
FunctionInfo -> FunctionClause -> Sem r FunctionClause
checkFunctionClause info FunctionClause{..} = do
let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
(patTys, restTys) = splitAt (length _clausePatterns) argTys
bodyTy = foldFunType restTys rty
when (length patTys /= length _clausePatterns) (throwErr "wrong number of patterns")
locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
return FunctionClause {
_clauseBody = clauseBody',
..
}
checkPattern :: forall r. Members '[Reader InfoTable, Error Err] r =>
Type -> Pattern -> Sem r LocalVars
checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
where
go :: Type -> Pattern -> Sem r [(VarName, Type)]
go ty p = case p of
PatternWildcard -> return []
PatternVariable v -> return [(v, ty)]
PatternConstructorApp a -> goConstr a
where
goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
goConstr (ConstructorApp c ps) = do
tys <- (^. constructorInfoArgs) <$> lookupConstructor c
when (length tys /= length ps) (throwErr "wrong number of arguments in constructor app")
concat <$> zipWithM go tys ps