Work on liquid

.direnv/flake-inputs/2hc9lg18zd6yabw9jqj0wy3s9kyvkzp0-source

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

.direnv/flake-inputs/79qk1r0q5xc9g3qhw0m143x04q6d7x2m-source

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

.direnv/flake-inputs/bv68i4l7g6s5sixxm0c9lcjdxhlkg0n5-source

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

.direnv/flake-inputs/hmiyz975p0bfnzfcbamn6d0v1gfv15ds-source

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

.direnv/flake-inputs/lwyjz70qh12nq6cb7fixl85vryzxqm3c-source

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

.direnv/flake-profile-a5d5b61aa8a61b7d9d765e1daf971a9a578f1cfa

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

.gitignore

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

Sudoku.cabal

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

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1709336216,
-        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
+        "lastModified": 1717285511,
+        "narHash": "sha256-iKzJcpdXih14qYVcZ9QC9XuZYnPc6T8YImb6dX166kw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
+        "rev": "2a55567fcf15b1b1c7ed712a2c6fadaec7412ea8",
         "type": "github"
       },
       "original": {
@@ -20,11 +20,11 @@
     },
     "haskell-flake": {
       "locked": {
-        "lastModified": 1710675764,
-        "narHash": "sha256-ZpBoh1dVLTxC3wccOnsji7u/Ceuwh2raQn/Vq6BBYwo=",
+        "lastModified": 1717944201,
+        "narHash": "sha256-h9cBnB1hfF73g/K7FJtsOdcE0mbi00qBGCJ+CFH7jRQ=",
         "owner": "srid",
         "repo": "haskell-flake",
-        "rev": "ef955d7d239d7f82f343b569a4cf2c7c1a4df1f4",
+        "rev": "8bffb2266b38fe7983d14fc4858aea2e64ad2175",
         "type": "github"
       },
       "original": {
@@ -35,11 +35,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "lastModified": 1718276985,
+        "narHash": "sha256-u1fA0DYQYdeG+5kDm1bOoGcHtX0rtC7qs2YA2N1X++I=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "rev": "3f84a279f1a6290ce154c5531378acc827836fbb",
         "type": "github"
       },
       "original": {
@@ -51,20 +51,14 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "dir": "lib",
-        "lastModified": 1709237383,
-        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
-        "type": "github"
+        "lastModified": 1717284937,
+        "narHash": "sha256-lIbdfCsf8LMFloheeE6N31+BMIeixqyQWbSr2vk79EQ=",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
       },
       "original": {
-        "dir": "lib",
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz"
       }
     },
     "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.haskellPackages;
+          basePackages = pkgs.haskell.packages.ghc981;
 
           # 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; ghcid = null; };
+            tools = hp: { fourmolu = hp.fourmolu; };
           
-            hlsCheck.enable = true;
+            # hlsCheck.enable = true;
            };
         };
 

src/Types.hs

