feat(ltl): Add formatting checks in nix build

src/ltl/app/Main.hs

@@ -5,18 +5,18 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeOperators #-}
+
 module Main where
 
 import qualified Data.Aeson as Aeson
 import qualified Data.Aeson.Text as AesonText
 import qualified Data.Text.Lazy.IO as TextIO
-import Options.Generic
-
 import Ltl
 import Ltl.Json
 import qualified Ltl.Proof as Proof
 import Ltl.Prop.Parser (parse)
 import qualified Ltl.Storage as Storage
+import Options.Generic
 
 ------------------------------------------------------------------------
 
@@ -38,37 +38,38 @@ gitHash = "unknown"
 
 data Config
   = Check
-    { testId  :: Int <?> "Which TestId to test",
-      runId   :: Int <?> "Which RunId to test",
-      formula :: Text <?> "LTL Formula to check"
-    }
+      { testId :: Int <?> "Which TestId to test",
+        runId :: Int <?> "Which RunId to test",
+        formula :: Text <?> "LTL Formula to check"
+      }
   | Version
   deriving (Generic)
 
 instance ParseRecord Config
 
 data Result = Result
-  { result :: Bool
-  , reason :: String
-  } deriving (Generic)
+  { result :: Bool,
+    reason :: String
+  }
+  deriving (Generic)
 
 instance Aeson.FromJSON Result
+
 instance Aeson.ToJSON Result
 
 main :: IO ()
 main = do
   (cfg, help) <- getWithHelp "LTL checker"
   case cfg of
     Version -> putStrLn gitHash
-    Check{..} -> do
+    Check {..} -> do
       trace <- Storage.sqliteLoad (unHelpful testId) (unHelpful runId)
       testFormula <- case parse (unHelpful formula) of
-        Left s  -> error s
+        Left s -> error s
         Right x -> pure x
-      let
-        dec = check testFormula trace
-        result = case dec of
-          Proof.No{} -> False
-          Proof.Yes{} -> True
-        r = Result result (Proof.reason dec)
+      let dec = check testFormula trace
+          result = case dec of
+            Proof.No {} -> False
+            Proof.Yes {} -> True
+          r = Result result (Proof.reason dec)
       TextIO.putStrLn $ AesonText.encodeToLazyText r

src/ltl/default.nix

@@ -18,5 +18,12 @@ pkg.overrideAttrs (attrs: {
     # patched in the `postInstall` phase of the top-level `default.nix`.
     [ "--ghc-option=-D__GIT_HASH__=\"0000000000000000000000000000000000000000-nix\"" ];
   # this should probably check that attrs.checkInputs doesn't exist
-  checkInputs = [ nixpkgs.pkgs.haskell.packages.${compiler}.tasty-discover ];
+  checkInputs = [
+    nixpkgs.pkgs.haskell.packages.${compiler}.cabal-fmt
+    nixpkgs.pkgs.haskell.packages.${compiler}.ormolu
+    nixpkgs.pkgs.haskell.packages.${compiler}.tasty-discover
+  ];
+  checkCabalFmt = "cabal-fmt --check ltl.cabal";
+  checkOrmolu = "ormolu --mode check $(find . -name '*.hs')";
+  preConfigurePhases = ["checkCabalFmt" "checkOrmolu"] ++ attrs.preConfigurePhases;
 })

src/ltl/ltl.cabal

@@ -19,18 +19,18 @@ tested-with:        GHC ==8.10.4
 library
   hs-source-dirs:   src/
   exposed-modules:
