Initial import

Setup.hs

+import Distribution.Simple
+main = defaultMain

ma.cabal

+-- Initial ma.cabal generated by cabal init.  For further documentation,
+-- see http://haskell.org/cabal/users-guide/
+
+name:                ma
+version:             0.1.0.0
+-- synopsis:
+-- description:
+--license:             GPL-3
+--license-file:        LICENSE
+author:              Hans-Peter Deifel
+maintainer:          hans-peter.deifel@fau.de
+-- copyright:
+-- category:
+build-type:          Simple
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     Data.MorphismEncoding
+                     , Data.RefinementInterface
+                     , Data.Functors.Powerset
+                     , Data.Functors.FixedProduct
+                     , Parser
+                     , Data.Functors
+  default-language:    Haskell2010
+  build-depends:       base
+                     , vector
+                     , text
+                     , aeson
+                     , yaml
+                     , unordered-containers
+                     , bytestring
+
+executable ma
+  main-is:             Main.hs
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.10 && <4.11
+  hs-source-dirs:      src/main
+  default-language:    Haskell2010
+  build-depends:       ma
+                     , containers
+                     , text
+                     , vector
+                     , bytestring

src/Data/Functors.hs

+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Data.Functors where
+
+import           Control.Arrow ((&&&))
+
+import           Data.HashMap.Strict (HashMap)
+import qualified Data.HashMap.Strict as HM
+import           Data.Text (Text)
+
+import           Data.RefinementInterface
+import           Data.Functors.Powerset (powerset)
+import           Data.Functors.FixedProduct (fixedProduct)
+
+data SomeRefinementInterface where
+  SomeRefinementInterface :: RefinementInterface h => h -> SomeRefinementInterface
+
+registeredFunctors :: HashMap Text RefinableFunctor
+registeredFunctors = HM.fromList $ map (name &&& id)
+  [ powerset
+  , fixedProduct
+  ]

src/Data/Functors/FixedProduct.hs

+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Data.Functors.FixedProduct where
+
+import qualified Data.Yaml as Yaml
+import qualified Data.Vector as V
+import           Data.Vector (Vector)
+import qualified Data.Text as T
+import           Data.Text (Text)
+
+import           Data.RefinementInterface
+import qualified Data.MorphismEncoding as Encoding
+
+data FixedProduct = FixedProduct (Vector Text)
+  deriving (Show)
+
+data Three = One | Two | Three
+  deriving (Show)
+
+instance RefinementInterface FixedProduct where
+  type Label FixedProduct = ()
+  type Weight FixedProduct = Int
+  type H1 FixedProduct = Int
+  type H3 FixedProduct = (Int, Three)
+
+  parse (FixedProduct labels) = Yaml.withArray "Morphisms" $ \arr -> do
+    zipped <- V.imapM parseNode arr
+    let structure = V.map fst zipped
+        edges = V.map snd zipped
+
+    return (Encoding.new structure edges)
+
+    where
+      parseNode :: Int -> Yaml.Value -> Yaml.Parser ((H1 FixedProduct), (Int, Label FixedProduct, Int))
+      parseNode morphIdx = Yaml.withText "label" $ \txt ->
+        case V.elemIndex txt labels of
+          Nothing -> fail $ "Label" ++ T.unpack txt ++ " not defined"
+          Just labelIdx -> return (labelIdx, (morphIdx, (), morphIdx))
+
+fixedProduct :: RefinableFunctor
+fixedProduct = RefinableFunctor
+  { name = "FixedProduct"
+    -- FIXME Ensure that labels are unique
+  , parseArguments = ArgumentParser $ \val ->
+      (FixedProduct . V.fromList) <$> Yaml.parseJSON val
+  }

src/Data/Functors/Powerset.hs

+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
+
+module Data.Functors.Powerset where
+
+import           Data.Vector (Vector)
+import qualified Data.Vector as V
+import qualified Data.Yaml as Yaml
+
+import           Data.RefinementInterface
+import qualified Data.MorphismEncoding as Encoding
+
+data Powerset = Powerset
+  deriving (Show)
+
+instance RefinementInterface Powerset where
+  type Label Powerset = ()
+  type Weight Powerset = (Int, Int)
+  type H1 Powerset = Bool
+  type H3 Powerset = (Bool, Bool, Bool)
+
+  parse _ = Yaml.withArray "Morphisms" $ \arr -> do
+    succsessors <- V.imapM parseNode arr
+
+    let structure = V.map (not . V.null . snd) succsessors
+        edges = V.concatMap (\(from, succs) -> fmap (from,(),) succs) succsessors
+
+    return $ Encoding.new structure edges
+
+    where
+      parseNode :: Int -> Yaml.Value -> Yaml.Parser (Int, Vector Int)
+      parseNode nodeIdx value = (nodeIdx,) <$> Yaml.parseJSON value
+
+powerset :: RefinableFunctor
+powerset = RefinableFunctor
+  { name = "Powerset"
+  , parseArguments = NoArguments Powerset
+  }

src/Data/MorphismEncoding.hs

+module Data.MorphismEncoding
+  ( Encoding
+  , new
+  ) where
+
+import Data.Vector (Vector)
+
+data Encoding a h1 = Encoding
+  { structure :: Vector h1
+  , edges :: Vector (Int, a, Int)
+  }
+  deriving (Show)
+
+new :: Vector h1 -> Vector (Int, a, Int) -> Encoding a h1
+new = Encoding

