From be618f9a741007b37f29eab9895c7ccccf6449f2 Mon Sep 17 00:00:00 2001
From: Greg Shuflin <greg.shuflin@protonmail.com>
Date: Mon, 30 May 2022 19:22:44 -0700
Subject: [PATCH] Add random game

---
 random_game.lean | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 random_game.lean

diff --git a/random_game.lean b/random_game.lean
new file mode 100644
index 0000000..4d034ff
--- /dev/null
+++ b/random_game.lean
@@ -0,0 +1,34 @@
+import system.io
+
+open char
+open list
+open io
+
+
+def rand_range(lo : nat)(hi: nat) : io nat := do
+  r <- io.cmd { cmd := "head", args := ["-c 80", "/dev/urandom"] },
+  let seed := foldl (+) 0 $ map to_nat r.to_list,
+  let gen := mk_std_gen seed,
+  let (target, _) := rand_nat gen lo hi,
+  return target
+
+def get_guess : io nat := do
+  put_str "Guess a number between 1 and 100 (inclusive)\n",
+  put_str "Your guess: ",
+  response <- get_line,
+  return $ string.to_nat response
+
+def main : io unit := do
+  target <- rand_range 1 100,
+  iterate 20 $ λ i,
+  if i > 0 then do {
+    put_str $ "You have " ++ (to_string i) ++ " guesses left\n",
+    guess <- get_guess,
+    match cmp guess target with
+    | ordering.eq := do { put_str "\nYou win!\n", return none }
+    | ordering.gt := do { put_str "\ntoo high\n", return $ some (i - 1) }
+    | ordering.lt := do { put_str "\ntoo low\n", return $ some (i - 1) }
+    end
+  } else
+    return none,
+  return ()