chore: add Nix support

.gitignore

@@ -14,3 +14,5 @@ cabal.sandbox.config
 .stack-work
 .*.sw?
 
+/dist-newstyle
+result

Connections.hs

@@ -1,5 +1,4 @@
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances,
-             GeneralizedNewtypeDeriving, TupleSections #-}
+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections #-}
 module Connections where
 
 import Control.Applicative
@@ -113,10 +112,10 @@ comparable alpha beta = alpha `leq` beta || beta `leq` alpha
 
 incomparables :: [Face] -> Bool
 incomparables []     = True
-incomparables (x:xs) = all (not . (x `comparable`)) xs && incomparables xs
+incomparables (x:xs) = not (any (x `comparable`) xs) && incomparables xs
 
 (~>) :: Name -> Dir -> Face
-i ~> d = singleton i d
+i ~> d = Map.singleton i d
 
 eps :: Face
 eps = Map.empty
@@ -237,8 +236,8 @@ merge a b =
 -- phi b = max {alpha : Face | phi alpha = b}
 invFormula :: Formula -> Dir -> [Face]
 invFormula (Dir b') b          = [ eps | b == b' ]
-invFormula (Atom i) b          = [ singleton i b ]
-invFormula (NegAtom i) b       = [ singleton i (- b) ]
+invFormula (Atom i) b          = [ Map.singleton i b ]
+invFormula (NegAtom i) b       = [ Map.singleton i (- b) ]
 invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0
 invFormula (phi :/\: psi) One  = meets (invFormula phi 1) (invFormula psi 1)
 invFormula (phi :\/: psi) b    = invFormula (negFormula phi :/\: negFormula psi) (- b)
@@ -400,7 +399,7 @@ mkSystem :: [(Face, a)] -> System a
 mkSystem = flip insertsSystem Map.empty
 
 unionSystem :: System a -> System a -> System a
-unionSystem us vs = insertsSystem (assocs us) vs
+unionSystem us = insertsSystem (assocs us)
 
 
 joinSystem :: System (System a) -> System a

Main.hs

@@ -90,10 +90,10 @@ initLoop :: [Flag] -> FilePath -> History -> IO ()
 initLoop flags f hist = do
   -- Parse and type check files
   (_,_,mods) <- E.catch (imports True ([],[],[]) f)
-                        (\e -> do putStrLn $ unlines $
+                        (\e -> do putStrLn $ unlines
                                     ("Exception: " :
-                                     (takeWhile (/= "CallStack (from HasCallStack):")
-                                                   (lines $ show (e :: SomeException))))
+                                     takeWhile (/= "CallStack (from HasCallStack):")
+                                                   (lines $ show (e :: E.SomeException)))
                                   return ([],[],[]))
   -- Translate to TT
   let res = runResolver $ resolveModules mods
@@ -106,13 +106,13 @@ initLoop flags f hist = do
       let ns = map fst names
           uns = nub ns
           dups = ns \\ uns
-      unless (dups == []) $
+      unless (null dups) $
         putStrLn $ "Warning: the following definitions were shadowed [" ++
                    intercalate ", " dups ++ "]"
       (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs
       case merr of
         Just err -> putStrLn $ "Type checking failed: " ++ shrink err
-        Nothing  -> unless (mods == []) $ putStrLn "File loaded."
+        Nothing  -> unless (null mods) $ putStrLn "File loaded."
       if Batch `elem` flags
         then return ()
         else -- Compute names for auto completion
@@ -154,10 +154,10 @@ loop flags f names tenv = do
                 start <- liftIO getCurrentTime
                 let e = mod $ E.eval (TC.env tenv) body
                 -- Let's not crash if the evaluation raises an error:
-                liftIO $ catch (putStrLn (msg ++ shrink (show e)))
+                liftIO $ E.catch (putStrLn (msg ++ shrink (show e)))
                                -- (writeFile "examples/nunivalence3.ctt" (show e))
                                (\e -> putStrLn ("Exception: " ++
-                                                show (e :: SomeException)))
+                                                show (e :: E.SomeException)))
                 stop <- liftIO getCurrentTime
                 -- Compute time and print nicely
                 let time = diffUTCTime stop start
@@ -181,7 +181,7 @@ imports v st@(notok,loaded,mods) f
   | f `elem` loaded = return st
   | otherwise       = do
     b <- doesFileExist f
-    when (not b) $ error (f ++ " does not exist")
+    unless b $ error (f ++ " does not exist")
     let prefix = dropFileName f
     s <- readFile f
     let ts = lexer s

Makefile

@@ -1,32 +1,29 @@
 # DO NOT DELETE: Beginning of Haskell dependencies
