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 ()