Implement check of bidirectionalizability.
[darcs-mirror-sem_syn.git] / SemSyn.hs
index 3d412df..cd51c89 100644 (file)
--- a/SemSyn.hs
+++ b/SemSyn.hs
@@ -32,45 +32,128 @@ data Config
     = Config 
       { 
         inputFile   :: Maybe String, -- ^ Path to input file
-        execMode    :: ExecMode,
-        outputMode  :: OutputMode, 
+        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
-
-defaultConfig = Config { 
-                  inputFile   = Nothing, 
-                  execMode    = Normal, 
-                  outputMode  = PseudoCode,
-                  isShowType  = True  }
+data OutputMode = PseudoCode | HaskellCode | ForwardCode | OM_NotSpecified 
+    deriving (Eq, Read, Show)
 
+data B18nMode = SyntacticB18n | SemanticB18n | CombinedB18n | NoB18n 
+    deriving (Eq, Read, Show)
 
-outputCode :: Config -> Bool -> AST -> AST -> IO ()
-outputCode conf isShapify orig ast =
+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 outputMode conf of 
-         ForwardCode -> 
-             do print $ ppr (typeFilter ast)
-         PseudoCode  ->
-             do print $ ppr (constructTypeDecl p2)
-                print $ ppr orig $$  ppr (typeFilter p1) $$ ppr (typeFilter p2) $$ ppr (typeFilterT p3)
-         HaskellCode ->
-             do putStrLn $ "import Control.Monad"
-                putStrLn $ "import BUtil"
-                when isShapify $
-                     print $ vcat $ map genBwdDef 
-                               (let AST decls = typeInference orig
-                                in map (\(Decl f t _ _:_) -> (f,t)) $ 
-                                     groupBy isSameFunc decls)
-                print $ ppr (constructTypeDecl p2)
-                print $ ppr $ generateCodeBwd (orig,p1,p2,p3)
+    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 AST decls = typeInference orig 
+                   in map (\(Decl f t _ _:_) -> f) $ groupBy isSameFunc decls) ++
+             [ ppr $ generateCodeDet p1 ]             
+         CombinedB18n -> vcat $ 
+             [ text "import Control.Monad"
+             , text "import BUtil"
+             ] ++ (
+             if isShapify
+             then map genBwdDef $
+                     let AST decls = typeInference orig
+                     in map (\(Decl f t _ _:_) -> (f,t)) $ groupBy isSameFunc decls
+             else []                                     
+             ) ++
+             [ ppr (constructTypeDecl p2)
+             , ppr $ generateCodeBwd (orig,p1,p2,p3)
+             ]
+                             
+-- case outputMode conf of 
+--          ForwardCode ->
+--                   ppr (typeFilter ast)
+--          PseudoCode  -> vcat
+--                 [ ppr (constructTypeDecl p2)
+--                 , ppr orig $$ ppr (typeFilter p1) $$ ppr (typeFilter p2) $$ ppr (typeFilterT p3)
+--                 ]
+--          HaskellCode -> vcat $
+--                 [ text "import Control.Monad"
+--                 , text "import BUtil"
+--                 ] ++ (
+--                 if isShapify
+--                 then map genBwdDef $
+--                         let 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) =
+          ppr (Name fName) <> text "_B" $$
+              nest 4 (text "= bff Main." <> ppr (Name fName)) $$
+          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  ->
@@ -89,22 +172,52 @@ outputCode conf isShapify orig ast =
                 empty
                                   
 
+checkBidirectionalizability :: AST -> AST 
+checkBidirectionalizability ast = 
+    case (checkTreeless $ eraseType ast, checkAffine $ eraseType ast)  of 
+      (Nothing, Nothing) -> ast
+      (Just (e,d),Nothing)       -> error $ showTreelessError (e,d) 
+      (Nothing, Just (vs,d'))    -> error $ showAffineError   (vs,d')
+      (Just (e,d), Just (vs,d')) -> error $ showTreelessError (e,d) ++ "\n" ++ showAffineError (vs,d') 
+    where
+      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)
 
-checkTreeless :: AST -> Bool
-checkTreeless (AST decls) = all checkTreelessD decls
+-- Nothing    : treeless
+-- Just (e,d) : not treeless because of d 
+checkTreeless :: AST -> Maybe (Exp, Decl)
+checkTreeless (AST decls) = msum $ map checkTreelessD decls
     where
-      checkTreelessD (Decl _ _ _ e) = checkTreelessE e
-      checkTreelessE (EVar _ _ _)    = True
-      checkTreelessE (ECon _ _ _ es) = all checkTreelessE es
-      checkTreelessE (EFun _ _ _ es) = all isVariable es
-      isVariable (EVar _ _ _) = True
-      isVariable _            = False
-
-checkAffine :: AST -> Bool 
-checkAffine (AST decls) = all checkAffineD decls
+      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    : treeless
+-- Just (e,d) : not treeless because of d 
+checkAffine :: AST -> Maybe ([Name],Decl)
+checkAffine (AST decls) = msum $ map checkAffineD decls
     where
-      checkAffineD (Decl _ _ _ e) = checkAffineE e 
-      checkAffineE e = (varsE e == snub (varsE e))
+      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