Exploration of the Lower Your Guards paper (#401)

* Init stack project explore/lower-your-guards * lyg test language parser works * basic gaurd tree desugaring * add basic uncovered set function * add pair datacons and pretty printer * inhabitants N function kind of works * Add types * inhabitants mostly working * pretty print patterns * start work on fresh * Fresh works! * Fixed arg id bug, fresh actually works now! * implement Show to make some printing better * done for day. Strange behavoir, check complex2/3 * switch to MaybeT / cleanup * nested patterns work! Still must tune up Int literal stuff, also see type equal TODO * positive info works * positive info and integer negative info work! * no longer list all dataconstructors anyway when covered * remove old negative only inhab code * cleanup comments in inhab hs * remove old TODO message * change refinement type formulas datatype to match paper Originally, I thought I had outsmarted the paper Not so, they broke things up into `Formula`s and `Literal`s for a good reason, which I rediscovered * auto run on files in test folder * huge overhaul to Inhabitants.hs. more to go, but significant cleanup done * refactor / cleanup adding constraints * refactor addLiteral previously known as (<+>) for readability * rename matching to onVar to avoid confusion * major cleanup to inhabitants + lots of documentation * cleanup Pos suffix, all functions use positive info now * small inhabitant cleanup + ready for big changes * play with map merge instead of logic solver idea in inhab2 * add Annotated tree and redundancy checking * attempt my own version of exhaustiveness checking * BROKEN, about to try list monad * match tree broken, might be a lost cause * combined UA function done! * Properly use Fresh moand in Inhabitation checks Before I was manually threading state By rewriting a few things, Fresh and Monad [] can coexist Really hope there are no regressions, I didn't spot any * add comments, prepare for simplification * add throol testcase, proves necessity of cart prod * create Possibilities newtype for lists, to make things more clear * cleanup inhabitants * document + move Possibilities to a new file * attempting to remove MatchInt (CURRENTLY BROKEN) * add int as opaque type, not weird exception (BROKEN) * inhab works again! needs cleanup * remove traces of IntLit, ready for MatchInfo merge * introduce HerebyBe, reads better, hopefully no regressions * Switch to TypedVar everywhere, add Be to MatchInfo * cleanup, commit to TypedVar * More cleanup * document bug, already fixed * clean up bug stuff / test case for termeq bug * small cleanup before merge * Remove unneeded todo * Restyle Exploration of the Lower Your Guards paper (#402) * Restyled by fourmolu * Restyled by hlint --------- Co-authored-by: Restyled.io <[email protected]> * Restyled by fourmolu (#403) Co-authored-by: Restyled.io <[email protected]> --------- Co-authored-by: restyled-io[bot] <32688539+restyled-io[bot]@users.noreply.github.com> Co-authored-by: Restyled.io <[email protected]>
disco-lang · Sep 21, 2024 · 250077c · 250077c
1 parent 3dd8b2f
commit 250077c
Show file tree

Hide file tree

Showing 37 changed files with 1,364 additions and 0 deletions.
diff --git a/explore/lower-your-guards/LICENSE b/explore/lower-your-guards/LICENSE
diff --git a/explore/lower-your-guards/Setup.hs b/explore/lower-your-guards/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/explore/lower-your-guards/hie.yaml b/explore/lower-your-guards/hie.yaml
@@ -0,0 +1,2 @@
+cradle:
+  stack:
diff --git a/explore/lower-your-guards/lower-your-guards.cabal b/explore/lower-your-guards/lower-your-guards.cabal
@@ -0,0 +1,50 @@
+cabal-version:       2.2
+
+name:                lower-your-guards
+version:             0.1.0.0
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Colin Phillips
+maintainer:          [email protected]
+copyright:           2024 Colin Phillips
+category:            Language
+build-type:          Simple
+
+executable lower-your-guards
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.7 && < 5,
+                       megaparsec >= 6.1.1 && < 9.7,
+                       text >= 2.0.2 && < 2.1,
+                       pretty-simple,
+                       containers,
+                       mtl,
+                       transformers,
+                       directory
+  ghc-options:         -Wall
+                       -Wcompat
+                       -Widentities
+                       -Wincomplete-record-updates
+                       -Wincomplete-uni-patterns
+                       -Wmissing-export-lists
+                       -Wmissing-home-modules
+                       -Wpartial-fields
+                       -Wredundant-constraints
+  default-extensions:  GADTs,
+                       OverloadedStrings,
+                       LambdaCase,
+                       TupleSections
+  other-modules:       Parse,
+                       GuardTree,
+                       Uncovered
+                       Inhabitants,
+                       Inhabitants2,
+                       Types,
+                       Fresh,
+                       Play,
+                       Annotated,
+                       MatchTree,
+                       UA,
+                       Possibilities,
+                       MatchInfo
diff --git a/explore/lower-your-guards/src/Annotated.hs b/explore/lower-your-guards/src/Annotated.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Annotated where
+
+import qualified GuardTree as G
+import MatchInfo
+import qualified Uncovered as U
+
+data Ant where
+  Grhs :: U.RefinementType -> Int -> Ant
+  Branch :: Ant -> Ant -> Ant
+
+annotated :: U.RefinementType -> G.Gdt -> Ant
+annotated ref gdt = case gdt of
+  G.Grhs i -> Grhs ref i
+  G.Branch t1 t2 -> Branch (annotated ref t1) (annotated (U.uncovered ref t1) t2)
+  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
diff --git a/explore/lower-your-guards/src/Fresh.hs b/explore/lower-your-guards/src/Fresh.hs
@@ -0,0 +1,44 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Fresh where
+
+import Control.Monad.State
+import Data.List.NonEmpty (NonEmpty ((:|)))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Map as M
+import qualified Data.Text as T
+
+type Fresh = State (NE.NonEmpty Frame)
+
+data Frame = Frame {fBound :: M.Map VarID (Maybe T.Text), fNextID :: Int}
+  deriving (Show, Eq, Ord)
+
+newtype VarID = Var Int
+  deriving (Show, Eq, Ord)
+
+blank :: NE.NonEmpty Frame
+blank = Frame {fBound = M.empty, fNextID = 0} :| []
+
+fresh :: Maybe T.Text -> Fresh VarID
+fresh mName = do
+  Frame {fBound = bound, fNextID = nextID} <- gets NE.head
+  t <- gets NE.tail
+  let h = Frame {fBound = M.insert (Var nextID) mName bound, fNextID = nextID + 1}
+  put $ h :| t
+  return (Var nextID)
+
+enterScope :: Fresh ()
+enterScope = do
+  nextID <- gets (fNextID . NE.head)
+  stack <- get
+  put $ Frame {fBound = M.empty, fNextID = nextID} :| NE.toList stack
+
+exitScope :: Fresh ()
+exitScope = modify (NE.fromList . NE.tail)
+
+performInNewScope :: Fresh a -> Fresh a
+performInNewScope m = do
+  enterScope
+  a <- m
+  exitScope
+  return a
diff --git a/explore/lower-your-guards/src/GuardTree.hs b/explore/lower-your-guards/src/GuardTree.hs
@@ -0,0 +1,50 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module GuardTree where
+
+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
+
+data Gdt where
+  Grhs :: Int -> Gdt
+  Branch :: Gdt -> Gdt -> Gdt
+  Guarded :: (TypedVar, Guard) -> Gdt -> Gdt
+  deriving (Show, Eq)
+
+data Guard where
+  GMatch :: Ty.DataConstructor -> [TypedVar] -> Guard
+  GWas :: TypedVar -> Guard
+  deriving (Show, Eq)
+
+enumerate :: NonEmpty a -> NonEmpty (Int, a)
+enumerate = NE.zip (1 :| [2 ..])
+
+desugarClauses :: [F.VarID] -> NonEmpty P.Clause -> F.Fresh Gdt
+desugarClauses args clauses = do
+  cl <- mapM (desugarClause args) (enumerate clauses)
+  return $ foldr1 Branch cl
+
+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
+  return $ foldr Guarded (Grhs i) guards
+
+desugarMatch :: TypedVar -> P.Pattern -> F.Fresh [(TypedVar, Guard)]
+desugarMatch var@(_, ty) pat = do
+  case pat of
+    P.PWild -> return []
+    P.PVar name -> do
+      x <- F.fresh (Just name)
+      let xTy = (x, ty)
+      return [(xTy, GWas var)]
+    P.PMatch dataCon subPats -> do
+      ys <- replicateM (length subPats) (F.fresh Nothing)
+      let typedYs = zip ys (Ty.dcTypes dataCon)
+      guards <- zipWithM desugarMatch typedYs subPats
+      return $ (var, GMatch dataCon typedYs) : concat guards