-Exp/ErrM.o : Exp/ErrM.hs
+Connections.o : Connections.hs
+CTT.o : CTT.hs
+CTT.o : Connections.hi
+Eval.o : Eval.hs
+Eval.o : CTT.hi
+Eval.o : Connections.hi
 Exp/Abs.o : Exp/Abs.hs
-Exp/Skel.o : Exp/Skel.hs
-Exp/Skel.o : Exp/ErrM.hi
-Exp/Skel.o : Exp/Abs.hi
-Exp/Print.o : Exp/Print.hs
-Exp/Print.o : Exp/Abs.hi
+Exp/ErrM.o : Exp/ErrM.hs
 Exp/Lex.o : Exp/Lex.hs
+Exp/Layout.o : Exp/Layout.hs
+Exp/Layout.o : Exp/Lex.hi
 Exp/Par.o : Exp/Par.hs
-Exp/Par.o : Exp/ErrM.hi
 Exp/Par.o : Exp/Lex.hi
 Exp/Par.o : Exp/Abs.hi
-Exp/Layout.o : Exp/Layout.hs
-Exp/Layout.o : Exp/Lex.hi
+Exp/Print.o : Exp/Print.hs
+Exp/Print.o : Exp/Abs.hi
+Exp/Skel.o : Exp/Skel.hs
+Exp/Skel.o : Exp/Abs.hi
 Exp/Test.o : Exp/Test.hs
-Exp/Test.o : Exp/ErrM.hi
-Exp/Test.o : Exp/Layout.hi
-Exp/Test.o : Exp/Abs.hi
-Exp/Test.o : Exp/Print.hi
 Exp/Test.o : Exp/Skel.hi
+Exp/Test.o : Exp/Print.hi
 Exp/Test.o : Exp/Par.hi
 Exp/Test.o : Exp/Lex.hi
-Connections.o : Connections.hs
-CTT.o : CTT.hs
-CTT.o : Connections.hi
-Eval.o : Eval.hs
-Eval.o : CTT.hi
-Eval.o : Connections.hi
+Exp/Test.o : Exp/Layout.hi
+Exp/Test.o : Exp/Abs.hi
 Resolver.o : Resolver.hs
 Resolver.o : Connections.hi
 Resolver.o : Connections.hi

README.md

@@ -92,6 +92,22 @@ To compile and install the project using [stack](https://haskellstack.org/), run
     stack install
 ```
 
+## Nix
+
+To development the project using [Nix](https://nixos.org/), run:
+
+```sh
+    nix-shell
+    # after entering Nix shell
+    make
+```
+
+To compile the project using [Nix](https://nixos.org/), run:
+
+```sh
+    nix-build
+```
+
 Usage
 -----
 
@@ -147,7 +163,7 @@ References and notes
  * HoTT book and webpage:
    [http://homotopytypetheory.org/](http://homotopytypetheory.org/)
 
- * [Cubical Type Theory](http://www.cse.chalmers.se/~coquand/face.pdf) - 
+ * [Cubical Type Theory](http://www.cse.chalmers.se/~coquand/face.pdf) -
    Old version of the typing rules of the system. See
    [this](http://www.cse.chalmers.se/~coquand/face.pdf) for a
    variation using isomorphisms instead of equivalences.

default.nix

@@ -0,0 +1,12 @@
+{pkgs ? import <nixpkgs> {}}:
+pkgs.stdenv.mkDerivation {
+  pname = "cubicaltt";
+  version = "1.0";
+
+  src = ./.;
+  buildInputs = (import ./deps.nix {inherit pkgs;}).buildInputs;
+  installPhase = ''
+    mkdir -p $out/bin
+    mv ./cubical $out/bin
+  '';
+}

deps.nix

@@ -0,0 +1,24 @@
+{
+  pkgs ? import <nixpkgs> {},
+  devDeps ? (ghcPkgs: []),
+}: {
+  buildInputs = with pkgs;
+    [
+      gnumake
+    ]
+    ++ [
+      (
+        haskellPackages.ghcWithPackages (ghcPkgs:
+          (with ghcPkgs; [
+            mtl
+            haskeline
+            directory
+            BNFC
+            alex
+            happy
+            QuickCheck
+          ])
+          ++ devDeps ghcPkgs)
+      )
+    ];
+}

shell.nix

@@ -0,0 +1,9 @@
+{pkgs ? import <nixpkgs> {}}:
+pkgs.mkShell {
+  buildInputs =
+    (import ./deps.nix {
+      inherit pkgs;
+      devDeps = ghcPkgs: with ghcPkgs; [haskell-language-server];
+    })
+    .buildInputs;
+}