diff --git a/osek-verification.cabal b/osek-verification.cabal index 0104064f7a645539c5d252611fdf099a707e0eaf..501121929cbc086fdffb61f900ec8bfe693cbdcd 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -25,6 +25,7 @@ library , Search.Types , Search.EpsilonElimination , Protocol + , Compare.JSON , Compare.Types , Compare.Matching hs-source-dirs: src diff --git a/src/Compare/JSON.hs b/src/Compare/JSON.hs new file mode 100644 index 0000000000000000000000000000000000000000..e2e0752d39f8d93cc98857e75015d81acb52859f --- /dev/null +++ b/src/Compare/JSON.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE OverloadedStrings #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +module Compare.JSON + ( Graph + , parseFile + ) where + +import Data.Aeson +import Data.Aeson.Types (typeMismatch) +import qualified Data.ByteString.Lazy as BS +import qualified Data.Graph.Inductive as G +import qualified Data.Map as M +import Data.Text (Text) + +import Data.Tuple + +import Compare.Types + +parseFile :: BS.ByteString -> Either String (Graph NodeLabel EdgeLabel) +parseFile = eitherDecode' + +type NodeLabel = Text +type EdgeLabel = Text + +newtype N = N { unN :: NodeLabel } +newtype E = E { unE :: (NodeLabel, NodeLabel, EdgeLabel) } + +instance FromJSON (Graph NodeLabel EdgeLabel) where + parseJSON (Object v) = mkGraph + <$> (map unN <$> v .: "nodes") + <*> (map unE <$> v .: "edges") + <*> v .: "entry" + parseJSON invalid = typeMismatch "Graph" invalid + +instance FromJSON N where + parseJSON (Object v) = N <$> v .: "id" + parseJSON invalid = typeMismatch "Node" invalid + +instance FromJSON E where + parseJSON (Object v) = + E <$> ((\a b c -> (a,b,c)) <$> v .: "from" <*> v .: "to" <*> v .: "label") + parseJSON invalid = typeMismatch "Edge" invalid + +mkGraph :: [NodeLabel] -> [(NodeLabel, NodeLabel, EdgeLabel)] -> NodeLabel -> Graph NodeLabel EdgeLabel +mkGraph nodes labels entry = + let + labNodes = zip [0..] nodes + nodeMap = M.fromList $ map swap labNodes + labEdges = map (\(from, to, label) -> (nodeMap M.! from, nodeMap M.! to, label)) labels + in + Graph (G.mkGraph labNodes labEdges) (nodeMap M.! entry)