@@ -1,103 +1,113 @@
+{-# 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 Row a = Vector a
+{-@ type NVector a N = {v : V.Vector a | vlen v == N} @-}
+{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}
 
-data Grid a = Grid
-  { grid :: Vector (Row a),
-    dimension :: Int
+{-@ data Grid a = GR { dim  :: Nat
+                     , grid :: NVector (NVector a dim) dim} @-}
+data Grid a = GR
+  { 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 d vs = Grid (V.fromList . map V.fromList $ chunksOf (d * d) vs) d
+initGrid n vs = GR n (V.fromList . map V.fromList $ chunksOf n vs)
 
-getRow :: Grid a -> Int -> Row a
-getRow (Grid g d) y =
-  if y >= d * d || y < 0
-    then error ("getRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
-    else g V.! y
+-- {-@ getRow :: g:Grid a -> Btwn 0 (vlen (grid g)) -> V.Vector a @-}
+-- getRow :: Grid a -> Int -> V.Vector a
+-- getRow (GR g d) y = g V.! y
 
-putRow :: Grid a -> Row a -> Int -> Grid a
-putRow (Grid g d) newRow y =
-  if y >= d * d || y < 0
-    then error ("putRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
-    else Grid (g V.// [(y, newRow)]) d
+-- putRow :: Grid a -> V.Vector a -> Int -> Grid a
+-- putRow (GR g d) newRow y =
+--   if y >= d * d || y < 0
+--     then error ("putRow: y=" ++ show y ++ " is out of dimension=" ++ show d)
+--     else GR (g V.// [(y, newRow)]) d
 
-updateRow :: Grid a -> (Row a -> Row a) -> Int -> Grid a
-updateRow gr upd y = putRow gr (upd oldRow) y
-  where
-    oldRow = getRow gr y
+-- updateRow :: Grid a -> (Row a -> Row a) -> Int -> Grid a
+-- updateRow gr upd y = putRow gr (upd oldRow) y
+--   where
+--     oldRow = getRow gr y
 
-putCell :: Grid a -> (Int, Int) -> a -> Grid a
-putCell gs@(Grid _ d) (x, y) v =
-  if x >= d * d || x < 0
-    then error "putCell out of bounds"
-    else updateRow gs (\row -> row V.// [(x, v)]) y
+-- putCell :: Grid a -> (Int, Int) -> a -> Grid a
+-- putCell gs@(GR _ d) (x, y) v =
+--   if x >= d * d || x < 0
+--     then error "putCell out of bounds"
+--     else updateRow gs (\row -> row V.// [(x, v)]) y
 
-getCell :: Grid a -> (Int, Int) -> a
-getCell gs@(Grid _ d) (x, y) =
-  if x >= d * d || x < 0
-    then error "getCell: x out of bounds"
-    else row V.! x
-  where
-    row = getRow gs y
+-- getCell :: Grid a -> (Int, Int) -> a
+-- getCell gs@(GR _ d) (x, y) =
+--   if x >= d * d || x < 0
+--     then error "getCell: x out of bounds"
+--     else row V.! x
+--   where
+--     row = getRow gs y
 
-printGrid :: (Show a) => Grid a -> String
-printGrid gr@(Grid _ d) = unwords . intercalate ["\n"] . chunksOf 3 . (split . keepDelimsL . whenElt) (== '\n') . unlines $ map printRow [0 .. (d * d) - 1]
-  where
-    printRow :: Int -> String
-    printRow _y = unwords $ map printSquare [0 .. d - 1]
-      where
-        y = checkDimension d _y
-        row = getRow gr y
-        printSquare :: Int -> String
-        printSquare n =
-          if n * d >= d * d || n < 0
-            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]
+-- 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]
+--   where
+--     printRow :: Int -> String
+--     printRow _y = unwords $ map printSquare [0 .. d - 1]
+--       where
+--         y = checkDimension d _y
+--         row = getRow gr y
+--         printSquare :: Int -> String
+--         printSquare n =
+--           if n * d >= d * d || n < 0
+--             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]
 
-checkDimension :: Int -> Int -> Int
-checkDimension d v =
-  if v >= d * d || v < 0
-    then error ("value " ++ show v ++ " out of dimension: " ++ show d)
-    else v
+-- checkDimension :: Int -> Int -> Int
+-- checkDimension d v =
+--   if v >= d * d || v < 0
+--     then error ("value " ++ show v ++ " out of dimension: " ++ show d)
+--     else v
 
-update :: Grid a -> Int -> Int -> a -> Grid a
-update (Grid g d) _x _y v = Grid newG d
-  where
-    x = checkDimension d _x
-    y = checkDimension d _y
-    row = g V.! y
-    newRow = row V.// [(x, v)]
-    newG = g V.// [(y, newRow)]
+-- update :: Grid a -> Int -> Int -> a -> Grid a
+-- update (GR g d) _x _y v = GR newG d
+--   where
+--     x = checkDimension d _x
+--     y = checkDimension d _y
+--     row = g V.! y
+--     newRow = row V.// [(x, v)]
+--     newG = g V.// [(y, newRow)]
 
-allCells :: Grid a -> (a -> Bool) -> Bool
-allCells (Grid g _) test = V.all id rows
-  where
-    rows :: Vector Bool
-    rows = V.map (V.all test) g
+-- allCells :: Grid a -> (a -> Bool) -> Bool
+-- allCells (GR g _) test = V.all id rows
+--   where
+--     rows :: Vector Bool
+--     rows = V.map (V.all test) g
 
-rowView :: Grid a -> Int -> Row a
-rowView = getRow
+-- rowView :: Grid a -> Int -> Row a
+-- rowView = getRow
 
-colView :: Grid a -> Int -> Row a
-colView gr@(Grid _ d) x = V.generate (d * d) (\y -> getCell gr (x, y))
+-- colView :: Grid a -> Int -> Row a
+-- colView gr@(GR _ d) x = V.generate (d * d) (\y -> getCell gr (x, y))
 
--- returns topleft coords of the square
-squareToCoords :: Grid a -> Int -> (Int, Int)
-squareToCoords (Grid _ d) m = ((m `mod` d) * d, (m `div` d) * d)
+-- -- returns topleft coords of the square
+-- squareToCoords :: Grid a -> Int -> (Int, Int)
+-- squareToCoords (GR _ d) m = ((m `mod` d) * d, (m `div` d) * d)
 
-squareView :: Grid a -> Int -> Row a
-squareView gr@(Grid _ d) n = V.concat (map (\y -> V.generate d (\x -> getCell gr (x + xoff, y + yoff))) [0 .. d - 1])
-  where
-    (xoff, yoff) = squareToCoords gr n
+-- 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])
+--   where
+--     (xoff, yoff) = squareToCoords gr n
 
-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 :: (Eq a) => Vector a -> a -> Int
+-- 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 f (Grid g d) = Grid (V.map (V.map f) g) d
+-- mapGrid :: (a -> b) -> Grid a -> Grid b
+-- mapGrid f (GR g d) = GR (V.map (V.map f) g) d