Restyle Exploration of the Lower Your Guards paper

explore/lower-your-guards/Setup.hs

@@ -1,2 +1,3 @@
 import Distribution.Simple
+
 main = defaultMain

explore/lower-your-guards/src/Annotated.hs

@@ -3,8 +3,8 @@
 module Annotated where
 
 import qualified GuardTree as G
-import qualified Uncovered as U
 import MatchInfo
+import qualified Uncovered as U
 
 data Ant where
   Grhs :: U.RefinementType -> Int -> Ant
@@ -17,4 +17,5 @@ annotated ref gdt = case gdt of
   G.Guarded (var, g) t -> case g of
     G.GMatch k args -> annotated (ref `U.liftAndLit` varInfo (Match k args)) t
     G.GWas new -> annotated (ref `U.liftAndLit` varInfo (WasOriginally new)) t
-    where varInfo = U.Info var
+   where
+    varInfo = U.Info var

explore/lower-your-guards/src/GuardTree.hs

@@ -6,9 +6,9 @@ import Control.Monad (replicateM, zipWithM)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Fresh as F
+import MatchInfo
 import qualified Parse as P
 import qualified Types as Ty
-import MatchInfo
 
 data Gdt where
   Grhs :: Int -> Gdt
@@ -32,11 +32,11 @@ desugarClauses args clauses = do
 desugarClause :: [F.VarID] -> (Int, P.Clause) -> F.Fresh Gdt
 desugarClause args (i, P.Clause pat typeIn _) = do
   let x1 = head args -- we only suport 1 arg for this toy lyg
-  guards <- desugarMatch (x1,typeIn) pat
+  guards <- desugarMatch (x1, typeIn) pat
   return $ foldr Guarded (Grhs i) guards
 
 desugarMatch :: TypedVar -> P.Pattern -> F.Fresh [(TypedVar, Guard)]
-desugarMatch var@(_,ty) pat = do
+desugarMatch var@(_, ty) pat = do
   case pat of
     P.PWild -> return []
     P.PVar name -> do

explore/lower-your-guards/src/Inhabitants.hs

@@ -45,9 +45,9 @@ accessableRedundant ant args = case ant of
 -- do a linear scan from right to left
 lookupVar :: TypedVar -> [ConstraintFor] -> TypedVar
 lookupVar x = foldr getNextId x
