{-# OPTIONS -XFlexibleInstances #-} module SemSyn where import Text.PrettyPrint import Control.Monad.State import Control.Monad.Error import Data.List import Data.Maybe (fromJust, isNothing, isJust) import Debug.Trace import Data.Function (on) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import Data.Graph import Util import AST import Parser import Type import Shapify import CodeGen data Config = Config { inputFile :: Maybe String, -- ^ Path to input file execMode :: ExecMode, b18nMode :: B18nMode, outputMode :: OutputMode, -- ^ Obsolete isHaskellify :: Bool, isShowType :: Bool } deriving Show data ExecMode = Normal | Shapify | ShapifyPlus | Help | Debug deriving (Eq, Read, Show) data OutputMode = PseudoCode | HaskellCode | ForwardCode | OM_NotSpecified deriving (Eq, Read, Show) data B18nMode = SyntacticB18n | SemanticB18n | CombinedB18n | NoB18n deriving (Eq, Read, Show) defaultConfig = Config { inputFile = Nothing, execMode = Normal, b18nMode = CombinedB18n, outputMode = OM_NotSpecified, isHaskellify = False, isShowType = True } -- | Since some combination of the config options is useless, -- this function adjust some configuration to valid one. adjustConfig :: Config -> Config -- adjustConfig (conf@(Config {b18nMode = CombinedB18n})) = -- conf { isHaskellify = True, execMode = ShapifyPlus } -- adjustConfig (conf@(Config {b18nMode = SemanticB18n})) = -- conf { isHaskellify = True, execMode = Normal, outputMode = ForwardCode } -- adjustConfig (conf@(Config {b18nMode = SyntacticB18n})) = -- conf { execMode = Normal, outputMode = PseudoCode } adjustConfig (conf@(Config {outputMode = ForwardCode})) = conf { b18nMode = NoB18n } adjustConfig (conf@(Config {outputMode = HaskellCode})) | execMode conf /= Help = conf { execMode = ShapifyPlus, isHaskellify = True, b18nMode = CombinedB18n } adjustConfig (conf@(Config {outputMode = PseudoCode})) = conf { isHaskellify = False, b18nMode = SyntacticB18n } adjustConfig conf = conf outputCode :: Config -> Bool -> AST -> AST -> Doc outputCode conf_ isShapify orig ast = let (p1,p2,p3) = constructBwdFunction ast in case b18nMode conf of NoB18n -> if isHaskellify conf then ppr (generateCodeDet ast) else ppr (typeFilter ast) SyntacticB18n -> if isHaskellify conf then vcat [ text "import Control.Monad" , text "import BUtil" , ppr (constructTypeDecl p2) , ppr $ generateCodeBwd (orig, p1, p2, p3) ] else vcat [ ppr (constructTypeDecl p2) , space , ppr orig , space , ppr (typeFilter p1) , space , ppr (typeFilter p2) , space , ppr (typeFilterT p3) ] SemanticB18n -> vcat $ [ text "import Data.Bff" ] ++ [ text "import BUtil" ] ++ (map genBwdDefBff $ let Right (AST decls) = typeInference orig in map (\(Decl f t _ _:_) -> (f,t)) $ groupBy isSameFunc decls) ++ [ ppr $ generateCodeDet orig ] CombinedB18n -> vcat $ [ text "import Control.Monad" , text "import BUtil" ] ++ ( if isShapify then map genBwdDef $ let Right (AST decls) = typeInference orig in map (\(Decl f t _ _:_) -> (f,t)) $ groupBy isSameFunc decls else [] ) ++ [ ppr (constructTypeDecl p2) , ppr $ generateCodeBwd (orig,p1,p2,p3) ] where conf = adjustConfig conf_ typeFilter = if isShowType conf then id else eraseType typeFilterT = if isShowType conf then id else eraseTypeT genBwdDefBff (Name fName,(TFun is ts t)) = case (ts,t) of ([TCon (Name "List") [TVar i]],TCon (Name "List") [TVar j]) | i == j -> ppr (Name fName) <> text "_B s v" $$ nest 4 (text "= bff Main." <> ppr (Name fName) <+> text "s v") _ -> empty -- ppr (Name fName) <> text "_B_Eq" $$ -- nest 4 (text "= bff_Eq Main." <> ppr (Name fName)) $$ -- ppr (Name fName) <> text "_B_Ord" $$ -- nest 4 (text "= bff_Ord Main." <> ppr (Name fName)) genBwdDef (Name fName,(TFun is ts t)) = case (ts,t) of ([TCon (Name "List") [TVar i]],TCon (Name "List") [TVar j]) | i == j -> ppr (Name fName) <> text "_Bb bias s v" $$ nest 4 (text "= gen_put_bias bias Main." <> ppr (Name fName) <> text "(\\x y -> castError $ (" <> ppr (NBwd $ IName fName is) <> text " $! x) $! y) s v" ) $$ ppr (Name fName) <> text "_Bbd = withDefaultBias " <> ppr (Name fName) <> text "_Bb" $$ ppr (Name fName) <> text "_Bd = withDefault " <> ppr (Name fName) <> text "_B" $$ ppr (Name fName) <> text "_B s v = " <> ppr (Name fName) <> text "_Bb rear s v" _ -> empty isNormalMode conf = ( b18nMode conf == SemanticB18n ) || ( (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n) && (execMode conf == Normal) ) isShapifyMode conf = (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n) && (execMode conf == Shapify) isShapifyPlusMode conf = (b18nMode conf == CombinedB18n) || ( (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n) && (execMode conf == ShapifyPlus) ) renderCode :: Config -> AST -> Doc renderCode conf cprog | isNormalMode conf = outputCode conf False (cprog) $ either error id $ typeInference cprog | isShapifyMode conf = outputCode conf False (cprog) $ shapify $ either error id $ typeInference cprog | isShapifyPlusMode conf = outputCode conf True (cprog) $ introNat $ shapify $ either error id $ typeInference cprog | otherwise = outputCode conf True (cprog) $ introNat $ shapify $ either error id $ typeInference cprog checkBidirectionalizability :: AST -> Maybe String checkBidirectionalizability ast = if isEmpty msgs then Nothing else Just (show msgs) where msgs = either (text.showTypeError) (const empty) (typeInference ast) $$ maybe empty (text.showTreelessError) (checkTreeless $ eraseType ast) $$ maybe empty (text.showAffineError) (checkAffine $ eraseType ast) showTypeError err = show $ text "Error: program does not typecheck" $$ nest 4 (text err) showTreelessError (e,d) = show $ text "Error: program is not treeless due to expression" $$ nest 4 (ppr e) $$ text "in declaration" $$ nest 4 (ppr d) showAffineError (vs,d) = show $ text "Error: program is not affine due to variables" $$ nest 4 (ppr vs) $$ text "in declaration" $$ nest 4 (ppr d) -- msum [] = mzero -- msum (m:ms) = mplus m (msum ms) -- Nothing : treeless -- Just (e,d) : not treeless because of e in d checkTreeless :: AST -> Maybe (Exp, Decl) checkTreeless (AST decls) = msum $ map checkTreelessD decls where checkTreelessD (d@(Decl _ _ _ e)) = checkTreelessE d e checkTreelessE d (EVar _ _ _) = Nothing checkTreelessE d (ECon _ _ _ es) = msum $ map (checkTreelessE d) es checkTreelessE d (e@(EFun _ _ _ es)) | all isVariable es = Nothing | otherwise = Just (e,d) isVariable (EVar _ _ _) = True isVariable e = False -- Nothing : affine -- Just (vs,d) : not affine because of vs in d checkAffine :: AST -> Maybe ([Name],Decl) checkAffine (AST decls) = msum $ map checkAffineD decls where checkAffineD (d@(Decl _ _ _ e)) = checkAffineE d e checkAffineE d e | (sort (varsE e) == snub (varsE e)) = Nothing | otherwise = Just (sort (varsE e) \\ snub (varsE e),d) varsE (EVar _ _ v) = [v] varsE (ECon _ _ _ es) = concatMap varsE es varsE (EFun _ _ _ es) = concatMap varsE es type Automaton s = Map s [Deriv s] data Deriv s = DCon Name [s] | DEps s | DAny pprAM :: (Ppr a, Ppr t) => Map t [Deriv a] -> Doc pprAM am = vcat $ map pprDs $ Map.toList am where pprDs (i,ds) = ppr i $$ nest 4 (vcat $ map (\d -> text " -> " <> pprD d) ds) pprD (DAny) = text "_" pprD (DEps s) = ppr s pprD (DCon c ss) = ppr c <> parens (hcat $ punctuate comma (map ppr ss)) data AState = ASType Int | ASExp Int | ASFun Name deriving (Eq,Ord) instance Ppr AState where ppr (ASType i) = text $ "T" ++ show i ppr (ASExp x) = text $ "E" ++ show x ppr (ASFun n) = text $ "F" ++ show n instance Show AState where show = show . ppr initTAMap :: Type -> State Int (AState, Map AState [Deriv AState]) initTAMap s = constructTypeMap s where uniq = do { i <- get; put (i+1); return i } listType t = do { (st,m) <- constructTypeMap t ; i <- uniq ; let m1 = Map.insert (ASType i) [DCon (Name "Nil")[], DCon (Name "Cons") [ASType i, st]] m ; return (ASType i, m1) } natType = do { let m1 = Map.insert (ASType 0) [DCon (Name "Z") [], DCon (Name "S") [ASType 0]] (Map.empty) ; return (ASType 0, m1) } anyType = do { let m1 = Map.insert (ASType 1) [DAny] (Map.empty) ; return (ASType 1, m1) } constructTypeMap (TCon (Name "List") [t]) = listType t constructTypeMap (TCon (Name "Nat") []) = natType constructTypeMap (TVar i) = anyType constructTypeMap _ = anyType -- Not Supported testOverlap :: AST -> Doc testOverlap (AST decl) = let fDs = groupBy isSameFunc decl in evalState (do { docs <- mapM f fDs ; return $ vcat docs }) initCAConf where am = constructAutomaton (AST decl) initTAMap f (ds@(Decl g t ps e:es)) = do { b <- checkInjectivity am (AST decl) g ; let di = text "Injectivity: " <> text (show $ b) ; ba <- checkAmbiguity am (ASFun g) ; let da = text "Ambiguity: " <> text (show $ ba) ; dol <- pol ds ; return $ text (show g) $$ nest 4 (da $$ di $$ dol) } pol ds = let is = [ ASExp $ fromJust $ idofE e | (Decl f t ps e) <- ds ] ijs = [ (i,j) | vs <- [zip is [0..]], (i,x) <- vs, (j,y) <- vs ] in do { bs <- mapM (uncurry $ checkOverlapS am (Set.empty)) ijs ; let vs = map (map snd) $ groupBy ((==) `on` (fst.fst)) $ zip ijs bs ; return $ vcat ( map g vs )} where g bs = hcat ( map (\h -> if h then text "O" else text "-") bs) isNonErasing :: Decl -> Bool isNonErasing (Decl _ _ ps e) = null $ (snub $ concatMap varsP ps) \\ varsE e checkInjectivity :: Automaton AState -> AST -> Name -> State (CAConf AState) Bool checkInjectivity am (AST decl) f = checkInj (Set.empty) f where checkInj env f = do { inj <- getInjSet ; ninj <- getNonInjSet ; if Set.member f inj || Set.member f env then return True else if Set.member f ninj then return False else do { b1 <- checkAmbiguity am (ASFun f) ; when b1 (addNonInj f) ; let dsF = filter (\(Decl g _ _ _) -> g == f) decl ; let b2 = all isNonErasing dsF ; when (not b2) (addNonInj f ) ; let fs = concatMap calledFunctions dsF ; b3 <- mapM (checkInj (Set.insert f env)) fs ; when (not $ and b3) (addNonInj f) ; if (not b1) && b2 && and b3 then when (Set.null env) (addInj f) >> return True else return False } } testTupling :: AST -> TAST testTupling ast = evalState (do { cAst <- optimizedComplementation am ast ; tAst <- doTupling am ast cAst ; return tAst }) initCAConf where am = constructAutomaton ast initTAMap data TypeDecl = TypeDecl Name [Int] [ConDef] data ConDef = ConDef Name [Type] -- NB: First Order instance Ppr TypeDecl where ppr (TypeDecl c is cdefs) = text "data" <+> ppr c <+> hsep (map (\i -> text "t" <> ppr i) is) $$ nest 4 (ppr cdefs) pprList decls = vcat $ map ppr decls instance Ppr ConDef where ppr (ConDef n ts) = ppr n <+> hsep (map pprT ts) where pprT (TVar i) = ppr (TVar i) pprT t = parens (ppr t) pprList [] = empty pprList (c:cs) = text "=" <+> ppr c $$ f cs where f [] = empty f [c] = text "|" <+> ppr c f (c:cs) = text "|" <+> ppr c $$ f cs -- Extract Type Definition from the complement definition -- FIXME: More Smart Definition constructTypeDecl :: AST -> [ TypeDecl ] constructTypeDecl (AST cdecls) = [ TypeDecl (cmplName) vs condef ] where cmplName = Name "Cmpl" vs = snub $ concat $ evalState (mapM extractVarsT cdecls) (0,[]) extractVarsT (Decl _ _ _ e) = case e of (ECon _ _ c es) -> do { trav <- traversedList ; if c `elem` trav then return [] else do { addTraversed c ; let ws = [ w | (EVar _ _ w) <- es ] ; is <- mapM (\_ -> uniq) ws ; return $ is }} _ -> return [] uniq = do { (i,t) <- get; put (i+1,t); return i } traversedList = do { (i,t) <- get; return t } addTraversed t = do { (i,tt) <- get; put (i,t:tt) } condef = concat $ evalState (mapM mkConDef cdecls) (0,[]) mkConDef (Decl _ _ _ e) = case e of (ECon _ _ c es) -> do { trav <- traversedList ; if c `elem` trav then return [] else do { addTraversed c ; let ws = [ w | (EVar _ _ w) <- es ] ; let fs = [ TCon cmplName [ TVar i | i <- vs ] | (EFun _ _ _ _) <- es ] ; is <- mapM (\_ -> uniq) ws ; return $ [ ConDef c (map TVar is ++ fs) ] } } _ -> return [] constructBwdFunction :: AST -> (AST, AST, TAST) constructBwdFunction ast = evalState ( do { cmpl <- optimizedComplementation am ast ; tpl <- doTupling am ast cmpl ; let itpl = localInversion tpl ; let fs = functions ast ; bwds <- mapM constructBWD fs ; return $ (AST bwds, cmpl, itpl) }) initCAConf where am = constructAutomaton ast initTAMap functions (AST decls) = map (\(Decl f _ _ _:_) -> f) $ groupBy isSameFunc decls pS = PVar Nothing TUndet (Name "s") pV = PVar Nothing TUndet (Name "v") eS = EVar Nothing TUndet (Name "s") eV = EVar Nothing TUndet (Name "v") constructBWD f = do { b <- checkInjectivity am ast f ; if b then return $ Decl (NBwd f) FTUndet [pS,pV] (EFun Nothing TUndet (NInv f) [eV]) else return $ Decl (NBwd f) FTUndet [pS,pV] (EFun Nothing TUndet (NInv (NTuple f)) [eV, EFun Nothing TUndet (NCmpl f) [eS]]) } localInversion :: TAST -> TAST localInversion (TAST tdecls) = TAST $ map localInversionD tdecls localInversionD :: TDecl -> TDecl localInversionD (TDecl f ps es vdecls) = TDecl (NInv f) (map e2p es) (map p2e ps) (map linvVD vdecls) where e2p (EVar i t v) = PVar i t v e2p (ECon i t c es) = PCon i t c (map e2p es) p2e (PVar i t v) = EVar i t v p2e (PCon i t c ps) = ECon i t c (map p2e ps) linvVD (VDecl vs f us) = VDecl us (NInv f) vs -- doTupling :: AST -> AST -> TAST doTupling :: Automaton AState -> AST -> AST -> State (CAConf AState) TAST doTupling am (AST decls) (AST cdecls) = do { tdecls <- mapM tupleD $ zip decls cdecls ; return $ TAST tdecls } where fCalls (EFun _ _ f es) = [(f,es)] fCalls (ECon _ _ _ es) = concatMap fCalls es fCalls _ = [] convE mp (EFun i t f es) = case lookup (f,es) mp of Just v -> EVar i t v Nothing -> EFun i t f es -- never happens convE mp (EVar i t v ) = EVar i t v convE mp (ECon i t c es) = ECon i t c (map (convE mp) es) tupleD (Decl f _ ps e, Decl _ _ _ ce) = do { b <- checkInjectivity am (AST decls) f ; if b then return $ tupleDInj f ps e else return $ tupleDNInj f ps e ce } tupleDInj f ps e = TDecl f ps [convE vnMap e] wdecls -- keep function-name if injective where funCalls = fCalls e vnMap = zip funCalls [ NTupleV i | i <- [1..] ] wdecls = map (\((f,es),v) -> VDecl [v] f [u | (EVar _ _ u) <- es ]) vnMap tupleDNInj f ps e ce = TDecl (NTuple f) ps [convE vnMap e, convE cnMap ce] wdecls where funCalls = fCalls e ninjCalls = [ (f,es) | (NCmpl f, es) <- fCalls ce ] injCalls = funCalls \\ ninjCalls vnMap = zip funCalls [ NTupleV i | i <- [1..] ] cnMap = zip (map (\(f,es) -> (NCmpl f,es)) funCalls) [ NTupleVC i | i <- [1..] ] wdecls = map convW vnMap where convW ((f,es),v@(NTupleV i)) | (f,es) `elem` injCalls = VDecl [v] f [u | (EVar _ _ u) <- es ] | otherwise = VDecl [v,NTupleVC i] (NTuple f) [u | (EVar _ _ u) <- es ] calledFunctions (Decl _ _ _ e) = snub $ calledFunctionsE e calledFunctionsE (ECon _ _ _ es) = concatMap calledFunctionsE es calledFunctionsE (EFun _ _ f es) = f:concatMap calledFunctionsE es calledFunctionsE _ = [] testComplementation (AST decls) = evalState (optimizedComplementation am (AST decls)) initCAConf where am = constructAutomaton (AST decls) initTAMap optimizedComplementation am (AST decls) = do { cmpl <- complementation am (AST decls) ; cmpl' <- optimizeByRemove am cmpl ; cmpl'' <- optimizeByRename am cmpl' ; return $ cmpl'' } optimizeByRename am (AST cdecls) = do { let cfdeclss = groupBy isSameFunc cdecls ; cfdeclss' <- mapM optRename cfdeclss ; return $ AST $ concat cfdeclss' } where optRename cfdecls = do { let ids = [ (i,[ (v,t) | (EVar _ t v) <- es ],length es) | (Decl _ _ _ (ECon _ _ (NCConE i) es)) <- cfdecls ] ; idss <- grouping [] ids ; return $ map (doRename idss) cfdecls } -- grouping :: [[(Int,[(Name,Type)])]] -> [(Int,[(Name,Type)])] -> State (CAConf AState) [[(Int,[(Name,Type)])]] grouping gs [] = return gs grouping gs (i:ids) = do { gs' <- checkGroup i gs ; grouping gs' ids } -- checkGroup :: (Int,[(Name,Type)]) -> [[(Int,[(Name,Type)])]] -> State (CAConf AState) [[(Int,[(Name,Type)])]] checkGroup i [] = return $ [ [i] ] checkGroup i (g:gs) = do { b <- compatible i g ; if b then return $ (i:g):gs else do { gs' <- checkGroup i gs ; return $ g:gs' } } compatible i [] = return $ True compatible (i,vs,l) ((i',vs',l'):ls) = do { b <- checkOverlapS am Set.empty (ASExp i) (ASExp i') ; let b2 = (sort $ map snd vs) == (sort $ map snd vs') ; if (not b) && b2 && l == l' then compatible (i,vs,l) ls else return False } doRename idss (Decl f t ps (ECon ei et (NCConE i) es)) = Decl f t ps (ECon ei et (NCConU f j) es') where j = fix (\f n iss -> case iss of is:iss -> if i `elem` (map (\(a,_,_) -> a) is) then n else f (n+1) iss) 1 idss es' = sortBy (compare `on` typeofE) [ e | (e@(EVar _ _ _)) <- es ] ++ [ e | (e@(EFun _ _ _ _)) <- es ] doRename idss d = d optimizeByRemove am (AST cdecls) = do { let cfdeclss = groupBy isSameFunc cdecls ; cfdeclss' <- mapM optRem cfdeclss ; return $ AST $ concat cfdeclss' } where fromInj (Decl _ _ _ (ECon _ _ (NCConF _) _)) = True fromInj _ = False optRem cfdecls | fromInj (head cfdecls) = return cfdecls | otherwise = mapM (\(Decl f t ps e) -> do { e' <- tryRemove e; return $ Decl f t ps e'}) cfdecls where ids = [ i | (Decl _ _ _ (ECon _ _ (NCConE i) _)) <- cfdecls ] tryRemove (ex@(ECon ei et (NCConE i) [EFun ei' et' f es])) = do { b <- checkNonOverlapAll i ids ; if b then return $ EFun ei' et' f es else return $ ex } tryRemove ex = return ex checkNonOverlapAll i [] = return $ True checkNonOverlapAll i (j:jds) | i == j = checkNonOverlapAll i jds | otherwise = do { b <- checkOverlapS am (Set.empty) (ASExp i) (ASExp j) ; if b then return False else checkNonOverlapAll i jds } complementation am (ast@(AST decls)) = do { cdecls <- mapM (complementationD am ast) decls ; return $ AST cdecls } complementationD am ast (Decl f ftype ps e) = do { b <- checkInjectivity am ast f ; if b then return $ (Decl (NCmpl f) FTUndet ps (ECon Nothing TUndet cNameC [])) else do { let fs = fCalls e ; fs' <- filterNonInj fs ; let e' = cExp unusedVars fs' ; return $ (Decl (NCmpl f) FTUndet ps e') } } where unusedVars = snub $ (snub $ concatMap varsWithTP ps) \\ (snub $ varsWithTE e) varsWithTP (PVar _ t v) = [EVar Nothing t v] varsWithTP (PCon _ _ _ ps) = concatMap varsWithTP ps varsWithTE (EVar _ t v) = [EVar Nothing t v] varsWithTE (ECon _ _ _ es) = concatMap varsWithTE es varsWithTE (EFun _ _ _ es) = concatMap varsWithTE es fCalls (ECon _ _ _ es) = concatMap fCalls es fCalls (EFun _ _ f es) = (f,es):concatMap fCalls es fCalls _ = [] filterNonInj [] = return [] filterNonInj ((f,es):fs) = do { b <- checkInjectivity am ast f ; if b then filterNonInj fs else do { fs' <- filterNonInj fs ; return $ (f,es):fs' } } cNameC = NCConF f cName = NCConE (fromJust $ idofE e) cExp vs fs = ECon Nothing TUndet cName $ vs ++ (map (\(f,es) -> EFun Nothing TUndet (NCmpl f) es) fs) constructAutomaton :: AST -> (Type -> State Int (AState,Automaton AState)) -> Automaton AState constructAutomaton (AST decl) initTAMap = removeEps $ evalState (unionM $ map constructAMD decl) 2 where unionM [] = return $ Map.empty unionM (m:ms) = do { r1 <- unionM ms ; r2 <- m ; return $ Map.unionWith (++) r1 r2 } constructAMD (Decl f t ps e) = do { (st,m) <- constructAME e ; return $ Map.insertWith (++) (ASFun f) [DEps st] m } constructAME (ECon i t c es) = do { ims <- mapM constructAME es ; let (is,ms) = unzip ims ; let m = Map.unions ms ; let s = ASExp $ fromJust i ; return (s, Map.insertWith (++) s [DCon c is] m)} constructAME (EFun i t f es) = -- Assume Treeless let s = ASExp $ fromJust i in return (s, Map.insertWith (++) s [DEps $ ASFun f] (Map.empty)) constructAME (EVar i t x) = do { (st,m) <- initTAMap t ; let s = ASExp $ fromJust i ; return (s, Map.insertWith (++) s [DEps st] m) } allStates :: Ord s => Automaton s -> [s] allStates am = snub $ foldr (++) [] $ map (\(i,d) -> i:concatMap allStatesDerive d) $ Map.toList am allStatesDerive (DCon _ is) = is allStatesDerive (DAny) = [] allStatesDerive (DEps i) = [i] removeEps :: Automaton AState -> Automaton AState removeEps am = foldr (Map.unionWith (++)) Map.empty $ map f $ Map.toList am where f (i,ds) = Map.fromList [ (j,filter nonEpsD ds) | j <- reachableA i ] isEps (_,DEps _) = True isEps _ = False nonEpsD (DEps _) = False nonEpsD _ = True erules = filter isEps $ concatMap (\(i,ds) -> [(i,d)|d<-ds]) $ Map.toList am aStates = allStates am (graph,v2n,k2v) = graphFromEdges $ map (\(i,is) -> (i,i,is)) $ Map.toList $ Map.fromListWith (++) $ (map (\(i,DEps j) -> (j,[i])) erules ++ map (\i->(i,[i])) aStates) reachableA k = map (\(n,_,_) -> n) $ map v2n $ reachable graph (fromJust $ k2v k) type AmbSet s = Set s type UnAmbSet s = Set s type OLSet s = Set (s,s) type UnOLSet s = Set (s,s) type InjSet = Set Name type NonInjSet = Set Name type CAConf s = (AmbSet s, UnAmbSet s, OLSet s, UnOLSet s, InjSet, NonInjSet) initCAConf = (Set.empty,Set.empty,Set.empty,Set.empty,Set.empty,Set.empty) ambset (s,_,_,_,_,_) = s unambset (_,s,_,_,_,_) = s olset (_,_,s,_,_,_) = s unolset (_,_,_,s,_,_) = s injset (_,_,_,_,s,_) = s noninjset (_,_,_,_,_,s) = s getAmbSet :: Ord s => State (CAConf s) (AmbSet s) getAmbSet = get >>= (return . ambset) getUnAmbSet :: Ord s => State (CAConf s) (UnAmbSet s) getUnAmbSet = get >>= (return . unambset) getOLSet :: Ord s => State (CAConf s) (OLSet s) getOLSet = get >>= (return . olset) getUnOLSet :: Ord s => State (CAConf s) (UnOLSet s) getUnOLSet = get >>= (return . unolset) getInjSet :: State (CAConf s) InjSet getInjSet = get >>= (return . injset) getNonInjSet :: State (CAConf s) NonInjSet getNonInjSet = get >>= (return . noninjset) addAmb x = do { (a,ua,o,uo,inj,ninj) <- get; put (Set.insert x a,ua,o,uo,inj,ninj) } addUnAmb x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,Set.insert x ua,o,uo,inj,ninj) } addOL x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,Set.insert x o,uo,inj,ninj) } addUnOL x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,Set.insert x uo,inj,ninj) } addInj x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,Set.insert x inj,ninj) } addNonInj x = do { (a,ua,o,uo,inj,ninj) <- get; put (a,ua,o,uo,inj,Set.insert x ninj) } checkAmbiguity :: Ord s => Automaton s -> s -> State (CAConf s) Bool checkAmbiguity am s = do { amb <- getAmbSet ; unamb <- getUnAmbSet ; if (Set.member s amb) then return True else if (Set.member s unamb) then return False else do { b <- checkAmb am unamb s ; when (not b) (addUnAmb s) ; return b } } where distinctPairs ds = let vs = zip ds [0..] in [ (d1,d2) | (d1,i) <- vs, (d2,j) <- vs, i < j ] checkOL (d1,d2) = checkOverlap am (Set.empty) d1 d2 checkAmb am env s = let derives = fromJust $ Map.lookup s am dPairs = distinctPairs derives in do { rs <- mapM checkOL dPairs ; if or rs then addAmb s >> return True else do { let ss = [ s | d <- derives, s <- allStatesDerive d, not (Set.member s env) ] ; rs <- mapM (checkAmb am (Set.insert s env)) ss ; return $ or rs }} checkOverlap am env (DEps s1) (DEps s2) = checkOverlapS am env s1 s2 checkOverlap am env (DCon c1 s1) (DCon c2 s2) | c1 == c2 = do { rs <- mapM (uncurry (checkOverlapS am env)) $ zip s1 s2 ; return $ and rs } | otherwise = return False checkOverlap am env DAny _ = return True checkOverlap am env _ DAny = return True checkOverlap am env _ _ = return False checkOverlapS :: Ord s => Automaton s -> Set (s,s) -> s -> s -> State (CAConf s) Bool checkOverlapS am env s1 s2 | Set.member (s1,s2) env || Set.member (s2,s1) env = return False | otherwise = do { ol <- getOLSet ; uol <- getUnOLSet ; if Set.member (s1,s2) ol || Set.member (s2,s1) ol then return True else if Set.member (s1,s2) uol || Set.member (s2,s1) uol then return False else let derives1 = fromJust $ Map.lookup s1 am derives2 = fromJust $ Map.lookup s2 am comb = [ (d1,d2) | d1 <- derives1, d2 <- derives2 ] in do { rs <- mapM (uncurry $ checkOverlap am (Set.insert (s1,s2) env)) comb ; if all not rs then do { when (Set.null env) (addUnOL (s1,s2)) ; return False } else do { addOL (s1,s2) ; return True } }}