.direnv/flake-inputs/2hc9lg18zd6yabw9jqj0wy3s9kyvkzp0-source

@@ -0,0 +1 @@
+/nix/store/2hc9lg18zd6yabw9jqj0wy3s9kyvkzp0-source

.direnv/flake-inputs/79qk1r0q5xc9g3qhw0m143x04q6d7x2m-source

@@ -0,0 +1 @@
+/nix/store/79qk1r0q5xc9g3qhw0m143x04q6d7x2m-source

.direnv/flake-inputs/bv68i4l7g6s5sixxm0c9lcjdxhlkg0n5-source

@@ -0,0 +1 @@
+/nix/store/bv68i4l7g6s5sixxm0c9lcjdxhlkg0n5-source

.direnv/flake-inputs/hmiyz975p0bfnzfcbamn6d0v1gfv15ds-source

@@ -0,0 +1 @@
+/nix/store/hmiyz975p0bfnzfcbamn6d0v1gfv15ds-source

.direnv/flake-inputs/lwyjz70qh12nq6cb7fixl85vryzxqm3c-source

@@ -0,0 +1 @@
+/nix/store/lwyjz70qh12nq6cb7fixl85vryzxqm3c-source

.direnv/flake-profile-a5d5b61aa8a61b7d9d765e1daf971a9a578f1cfa

@@ -1 +1 @@
-/nix/store/kjyxmjgg4yqk90hcvjdbj984af6jxjkv-ghc-shell-for-Sudoku-0.1.0.0-0-env
+/nix/store/dl8p5s0m5prz82vbshy9n1k12yj1imsg-ghc-shell-for-Sudoku-0.1.0.0-0-env

.gitignore

@@ -22,5 +22,4 @@ cabal.project.local
 cabal.project.local~
 .HTF/
 .ghc.environment.*
-.direnv/
+
-src/.liquid/

Sudoku.cabal

@@ -68,12 +68,10 @@ library
     -- other-extensions:
 
     -- Other library packages from which modules are imported.
-    build-depends:    base ^>=4.19.0.0,
+    build-depends:    base ^>=4.18.2.0,
                       vector ^>=0.13.1.0,
                       mtl ^>=2.3.1,
-                      split ^>=0.2.2,
+                      split ^>=0.2.2
-                      liquidhaskell,
-                      liquid-vector
 
     -- Directories containing source files.
     hs-source-dirs:   src
@@ -96,10 +94,10 @@ executable Sudoku
 
     -- Other library packages from which modules are imported.
     build-depends:
-        base ^>=4.19.0.0,
+        base ^>=4.18.2.0,
         Sudoku,
         vector ^>=0.13.1.0,
-        mtl ^>=2.3.1,
+        mtl ^>=2.3.1
 
     -- Directories containing source files.
     hs-source-dirs:   app
@@ -131,5 +129,5 @@ test-suite Sudoku-test
 
     -- Test dependencies.
     build-depends:
-        base ^>=4.19.0.0,
+        base ^>=4.18.2.0,
         Sudoku

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1717285511,
+        "lastModified": 1709336216,
-        "narHash": "sha256-iKzJcpdXih14qYVcZ9QC9XuZYnPc6T8YImb6dX166kw=",
+        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "2a55567fcf15b1b1c7ed712a2c6fadaec7412ea8",
+        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
         "type": "github"
       },
       "original": {
@@ -20,11 +20,11 @@
     },
     "haskell-flake": {
       "locked": {
-        "lastModified": 1717944201,
+        "lastModified": 1710675764,
-        "narHash": "sha256-h9cBnB1hfF73g/K7FJtsOdcE0mbi00qBGCJ+CFH7jRQ=",
+        "narHash": "sha256-ZpBoh1dVLTxC3wccOnsji7u/Ceuwh2raQn/Vq6BBYwo=",
         "owner": "srid",
         "repo": "haskell-flake",
-        "rev": "8bffb2266b38fe7983d14fc4858aea2e64ad2175",
+        "rev": "ef955d7d239d7f82f343b569a4cf2c7c1a4df1f4",
         "type": "github"
       },
       "original": {
@@ -35,11 +35,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1718276985,
+        "lastModified": 1710889954,
-        "narHash": "sha256-u1fA0DYQYdeG+5kDm1bOoGcHtX0rtC7qs2YA2N1X++I=",
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "3f84a279f1a6290ce154c5531378acc827836fbb",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
@@ -51,14 +51,20 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1717284937,
+        "dir": "lib",
-        "narHash": "sha256-lIbdfCsf8LMFloheeE6N31+BMIeixqyQWbSr2vk79EQ=",
+        "lastModified": 1709237383,
-        "type": "tarball",
+        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
-        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
+        "dir": "lib",
-        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
       }
     },
     "root": {

flake.nix

@@ -21,7 +21,7 @@
           # The base package set representing a specific GHC version.
           # By default, this is pkgs.haskellPackages.
           # You may also create your own. See https://haskell.flake.page/package-set
-          basePackages = pkgs.haskell.packages.ghc981;
+          # basePackages = pkgs.haskellPackages;
 
           # Dependency overrides go here. See https://haskell.flake.page/dependency
           # source-overrides = { };
@@ -33,9 +33,9 @@
           
             # Programs you want to make available in the shell.
             # Default programs can be disabled by setting to 'null'
-            tools = hp: { fourmolu = hp.fourmolu; };
+            tools = hp: { fourmolu = hp.fourmolu; ghcid = null; };
           
-            # hlsCheck.enable = true;
+            hlsCheck.enable = true;
            };
         };
 

