Permalink
Browse files

fix for longstanding problem involving occur check being too pessimis…

…tic in combi with complex predicated types
  • Loading branch information...
1 parent acdf32b commit 029e8c3963bce5c6cf4512c85e6a493ed53f597f @atzedijkstra atzedijkstra committed Sep 16, 2012
View
@@ -215,7 +215,7 @@ www: $(WWW_DOC_FILES)
www/DoneSyncStamp: www
(date "+%G%m%d %H:%M") > www/DoneSyncStamp ; \
chmod 664 www/* ; \
- rsync --progress -azv -e ssh www/* `whoami`@shell.cs.uu.nl:/users/www/groups/ST/Projects/ehc
+ rsync --progress -azv -e ssh www/* dijks106@csstaff.science.uu.nl:/users/www/groups/ST/Projects/ehc
www-sync: www/DoneSyncStamp
@@ -66,7 +66,7 @@ SEM AGItf
%%[(9 hmtyinfer)
SEM Expr
- | Let loc . finTyVarMp = varUpd @tmpoTyVarMp $
+ | Let loc . finTyVarMp = -- varUpd @tmpoTyVarMp $
@lhs.finTyVarMp
%%]
View
@@ -131,7 +131,7 @@ SEM Expr
. (quValGam_qu_,quTyVarMp, (cycTyVarMp_l,tqoGam))
:= @doValGamQuantify True @tyVarMpDeclsQuant @toQuantOverPrOccL
. tmpoTyVarMp = foldr (\tmpo c -> tmpoImplsVarMp tmpo `varUpd` c) emptyVarMp (gamElts @tqoGam)
- . bodyVarMp2 := @chrSolve1SimpTyVarMp `varUpd` (@exTyVarMp2 :: VarMp) `varUpd` @bodyVarMp1
+ . bodyVarMp2 := @tmpoTyVarMp `varUpd` @chrSolve1SimpTyVarMp `varUpd` (@exTyVarMp2 :: VarMp) `varUpd` @bodyVarMp1
%%]
decls . patTyVarMp := foVarMp @foKnRes `varUpd` @exTyVarMp1b -- @forExprTyVarMp `varUpd` @exTyVarMp1b
@@ -309,7 +309,7 @@ SEM TyExpr
%%[(3 hmtyinfer)
SEM Expr
- | Let loc . info_3 := [ -- mkInfo1 "valGam_l_ (+ decls.tyVarMp)" (ppGam $ @tyVarMpDeclsL0 `varUpd` @valGam_l_)
+ | Let loc . info_3 := [ mkInfo1 "cycTyVarMp_l" (ppVarMpV @cycTyVarMp_l)
]
| TypeAs loc . info_3 := [ mkInfo1 "knTy+lhs.tyVarMp" (ppTy (@lhs.tyVarMp `varUpd` @lhs.knTy))
, mkInfo1 "lhs.tyVarMp" (ppVarMpV @lhs.tyVarMp)
@@ -888,6 +888,7 @@ SEM Decl
SEM AGItf
| AGItf loc . info_9 := [ mkInfo1 "chrSolveSimpTyVarMp" (pp @chrSolveSimpTyVarMp)
+ , mkInfo1 "finTyVarMp" (pp @finTyVarMp)
]
++ mkInfo1Dbg @lhs.opts "chrStore" (ppCHRStore @chrStore)
%%]
@@ -943,6 +944,7 @@ SEM Expr
, mkInfo1 "toQuantOverPrOccL (decl)" (ppBracketsCommasV @toQuantOverPrOccL)
, mkInfo1 "quantCnstrMp" (ppAssocLV $ assocLMapElt ppBracketsCommas $ Map.toList @quantCnstrMp)
, mkInfo1 "tqoGam" (ppGam @tqoGam)
+ -- , mkInfo1 "quTyVarMp" (pp @quTyVarMp)
, mkInfo1 "tmpoTyVarMp" (pp @tmpoTyVarMp)
, mkInfo1 "chrSolve1RedGraph" (pp $ show @chrSolve1RedGraph)
, mkInfo1 "chrSimplifyResult1 redgraphs" (ppAssocLV $ assocLMapElt show $ simpresRedGraphs @chrSimplifyResult1)
View
@@ -152,6 +152,18 @@ type LabelVarId = UID
%%]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% Lookup types
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%[(2 hmtyinfer) hs export(LookupTy)
+type LookupTy = TyVarId -> Maybe Ty
+%%]
+
+%%[(9 hmtyinfer) hs export(LookupImpls)
+type LookupImpls = ImplsVarId -> Maybe Impls
+%%]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Misc types
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1048,18 +1060,18 @@ tyString o = appCon (ehcOptBuiltin o ehbnPrelString)
Substitution aware variants
%%[(9 hmtyinfer || hmtyast) hs export(tyArrowArgResWithLkup)
-tyArrowArgResWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (Ty,Ty)
+tyArrowArgResWithLkup :: LookupTy -> Ty -> (Ty,Ty)
tyArrowArgResWithLkup lookup = tyVarChkVisitLift lookup appUn1Arr appUn1Arr
%%]
%%[(9 hmtyinfer || hmtyast) hs export(tyArrowImplsResWithLkup,tyArrowImplsArgResWithLkup)
-tyArrowImplsArgResWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (TyL,Ty,Ty)
+tyArrowImplsArgResWithLkup :: LookupTy -> Ty -> (TyL,Ty,Ty)
tyArrowImplsArgResWithLkup lookup t
= (i,a,r)
where (i,t') = tyArrowImplsResWithLkup lookup t
(a,r) = tyArrowArgResWithLkup lookup t'
-tyMbArrowImplsResWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Maybe (TyL,Ty)
+tyMbArrowImplsResWithLkup :: LookupTy -> Ty -> Maybe (TyL,Ty)
tyMbArrowImplsResWithLkup lookup t
= extr t
where extr t = case appMb1Arr t of
@@ -1075,7 +1087,7 @@ tyMbArrowImplsResWithLkup lookup t
isImpls _ = False
_ -> tyVarLift lookup extr (const Nothing) t
-tyArrowImplsResWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (TyL,Ty)
+tyArrowImplsResWithLkup :: LookupTy -> Ty -> (TyL,Ty)
tyArrowImplsResWithLkup lookup t = maybe ([],t) id $ tyMbArrowImplsResWithLkup lookup t
%%]
@@ -1098,7 +1110,7 @@ tyLHdAndTl :: [Ty] -> (Ty,TyL)
%%[(6 hmtyinfer || hmtyast) hs export(tyAppFunArgsWithLkup)
-- Substitution aware
-tyAppFunArgsWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (Ty,TyL)
+tyAppFunArgsWithLkup :: LookupTy -> Ty -> (Ty,TyL)
tyAppFunArgsWithLkup lookup = tyVarChkVisitLift lookup appUnApp appUnApp
{-# INLINE tyAppFunArgsWithLkup #-}
%%]
@@ -1137,7 +1149,7 @@ tyConNm = maybe hsnUnknown id . tyMbCon
%%]
%%[(7 hmtyinfer || hmtyast) hs export(tyMbConWithLkup)
-tyMbConWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Maybe HsName
+tyMbConWithLkup :: LookupTy -> Ty -> Maybe HsName
tyMbConWithLkup lookup = tyVarChkVisitLift lookup tyMbCon tyMbCon
{-# INLINE tyMbConWithLkup #-}
%%]
@@ -1269,13 +1281,13 @@ mkTyRecExt recd al
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%[(6 hmtyinfer || hmtyast) hs
-tyVarChkVisitLift :: (TyVarId -> Maybe Ty) -> (Ty -> x) -> (Ty -> x) -> Ty -> x
+tyVarChkVisitLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarChkVisitLift
= withLkupChkVisitLift tyMbVar (noVisit . tyUnAnn)
where noVisit (Ty_TBind _ qv _ _) = Set.singleton qv
noVisit _ = Set.empty
-tyVarLift :: (TyVarId -> Maybe Ty) -> (Ty -> x) -> (Ty -> x) -> Ty -> x
+tyVarLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarLift = withLkupLift tyMbVar
{-# INLINE tyVarLift #-}
%%]
@@ -1293,24 +1305,24 @@ implsTailVarLiftCyc = withLkupLiftCyc1 implsMbVar (const Set.empty)
Substitution aware variants
%%[(7 hmtyinfer || hmtyast) hs export(tyRowExtsWithLkup,tyRecExtrWithLkup,tyRecExtsWithLkup)
-tyRowExtsWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (Ty,AssocL HsName Ty)
+tyRowExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRowExtsWithLkup lookup
= extr []
where extr as t
= case tyUnAnn t of
(Ty_Ext r l e) -> extr ((l,e):as) r
t' -> tyVarLift lookup (extr as) (flip (,) as) t'
-tyRecExtsWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> (Ty,AssocL HsName Ty)
+tyRecExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRecExtsWithLkup lookup t
= case tyRecRowWithLkup lookup t of
Ty_Any -> (Ty_Any,[])
row -> tyRowExtsWithLkup lookup row
-tyRecRowWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Ty
+tyRecRowWithLkup :: LookupTy -> Ty -> Ty
tyRecRowWithLkup lookup = maybe Ty_Any id . tyMbRecRowWithLkup lookup
-tyRowExtrWithLkup :: (TyVarId -> Maybe Ty) -> HsName -> Ty -> Maybe (Ty,Ty)
+tyRowExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRowExtrWithLkup lookup lbl t
= extr t
where extr t
@@ -1319,13 +1331,13 @@ tyRowExtrWithLkup lookup lbl t
| otherwise -> maybe Nothing (\(r',e') -> Just (Ty_Ext r' l e,e')) (extr r)
t' -> tyVarLift lookup extr (const Nothing) t'
-tyRecExtrWithLkup :: (TyVarId -> Maybe Ty) -> HsName -> Ty -> Maybe (Ty,Ty)
+tyRecExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRecExtrWithLkup lookup lbl t
= case tyRowExtrWithLkup lookup lbl (tyRecRowWithLkup lookup t) of
Nothing -> Nothing
Just (r,e) -> Just (hsnRec `appConApp` [r],e)
-tyMbRecRowWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Maybe Ty
+tyMbRecRowWithLkup :: LookupTy -> Ty -> Maybe Ty
tyMbRecRowWithLkup lookup t
= case tyAppFunArgsWithLkup lookup t of
(f,[row])
@@ -1458,7 +1470,7 @@ tyRecOffset lbl t
Substitution aware
%%[(8 hmtyinfer || hmtyast) hs export(tyRecOffsetWithLkup)
-tyRecOffsetWithLkup :: (TyVarId -> Maybe Ty) -> HsName -> Ty -> Int
+tyRecOffsetWithLkup :: LookupTy -> HsName -> Ty -> Int
tyRecOffsetWithLkup lookup nm
= tyVarLift lookup o o
where o = tyRecOffset nm
@@ -1589,7 +1601,7 @@ implsPredsTailWithLkup lookup sc i
= (map fst is,t)
where (is,t) = implsPredsTailWithLkup' lookup sc i
-tyImplsWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Impls
+tyImplsWithLkup :: LookupTy -> Ty -> Impls
tyImplsWithLkup lookup = tyVarLift lookup tyImpls tyImpls
{-# INLINE tyImplsWithLkup #-}
@@ -1599,6 +1611,11 @@ implsPrIdLWithLkup lookup = map poPoi . fst . implsPredsTailWithLkup lookup init
%%]
+%%[(9 hmtyinfer || hmtyast) hs export()
+tyMbVarWithLkup :: LookupTy -> Ty -> Maybe TyVarId
+tyMbVarWithLkup lookup = tyVarLift lookup tyMbVar tyMbVar
+%%]
+
%%[(9 hmtyinfer || hmtyast) hs export(tyImpls,implsPredsTail,implsPredsMbTail,implsIsTail,tyIsImplsTail,tyImplsPreds,implsPrIdPredL,implsPrIdL)
tyMbImpls :: Ty -> Maybe Impls
tyMbImpls
@@ -1643,6 +1660,28 @@ implsPrIdL = map fst . implsPrIdPredL
{-# INLINE implsPrIdL #-}
%%]
+%%[(9 hmtyinfer || hmtyast) hs export(tyMb1ArrTailVar2VarWithLkup)
+-- | Is an 'Impls' the tail (last empty element) of a sequence?
+implsMbTailVarWithLkup :: LookupImpls -> Impls -> Maybe ImplsVarId
+implsMbTailVarWithLkup lkup (Impls_Tail iv _) = maybe (Just iv) (const Nothing) (lkup iv)
+implsMbTailVarWithLkup _ _ = Nothing
+{-# INLINE implsMbTailVarWithLkup #-}
+
+-- | Is a 'Ty' the tail of an Impls?
+tyMbTailVarWithLkup :: LookupImpls -> Ty -> Maybe ImplsVarId
+tyMbTailVarWithLkup lkup t = do { i <- tyMbImpls t ; implsMbTailVarWithLkup lkup i }
+{-# INLINE tyMbTailVarWithLkup #-}
+
+-- | Is 'Ty' a function type from an Impls tail to ...
+tyMb1ArrTailVarWithLkup :: LookupImpls -> Ty -> Maybe (ImplsVarId,Ty)
+tyMb1ArrTailVarWithLkup lkup t = do { (a,r) <- appMb1Arr t; i <- tyMbTailVarWithLkup lkup a; return (i,r) }
+{-# INLINE tyMb1ArrTailVarWithLkup #-}
+
+-- | Is 'Ty' a function type from an Impls tail to a ty var
+tyMb1ArrTailVar2VarWithLkup :: LookupTy -> LookupImpls -> Ty -> Maybe (ImplsVarId,TyVarId)
+tyMb1ArrTailVar2VarWithLkup lkupt lkupi t = do { (i,r) <- tyMb1ArrTailVarWithLkup lkupi t; v <- tyMbVarWithLkup lkupt r; return (i,v) }
+%%]
+
%%[(9 hmtyinfer || hmtyast) hs export(implsMbVar,implsTailVar)
implsMbVar :: Impls -> Maybe TyVarId
implsMbVar (Impls_Tail v _) = Just v
@@ -1671,7 +1710,7 @@ tyIsPredicated t = isPr a
isPr (Ty_Pred p:_) = True
isPr _ = False
-tyIsPredicatedWithLkup :: (TyVarId -> Maybe Ty) -> Ty -> Bool
+tyIsPredicatedWithLkup :: LookupTy -> Ty -> Bool
tyIsPredicatedWithLkup lookup = tyVarLift lookup tyIsPredicated tyIsPredicated
{-# INLINE tyIsPredicatedWithLkup #-}
%%]
View
@@ -1114,33 +1114,17 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
| lBefR && fiAllowTyVarBind fi t1 = Just $ bind fi True v1 (updTy t2)
| not lBefR && fiAllowTyVarBind fi t2 = Just $ bind fi False v2 (updTy t1)
where lBefR = fioBindLBeforeR (fiFIOpts fi)
- {-
- varBind1 fi updTy t1@(Ty_Var v1 f1) t2
- | isJust mbNoise = case fromJust mbNoise of
- (Ty_Var v2 f2) | v1 == v2 && f1 == f2 -> Just $ res fi t1
- where mbNoise = tyUnNoiseForVarBind t2
- varBind1 fi updTy t1 t2@(Ty_Var v2 f2)
- | isJust mbNoise = case fromJust mbNoise of
- (Ty_Var v1 f1) | v1 == v2 && f1 == f2 -> Just $ res fi t2
- where mbNoise = tyUnNoiseForVarBind t1
- -}
varBind1 _ _ _ _ = Nothing
-- | tvar binding part 2: 1 of 2 tvars, impredicatively
varBind2 fi updTy t1@(Ty_Var v1 _) t2
+ | isJust m && v1 == v2 = Just $ res (fiBindImplsVar iv2 Impls_Nil fi) (updTy t1)
| allowImpredTVBindL fi t1 t2 = Just $ occurBind fi True v1 (updTy t2)
+ where m@(~(Just (iv2,v2))) = tyMb1ArrTailVar2VarWithLkup (fiLookupTyVarCyc fi) (lookupImplsVarCyc fi) t2
varBind2 fi updTy t1 t2@(Ty_Var v2 _)
+ | isJust m && v1 == v2 = Just $ res (fiBindImplsVar iv1 Impls_Nil fi) (updTy t2)
| allowImpredTVBindR fi t2 t1 = Just $ occurBind fi False v2 (updTy t1)
- {-
- varBind2 fi updTy t1@(Ty_Var v1 f1) t2
- | isJust mbNoise = case fromJust mbNoise of
- (Ty_Var v2 f2) | v1 == v2 && f1 == f2 -> Just $ res fi t1
- where mbNoise = tyUnNoiseForVarBind t2
- varBind2 fi updTy t1 t2@(Ty_Var v2 f2)
- | isJust mbNoise = case fromJust mbNoise of
- (Ty_Var v1 f1) | v1 == v2 && f1 == f2 -> Just $ res fi t2
- where mbNoise = tyUnNoiseForVarBind t1
- -}
+ where m@(~(Just (iv1,v1))) = tyMb1ArrTailVar2VarWithLkup (fiLookupTyVarCyc fi) (lookupImplsVarCyc fi) t1
varBind2 _ _ _ _ = Nothing
-- | tvar binding part 3: 1 of 2 tvars, non impredicatively
@@ -1181,11 +1165,11 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
%%[(9 hmtyinfer)
fVarPred2 f fi tpr1 (Ty_Impls (Impls_Tail iv2 _))
- | isJust mbTl = f fi tpr1 (Ty_Impls (fromJust mbTl))
- where mbTl = lookupImplsVarCyc fi iv2
+ | isJust mbTl = f fi tpr1 (Ty_Impls tl2)
+ where mbTl@(~(Just tl2)) = lookupImplsVarCyc fi iv2
fVarPred2 f fi (Ty_Impls (Impls_Tail iv1 _)) tpr2
- | isJust mbTl = f fi (Ty_Impls (fromJust mbTl)) tpr2
- where mbTl = lookupImplsVarCyc fi iv1
+ | isJust mbTl = f fi (Ty_Impls tl1) tpr2
+ where mbTl@(~(Just tl1)) = lookupImplsVarCyc fi iv1
fVarPred2 f fi tpr1 tpr2
= f fi tpr1 tpr2
fVarPred1 f fi (Ty_Impls (Impls_Tail iv1 _))
@@ -1231,15 +1215,15 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
t2
| hsnIsArrow c1 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
= fromJust mbfp
- where mbfp = fVarPred1 fP fi tpr1
+ where mbfp = fVarPred1 fP fi tpr1
fP fi (Ty_Impls (Impls_Nil))
= Just (fVar' fTySyn fi updTy tr1 t2)
fP fi _ = Nothing
fBase fi updTy t1
t2@(Ty_App (Ty_App (Ty_Con c2) tpr2) tr2)
| hsnIsArrow c2 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
= fromJust mbfp
- where mbfp = fVarPred1 fP fi tpr2
+ where mbfp = fVarPred1 fP fi tpr2
fP fi (Ty_Impls (Impls_Nil))
= Just (fVar' fTySyn fi updTy t1 tr2)
fP fi _ = Nothing
@@ -1325,6 +1309,7 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
%%]
%%[(9 hmtyinfer)
+ -- tpr1 => tr1 `fit` tpr2 => tr2
fBase fi updTy t1@(Ty_App (Ty_App (Ty_Con c1) tpr1) tr1)
t2@(Ty_App (Ty_App (Ty_Con c2) tpr2) tr2)
| hsnIsArrow c1 && c1 == c2 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
@@ -1424,6 +1409,7 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
%%]
%%[(9 hmtyinfer)
+ -- t1 `fit` tpr2 => tr2
fBase fi updTy t1
t2@(Ty_App (Ty_App (Ty_Con c2) tpr2) tr2)
| hsnIsArrow c2 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
@@ -1508,6 +1494,7 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
%%]
%%[(9 hmtyinfer)
+ -- tpr1 => tr1 `fit` t2
fBase fi updTy t1@(Ty_App (Ty_App (Ty_Con c1) tpr1) tr1)
t2
| hsnIsArrow c1 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
@@ -1625,6 +1612,7 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
%%]
%%[(4 hmtyinfer).fitsIn.App
+ -- tf1 ta1 `fit` tf2 ta2
fBase fi updTy t1@(Ty_App tf1 ta1)
t2@(Ty_App tf2 ta2)
= manyFO [ ffo, afo
@@ -181,3 +181,8 @@ fiBindTyVar :: TyVarId -> Ty -> FIIn' gm -> FIIn' gm
fiBindTyVar v t = fiPlusVarMp (v `varmpTyUnit` t)
%%]
+%%[(9 hmtyinfer) export(fiBindImplsVar)
+fiBindImplsVar :: ImplsVarId -> Impls -> FIIn' gm -> FIIn' gm
+fiBindImplsVar v i = fiPlusVarMp (v `varmpImplsUnit` i)
+%%]
+
Oops, something went wrong.

0 comments on commit 029e8c3

Please sign in to comment.