src/Data/RefinementInterface.hs

+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+module Data.RefinementInterface where
+
+import Data.Text (Text)
+import Data.Yaml as Yaml
+
+import Data.MorphismEncoding
+
+data ArgumentParser h
+  = NoArguments h
+  | ArgumentParser (Yaml.Value -> Yaml.Parser h)
+
+data RefinableFunctor = forall h. RefinementInterface h => RefinableFunctor
+  { name :: Text
+  , parseArguments :: ArgumentParser h
+  }
+
+class (Show h, Show (Label h), Show (H1 h)) => RefinementInterface h where
+  type Label h :: *
+  type Weight h :: *
+  type H1 h :: *
+  type H3 h :: *
+
+  parse :: h -> Yaml.Value -> Yaml.Parser (Encoding (Label h) (H1 h))

src/Parser.hs

+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Parser where
+
+import           Control.Monad
+
+import qualified Data.Yaml as Yaml
+import           Data.Yaml ((.:))
+import           Data.Vector (Vector)
+import qualified Data.Vector as V
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.Text as T
+import           Data.ByteString (ByteString)
+
+import           Data.RefinementInterface
+import           Data.Functors (registeredFunctors)
+import           Data.MorphismEncoding
+
+
+data SomeRefinementInterface where
+  SRI :: RefinementInterface h => h -> SomeRefinementInterface
+
+deriving instance Show SomeRefinementInterface
+
+newtype RFIList = RFIList { fromRFIList :: Vector SomeRefinementInterface }
+
+instance Yaml.FromJSON RFIList where
+  parseJSON = Yaml.withArray "list of functors" $ \arr ->
+    RFIList <$> mapM parseFunctor arr
+
+parseFunctor :: Yaml.Value -> Yaml.Parser SomeRefinementInterface
+parseFunctor value =
+  case value of
+    Yaml.String name -> case HashMap.lookup name registeredFunctors of
+      Nothing -> failUnknownFunctor name
+      Just (RefinableFunctor { parseArguments = NoArguments h }) -> return (SRI h)
+      _ -> fail ("Functor" ++ T.unpack name ++ "requires an argument")
+
+    Yaml.Object obj -> case HashMap.toList obj of
+      [(name, argument)] -> case HashMap.lookup name registeredFunctors of
+        Nothing -> failUnknownFunctor name
+        Just (RefinableFunctor { parseArguments = ArgumentParser parser }) -> SRI <$> parser argument
+        _ -> fail ("Functor" ++ T.unpack name ++ "doesn't have arguments")
+
+      _ -> failIllegalJson
+
+    _ -> failIllegalJson
+
+  where
+    failUnknownFunctor name = fail ("Functor " ++ T.unpack name ++ " not found")
+    failIllegalJson = fail "Illegal functor specification"
+
+data SomeEncoding where
+  SomeEncoding :: (Show a, Show h1) => Encoding a h1 -> SomeEncoding
+
+deriving instance Show SomeEncoding
+
+parseSomeEncoding :: SomeRefinementInterface -> Yaml.Value -> Yaml.Parser SomeEncoding
+parseSomeEncoding (SRI ri) value = SomeEncoding <$> parse ri value
+
+newtype CoalgebraSpecification = CoalgebraSpecification (Vector SomeEncoding)
+  deriving (Show)
+
+instance Yaml.FromJSON CoalgebraSpecification where
+  parseJSON = Yaml.withObject "coalgebra" $ \obj -> do
+    functors <- fromRFIList <$> obj .: "functors"
+    morphisms <- obj .: "morphisms"
+    -- TODO Ensure functors and morphisms are of equal length
+    encodings <- forM (V.zip functors morphisms) $ \(functor, morphs) ->
+      parseSomeEncoding functor morphs
+
+    return (CoalgebraSpecification encodings)
+
+decodeCoalgebra :: ByteString -> Either String CoalgebraSpecification
+decodeCoalgebra = Yaml.decodeEither

src/main/Main.hs

+{-# LANGUAGE LambdaCase #-}
+
+module Main where
+
+import qualified Data.ByteString as BS
+
+import           System.Environment
+import           System.IO
+
+import           Parser
+
+main :: IO ()
+main = getArgs >>= \case
+  [file] -> BS.readFile file >>= print . decodeCoalgebra
+  _ -> do
+    prog <- getProgName
+    hPutStrLn stderr ("Usage: " ++ prog ++ " FILE")
+

stack.yaml

+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-3.5
+# resolver: nightly-2015-09-21
+# resolver: ghc-7.10.2
+# resolver: ghcjs-0.1.0_ghc-7.10.2
+# resolver:
+#  name: custom-snapshot
+#  location: "./custom-snapshot.yaml"
+resolver: lts-11.9
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+# - location:
+#    git: https://github.com/commercialhaskell/stack.git
+#    commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#   extra-dep: true
+#  subdirs:
+#  - auto-update
+#  - wai
+#
+# A package marked 'extra-dep: true' will only be built if demanded by a
+# non-dependency (i.e. a user package), and its test suites and benchmarks
+# will not be run. This is useful for tweaking upstream packages.
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver
+# (e.g., acme-missiles-0.3)
+# extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=1.6"
+#
+# Override the architecture used by stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor
\ No newline at end of file