-  where
-    getNextId (x', MatchInfo (WasOriginally y)) | x' == x = const y
-    getNextId _ = id
+ where
+  getNextId (x', MatchInfo (WasOriginally y)) | x' == x = const y
+  getNextId _ = id
 
 alistLookup :: (Eq a) => a -> [(a, b)] -> [b]
 alistLookup a = map snd . filter ((== a) . fst)
@@ -101,10 +101,10 @@ findVarInhabitants var nref@(_, cns) =
               if null posNrefs
                 then Poss.retSingle $ IPNot []
                 else Poss.anyOf <$> forM posNrefs (findVarInhabitants var)
-  where
-    constraintsOnX = onVar var cns
-    posMatch = listToMaybe $ mapMaybe (\case MatchInfo (Match k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX
-    negMatch = mapMaybe (\case MatchInfo (Not k) -> Just k; _ -> Nothing) constraintsOnX
+ where
+  constraintsOnX = onVar var cns
+  posMatch = listToMaybe $ mapMaybe (\case MatchInfo (Match k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX
+  negMatch = mapMaybe (\case MatchInfo (Not k) -> Just k; _ -> Nothing) constraintsOnX
 
 normalize :: NormRefType -> U.Formula -> F.Fresh (S.Set NormRefType)
 normalize nref (f1 `U.And` f2) = do
@@ -155,8 +155,8 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of
         else do
           let (noX', withX') = partition ((/= origX) . fst) cns
           addConstraints (ctx, noX' ++ [cf]) (substituteVarIDs origY origX withX')
-  where
-    added = (ctx, cns ++ [cf])
+ where
+  added = (ctx, cns ++ [cf])
 
 -----
 ----- Helper functions for adding constraints:

explore/lower-your-guards/src/Main.hs

@@ -147,5 +147,5 @@ niceInhabPattern (I.IPNot nots) = "(Not " ++ niceList (map Ty.dcName nots) ++ ")
 
 niceList :: [Text] -> String
 niceList as = concat $ tail $ concatMap comma as
-  where
-    comma x = [", ", T.unpack x]
+ where
+  comma x = [", ", T.unpack x]

explore/lower-your-guards/src/MatchTree.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE EmptyCase #-}
+
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
 {-# HLINT ignore "Eta reduce" #-}
@@ -39,9 +39,9 @@ final2 = ([full] \\\ c2) \\\ c1
 
 -- true = Status $ Is $ Just $ head $ Ty.dataCons Ty.bool
 
-e1 = Pair (Either [(isInt 10)] []) (isInt 2)
+e1 = Pair (Either [isInt 10] []) (isInt 2)
 
-e2 = Pair (Either [(isInt 4)] []) (isInt 5)
+e2 = Pair (Either [isInt 4] []) (isInt 5)
 
 -- e3 = Pair (Either [] [true]) (isInt 5)
 
@@ -73,21 +73,21 @@ treeMinus t1 t2 = case (t1, t2) of
   (Pair _ _, Either _ _) -> error "type error6"
   (Pair a b, Pair c d) ->
     map mkPairL aMinusC ++ map mkPairR bMinusD ++ both
-    where
-      mkPairL aSubC = Pair aSubC d
-      mkPairR bSubD = Pair c bSubD
-      both = [Pair aSubC bSubD | aSubC <- aMinusC, bSubD <- bMinusD]
-      c' = treeIntersect a c
-      d' = treeIntersect b d
-      aMinusC = concatMap (a \\) c'
-      bMinusD = concatMap (b \\) d'
-      -- [Pair d' aSubC, Pair c' bSubD, Pair aSubC bSubD]
+   where
+    mkPairL aSubC = Pair aSubC d
+    mkPairR bSubD = Pair c bSubD
+    both = [Pair aSubC bSubD | aSubC <- aMinusC, bSubD <- bMinusD]
+    c' = treeIntersect a c
+    d' = treeIntersect b d
+    aMinusC = concatMap (a \\) c'
+    bMinusD = concatMap (b \\) d'
+  -- [Pair d' aSubC, Pair c' bSubD, Pair aSubC bSubD]
   (Either a b, Either c d) ->
     [Either left right]
-    where
-      -- l = foldr a (flip map (\\)) c
-      left = concat [x \\ y | x <- a, y <- c]
-      right = concat [x \\ y | x <- b, y <- d]
+   where
+    -- l = foldr a (flip map (\\)) c
+    left = concat [x \\ y | x <- a, y <- c]
+    right = concat [x \\ y | x <- b, y <- d]
 
 treeIntersect :: MatchTree -> MatchTree -> [MatchTree]
 treeIntersect m1 m2 = case (m1, m2) of
@@ -105,20 +105,20 @@ treeIntersect m1 m2 = case (m1, m2) of
   (Either _ _, Pair _ _) -> error "type error5"
   (Pair _ _, Either _ _) -> error "type error6"
   (Pair a b, Pair c d) -> error "pairs"
-    -- map mkPairL (a \\ c) ++ map mkPairR (b \\ d) ++ both
-    -- where
-    --   mkPairL aSubC = Pair aSubC d
-    --   mkPairR bSubD = Pair c bSubD
-    --   both = [Pair aSubC bSubD | aSubC <- a \\ c, bSubD <- b \\ d]
-      -- c' = statIntersect a c
-      -- d' = statIntersect b d
+  -- map mkPairL (a \\ c) ++ map mkPairR (b \\ d) ++ both
+  -- where
+  --   mkPairL aSubC = Pair aSubC d
+  --   mkPairR bSubD = Pair c bSubD
+  --   both = [Pair aSubC bSubD | aSubC <- a \\ c, bSubD <- b \\ d]
+  -- c' = statIntersect a c
+  -- d' = statIntersect b d
   (Either a b, Either c d) -> error "eithers"
-    -- [Either left right]
-    -- where
-    --   -- l = foldr a (flip map (\\)) c
-    --   left = concat [x \\ y | x <- a, y <- c]
-    --   right = concat [x \\ y | x <- b, y <- d]
-  
+
+-- [Either left right]
+-- where
+--   -- l = foldr a (flip map (\\)) c
+--   left = concat [x \\ y | x <- a, y <- c]
+--   right = concat [x \\ y | x <- b, y <- d]
 
 -- (a-c)*(b-d) + c*(b-d) + (a-c)*d
 

explore/lower-your-guards/src/Parse.hs

@@ -105,9 +105,9 @@ pDataConsMatch typeIn =
 pPattern :: Ty.Type -> Parser Pattern
 pPattern typeIn =
   choice
-    [ symbol "_" $> PWild,
-      pDataConsMatch typeIn,
-      pName <&> PVar
+    [ symbol "_" $> PWild
+    , pDataConsMatch typeIn
+    , pName <&> PVar
     ]
 
 pClause :: Text -> Ty.Type -> Parser Clause
@@ -133,15 +133,15 @@ pFn = do
 pType :: Parser Ty.Type
 pType =
   choice
-    [ Ty.int <$ lexeme (string "Int"),
-      Ty.bool <$ lexeme (string "Bool"),
-      Ty.throol <$ lexeme (string "Throol"),
-      do
+    [ Ty.int <$ lexeme (string "Int")
+    , Ty.bool <$ lexeme (string "Bool")
+    , Ty.throol <$ lexeme (string "Throol")
+    , do
         _ <- symbol ","
         l <- pType
         r <- pType
-        return $ Ty.pair l r,
-      do
+        return $ Ty.pair l r
+    , do
         _ <- lexeme (string "Either")
         l <- pType
         r <- pType

explore/lower-your-guards/src/Play.hs

@@ -1,8 +1,8 @@
 module Play where
 
 thing :: (Int, Bool) -> ()
-thing (n,True) = ()
-thing (0,n) = ()
+thing (n, True) = ()
+thing (0, n) = ()
 
 triple :: (Int, Int, Int) -> ()
 triple (7, 5, 3) = ()
@@ -11,19 +11,19 @@ triple2 :: (Int, (Int, Int)) -> ()
 triple2 (7, (5, 3)) = ()
 
 foo :: (Either Int Bool, Int) -> Bool
-foo (Left  1     , 2) = True
-foo (Right False , n) = True
-foo (Right True  , n) = True
-foo (Left  3     , n) = True
-foo (Left  3     , n) = True
+foo (Left 1, 2) = True
+foo (Right False, n) = True
+foo (Right True, n) = True
+foo (Left 3, n) = True
+foo (Left 3, n) = True
 
 foo2 :: (Either Int Bool, Int) -> Bool
-foo2 (Left  1    , n) = True
-foo2 (Right False , n) = True
+foo2 (Left 1, n) = True
+foo2 (Right False, n) = True
 
 foo3 :: (Either Bool Bool, Bool) -> Bool
-foo3 (Left  True    , b) = True
-foo3 (Right False   , b) = True
+foo3 (Left True, b) = True
+foo3 (Right False, b) = True
 
 foo4 :: (Int, Int) -> Bool
 foo4 (1, n) = True
@@ -42,24 +42,25 @@ foo7 (1, 2, 3) = False
 
 foo8 :: (Either Int Bool, Int) -> ()
 foo8 (Left 10, 2) = ()
+
 -- foo8 (Right True, 5) = ()
 
 data Pat where
-    Base :: Pat
-    Kon :: Pat -> Pat
-    DonKon :: Pat -> Pat -> Pat
-    deriving (Show, Eq)
+  Base :: Pat
+  Kon :: Pat -> Pat
+  DonKon :: Pat -> Pat -> Pat
+  deriving (Show, Eq)
 
 timelineSplitter :: Int -> [Pat]
 timelineSplitter p = do
-    case p of
-        0 -> return Base
-        2 -> [Base, Base]
-        4 -> do
-            a <- timelineSplitter (p - 1)
-            b <- timelineSplitter (p - 2)
-            
-            return $ DonKon a b
-        _ -> do
-            n <- timelineSplitter (p - 1)
-            return $ Kon n
+  case p of
+    0 -> return Base
+    2 -> [Base, Base]
+    4 -> do
+      a <- timelineSplitter (p - 1)
+      b <- timelineSplitter (p - 2)
+
+      return $ DonKon a b
+    _ -> do
+      n <- timelineSplitter (p - 1)
+      return $ Kon n

explore/lower-your-guards/src/Possibilities.hs

@@ -55,10 +55,10 @@ retSingle i = return $ Possibilities [i]
 -- cartesian product of multiple sets
 allCombinations :: [Possibilities a] -> Possibilities [a]
 allCombinations = foldr prod nil
-  where
-    -- note, nil /= mempty
-    -- VERY important
-    nil = Possibilities [[]]
+ where
+  -- note, nil /= mempty
+  -- VERY important
+  nil = Possibilities [[]]
 
 prod :: Possibilities a -> Possibilities [a] -> Possibilities [a]
 prod (Possibilities xs) (Possibilities yss) = Possibilities [x : ys | x <- xs, ys <- yss]