Add Nat to initial ghci environment for lols

2 files changed, 20 insertions, 0 deletions

diff --git a/bwrap-files/workdir/initdefs.hs b/bwrap-files/workdir/initdefs.hs
new file mode 100644
index 0000000..7083fe0
--- /dev/null
+++ b/bwrap-files/workdir/initdefs.hs
@@ -0,0 +1,19 @@
+:{
+data Nat = Z | S Nat deriving (Show, Eq, Ord)
+
+instance Num Nat where
+  Z + n = n
+  S m + n = S (m + n)
+  Z * _ = Z
+  S m * n = n + m * n
+  negate _ = error "negate on Nat"
+  abs = id
+  signum Z = Z
+  signum _ = 1
+  fromInteger n
+    | n < 0 = error "fromInteger to Nat on negative number"
+    | otherwise =
+        let go 0 = Z
+            go m = S (go (m-1))
+        in go n
+:}
diff --git a/src/Ghci.hs b/src/Ghci.hs
index d339d74..ae44881 100644
--- a/src/Ghci.hs
+++ b/src/Ghci.hs
@@ -75,6 +75,7 @@ makeGhci = do
       , std_err = UseHandle pipeIn }
   ghciPutStrLn stdinH ":set -interactive-print=Yahb2Defs.limitedPrint"
   ghciPutStrLn stdinH ":m"
+  ghciPutStrLn stdinH ":script initdefs.hs"
   hFlush stdinH
   return Ghci { ghciProc = proch
               , ghciStdin = stdinH