Implement check of bidirectionalizability.
[darcs-mirror-sem_syn.git] / Main.hs
1 {-# OPTIONS -XFlexibleInstances #-}
2
3 module Main where
4
5 import Text.PrettyPrint
6 import Control.Monad.State
7 import Control.Monad.Error
8 import Data.List
9 import Data.Maybe (fromJust, isNothing, isJust)
10 import Debug.Trace 
11
12 import Data.Function (on)
13
14 import Data.Map (Map)
15 import qualified Data.Map as Map
16
17 import Data.Set (Set)
18 import qualified Data.Set as Set
19
20 import Data.Graph 
21
22 import Util 
23 import AST
24
25 import Parser
26 import Type
27 import Shapify
28 import CodeGen 
29
30 import SemSyn
31
32 import System.IO
33 import System.Environment
34 import System.IO.Unsafe
35
36 data OptionAction 
37     = NullaryAction (Config -> Config)
38     | UnaryAction   (String -> Config -> Config)
39
40 interpretAction (NullaryAction f) xs c 
41     = Just (xs, f c)
42 interpretAction (UnaryAction f) [] c 
43     = Nothing
44 interpretAction (UnaryAction f) (x:xs) c 
45     = Just (xs, f x c) 
46
47       
48 data Option 
49     = Option { optionString :: String, 
50                optionLongString :: Maybe String,
51                optionArgDescription :: Doc, 
52                optionDescription :: Doc, 
53                optionAction :: OptionAction }
54
55 instance Ppr Option where
56     ppr (Option s ls argdesc desc _) =
57         ppr s <> (case ls of 
58                     Just ls -> comma <+> ppr ls
59                     Nothing -> empty)
60               <+> argdesc  $$
61               nest 4 desc
62     pprList opts =
63         vcat $ (punctuate (text "\n") $ map ppr opts)
64         
65
66 options = 
67     [ Option "-f" (Just "--file") (text "FILENAME")
68              (text "Specify program's input file")
69              (UnaryAction (\x conf -> 
70                                conf { inputFile = Just x })),
71       Option "-s" (Just "--shapify") (empty)
72              (text "Convert terms with type \"T a\" to \"T Unit\".")
73              (NullaryAction (\conf -> conf {execMode = Shapify})),
74       Option "-n" (Just "--natify") empty
75              (text "Convert terms with \"List a\" to \"Nat\".")
76              (NullaryAction (\conf -> conf {execMode = ShapifyPlus})),
77       Option "-h"  (Just "--help") empty
78              (text "Show this help message.")
79              (NullaryAction (\conf -> conf {execMode = Help})),
80       Option "-H"  (Just "--haskell-code") empty
81              (text "(Obsolete) Return a Haskell source code of \"put\" function."
82               $$ text "This options implies \"-n\".")
83              (NullaryAction (\conf -> conf {outputMode = HaskellCode, execMode = ShapifyPlus})),
84       Option "-P"  (Just "--pseudo-code") empty
85              (text "(Obsolete) Return a pseudo code only after syntatic bidirectionalizatoin."
86               $$ text "Note that \"wrapping\" code for semantic bidirectionalization is not produced.")
87              (NullaryAction (\conf -> conf {outputMode = PseudoCode })),
88       Option "-F"  (Just "--forward-only") empty
89              (text"(Obsolete) Return a pseudo code without bidirecionalization.")
90              (NullaryAction (\conf -> conf {outputMode = ForwardCode })), 
91       Option "-U"  (Just "--without-type") empty 
92              (text"Pseudo code without type. This option affects the output of \"-P\" and \"-F\".")
93              (NullaryAction (\conf -> conf {isShowType = False})),
94       Option "-T"  (Just "--with-type") empty 
95              (text"Pseudo code with type. This option affects the output of \"-P\" and \"-F\".")
96              (NullaryAction (\conf -> conf {isShowType = True})),
97       Option "-no"  (Just "--no-bidrectionalization") empty
98              (text"No Bidirectionalization (transformation stops after pre-processing)")
99              (NullaryAction (\conf -> conf {b18nMode = NoB18n})),
100       Option "-syn" (Just "--syntactic") empty 
101              (text"Syntatic Bidirectionalization.")
102              (NullaryAction (\conf -> conf {b18nMode = SyntacticB18n, outputMode = OM_NotSpecified  })),
103       Option "-sem" (Just "--semantic") empty 
104              (text"Semantic Bidirectionalization.")
105              (NullaryAction (\conf -> conf {b18nMode = SemanticB18n, outputMode = OM_NotSpecified  })),
106       Option "-comb" (Just "--combined") empty
107              (text"Combined Bidirectionalization.")
108              (NullaryAction (\conf -> conf {b18nMode = CombinedB18n, outputMode = OM_NotSpecified })),
109       Option "-hs"   (Just "--haskell") empty
110              (text"Output Haskell-runnable code.")
111              (NullaryAction (\conf -> conf {isHaskellify = True}))
112 --       Option "-d" (Just "--debug-exec") empty
113 --              (text"Debug Execution (Do not use this option).")
114 --              (NullaryAction $ \conf -> conf {execMode = Debug})
115     ]
116
117       
118 matchOption optString options 
119     = foldr f Nothing options 
120     where f o r = 
121               if (optionString o == optString) 
122                  || (isJust (optionLongString o) 
123                      && (fromJust (optionLongString o) == optString)) then 
124                   Just o 
125               else
126                   r
127            
128 parseArgs :: [[Char]] -> Config -> Config 
129 parseArgs args conf = 
130     case args of 
131       ("-d":xs) -> 
132           parseArgs xs (conf { execMode = Debug })
133       ("--debug":xs) -> 
134           parseArgs xs (conf { execMode = Debug })
135       (x:xs) -> case matchOption x options of 
136                   Just o -> 
137                       case  interpretAction (optionAction o) xs conf of 
138                         Just (rest, c) -> 
139                             parseArgs rest c 
140                         Nothing ->
141                             error "Error: #Argument of option mismatch." 
142                   Nothing -> 
143                       case x of 
144                         '-':_ -> 
145                             error $ "Error: Unknown option " ++ show x 
146                         _ -> 
147                             if isNothing (inputFile conf) then 
148                                 parseArgs xs (conf { inputFile = Just x })
149                             else 
150                                 parseArgs xs conf
151       []     -> conf
152
153
154
155 -- parseArgs :: [[Char]] -> Config -> Config 
156 -- parseArgs args conf =
157 --     case args of 
158 --       ("-f":x:xs) ->
159 --           parseArgs xs (conf { inputFile = Just x })
160 --       ("-s":xs) ->
161 --           parseArgs xs (conf { execMode = Shapify })
162 --       ("-ss":xs) ->
163 --           parseArgs xs (conf { execMode = ShapifyPlus })
164 --       ("-h":xs) ->
165 --           parseArgs xs (conf { execMode = Help })
166 --       ("-H":xs) ->
167 --           parseArgs xs (conf { outputMode = HaskellCode, execMode = ShapifyPlus } )
168 --       ("-P":xs) ->
169 --           parseArgs xs (conf { outputMode = PseudoCode } )
170 --       ("-d":xs) ->
171 --           parseArgs xs (conf { execMode = Debug })
172 --       (x:xs) | isNothing (inputFile conf) ->
173 --           parseArgs xs (conf { inputFile = Just x })
174 --       (x:xs) ->
175 --           parseArgs xs conf
176 --       [] ->
177 --           conf
178
179
180 progName = unsafePerformIO getProgName
181
182 usage = show $ 
183     text "USAGE" $$
184     text "-----" $$
185          nest 4 (text $ progName ++ " (-n|-s) (-T|-U) (-P|-H|-F) [-f] [FILENAME]\n") $+$ 
186                   
187          text ("This program is a prototype implementation of the paper:\n") $$
188          nest 4 (sep [text "Janis Voigtlander, Zhenjiang Hu, Kazutaka Matsuda and Meng Wang:",
189                        text "Combining Syntactic and Semantic Bidirectionalization.",
190                        text "ICFP 2010.\n"])
191          $$
192          wrap 80 ( "Given a \"get\" function defined in a file specified by FILENAME,"
193                   ++ "the program returns \"put\" function by combining "
194                   ++ "semantic bidirectionalization (Janis Voiglander: POPL'09) "
195                   ++ "and syntatic bidirectionalization (Kazutaka Matsuda et al.: ICFP'07). A typical usage is \""++ progName ++ " -H FILENAME\", which correspondes to the paper.\n"
196                   ) $+$
197     text "OPTIONS" $$
198     text "-------" $$
199          ppr options
200     where
201       pprOptions ps = vcat $ concatMap 
202                       (\(a,b) -> [nest 4 a,nest 8 b]) ps 
203       wrap n s = wrap' n s [] 
204           where wrap' 0 (' ':s) buf = wrap' 0 s buf 
205                 wrap' 0 s buf  = (text (reverse buf)) $$ wrap' n s []
206                 wrap' m [] buf = (text (reverse buf))
207                 wrap' m (' ':s) buf  
208                     | m - lnextSpace s < 0 =
209                         text (reverse buf) $$ wrap' n s []
210                     | otherwise = 
211                         wrap' (m-1) s (' ':buf)
212                 wrap' m (c:s) buf | m > 0 =
213                     wrap' (m-1) s (c:buf)
214                 lnextSpace [] = 0
215                 lnextSpace (' ':_) = 0
216                 lnextSpace (c:s)   = 1 + lnextSpace s 
217
218 isNormalMode conf =
219     ( b18nMode conf == SemanticB18n ) 
220     || ( (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n)
221          && (execMode conf == Normal) )
222     
223
224 isShapifyMode conf = 
225     (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n)
226     && (execMode conf == Shapify)
227
228 isShapifyPlusMode conf =
229     (b18nMode conf == CombinedB18n) 
230     || ( (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n)
231          && (execMode conf == ShapifyPlus) )
232
233 main :: IO ()
234 main = do { args <- getArgs 
235           ; let conf = adjustConfig $ parseArgs args defaultConfig
236           ; case execMode conf of 
237               Help -> putStrLn usage 
238               _ -> 
239                   do { csterr <- case inputFile conf of
240                                    Nothing -> 
241                                        do cont <- getContents
242                                           return $ parseString cont
243                                    Just filename ->
244                                        parseFile filename
245                      ; case csterr of
246                          Left err -> hPutStrLn stderr (show err)
247                          Right cprog -> 
248                              case execMode conf of 
249 --                                Normal | (b18nMode conf == SyntacticB18n || b18nMode conf == NoB18n) -> 
250 --                                    print $
251 --                                          outputCode conf False (cprog) (typeInference cprog)
252 -- --                                Shapify -> print $
253 -- --                                    outputCode conf False (cprog) (shapify $ typeInference cprog)
254 -- --                                    -- putStrLn "Not Supported Now."
255 --                                ShapifyPlus -> 
256 --                                    print $
257 --                                          outputCode conf True  (cprog) (introNat $ shapify $ typeInference cprog)
258                                Debug ->
259                                    do { print $ ppr   $ cprog
260                                       -- ; print $ pprAM $ constructAutomaton (typeInference cprog) initTAMap
261                                       ; let (p1,p2,p3) = constructBwdFunction (typeInference cprog)
262                                       ; print $ ppr p1 $$ ppr p2 $$ ppr p3
263                                       ; print $ ppr $ constructTypeDecl p2 
264                                       ; print $ ppr $ generateCodeBwd (typeInference cprog, p1,p2,p3)
265                                       ; putStrLn ""
266                                       ; putStrLn $ "---- After \"Shapify\" ----" 
267                                       ; let cprog' = introNat $ shapify $ typeInference cprog 
268                                       -- ; print $ pprAM $ constructAutomaton cprog' initTAMap
269                                       ; print $ cprog'                                       
270                                       ; let (p1,p2,p3) = constructBwdFunction cprog' 
271                                       ; print $ ppr p1 $$ ppr p2 $$ ppr p3
272                                       ; putStrLn ""
273                                       }
274                                _ | isNormalMode conf ->
275                                      print $ outputCode conf False (cprog) (typeInference cprog)
276                                _ | isShapifyMode conf -> 
277                                      print $ outputCode conf False (cprog) (shapify $ typeInference cprog)
278                                _ | isShapifyPlusMode conf -> 
279                                      print $ outputCode conf True  (cprog) (introNat $ shapify $ typeInference cprog)
280                                _ ->
281                                    print $ outputCode conf True  (cprog) (introNat $ shapify $ typeInference cprog)
282                      }
283           }
284