From 39d8d700c6bfa06e0e9760dabfdf0ad27fb4b46f Mon Sep 17 00:00:00 2001 From: lucques Date: Tue, 27 Jun 2017 17:05:42 +0100 Subject: [PATCH] =?UTF-8?q?Fixed=20the=20pattern-match-fail-bug=20discover?= =?UTF-8?q?ed=20by=20M.=20Pickering=20(https://github.com/mpickering)=20at?= =?UTF-8?q?=20https://github.com/cmcl/frankjnr/issues/11.=20The=20bug=20wa?= =?UTF-8?q?s=20an=20occurring=20pattern=20match=20failure=20in=20the=20com?= =?UTF-8?q?piler=20code,=20very=20likely=20caused=20by=20a=20violation=20o?= =?UTF-8?q?f=20an=20invariant.=20It=20turned=20out=20that=20implicit=20[?= =?UTF-8?q?=C2=A3]=20arguments=20were=20not=20considered=20correctly=20(fi?= =?UTF-8?q?xed=20now)=20which=20then=20must=20have=20violated=20this=20inv?= =?UTF-8?q?ariant.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Debug.hs | 6 + RefineSyntax.hs | 1 + RefineSyntaxConcretiseEps.hs | 234 +++++++++++++++------------- examples/actorMultiMailbox.fk | 2 +- tests/should-pass/r.patMatchFail.fk | 25 +++ 5 files changed, 159 insertions(+), 109 deletions(-) create mode 100644 tests/should-pass/r.patMatchFail.fk diff --git a/Debug.hs b/Debug.hs index c8ec6ac..601c5eb 100644 --- a/Debug.hs +++ b/Debug.hs @@ -74,6 +74,12 @@ logEndUnifyAb ab0 ab1 = ifDebugTypeCheckOnThen $ do ctx <- getContext traceM $ "ended unifying\n " ++ show (ppAb ab0) ++ "\nwith\n " ++ show (ppAb ab1) ++ "\nCurrent context:\n" ++ show (ppContext ctx) ++ "\n\n" +debug :: String -> a -> a +debug = trace + +debugM :: Applicative f => String -> f () +debugM = traceM + {- Syntax pretty printers -} (<+>) = (PP.<+>) diff --git a/RefineSyntax.hs b/RefineSyntax.hs index 17a18a7..f099e76 100644 --- a/RefineSyntax.hs +++ b/RefineSyntax.hs @@ -15,6 +15,7 @@ import Syntax import RefineSyntaxCommon import RefineSyntaxConcretiseEps import RefineSyntaxSubstitItfAliases +import Debug -- Main refinement function refine :: Prog Raw -> Either String (Prog Refined) diff --git a/RefineSyntaxConcretiseEps.hs b/RefineSyntaxConcretiseEps.hs index 4168604..d019e5f 100644 --- a/RefineSyntaxConcretiseEps.hs +++ b/RefineSyntaxConcretiseEps.hs @@ -12,8 +12,7 @@ import qualified Data.Map.Strict as M import qualified Data.Set as S import Syntax - -import Debug.Trace +import Debug -- Node container for the graph algorithm data Node = DtNode (DataT Raw) | ItfNode (Itf Raw) | ItfAlNode (ItfAlias Raw) @@ -39,53 +38,134 @@ data HasEps = HasEps | -- "Yes" with certainty -- explicitly have it, are added an additional [£] eff var. concretiseEps :: [DataT Raw] -> [Itf Raw] -> [ItfAlias Raw] -> ([DataT Raw], [Itf Raw], [ItfAlias Raw]) concretiseEps dts itfs itfAls = - let nodes = map DtNode dts ++ map ItfNode itfs ++ map ItfAlNode itfAls - posIds = map nodeId (decideGraph (nodes, [], [])) in + let posIds = map nodeId (decideGraph (nodes, [], [])) in (map (concretiseEpsInDataT posIds) dts, map (concretiseEpsInItf posIds) itfs, map (concretiseEpsInItfAl posIds) itfAls) - --- Given graph (undecided-nodes, positive-nodes, negative-nodes), decide --- subgraphs as long as there are unvisited nodes. Finally (base case), --- return positive nodes. -decideGraph :: ([Node], [Node], [Node]) -> [Node] -decideGraph ([], pos, _ ) = pos -decideGraph (x:xr, pos, neg) = decideGraph $ runIdentity $ execStateT (decideSubgraph x) (xr, pos, neg) - --- Given graph (passed as state, same as for decideGraph) and a starting --- node x (already excluded from the graph), visit the whole subgraph --- reachable from x and thereby decide each node. --- To avoid cycles, x must always be excluded from graph. --- Method: 1) Try to decide x on its own. Either: --- (1), (2) Already decided --- (3), (4) Decidable without dependencies --- 2) If x's decision is dependent on neighbours' ones, visit all --- and recursively decide them, too. Either: --- (5)(i) A neighbour y is decided pos. => x is pos. --- (5)(ii) All neighbours y are decided neg. => x is neg. -decideSubgraph :: Node -> State ([Node], [Node], [Node]) Bool -decideSubgraph x = do - (xs, pos, neg) <- get - if x `elem` pos then return True -- (1) - else if x `elem` neg then return False -- (2) - else case hasEpsNode x of - HasEps -> do put (xs, x:pos, neg) -- (3) - return True - HasEpsIfAny ids -> - let neighbours = filter ((`elem` ids) . nodeId) (xs ++ pos ++ neg) in - do dec <- foldl (\dec y -> do -- Exclude neighbour from graph - (xs', pos', neg') <- get - put (xs' \\ [y], pos', neg') - d <- dec - d' <- decideSubgraph y - -- Once pos. y found, result stays pos. - return $ d || d') - (return False) -- (4) (no neighbours) - neighbours - (xs', pos', neg') <- get - if dec then put (xs', x:pos', neg') -- (5)(i) - else put (xs', pos', x:neg') -- (5)(ii) - return dec + where + + nodes :: [Node] + nodes = map DtNode dts ++ map ItfNode itfs ++ map ItfAlNode itfAls + + ids :: [Id] + ids = map nodeId nodes + + -- Given graph (undecided-nodes, positive-nodes, negative-nodes), decide + -- subgraphs as long as there are unvisited nodes. Finally (base case), + -- return positive nodes. + decideGraph :: ([Node], [Node], [Node]) -> [Node] + decideGraph ([], pos, _ ) = pos + decideGraph (x:xr, pos, neg) = decideGraph $ runIdentity $ execStateT (decideSubgraph x) (xr, pos, neg) + + -- Given graph (passed as state, same as for decideGraph) and a starting + -- node x (already excluded from the graph), visit the whole subgraph + -- reachable from x and thereby decide each node. + -- To avoid cycles, x must always be excluded from graph. + -- Method: 1) Try to decide x on its own. Either: + -- (1), (2) Already decided + -- (3), (4) Decidable without dependencies + -- 2) If x's decision is dependent on neighbours' ones, visit all + -- and recursively decide them, too. Either: + -- (5)(i) A neighbour y is decided pos. => x is pos. + -- (5)(ii) All neighbours y are decided neg. => x is neg. + decideSubgraph :: Node -> State ([Node], [Node], [Node]) Bool + decideSubgraph x = do + (xs, pos, neg) <- get + if x `elem` pos then return True -- (1) + else if x `elem` neg then return False -- (2) + else case hasEpsNode x of + HasEps -> do put (xs, x:pos, neg) -- (3) + return True + HasEpsIfAny ids -> + let neighbours = filter ((`elem` ids) . nodeId) (xs ++ pos ++ neg) in + do dec <- foldl (\dec y -> do -- Exclude neighbour from graph + (xs', pos', neg') <- get + put (xs' \\ [y], pos', neg') + d <- dec + d' <- decideSubgraph y + -- Once pos. y found, result stays pos. + return $ d || d') + (return False) -- (4) (no neighbours) + neighbours + (xs', pos', neg') <- get + if dec then put (xs', x:pos', neg') -- (5)(i) + else put (xs', pos', x:neg') -- (5)(ii) + return dec + + {- hasEpsX functions examine an instance of X and determine whether it + 1) has an [£] for sure or + 2) has an [£] depending on other definitions + + The tvs parameter hold the locally introduced value type variables. It + serves the following purpose: If an identifier is encountered, we cannot be + sure if it was correctly determined as either data type or local type + variable. This is the exact same issue to deal with as in refineVType, + now in hasEpsVType -} + + hasEpsNode :: Node -> HasEps + hasEpsNode node = case node of (DtNode dt) -> hasEpsDataT dt + (ItfNode itf) -> hasEpsItf itf + (ItfAlNode itfAl) -> hasEpsItfAl itfAl + + hasEpsDataT :: DataT Raw -> HasEps + hasEpsDataT (MkDT _ ps ctrs) = if any ((==) ("£", ET)) ps then HasEps + else let tvs = [x | (x, VT) <- ps] in + anyHasEps (map (hasEpsCtr tvs) ctrs) + + hasEpsItf :: Itf Raw -> HasEps + hasEpsItf (MkItf _ ps cmds) = if any ((==) ("£", ET)) ps then HasEps + else let tvs = [x | (x, VT) <- ps] in + anyHasEps (map (hasEpsCmd tvs) cmds) + + hasEpsItfAl :: ItfAlias Raw -> HasEps + hasEpsItfAl (MkItfAlias _ ps itfMap) = if any ((==) ("£", ET)) ps then HasEps + else let tvs = [x | (x, VT) <- ps] in + hasEpsItfMap tvs itfMap + + hasEpsCmd :: [Id] -> Cmd Raw -> HasEps + hasEpsCmd tvs (MkCmd _ ps ts t) = let tvs' = tvs ++ [x | (x, VT) <- ps] in + anyHasEps $ map (hasEpsVType tvs') ts ++ [hasEpsVType tvs' t] + + hasEpsCtr :: [Id] -> Ctr Raw -> HasEps + hasEpsCtr tvs (MkCtr _ ts) = anyHasEps (map (hasEpsVType tvs) ts) + + hasEpsVType :: [Id] -> VType Raw -> HasEps + hasEpsVType tvs (MkDTTy x ts) = + if x `elem` ids then anyHasEps $ HasEpsIfAny [x] : map (hasEpsTyArg tvs) ts -- indeed data type + else anyHasEps $ map (hasEpsTyArg tvs) ts -- ... or not + hasEpsVType tvs (MkSCTy ty) = hasEpsCType tvs ty + hasEpsVType tvs (MkTVar x) = if x `elem` tvs then HasEpsIfAny [] -- indeed type variable + else HasEpsIfAny [x] -- ... or not + hasEpsVType tvs MkStringTy = HasEpsIfAny [] + hasEpsVType tvs MkIntTy = HasEpsIfAny [] + hasEpsVType tvs MkCharTy = HasEpsIfAny [] + + hasEpsCType :: [Id] -> CType Raw -> HasEps + hasEpsCType tvs (MkCType ports peg) = anyHasEps $ map (hasEpsPort tvs) ports ++ [hasEpsPeg tvs peg] + + hasEpsPort :: [Id] -> Port Raw -> HasEps + hasEpsPort tvs (MkPort adj ty) = anyHasEps [hasEpsAdj tvs adj, hasEpsVType tvs ty] + + hasEpsAdj :: [Id] -> Adj Raw -> HasEps + hasEpsAdj tvs (MkAdj itfmap) = hasEpsItfMap tvs itfmap + + hasEpsPeg :: [Id] -> Peg Raw -> HasEps + hasEpsPeg tvs (MkPeg ab ty) = anyHasEps [hasEpsAb tvs ab, hasEpsVType tvs ty] + + hasEpsAb :: [Id] -> Ab Raw -> HasEps + hasEpsAb tvs (MkAb v m) = anyHasEps [hasEpsAbMod tvs v, hasEpsItfMap tvs m] + + hasEpsItfMap :: [Id] -> ItfMap Raw -> HasEps + hasEpsItfMap tvs = anyHasEps . (map (hasEpsTyArg tvs)) . concat . M.elems + + hasEpsAbMod :: [Id] -> AbMod Raw -> HasEps + hasEpsAbMod tvs MkEmpAb = HasEpsIfAny [] + hasEpsAbMod tvs (MkAbVar "£") = HasEps + hasEpsAbMod tvs (MkAbVar _) = HasEpsIfAny [] + + hasEpsTyArg :: [Id] -> TyArg Raw -> HasEps + hasEpsTyArg tvs (VArg t) = hasEpsVType tvs t + hasEpsTyArg tvs (EArg ab) = hasEpsAb tvs ab concretiseEpsInDataT :: [Id] -> DataT Raw -> DataT Raw concretiseEpsInDataT posIds (MkDT dt ps ctrs) = (MkDT dt ps' ctrs) where @@ -99,68 +179,6 @@ concretiseEpsInItfAl :: [Id] -> ItfAlias Raw -> ItfAlias Raw concretiseEpsInItfAl posIds (MkItfAlias itfAl ps itfMap) = (MkItfAlias itfAl ps' itfMap) where ps' = if not (any ((==) ("£", ET)) ps) && itfAl `elem` posIds then ps ++ [("£", ET)] else ps -{- hasEpsX functions examine an instance of X and determine whether it - 1) has an [£] for sure or - 2) has an [£] depending on other definitions -} - -hasEpsNode :: Node -> HasEps -hasEpsNode (DtNode dt) = hasEpsDataT dt -hasEpsNode (ItfNode itf) = hasEpsItf itf -hasEpsNode (ItfAlNode itfAl) = hasEpsItfAl itfAl - -hasEpsDataT :: DataT Raw -> HasEps -hasEpsDataT (MkDT _ ps ctrs) = if any ((==) ("£", ET)) ps then HasEps - else anyHasEps (map hasEpsCtr ctrs) - -hasEpsItf :: Itf Raw -> HasEps -hasEpsItf (MkItf _ ps cmds) = if any ((==) ("£", ET)) ps then HasEps - else anyHasEps (map hasEpsCmd cmds) - -hasEpsItfAl :: ItfAlias Raw -> HasEps -hasEpsItfAl (MkItfAlias _ ps itfMap) = if any ((==) ("£", ET)) ps then HasEps - else hasEpsItfMap itfMap - -hasEpsCmd :: Cmd Raw -> HasEps -hasEpsCmd (MkCmd _ _ ts t) = anyHasEps $ map hasEpsVType ts ++ [hasEpsVType t] - -hasEpsCtr :: Ctr Raw -> HasEps -hasEpsCtr (MkCtr _ ts) = anyHasEps (map hasEpsVType ts) - -hasEpsVType :: VType Raw -> HasEps -hasEpsVType (MkDTTy _ ts) = anyHasEps (map hasEpsTyArg ts) -hasEpsVType (MkSCTy ty) = hasEpsCType ty -hasEpsVType (MkTVar _) = HasEpsIfAny [] -hasEpsVType MkStringTy = HasEpsIfAny [] -hasEpsVType MkIntTy = HasEpsIfAny [] -hasEpsVType MkCharTy = HasEpsIfAny [] - -hasEpsCType :: CType Raw -> HasEps -hasEpsCType (MkCType ports peg) = anyHasEps $ map hasEpsPort ports ++ [hasEpsPeg peg] - -hasEpsPort :: Port Raw -> HasEps -hasEpsPort (MkPort adj ty) = anyHasEps [hasEpsAdj adj, hasEpsVType ty] - -hasEpsAdj :: Adj Raw -> HasEps -hasEpsAdj (MkAdj itfmap) = hasEpsItfMap itfmap - -hasEpsPeg :: Peg Raw -> HasEps -hasEpsPeg (MkPeg ab ty) = anyHasEps [hasEpsAb ab, hasEpsVType ty] - -hasEpsAb :: Ab Raw -> HasEps -hasEpsAb (MkAb v m) = anyHasEps [hasEpsAbMod v, hasEpsItfMap m] - -hasEpsItfMap :: ItfMap Raw -> HasEps -hasEpsItfMap = anyHasEps . (map hasEpsTyArg) . concat . M.elems - -hasEpsAbMod :: AbMod Raw -> HasEps -hasEpsAbMod MkEmpAb = HasEpsIfAny [] -hasEpsAbMod (MkAbVar "£") = HasEps -hasEpsAbMod (MkAbVar _) = HasEpsIfAny [] - -hasEpsTyArg :: TyArg Raw -> HasEps -hasEpsTyArg (VArg t) = hasEpsVType t -hasEpsTyArg (EArg ab) = hasEpsAb ab - {- Helper functions -} nodeId :: Node -> Id diff --git a/examples/actorMultiMailbox.fk b/examples/actorMultiMailbox.fk index 70cd39a..1d5fb07 100644 --- a/examples/actorMultiMailbox.fk +++ b/examples/actorMultiMailbox.fk @@ -182,4 +182,4 @@ roundRobin unit = popProcs! main: {[Console, RefState]Unit} main! = let me = mbox (new (zipq [] [])) in - runZipQueue' (roundRobin (step me divConqActor!)) (zipq [] []); unit + runZipQueue {roundRobin (step me divConqActor!)} (zipq [] []); unit diff --git a/tests/should-pass/r.patMatchFail.fk b/tests/should-pass/r.patMatchFail.fk new file mode 100644 index 0000000..3232824 --- /dev/null +++ b/tests/should-pass/r.patMatchFail.fk @@ -0,0 +1,25 @@ +-- Regression for the fixed bug discovered by M. Pickering +-- (https://github.com/mpickering) at https://github.com/cmcl/frankjnr/issues/11. +-- The bug was an occurring pattern match failure in the compiler code, very +-- likely caused by a violation of an invariant. It turned out that implicit [£] +-- arguments were not considered correctly which then must have violated this +-- invariant. +-- #desc This checks the code which used to cause a 'pattern match fail' in the compiler code +-- #return unit + +--- start of standard stuff --- +on : {X -> {X -> Y} -> Y} +on x f = f x + +data S = S (List Card) + +data Card = Card { Unit } + +interface State = get : S | put : S -> Unit + +drawCardDeck : [State]Card +drawCardDeck! = + on get! { (S (cons top deck)) -> put (S deck); top } + +main : { [Console]Unit } +main! = unit