Skip to content

Commit

Permalink
Restyle Exploration of the Lower Your Guards paper (#402)
Browse files Browse the repository at this point in the history
* Restyled by fourmolu

* Restyled by hlint

---------

Co-authored-by: Restyled.io <[email protected]>
  • Loading branch information
restyled-io[bot] and restyled-commits authored Sep 3, 2024
1 parent 9340ec1 commit 6ca6f7c
Show file tree
Hide file tree
Showing 12 changed files with 122 additions and 114 deletions.
1 change: 1 addition & 0 deletions explore/lower-your-guards/Setup.hs
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
import Distribution.Simple

main = defaultMain
5 changes: 3 additions & 2 deletions explore/lower-your-guards/src/Annotated.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
6 changes: 3 additions & 3 deletions explore/lower-your-guards/src/GuardTree.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
18 changes: 9 additions & 9 deletions explore/lower-your-guards/src/Inhabitants.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down
4 changes: 2 additions & 2 deletions explore/lower-your-guards/src/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
58 changes: 29 additions & 29 deletions explore/lower-your-guards/src/MatchTree.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{-# LANGUAGE EmptyCase #-}

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down
18 changes: 9 additions & 9 deletions explore/lower-your-guards/src/Parse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
53 changes: 27 additions & 26 deletions explore/lower-your-guards/src/Play.hs
Original file line number Diff line number Diff line change
@@ -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) = ()
Expand All @@ -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
Expand All @@ -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
8 changes: 4 additions & 4 deletions explore/lower-your-guards/src/Possibilities.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Loading

0 comments on commit 6ca6f7c

Please sign in to comment.