Skip to content
Snippets Groups Projects
Commit a3dca196 authored by Artin Ghasivand's avatar Artin Ghasivand
Browse files

Small stuff

parent 595f7c99
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
typechecker/src/Tc/Gen/Match.hs
+ 9
− 9
View file @ a3dca196
......@@ -105,7 +105,7 @@ tcMatches gamma mchs (Check sigma) = do
throwError (ArityMisMatch $
pretty "Arity mismatch:" <+>
pprList (vsep . map pprMatch) mchs)
let (psis, rho) = splitStar arity sigma
let (psis, rho) = tcSplit arity sigma
mapM_ (\mch -> tcMatchCheck gamma mch psis rho) mchs
......@@ -151,22 +151,22 @@ tcMatchCheck gamma (MkMatch aps e) psis rho = do
* *
********************************************************************* -}
splitStar :: HasCallStack => Arity -> Sigma -> ([Psi], Rho)
splitStar n (QuantifiedS psi sg)
-- TODO: Rename
tcSplit :: HasCallStack => Arity -> Sigma -> ([Psi], Rho)
tcSplit n (QuantifiedS psi sg)
-- | Rule: Split-Vis
| isVisibleP psi
, n > 0
= first (psi :) (splitStar (n - 1) sg)
= first (psi :) (tcSplit (n - 1) sg)
-- | Rule: Split-Invis
| isInvisForallP psi
|| isFatArrowP psi
= first (psi :) (splitStar n sg)
| isInvisibleP psi
= first (psi :) (tcSplit n sg)
-- | Rule: Split-Empty
splitStar 0 (RhoSg rho) = ([], rho)
splitStar n sg = pprPanic "splitStar" (vsep [pretty n
tcSplit 0 (RhoSg rho) = ([], rho)
tcSplit n sg = pprPanic "tcSplit" (vsep [pretty n
,pretty $ show sg])
{- *********************************************************************
......
typechecker/src/Tc/Gen/Pat.hs
+ 95
− 90
View file @ a3dca196
......@@ -42,30 +42,20 @@ import Data.Bifunctor
tcPat :: Gamma -> SigmaEnv -> Pat -> ExpType -> Tc (Delta, [Q])
-- | Rule: Pat-Constraint
tcPat gamma sigs pat (Check sigma)
| FatArrowS q rho' <- sigma
tcPat gamma sigs pat (Check (FatArrowS q rho'))
= do emitSimple (mkCt CtGiven q)
(lcl', qs) <- tcPat gamma sigs pat (Check rho')
pure (lcl', q : qs)
-- | Rule: Pat-WildCardCheck
tcPat _ _ TWildCardT (Check _) = pure (emptyDelta, [])
-- | Rule: Pat-WildCardInfer
tcPat _ _ TWildCardT (Infer inferResult) = do
tau <- newTauMetaVar typeSigma
tau <- newMetaVarOfKindType
fillInferResult (tauToRho . metaTyVarT $ tau) inferResult
pure (emptyDelta, [])
-- | Rule: Pat-AsPat
tcPat gamma sigs (TAs x pat) expType = do
(dlt@(MkDelta { variables = vars }), qs) <- tcPat gamma sigs pat expType
when (x `elem` dom vars)
$ throwError (ScopingError $
pprVar x <+>
pretty "is being brought to scope more than once.")
sigma <- expTypeToSigma expType
pure (dlt { variables = (x, sigma) : vars }, qs)
tcPat gamma sigs (TVarT var) (Check sigma)
= case lookup var sigs of
......@@ -97,6 +87,94 @@ tcPat gamma sigs (TVarT var) (Infer inferResult)
traceTc "tcPat-Pat-VarInfer" (pprVarBinding (var,tauToSigma tau))
pure (emptyDelta { variables = [(var, tauToSigma tau)] }, [])
-- | Rule: Pat-ViewPat
tcPat gamma sigs (TArrow expr pat) expType = do
(_, rho') <- tcInfer (tcExpr gamma expr)
case splitArrowR rho' of
Just (sigma1, sigma2) -> do
sigma <- expTypeToSigma expType
traceTc "tcPat-Pat-ViewPat:" (pprSigma sigma)
flg <- deepSubFlag
tcSub gamma flg sigma sigma1
case expType of
Infer ir -> do rho <- sigmaToRhoTc sigma
fillInferResult rho ir
tcPat gamma sigs pat (Check sigma2)
Check _ -> tcPat gamma sigs pat (Check sigma2)
Nothing -> pprPanic "tcPat-Pat-ViewPat"
(pretty "Inferred the wrong type!" <+>
pprRho rho')
-- | Rule: Pat-AsPat
tcPat gamma sigs (TAs x pat) expType = do
(dlt@(MkDelta { variables = vars }), qs) <- tcPat gamma sigs pat expType
when (x `elem` dom vars)
$ throwError (ScopingError $
pprVar x <+>
pretty "is being brought to scope more than once.")
sigma <- expTypeToSigma expType
pure (dlt { variables = (x, sigma) : vars }, qs)
-- | Rule: Pat-Inst
tcPat gamma sigs pat@(TApp (HConLike _) _) expType
| Check (SpecifiedS (alpha, kappa) sigma) <- expType
= do tau <- newTauMetaVar kappa
tcPat gamma sigs pat (Check $ appTvSubstTau (mkSingSubst alpha (metaTyVarT tau)) sigma)
tcPat gamma sigs (TApp (HConLike cl) apats) expType = do
lookupRes <- lookupGammaTc gamma (GKP cl)
case lookupRes of
-- | Rule: Pat-ConCheck
-- | Rule: Pat-KPInfer
DataConRes dt@(MkDataConType { dctPsis = psis
, dctTyCon = tyCon
, dctArgs = taus }) ->
do traceTc "tcPat-Pat-{ConCheck, KPInfer}"
$ vsep [pretty "DataCon:" <+> pprConLike cl
,pretty "DataCon's type:" <+> pprDataConType dt
,pretty "APats:" <+> pprArgs apats]
mvs <- matchExpectedConTy expType tyCon taus -- See Note [matchExpectedConTy]
(psps, dlt, qs1, toSkolSubst) <- tcSkolAPats gamma psis apats
-- TODO: Refactor me
(omegaSk, gadtWanteds) <- tcSolve $ zip (map (tauToSigma . appTvSubstTau toSkolSubst) taus)
(map tauToSigma mvs)
traceTc "Delta returned by tcSkolAPats:" (pprDelta dlt)
qs1ts <- mapM (fmap (mkCt CtGiven) . sigmaToTauTc . appSkSubstSigma omegaSk) qs1
emitSimples $ gadtWanteds ++ qs1ts
(dlt', qs3) <- tcPatsCheck (modifyDelta (dlt <>) gamma)
(map (second (appSkSubstSigma omegaSk)) psps)
traceTc "Delta returned by tcPatsCheck:" (pprDelta dlt')
pure (dlt <> dlt', qs1 ++ qs3)
{- TODO: Instead of having matchExpectedConTy, pattern match like this.
DataconRes ..
case expType of
Infer ir -> newMetaVarOfKindType
Check _ -> blah blah -}
-- | Rule: Pat-SynCheck
PatSynRes _ (MkPatSynType { pstUnivs = univs
, pstReqs = reqs
, pstPsis = psis
, pstRes = res }) ->
pprPanic "tcPat-Pat-SynCheck" (pretty "Pattern synonyms are not supported yet")
-- TODO: Fix this. The skolemisation stuff might be out of order
-- do emitSimple $ mkNCEqCt CtWanted sg res
-- omega <- tcTyVarsToMus univs
-- let phi' = appOmega omega res
-- theta1 <- mguql gamma phi' sg
-- theta2 <- tcSubstFill $ fiv (appTheta theta1 phi')
-- (psps, dlt, qs1, subst1) <- tcSkolAPats gamma psis apats
-- let theta = theta2 <> theta1
-- subst = appTheta theta . appOmega (subst1 <> omega)
-- emitSimples $ map ( mkCt CtWanted . subst) reqs
-- emitSimples $ map (mkCt CtGiven) qs1
-- (dlt', qs2) <- tcPatsCheck (modifyDelta (dlt <>) gamma)
-- (map (second subst) psps)
-- emitSimples $ map (mkCt CtGiven) qs2
-- pure (dlt <> dlt', qs1 ++ qs2)
-- | Rule: Pat-SigCheck
tcPat gamma sigs (TAnnT p ty) (Check sigma) = do
psb <- patSigBindFlag
......@@ -118,86 +196,12 @@ tcPat gamma sigs (TAnnT p ty) (Infer inferResult) = do
fillInferResult rho inferResult
pure (modifyScopedTyVars (tvbs <>) lcl', qs)
tcPat gamma sigs pat@(TApp head apats) expType
-- | Rule: Pat-Inst
| HConLike _ <- head
, Check (SpecifiedS (alpha, kappa) sigma) <- expType
= do tau <- newTauMetaVar kappa
tcPat gamma sigs pat (Check $ appTvSubstTau (mkSingSubst alpha (metaTyVarT tau)) sigma)
| HConLike cl <- head
= do lookupRes <- lookupGammaTc gamma (GKP cl)
case lookupRes of
-- | Rule: Pat-ConCheck
-- | Rule: Pat-KPInfer
DataConRes dt@(MkDataConType { dctPsis = psis
, dctTyCon = tyCon
, dctArgs = taus }) ->
do traceTc "tcPat-Pat-{ConCheck,KPInfer}"
$ vsep [pretty "DataCon:" <+> pprConLike cl
,pretty "DataCon's type:" <+> pprDataConType dt
,pretty "APats:" <+> pprArgs apats]
mvs <- matchExpectedConTy expType tyCon taus -- See Note [matchExpectedConTy]
(psps, dlt, qs1, toSkolSubst) <- tcSkolAPats gamma psis apats
-- TODO: Refactor me
(omegaSk, gadtWanteds) <- tcSolve $ zip (map (tauToSigma . appTvSubstTau toSkolSubst) taus)
(map tauToSigma mvs)
traceTc "Delta returned by tcSkolAPats:" (pprDelta dlt)
qs1ts <- mapM (fmap (mkCt CtGiven) . sigmaToTauTc . appSkSubstSigma omegaSk) qs1
emitSimples $ gadtWanteds ++ qs1ts
(dlt', qs3) <- tcPatsCheck (modifyDelta (dlt <>) gamma)
(map (second (appSkSubstSigma omegaSk)) psps)
traceTc "Delta returned by tcPatsCheck:" (pprDelta dlt')
pure (dlt <> dlt', qs1 ++ qs3)
-- | Rule: Pat-SynCheck
PatSynRes _ (MkPatSynType { pstUnivs = univs
, pstReqs = reqs
, pstPsis = psis
, pstRes = res }) ->
pprPanic "tcPat - Pat-SynCheck" (pretty "Pattern synonyms are not support yet")
-- TODO: Fix this. The skolemisation stuff might be out of order
-- do emitSimple $ mkNCEqCt CtWanted sg res
-- omega <- tcTyVarsToMus univs
-- let phi' = appOmega omega res
-- theta1 <- mguql gamma phi' sg
-- theta2 <- tcSubstFill $ fiv (appTheta theta1 phi')
-- (psps, dlt, qs1, subst1) <- tcSkolAPats gamma psis apats
-- let theta = theta2 <> theta1
-- subst = appTheta theta . appOmega (subst1 <> omega)
-- emitSimples $ map ( mkCt CtWanted . subst) reqs
-- emitSimples $ map (mkCt CtGiven) qs1
-- (dlt', qs2) <- tcPatsCheck (modifyDelta (dlt <>) gamma)
-- (map (second subst) psps)
-- emitSimples $ map (mkCt CtGiven) qs2
-- pure (dlt <> dlt', qs1 ++ qs2)
| otherwise
= throwError (IllegalTermError $ pretty "tcPat:" <+> pprTerm (TApp head apats))
-- | Rule: Pat-ViewPat
tcPat gamma sigs (TArrow expr pat) expType = do
(_, rho') <- tcInfer (tcExpr gamma expr)
case splitArrowR rho' of
Just (sigma1, sigma2) -> do
sigma <- expTypeToSigma expType
traceTc "tcPat-Pat-ViewPat:" (pprSigma sigma)
flg <- deepSubFlag
tcSub gamma flg sigma sigma1
case expType of
Infer ir -> do rho <- sigmaToRhoTc sigma
fillInferResult rho ir
tcPat gamma sigs pat (Check sigma2)
Check _ -> tcPat gamma sigs pat (Check sigma2)
Nothing -> pprPanic "tcPat-Pat-ViewPat"
(pretty "Inferred the wrong type!" <+>
pprRho rho')
tcPat _ _ (TLit lit) expType = tcLit lit expType >> pure (emptyDelta,[])
tcPat _ _ (TLit lit) expType = tcLit lit expType >> pure (emptyDelta, [])
tcPat _ _ pat _ = throwError (IllegalTermError $ pprTerm pat)
-- TODO: This is not in a one-to-one relation with the rule.
-- TODO: Get rid of this
-- See Note [matchExpectedConTy]
matchExpectedConTy :: ExpType -> TyCon -> [Tau] -> Tc [Tau]
matchExpectedConTy (Check sg) tyCon taus = do
......@@ -224,6 +228,7 @@ tcPatsCheck :: Gamma -> [(Pat, Sigma)] -> Tc (Delta, [Q])
-- | Rule: PatsCheck-Base
tcPatsCheck _ [] = pure (emptyDelta, [])
-- TODO: Shouldn't we use the normal tcPat in here?
-- | Rule: PatsCheck-Induction
tcPatsCheck gamma ((p,sg) : psps) = do
(dlt1, qs1) <- tcPatStar gamma p (Check sg)
......
typechecker/src/Type.hs
+ 4
− 0
View file @ a3dca196
......@@ -97,6 +97,7 @@ module Type(
isSpecifiedP,
isRequiredP,
isVisibleP,
isInvisibleP,
forallQuantifieP,
appSkSubstTauPsi,
......@@ -577,6 +578,9 @@ isArrowP _ = False
isVisibleP :: Psi -> Bool
isVisibleP psi = isRequiredP psi || isArrowP psi
isInvisibleP :: Psi -> Bool
isInvisibleP psi = isFatArrowP psi || isInvisForallP psi
splitAppArrowT :: Tau -> Maybe (Tau, Tau)
splitAppArrowT (AppT t1 t2) = Just (t1, t2)
splitAppArrowT (ArrowT t1 t2) = Just (t1, t2)
......
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