-      Ltl
-    , Ltl.Json
-    , Ltl.Proof
-    , Ltl.Prop
-    , Ltl.Prop.Parser
-    , Ltl.Storage
-    , Ltl.Traces
+    Ltl
+    Ltl.Json
+    Ltl.Proof
+    Ltl.Prop
+    Ltl.Prop.Parser
+    Ltl.Storage
+    Ltl.Traces
 
   -- GHC boot library dependencies:
   -- (https://gitlab.haskell.org/ghc/ghc/-/blob/master/packages)
   build-depends:
-      base              >=4.14 && <4.15
+      base        >=4.14 && <4.15
     , bytestring
     , containers
     , filepath
@@ -80,8 +80,8 @@ executable detsys-ltl
   hs-source-dirs:   app/
   main-is:          Main.hs
   build-depends:
-      base
-    , aeson
+      aeson
+    , base
     , ltl
     , optparse-generic
     , text

src/ltl/src/Ltl.hs

@@ -1,55 +1,52 @@
-{-# language OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
+
 module Ltl where
 
-import Data.Maybe (fromMaybe)
 import qualified Data.Aeson as Aeson
-import Data.List.NonEmpty (NonEmpty(..))
+import Data.Foldable (toList)
+import qualified Data.HashMap.Strict as H
+import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Foldable (toList)
+import Data.Maybe (fromMaybe)
 import Data.Text (Text)
-import qualified Data.HashMap.Strict as H
-
 import Ltl.Json
+import Ltl.Proof
 import Ltl.Prop
 import Ltl.Traces
-import Ltl.Proof
 
 --------------------------------------------------------------------------------
 
-
 evalExpr :: CheckState -> StateBehaviour -> Expr -> Json
 evalExpr _ _ (Constant js) = js
 evalExpr state sb (Variable (Var t n e)) =
-  let
-    State s = case t of
+  let State s = case t of
         Before -> before sb
-        After  -> after sb
-  in jq e (fromMaybe Aeson.Null $ Map.lookup (evalNode (nodeEnv state) n) s)
+        After -> after sb
+   in jq e (fromMaybe Aeson.Null $ Map.lookup (evalNode (nodeEnv state) n) s)
 evalExpr state _ (IntLang e) = Aeson.Number $ fromInteger $ evalInt (intEnv state) e
 evalExpr state sb (EEvent e) =
   let Event js = action sb
-  in jq e js
+   in jq e js
 
 checkPredicate :: CheckState -> Predicate -> StateBehaviour -> Dec
 checkPredicate state p sb = case p of
   Eq e e' ->
     let lhs = evalExpr state sb e
         rhs = evalExpr state sb e'
-    in if lhs == rhs then Yes (PP (PEq lhs)) else No (RP (REq lhs rhs))
-
+     in if lhs == rhs then Yes (PP (PEq lhs)) else No (RP (REq lhs rhs))
 
 --------------------------------------------------------------------------------
 
-
 futures :: NonEmpty a -> [NonEmpty a]
 futures (t@(_ :| [])) = [t]
-futures (t :| (t':ts)) = let f = futures (t' :| ts)
-                             h = case f of
-                               [] -> []
-                               (x:xs) -> toList x
- in (t :| h) : f
+futures (t :| (t' : ts)) =
+  let f = futures (t' :| ts)
+      h = case f of
+        [] -> []
+        (x : xs) -> toList x
+   in (t :| h) : f
 
 data CheckState = CheckState
   { nodeEnv :: NodeEnvironment,
@@ -80,7 +77,7 @@ check' state formula ts = case formula of
     anyDec (\i -> check' (updateIenv b i state) f ts) is PExistsInt RExistsInt
   Imp f g -> (check' state f ts) `impDec` check' state g ts
   And f g -> check' state f ts `andDec` check' state g ts
-  Or  f g -> check' state f ts `orDec` check' state g ts
+  Or f g -> check' state f ts `orDec` check' state g ts
   Neg f -> notDec (check' state f ts)
   TT -> Yes PTT
   FF -> No RFF
@@ -90,19 +87,21 @@ check f t = check' state (concreteNodes (nodesFromTrace t) f) t
   where
     state = CheckState Map.empty Map.empty (nodesFromTrace t)
     nodesFromTrace (StateBehaviour (State x) _ _ _ :| _) = Map.keys x
+
 --------------------------------------------------------------------------------
 
 exampleTrace :: Trace
 exampleTrace =
-  sb 0 [(a, sa1), (b, sb1)] [(a,sa2), (b,sb2)] :| [
-  sb 1 [(a, sa2), (b, sb2)] [(a,sa3), (b,sb3)],
-  sb 2 [(a, sa3), (b, sb3)] [(a,sa4), (b,sb4)]]
+  sb 0 [(a, sa1), (b, sb1)] [(a, sa2), (b, sb2)]
+    :| [ sb 1 [(a, sa2), (b, sb2)] [(a, sa3), (b, sb3)],
+         sb 2 [(a, sa3), (b, sb3)] [(a, sa4), (b, sb4)]
+       ]
   where
     sb i x y = StateBehaviour (State (Map.fromList x)) i (Event Aeson.Null) (State (Map.fromList y))
     a = "NodeA"
     b = "NodeB"
     sa1 = Aeson.object [("state", Aeson.Bool True)]
-    (sa2:sa3:sa4:_) = repeat sa1
+    (sa2 : sa3 : sa4 : _) = repeat sa1
     sb1 = Aeson.object [("bstate", Aeson.Bool True)]
-    (sb2:sb3:_) = repeat sb1
+    (sb2 : sb3 : _) = repeat sb1
     sb4 = Aeson.object [("bstate", Aeson.Bool False)]

src/ltl/src/Ltl/Json.hs

@@ -2,12 +2,12 @@ module Ltl.Json where
 
 import qualified Data.Aeson as Aeson
 import Data.Aeson.QQ.Simple
+import qualified Data.HashMap.Strict as HashMap
 import Data.List (sort)
 import qualified Data.Maybe as Maybe
-import Data.Text(Text)
+import Data.Text (Text)
 import qualified Data.Text.Lazy as LazyText
 import qualified Data.Text.Lazy.Encoding as TextEncoding
-import qualified Data.HashMap.Strict as HashMap
 import qualified Data.Vector as Vector
 
 type Json = Aeson.Value
@@ -27,7 +27,7 @@ jq (Lookup f k) js = case js of
     Just js' -> jq f js'
   _ -> Aeson.Null -- or fail?
 jq (Index f i) js = case js of
-  Aeson.Array xs ->case xs Vector.!? (fromInteger i) of
+  Aeson.Array xs -> case xs Vector.!? (fromInteger i) of
     Just js' -> jq f js'
     Nothing -> Aeson.Null
   _ -> Aeson.Null
@@ -36,6 +36,7 @@ jq (Index f i) js = case js of
 
 decode :: Text -> Either String Json
 decode = Aeson.eitherDecode . TextEncoding.encodeUtf8 . LazyText.fromStrict
+
 --------------------------------------------------------------------------------
 
 {-
@@ -58,15 +59,14 @@ decode = Aeson.eitherDecode . TextEncoding.encodeUtf8 . LazyText.fromStrict
 
 mergePatch :: Json -> Json -> Json
 mergePatch target (Aeson.Object hm) =
-  let
-    targetKV = case target of
+  let targetKV = case target of
         Aeson.Object kv -> kv
         _ -> HashMap.empty
-    go tKv [] = Aeson.Object tKv
-    go tKv ((k, v):ps) = go (HashMap.alter f k tKv) ps
-      where
-        f tv = case v of
-          Aeson.Null -> Nothing
-          _ -> Just $ mergePatch (Maybe.fromMaybe Aeson.Null tv) v
-  in go targetKV (sort $ HashMap.toList hm) -- sort to make deterministic?
+      go tKv [] = Aeson.Object tKv
+      go tKv ((k, v) : ps) = go (HashMap.alter f k tKv) ps
+        where
+          f tv = case v of
+            Aeson.Null -> Nothing
+            _ -> Just $ mergePatch (Maybe.fromMaybe Aeson.Null tv) v
+   in go targetKV (sort $ HashMap.toList hm) -- sort to make deterministic?
 mergePatch _ patch = patch

src/ltl/src/Ltl/Proof.hs

@@ -70,15 +70,15 @@ allDec :: (r -> Dec) -> [r] -> (r -> Refutation -> Refutation) -> Proof -> Dec
 allDec pred xs ref pro = go xs
   where
     go [] = Yes pro
-    go (x:xs) = case pred x of
+    go (x : xs) = case pred x of
       Yes _ -> go xs
       No r -> No $ ref x r
 
 anyDec :: (r -> Dec) -> [r] -> (r -> Proof -> Proof) -> Refutation -> Dec
 anyDec pred xs pro ref = go xs
   where
     go [] = No ref
-    go (x:xs) = case pred x of
+    go (x : xs) = case pred x of
       Yes p -> Yes $ pro x p
       No _ -> go xs
 

src/ltl/src/Ltl/Prop.hs

@@ -3,10 +3,8 @@ module Ltl.Prop where
 import Data.List ((\\))
 import Data.Map (Map)
 import qualified Data.Map as Map
-
 import Ltl.Json (JQ, Json)
-import Ltl.Traces(Node)
-
+import Ltl.Traces (Node)
 
 data VTemporal = Before | After
   deriving (Eq, Show)
@@ -22,13 +20,13 @@ evalNode :: NodeEnvironment -> NodeExpression -> Node
 evalNode _ (ConcreteNode node) = node
 evalNode env (VariableNode var) = env Map.! var
 
-bindNodeEnvironment :: NodeVar ->  Node -> NodeEnvironment -> NodeEnvironment
+bindNodeEnvironment :: NodeVar -> Node -> NodeEnvironment -> NodeEnvironment
 bindNodeEnvironment = Map.insert
 
 data Var = Var
-  { time :: VTemporal
-  , node :: NodeExpression
-  , expr :: JQ
+  { time :: VTemporal,
+    node :: NodeExpression,
+    expr :: JQ
   }
   deriving (Eq, Show)
 
@@ -73,16 +71,16 @@ data Formula
   deriving (Eq, Show)
 
 concreteN :: [Node] -> NodeExpression -> NodeExpression
-concreteN nodes n@(ConcreteNode{}) = n
+concreteN nodes n@(ConcreteNode {}) = n
 concreteN nodes (VariableNode n)
   | n `elem` nodes = ConcreteNode n
   | otherwise = VariableNode n
 
 concreteE :: [Node] -> Expr -> Expr
 concreteE nodes (Variable (Var t n jq)) = Variable (Var t (concreteN nodes n) jq)
-concreteE nodes j@(Constant{}) = j
-concreteE nodes i@(IntLang{}) = i
-concreteE nodes e@(EEvent{}) = e
+concreteE nodes j@(Constant {}) = j
+concreteE nodes i@(IntLang {}) = i
+concreteE nodes e@(EEvent {}) = e
 
 concreteP :: [Node] -> Predicate -> Predicate
 concreteP nodes (Eq l r) = Eq (concreteE nodes l) (concreteE nodes r)