e38219f3dd2f5711440478cbffa76ce3db530543cmaeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Logic/LGToJson.hs
e38219f3dd2f5711440478cbffa76ce3db530543cmaederDescription : export logic graph information as Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaederCopyright : (c) Christian Maeder DFKI GmbH 2013
e38219f3dd2f5711440478cbffa76ce3db530543cmaederLicense : GPLv2 or higher, see LICENSE.txt
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederMaintainer : Christian.Maeder@dfki.de
e38219f3dd2f5711440478cbffa76ce3db530543cmaederStability : provisional
e38219f3dd2f5711440478cbffa76ce3db530543cmaederPortability : non-portable (via imports)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederexport logic graph information as Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder-}
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaedermodule Logic.LGToJson where
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Logic.Comorphism
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Logic.Grothendieck
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Logic.Logic
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Logic.Prover
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Control.Monad
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport qualified Data.Map as Map
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Data.Maybe
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Common.Consistency
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Common.Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederusableProvers :: LogicGraph -> IO Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaederusableProvers lg = do
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ps <- mapM proversOfLogic . Map.elems $ logics lg
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder return $ mkJObj [("provers", mkJArr $ concat ps)]
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederproversOfLogic :: AnyLogic -> IO [Json]
e38219f3dd2f5711440478cbffa76ce3db530543cmaederproversOfLogic (Logic lid) = do
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder bps <- filterM (fmap isNothing . proverUsable) $ provers lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder return $ map (\ p ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder mkJObj [ mkNameJPair $ proverName p
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "logic" $ language_name lid ]) bps
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederlGToJson :: LogicGraph -> IO Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaederlGToJson lg = do
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder let cs = Map.elems $ comorphisms lg
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder groupC = Map.toList . Map.fromListWith (++)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ssubs = groupC
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder $ map (\ (Comorphism cid) -> (G_sublogics (sourceLogic cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder $ sourceSublogic cid, [language_name cid])) cs
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder tsubs = groupC
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder $ map (\ (Comorphism cid) -> (G_sublogics (targetLogic cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder $ targetSublogic cid, [language_name cid])) cs
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ls <- mapM logicToJson . Map.elems $ logics lg
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder return $ mkJObj [("logic_graph", mkJObj
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder [ ("logics", mkJArr ls)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("source_sublogics", mkJArr $ map (\ (a, ns) -> mkJObj
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder [ mkNameJPair $ show a
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("comorphisms", mkJArr $ map mkJStr ns)]) ssubs)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("target_sublogics", mkJArr $ map (\ (a, ns) -> mkJObj
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder [ mkNameJPair $ show a
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("comorphisms", mkJArr $ map mkJStr ns)]) tsubs)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("comorphisms", mkJArr $ map comorphismToJson cs)] )]
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederlogicToJson :: AnyLogic -> IO Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaederlogicToJson (Logic lid) = do
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder let ps = provers lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder cs1 = cons_checkers lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder cs2 = conservativityCheck lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ua b = ("usable", mkJBool $ isNothing b)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder bps <- mapM proverUsable ps
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder bcs1 <- mapM ccUsable cs1
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder bcs2 <- mapM checkerUsable cs2
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder return $ mkJObj
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder [ mkNameJPair $ language_name lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "Stability" . show $ stability lid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("has_basic_parser", mkJBool . not . Map.null $ parsersAndPrinters lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("has_basic_analysis", mkJBool . isJust $ basic_analysis lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("has_symbol_list_parser", mkJBool . isJust $ parse_symb_items lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("has_symbol_map_parser", mkJBool . isJust $ parse_symb_map_items lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("is_a_process_logic", mkJBool . isJust $ data_logic lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("description_lines", mkJArr . map mkJStr . lines $ description lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("serializations", mkJArr . map mkJStr
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder . filter (not . null) . Map.keys $ parsersAndPrinters lid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("provers", mkJArr $ zipWith (\ a b ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder mkJObj [mkNameJPair $ proverName a, ua b]) ps bps)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("consistency_checkers", mkJArr $ zipWith (\ a b ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder mkJObj [mkNameJPair $ ccName a, ua b]) cs1 bcs1)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("conservativity_checkers", mkJArr $ zipWith (\ a b ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder mkJObj [mkNameJPair $ checkerId a, ua b]) cs2 bcs2)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("sublogics", mkJArr . map (mkJStr . sublogicName) $ all_sublogics lid)]
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaedercomorphismToJson :: AnyComorphism -> Json
e38219f3dd2f5711440478cbffa76ce3db530543cmaedercomorphismToJson (Comorphism cid) = mkJObj
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder [ mkNameJPair $ language_name cid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "source" $ language_name (sourceLogic cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "target" $ language_name (targetLogic cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "sourceSublogic" . sublogicName $ sourceSublogic cid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , mkJPair "targetSublogic" . sublogicName $ targetSublogic cid
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("is_inclusion", mkJBool $ isInclusionComorphism cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("has_model_expansion", mkJBool $ has_model_expansion cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder , ("is_weakly_amalgamable", mkJBool $ is_weakly_amalgamable cid)
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ]