Skip to content

Commit

Permalink
Fixed the pattern-match-fail-bug discovered by M. Pickering (https://…
Browse files Browse the repository at this point in the history
…github.com/mpickering) at cmcl#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 (fixed now) which then must have violated this invariant.
  • Loading branch information
Lukas Convent committed Jun 27, 2017
1 parent 93f2559 commit 4101e28
Show file tree
Hide file tree
Showing 5 changed files with 159 additions and 109 deletions.
6 changes: 6 additions & 0 deletions Debug.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.<+>)
Expand Down
1 change: 1 addition & 0 deletions RefineSyntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ import Syntax
import RefineSyntaxCommon
import RefineSyntaxConcretiseEps
import RefineSyntaxSubstitItfAliases
import Debug

-- Main refinement function
refine :: Prog Raw -> Either String (Prog Refined)
Expand Down
234 changes: 126 additions & 108 deletions RefineSyntaxConcretiseEps.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion examples/actorMultiMailbox.fk
Original file line number Diff line number Diff line change
Expand Up @@ -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
25 changes: 25 additions & 0 deletions tests/should-pass/r.patMatchFail.fk
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 4101e28

Please sign in to comment.