src/Types.hs

@@ -1,113 +1,103 @@
-{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
-
 module Types where
 
--- import Data.List (intercalate)
+import Data.List (intercalate)
 import Data.List.Split (chunksOf, keepDelimsL, split, whenElt)
--- import Data.Vector (Vector)
+import Data.Vector (Vector)
 import qualified Data.Vector as V
 
-{-@ type NVector a N = {v : V.Vector a | vlen v == N} @-}
+type Row a = Vector a
-{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}
 
-{-@ data Grid a = GR { dim  :: Nat
+data Grid a = Grid
-                     , grid :: NVector (NVector a dim) dim} @-}
+  { grid :: Vector (Row a),
-data Grid a = GR
+    dimension :: Int
-  { dim :: Int,
-    grid :: V.Vector (V.Vector a)
   }
 
--- TODO make NSquareList
-{-@ type NList a N = {xs:[a] | len xs == N} @-}
-
--- {-@ assume chunksOf :: forall a. n:Nat -> x:{vs:[a] | (len vs) mod n == 0} -> {vs:[NList a n] | (len vs) != ((len x) // n)} @-}
-
--- {-@ ignore initGrid @-}
-{-@ initGrid :: forall a. n:Nat -> NList a (n + n) -> Grid a @-}
 initGrid :: Int -> [a] -> Grid a
-initGrid n vs = GR n (V.fromList . map V.fromList $ chunksOf n vs)
+initGrid d vs = Grid (V.fromList . map V.fromList $ chunksOf (d * d) vs) d
 
--- {-@ getRow :: g:Grid a -> Btwn 0 (vlen (grid g)) -> V.Vector a @-}
+getRow :: Grid a -> Int -> Row a
--- getRow :: Grid a -> Int -> V.Vector a
+getRow (Grid g d) y =
--- getRow (GR g d) y = g V.! y
+  if y >= d * d || y < 0
+    then error ("getRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
+    else g V.! y
 
--- putRow :: Grid a -> V.Vector a -> Int -> Grid a
+putRow :: Grid a -> Row a -> Int -> Grid a
--- putRow (GR g d) newRow y =
+putRow (Grid g d) newRow y =
---   if y >= d * d || y < 0
+  if y >= d * d || y < 0
---     then error ("putRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
+    then error ("putRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
---     else GR (g V.// [(y, newRow)]) d
+    else Grid (g V.// [(y, newRow)]) d
 
--- updateRow :: Grid a -> (Row a -> Row a) -> Int -> Grid a
+updateRow :: Grid a -> (Row a -> Row a) -> Int -> Grid a
--- updateRow gr upd y = putRow gr (upd oldRow) y
+updateRow gr upd y = putRow gr (upd oldRow) y
---   where
+  where
---     oldRow = getRow gr y
+    oldRow = getRow gr y
 
--- putCell :: Grid a -> (Int, Int) -> a -> Grid a
+putCell :: Grid a -> (Int, Int) -> a -> Grid a
--- putCell gs@(GR _ d) (x, y) v =
+putCell gs@(Grid _ d) (x, y) v =
---   if x >= d * d || x < 0
+  if x >= d * d || x < 0
---     then error "putCell out of bounds"
+    then error "putCell out of bounds"
---     else updateRow gs (\row -> row V.// [(x, v)]) y
+    else updateRow gs (\row -> row V.// [(x, v)]) y
 
--- getCell :: Grid a -> (Int, Int) -> a
+getCell :: Grid a -> (Int, Int) -> a
--- getCell gs@(GR _ d) (x, y) =
+getCell gs@(Grid _ d) (x, y) =
---   if x >= d * d || x < 0
+  if x >= d * d || x < 0
---     then error "getCell: x out of bounds"
+    then error "getCell: x out of bounds"
---     else row V.! x
+    else row V.! x
---   where
+  where
---     row = getRow gs y
+    row = getRow gs y
 
--- printGrid :: (Show a) => Grid a -> String
+printGrid :: (Show a) => Grid a -> String
--- printGrid gr@(GR _ d) = unwords . intercalate ["\n"] . chunksOf 3 . (split . keepDelimsL . whenElt) (== '\n') . unlines $ map printRow [0 .. (d * d) - 1]
+printGrid gr@(Grid _ d) = unwords . intercalate ["\n"] . chunksOf 3 . (split . keepDelimsL . whenElt) (== '\n') . unlines $ map printRow [0 .. (d * d) - 1]
---   where
+  where
---     printRow :: Int -> String
+    printRow :: Int -> String
---     printRow _y = unwords $ map printSquare [0 .. d - 1]
+    printRow _y = unwords $ map printSquare [0 .. d - 1]
---       where
+      where
---         y = checkDimension d _y
+        y = checkDimension d _y
---         row = getRow gr y
+        row = getRow gr y
---         printSquare :: Int -> String
+        printSquare :: Int -> String
---         printSquare n =
+        printSquare n =
---           if n * d >= d * d || n < 0
+          if n * d >= d * d || n < 0
---             then error ("trying to print square " ++ show n ++ " which is out of bounds (dimension: " ++ show d ++ ")")
+            then error ("trying to print square " ++ show n ++ " which is out of bounds (dimension: " ++ show d ++ ")")
---             else concatMap (\m -> show $ row V.! (n * d + m)) [0 .. d - 1]
+            else concatMap (\m -> show $ row V.! (n * d + m)) [0 .. d - 1]
 
--- checkDimension :: Int -> Int -> Int
+checkDimension :: Int -> Int -> Int
--- checkDimension d v =
+checkDimension d v =
---   if v >= d * d || v < 0
+  if v >= d * d || v < 0
---     then error ("value " ++ show v ++ " out of dimension: " ++ show d)
+    then error ("value " ++ show v ++ " out of dimension: " ++ show d)
---     else v
+    else v
 
--- update :: Grid a -> Int -> Int -> a -> Grid a
+update :: Grid a -> Int -> Int -> a -> Grid a
--- update (GR g d) _x _y v = GR newG d
+update (Grid g d) _x _y v = Grid newG d
---   where
+  where
---     x = checkDimension d _x
+    x = checkDimension d _x
---     y = checkDimension d _y
+    y = checkDimension d _y
---     row = g V.! y
+    row = g V.! y
---     newRow = row V.// [(x, v)]
+    newRow = row V.// [(x, v)]
---     newG = g V.// [(y, newRow)]
+    newG = g V.// [(y, newRow)]
 
--- allCells :: Grid a -> (a -> Bool) -> Bool
+allCells :: Grid a -> (a -> Bool) -> Bool
--- allCells (GR g _) test = V.all id rows
+allCells (Grid g _) test = V.all id rows
---   where
+  where
---     rows :: Vector Bool
+    rows :: Vector Bool
---     rows = V.map (V.all test) g
+    rows = V.map (V.all test) g
 
--- rowView :: Grid a -> Int -> Row a
+rowView :: Grid a -> Int -> Row a
--- rowView = getRow
+rowView = getRow
 
--- colView :: Grid a -> Int -> Row a
+colView :: Grid a -> Int -> Row a
--- colView gr@(GR _ d) x = V.generate (d * d) (\y -> getCell gr (x, y))
+colView gr@(Grid _ d) x = V.generate (d * d) (\y -> getCell gr (x, y))
 
--- -- returns topleft coords of the square
+-- returns topleft coords of the square
--- squareToCoords :: Grid a -> Int -> (Int, Int)
+squareToCoords :: Grid a -> Int -> (Int, Int)
--- squareToCoords (GR _ d) m = ((m `mod` d) * d, (m `div` d) * d)
+squareToCoords (Grid _ d) m = ((m `mod` d) * d, (m `div` d) * d)
 
--- squareView :: Grid a -> Int -> Row a
+squareView :: Grid a -> Int -> Row a
--- squareView gr@(GR _ d) n = V.concat (map (\y -> V.generate d (\x -> getCell gr (x + xoff, y + yoff))) [0 .. d - 1])
+squareView gr@(Grid _ d) n = V.concat (map (\y -> V.generate d (\x -> getCell gr (x + xoff, y + yoff))) [0 .. d - 1])
---   where
+  where
---     (xoff, yoff) = squareToCoords gr n
+    (xoff, yoff) = squareToCoords gr n
 
--- count :: (Eq a) => Vector a -> a -> Int
+count :: (Eq a) => Vector a -> a -> Int
--- count v a = V.foldl (\c b -> if a == b then c + 1 else c) 0 v
+count v a = V.foldl (\c b -> if a == b then c + 1 else c) 0 v
 
--- mapGrid :: (a -> b) -> Grid a -> Grid b
+mapGrid :: (a -> b) -> Grid a -> Grid b
--- mapGrid f (GR g d) = GR (V.map (V.map f) g) d
+mapGrid f (Grid g d) = Grid (V.map (V.map f) g) d