CLI Tictactoe for HVM

ttt.hvm

// Piece.equal (a: (Piece)) (b: (Piece)) : (Bool)
(Piece.equal (Piece.o) (Piece.o)) = (Bool.true)
(Piece.equal (Piece.x) (Piece.x)) = (Bool.true)
(Piece.equal (Piece.o) (Piece.x)) = (Bool.false)
(Piece.equal (Piece.x) (Piece.o)) = (Bool.false)

// Piece.show (piece: (Piece)) : (String)
(Piece.show (Piece.o)) = "O"
(Piece.show (Piece.x)) = "X"

// Tile.is_empty (tile: (Tile)) : (Bool)
(Tile.is_empty (Tile.empty)) = (Bool.true)
(Tile.is_empty tile) = (Bool.false)

// Tile.is_x (tile: (Tile)) : (Bool)
(Tile.is_x (Tile.filled (Piece.x))) = (Bool.true)
(Tile.is_x tile) = (Bool.false)

// Tile.is_o (tile: (Tile)) : (Bool)
(Tile.is_o (Tile.filled (Piece.o))) = (Bool.true)
(Tile.is_o tile) = (Bool.false)

// Tile.show (tile: (Tile)) : (String)
(Tile.show (Tile.empty)) = " "
(Tile.show (Tile.filled piece)) = (Piece.show piece)

// Board.set_tile (coord: (Coord)) (piece: (Piece)) (board: (Board)) : (Board)
(Board.set_tile (Coord.new (Num3.1) (Num3.1)) piece (Board.new (Triple.new t1 t2 t3) r2 r3)) = (Board.new (Triple.new (Tile.filled piece) t2 t3) r2 r3)
(Board.set_tile (Coord.new (Num3.1) (Num3.2)) piece (Board.new (Triple.new t1 t2 t3) r2 r3)) = (Board.new (Triple.new t1 (Tile.filled piece) t3) r2 r3)
(Board.set_tile (Coord.new (Num3.1) (Num3.3)) piece (Board.new (Triple.new t1 t2 t3) r2 r3)) = (Board.new (Triple.new t1 t2 (Tile.filled piece)) r2 r3)
(Board.set_tile (Coord.new (Num3.2) (Num3.1)) piece (Board.new r1 (Triple.new t1 t2 t3) r3)) = (Board.new r1 (Triple.new (Tile.filled piece) t2 t3) r3)
(Board.set_tile (Coord.new (Num3.2) (Num3.2)) piece (Board.new r1 (Triple.new t1 t2 t3) r3)) = (Board.new r1 (Triple.new t1 (Tile.filled piece) t3) r3)
(Board.set_tile (Coord.new (Num3.2) (Num3.3)) piece (Board.new r1 (Triple.new t1 t2 t3) r3)) = (Board.new r1 (Triple.new t1 t2 (Tile.filled piece)) r3)
(Board.set_tile (Coord.new (Num3.3) (Num3.1)) piece (Board.new r1 r2 (Triple.new t1 t2 t3))) = (Board.new r1 r2 (Triple.new (Tile.filled piece) t2 t3))
(Board.set_tile (Coord.new (Num3.3) (Num3.2)) piece (Board.new r1 r2 (Triple.new t1 t2 t3))) = (Board.new r1 r2 (Triple.new t1 (Tile.filled piece) t3))
(Board.set_tile (Coord.new (Num3.3) (Num3.3)) piece (Board.new r1 r2 (Triple.new t1 t2 t3))) = (Board.new r1 r2 (Triple.new t1 t2 (Tile.filled piece)))

// Board.get_tile (coord: (Coord)) (board: (Board)) : (Tile)
(Board.get_tile (Coord.new (Num3.1) (Num3.1)) (Board.new (Triple.new t1 t2 t3) r2 r3)) = t1
(Board.get_tile (Coord.new (Num3.1) (Num3.2)) (Board.new (Triple.new t1 t2 t3) r2 r3)) = t2
(Board.get_tile (Coord.new (Num3.1) (Num3.3)) (Board.new (Triple.new t1 t2 t3) r2 r3)) = t3
(Board.get_tile (Coord.new (Num3.2) (Num3.1)) (Board.new r1 (Triple.new t1 t2 t3) r3)) = t1
(Board.get_tile (Coord.new (Num3.2) (Num3.2)) (Board.new r1 (Triple.new t1 t2 t3) r3)) = t2
(Board.get_tile (Coord.new (Num3.2) (Num3.3)) (Board.new r1 (Triple.new t1 t2 t3) r3)) = t3
(Board.get_tile (Coord.new (Num3.3) (Num3.1)) (Board.new r1 r2 (Triple.new t1 t2 t3))) = t1
(Board.get_tile (Coord.new (Num3.3) (Num3.2)) (Board.new r1 r2 (Triple.new t1 t2 t3))) = t2
(Board.get_tile (Coord.new (Num3.3) (Num3.3)) (Board.new r1 r2 (Triple.new t1 t2 t3))) = t3

// Board.winner (board: (Board)) : (Maybe (Piece))
(Board.winner board) = let coords = (List.cons (Triple.new (Pair.new 1 1) (Pair.new 1 2) (Pair.new 1 3)) (List.cons (Triple.new (Pair.new 2 1) (Pair.new 2 2) (Pair.new 2 3)) (List.cons (Triple.new (Pair.new 3 1) (Pair.new 3 2) (Pair.new 3 3)) (List.cons (Triple.new (Pair.new 1 1) (Pair.new 2 1) (Pair.new 3 1)) (List.cons (Triple.new (Pair.new 1 2) (Pair.new 2 2) (Pair.new 3 2)) (List.cons (Triple.new (Pair.new 1 3) (Pair.new 2 3) (Pair.new 3 3)) (List.cons (Triple.new (Pair.new 1 1) (Pair.new 2 2) (Pair.new 3 3)) (List.cons (Triple.new (Pair.new 3 1) (Pair.new 2 2) (Pair.new 1 3)) (List.nil))))))))); let tiles = (List.map coords @c (Board.get_line c board)); let winners = (List.map tiles @t (Board.line_winner t)); (Maybe.first_some winners)

// Board.get_line (coords: (Triple (Pair U60 U60))) (board: (Board)) : (Triple (Tile))
(Board.get_line (Triple.new c1 c2 c3) board) = let c1 = (Coord.from_u60_force c1); let c2 = (Coord.from_u60_force c2); let c3 = (Coord.from_u60_force c3); let t1 = (Board.get_tile c1 board); let t2 = (Board.get_tile c2 board); let t3 = (Board.get_tile c3 board); (Triple.new t1 t2 t3)

// Board.line_winner (line: (Triple (Tile))) : (Maybe (Piece))
(Board.line_winner (Triple.new t1 t2 t3)) = (Bool.if (Bool.and (Bool.and (Tile.is_x t1) (Tile.is_x t2)) (Tile.is_x t3)) (Maybe.some (Piece.x)) (Bool.if (Bool.and (Bool.and (Tile.is_o t1) (Tile.is_o t2)) (Tile.is_o t3)) (Maybe.some (Piece.o)) (Maybe.none)))

// Maybe.first_some -(t: Type) (xs: (List (Maybe t))) : (Maybe t)
(Maybe.first_some (List.cons x xs)) = (Maybe.or x (Maybe.first_some xs))
(Maybe.first_some (List.nil)) = (Maybe.none)

// Board.show (board: (Board)) : (String)
(Board.show (Board.new (Triple.new t11 t12 t13) (Triple.new t21 t22 t23) (Triple.new t31 t32 t33))) = (String.flatten (List.cons " " (List.cons (Tile.show t11) (List.cons " | " (List.cons (Tile.show t12) (List.cons " | " (List.cons (Tile.show t13) (List.cons " " (List.cons (String.new_line) (List.cons "-----------" (List.cons (String.new_line) (List.cons " " (List.cons (Tile.show t21) (List.cons " | " (List.cons (Tile.show t22) (List.cons " | " (List.cons (Tile.show t23) (List.cons " " (List.cons (String.new_line) (List.cons "-----------" (List.cons (String.new_line) (List.cons " " (List.cons (Tile.show t31) (List.cons " | " (List.cons (Tile.show t32) (List.cons " | " (List.cons (Tile.show t33) (List.cons " " (List.cons (String.new_line) (List.nil))))))))))))))))))))))))))))))

// Coord.from_u60 (coord: (Pair U60 U60)) : (Maybe (Coord))
(Coord.from_u60 (Pair.new 1 1)) = (Maybe.some (Coord.new (Num3.1) (Num3.1)))
(Coord.from_u60 (Pair.new 1 2)) = (Maybe.some (Coord.new (Num3.1) (Num3.2)))
(Coord.from_u60 (Pair.new 1 3)) = (Maybe.some (Coord.new (Num3.1) (Num3.3)))
(Coord.from_u60 (Pair.new 2 1)) = (Maybe.some (Coord.new (Num3.2) (Num3.1)))
(Coord.from_u60 (Pair.new 2 2)) = (Maybe.some (Coord.new (Num3.2) (Num3.2)))
(Coord.from_u60 (Pair.new 2 3)) = (Maybe.some (Coord.new (Num3.2) (Num3.3)))
(Coord.from_u60 (Pair.new 3 1)) = (Maybe.some (Coord.new (Num3.3) (Num3.1)))
(Coord.from_u60 (Pair.new 3 2)) = (Maybe.some (Coord.new (Num3.3) (Num3.2)))
(Coord.from_u60 (Pair.new 3 3)) = (Maybe.some (Coord.new (Num3.3) (Num3.3)))
(Coord.from_u60 coord) = (Maybe.none)

// Coord.from_u60_force (coord: (Pair U60 U60)) : (Coord)
(Coord.from_u60_force coord) = (Maybe.default (Coord.from_u60 coord) (Coord.new (Num3.1) (Num3.1)))

// Coord.read (input: (String)) : (Maybe (Coord))
(Coord.read input) = let split_input = (String.split input " "); let num_parser = @code (Parser.run (Parser.u60_decimal) code); let maybe_nums = (List.map split_input num_parser); let num_extract = @n (Either.left_or n 0); let nums = (List.map maybe_nums num_extract); let row = (Maybe.default (List.at nums (Nat.zero)) 0); let col = (Maybe.default (List.at nums (Nat.one)) 0); let maybe_coord = (Coord.from_u60 (Pair.new row col)); let parse_ok = (List.all maybe_nums @e (Either.is_left e)); let is_len2 = (Nat.equal (List.length nums) (Nat.two)); (Bool.if (Bool.and parse_ok is_len2) maybe_coord (Maybe.none))

// State.get_turn (state: (State)) : U60
(State.get_turn (State.new turn board)) = turn

// State.empty : (State)
(State.empty) = (State.new 0 (Board.new (Triple.new (Tile.empty) (Tile.empty) (Tile.empty)) (Triple.new (Tile.empty) (Tile.empty) (Tile.empty)) (Triple.new (Tile.empty) (Tile.empty) (Tile.empty))))

// State.show (state: (State)) : (String)
(State.show (State.new turn board)) = let turn_str = (String.concat "Turn: " ((U60.show turn) "")); let player_str = (String.concat "Next: " (Piece.show (State.next_piece (State.new turn board)))); let board_str = (Board.show board); (String.intercalate (String.new_line) (List.cons (String.new_line) (List.cons turn_str (List.cons player_str (List.cons board_str (List.nil))))))

// State.is_move_valid (coord: (Coord)) (state: (State)) : (Bool)
(State.is_move_valid coord (State.new turn board)) = let tile = (Board.get_tile coord board); (Bool.not (Tile.is_empty tile))

// State.next_piece (state: (State)) : (Piece)
(State.next_piece (State.new turn x0_)) = (Bool.if (U60.is_even turn) (Piece.x) (Piece.o))

// State.do_move (coord: (Coord)) (state: (State)) : (State)
(State.do_move coord (State.new turn board)) = let next_piece = (State.next_piece (State.new turn board)); let board = (Board.set_tile coord next_piece board); let turn = (+ 1 turn); (State.new turn board)

// State.get_tile (coord: (Coord)) (state: (State)) : (Tile)
(State.get_tile coord (State.new turn board)) = (Board.get_tile coord board)

// State.winner (state: (State)) : (Maybe (Piece))
(State.winner (State.new turn board)) = (Board.winner board)

// Main : (IO (Unit))
(Main) = let state = (State.empty); (IO.bind (IO.output (State.show state)) @_ (TicTacToe.play state))

// TicTacToe.play (state: (State)) : (IO (Unit))
(TicTacToe.play state) = (IO.bind (IO.output "Where will you place the next piece? ") @_ (IO.bind (IO.input) @line let coord = (Coord.read line); (IO.bind (Maybe.match coord (IO.bind (IO.output "Invalid entry") @_ (IO.pure state)) @coord.value let is_available = (Tile.is_empty (State.get_tile coord.value state)); (Bool.if is_available let state = (State.do_move coord.value state); (IO.pure state) (IO.bind (IO.output "You cannot play there!") @_ (IO.pure state)))) @state (IO.bind (IO.output (State.show state)) @_ let winner = (State.winner state); (Maybe.match winner (Bool.if (U60.equal (State.get_turn state) 9) (IO.bind (IO.output (String.new_line)) @_ (IO.bind (IO.output "Draw!") @_ (IO.pure (Unit.new)))) (TicTacToe.play state)) @winner.value (IO.bind (IO.output (String.new_line)) @_ let win_str = (String.concat (Piece.show winner.value) " wins!"); (IO.bind (IO.output win_str) @_ (IO.pure (Unit.new)))))))))

// IO.output (text: (String)) : (IO U60)
(IO.output text) = (IO.do_output text @x (IO.done x))

// String.intercalate (sep: (String)) (xs: (List (String))) : (String)
(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))

// String.flatten (xs: (List (String))) : (String)
(String.flatten (List.nil)) = ""
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))

// String.concat (xs: (String)) (ys: (String)) : (String)
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
(String.concat "" ys) = ys

// List.intersperse -(a: Type) (sep: a) (xs: (List a)) : (List a)
(List.intersperse sep (List.nil)) = (List.nil)
(List.intersperse sep (List.cons xh (List.nil))) = (List.pure xh)
(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))

// List.pure -(t: Type) (x: t) : (List t)
(List.pure x) = (List.cons x (List.nil))

// String.split (str: (String)) (find: (String)) : (List (String))
(String.split str find) = (String.split.go str find "")

// String.split.go (str: (String)) (find: (String)) (last: (String)) : (List (String))
(String.split.go "" find last) = (List.pure last)
(String.split.go (String.cons x xs) find last) = let str = (String.cons x xs); (Bool.if (String.starts_with str find) let len = (String.length find); let drop = (String.drop len str); let tail = (String.split.go drop find ""); (List.cons last tail) let next = (String.pure x); (String.split.go xs find (String.concat last next)))

// String.starts_with (str: (String)) (pre: (String)) : (Bool)
(String.starts_with str "") = (Bool.true)
(String.starts_with "" (String.cons pre.head pre.tail)) = (Bool.false)
(String.starts_with (String.cons str.head str.tail) (String.cons pre.head pre.tail)) = let head = (U60.equal str.head pre.head); let tail = (String.starts_with str.tail pre.tail); (Bool.and head tail)

// U60.equal (a: U60) (b: U60) : (Bool)
(U60.equal a b) = (U60.to_bool (== a b))

// U60.to_bool (n: U60) : (Bool)
(U60.to_bool 0) = (Bool.false)
(U60.to_bool n) = (Bool.true)

// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
(Bool.and (Bool.true) b) = b
(Bool.and (Bool.false) b) = (Bool.false)

// String.length (xs: (String)) : (Nat)
(String.length "") = (Nat.zero)
(String.length (String.cons x xs)) = (Nat.succ (String.length xs))

// String.pure (x: (Char)) : (String)
(String.pure x) = (String.cons x "")

// Char : Type
(Char) = 0

// Bool.if -(a: Type) (b: (Bool)) (t: a) (f: a) : a
(Bool.if (Bool.true) t f) = t
(Bool.if (Bool.false) t f) = f

// String.drop (n: (Nat)) (xs: (String)) : (String)
(String.drop (Nat.zero) xs) = xs
(String.drop (Nat.succ np) "") = ""
(String.drop (Nat.succ np) (String.cons h t)) = (String.drop np t)

// String.new_line : (String)
(String.new_line) = (String.pure (Char.newline))

// Char.newline : (Char)
(Char.newline) = 10

// Maybe.default -(a: Type) (m: (Maybe a)) (dflt: a) : a
(Maybe.default (Maybe.none) dflt) = dflt
(Maybe.default (Maybe.some val) dflt) = val

// Maybe.or -(t: Type) (a: (Maybe t)) (b: (Maybe t)) : (Maybe t)
(Maybe.or (Maybe.none) b) = b
(Maybe.or a b) = a

// Either.is_left -(l: Type) -(r: Type) (x: (Either l r)) : (Bool)
(Either.is_left (Either.left val)) = (Bool.true)
(Either.is_left (Either.right val)) = (Bool.false)

// Parser.run -(r: Type) (prs: (Parser r)) (code: (String)) : (Either r (Parser.Error))
(Parser.run prs code) = let state = (Parser.State.new code "" 0); (Parser.Result.match (prs state) @res.state @res.result (Either.left res.result) @res.state @res.error (Either.right res.error))

// Parser (r: Type) : Type
(Parser r) = 0

// Parser.Result.match -(r: Type) (x: (Parser.Result r)) -(p: (x: (Parser.Result r)) Type) (done: (state: (Parser.State)) (result: r) (p (Parser.Result.done r state result))) (fail: (state: (Parser.State)) (error: (Parser.Error)) (p (Parser.Result.fail r state error))) : (p x)
(Parser.Result.match (Parser.Result.done state_ result_) done fail) = ((done state_) result_)
(Parser.Result.match (Parser.Result.fail state_ error_) done fail) = ((fail state_) error_)

// IO.input : (IO (String))
(IO.input) = (IO.do_input @x (IO.done x))

// IO.pure -(a: Type) (val: a) : (IO a)
(IO.pure val) = (IO.done val)

// Maybe.match -(t: Type) (x: (Maybe t)) -(p: (x: (Maybe t)) Type) (none: (p (Maybe.none t))) (some: (value: t) (p (Maybe.some t value))) : (p x)
(Maybe.match (Maybe.none) none some) = none
(Maybe.match (Maybe.some value_) none some) = (some value_)

// Nat.two : (Nat)
(Nat.two) = (Nat.succ (Nat.succ (Nat.zero)))

// Parser.u60_decimal : (Parser U60)
(Parser.u60_decimal) = let f = @str (U60.read_decimal str); let prs = (Parser.take_while1 @c (Char.is_decimal c)); let prs = (Parser.fail_on_none (Parser.map f prs)); (Parser.expecting prs "decimal number")

// Parser.take_while1 (cond: (_: (Char)) (Bool)) : (Parser (String))
(Parser.take_while1 cond) = (Parser.bind (Parser.take_while cond) @r (String.match r (Parser.empty) @r.head @r.tail (Parser.pure (String.cons r.head r.tail))))

// Parser.bind -(a: Type) -(b: Type) (pa: (Parser a)) (pb: (_: a) (Parser b)) : (Parser b)
(Parser.bind pa pb) = @state let ra = (pa state); (Parser.Result.match ra @ra.state @ra.result ((pb ra.result) ra.state) @ra.state @ra.error (Parser.Result.fail ra.state ra.error))

// Parser.pure -(r: Type) (value: r) : (Parser r)
(Parser.pure value) = @state (Parser.Result.done state value)

// String.match (x: (String)) -(p: (x: (String)) Type) (nil: (p "")) (cons: (head: U60) (tail: (String)) (p (String.cons head tail))) : (p x)
(String.match "" nil cons) = nil
(String.match (String.cons head_ tail_) nil cons) = ((cons head_) tail_)

// Parser.empty -(a: Type) : (Parser a)
(Parser.empty) = (Parser.bind (Parser.get_index) @index (Parser.fail "" index index))

// Parser.get_index : (Parser U60)
(Parser.get_index) = @state (Parser.State.match state @state.left @state.back @state.index let state = (Parser.State.new state.left state.back state.index); (Parser.Result.done state state.index))

// Parser.State.match (x: (Parser.State)) -(p: (x: (Parser.State)) Type) (new: (left: (String)) (back: (String)) (index: U60) (p (Parser.State.new left back index))) : (p x)
(Parser.State.match (Parser.State.new left_ back_ index_) new) = (((new left_) back_) index_)

// Parser.fail -(a: Type) (msg: (String)) (init: U60) (last: U60) : (Parser a)
(Parser.fail msg init last) = @state let error = (Parser.Error.new msg init last); (Parser.Result.fail state error)

// Parser.take_while (cond: (_: (Char)) (Bool)) : (Parser (String))
(Parser.take_while cond) = (Parser.bind (Parser.try (Parser.satisfy cond)) @mh (Maybe.match mh (Parser.pure "") @mh.value (Parser.bind (Parser.take_while cond) @tail (Parser.pure (String.cons mh.value tail)))))

// Parser.try -(a: Type) (prs: (Parser a)) : (Parser (Maybe a))
(Parser.try prs) = @state (Parser.State.match state @state.left @state.back @state.index let init_idx = state.index; let state = (Parser.State.new state.left state.back state.index); (Parser.Result.match (prs state) @r.state @r.result (Parser.Result.done r.state (Maybe.some r.result)) @r.state @r.error (Parser.State.match r.state @r.state.left @r.state.back @r.state.index let n_back = (- r.state.index init_idx); let new_state = (Parser.State.new r.state.left r.state.back r.state.index); let old_state = (Parser.State.backtrack n_back new_state); (Parser.Result.done old_state (Maybe.none)))))

// Parser.State.backtrack (n: U60) (state: (Parser.State)) : (Parser.State)
(Parser.State.backtrack 0 state) = state
(Parser.State.backtrack n (Parser.State.new left "" index)) = (Parser.State.new left "" index)
(Parser.State.backtrack n (Parser.State.new left (String.cons head tail) index)) = let n = (- n 1); let state = (Parser.State.new (String.cons head left) tail (- index 1)); (Parser.State.backtrack n state)

// Parser.satisfy (cond: (_: (Char)) (Bool)) : (Parser (Char))
(Parser.satisfy cond) = @state (Parser.satisfy.go cond state)

// Parser.satisfy.go (cond: (_: (Char)) (Bool)) (state: (Parser.State)) : (Parser.Result (Char))
(Parser.satisfy.go cond (Parser.State.new "" back index)) = let state = (Parser.State.new "" back index); let error = (Parser.Error.new "Unexpected EOF" index index); (Parser.Result.fail state error)
(Parser.satisfy.go cond (Parser.State.new (String.cons head tail) back index)) = let state = (Parser.State.new (String.cons head tail) back index); let state = (Parser.State.forward 1 state); (Parser.satisfy.cond (cond head) state head)

// Parser.satisfy.cond (cond: (Bool)) (state: (Parser.State)) (head: (Char)) : (Parser.Result (Char))
(Parser.satisfy.cond (Bool.true) state head) = (Parser.Result.done state head)
(Parser.satisfy.cond (Bool.false) (Parser.State.new left back index) head) = let state = (Parser.State.new left back index); let error = (Parser.Error.new "" (- index 1) index); (Parser.Result.fail state error)

// Parser.State.forward (n: U60) (state: (Parser.State)) : (Parser.State)
(Parser.State.forward 0 state) = state
(Parser.State.forward n (Parser.State.new "" back index)) = (Parser.State.new "" back index)
(Parser.State.forward n (Parser.State.new (String.cons head tail) back index)) = let n = (- n 1); let state = (Parser.State.new tail (String.cons head back) (+ index 1)); (Parser.State.forward n state)

// Parser.expecting -(a: Type) (prs: (Parser a)) (name: (String)) : (Parser a)
(Parser.expecting prs name) = @state (Parser.State.match state @state.left @state.back @state.index let state = (Parser.State.new state.left state.back state.index); let init = state.index; (Parser.Result.match (prs state) @r.state @r.result (Parser.Result.done r.state r.result) @r.state @r.error let msg = (String.concat "Expected " name); (Parser.Error.match r.error @r.error.msg @r.error.init @r.error.last let last = r.error.last; let error = (Parser.Error.new msg init last); (Parser.Result.fail r.state error))))

// Parser.Error.match (x: (Parser.Error)) -(p: (x: (Parser.Error)) Type) (new: (msg: (String)) (init: U60) (last: U60) (p (Parser.Error.new msg init last))) : (p x)
(Parser.Error.match (Parser.Error.new msg_ init_ last_) new) = (((new msg_) init_) last_)

// Char.is_decimal (c: (Char)) : (Bool)
(Char.is_decimal c) = (Char.between 48 c 57)

// Char.between (a: (Char)) (b: (Char)) (c: (Char)) : (Bool)
(Char.between a b c) = (U60.between a b c)

// U60.between (small: U60) (val: U60) (big: U60) : (Bool)
(U60.between small val big) = (U60.to_bool (& (<= small val) (< val big)))

// U60.read_decimal (xs: (String)) : (Maybe U60)
(U60.read_decimal "") = (Maybe.some 0)
(U60.read_decimal (String.cons x xs)) = (Maybe.bind (Char.to_decimal x) @digit (Maybe.bind (U60.read_decimal xs) @tail (Maybe.pure (+ (* 10 tail) digit))))

// Maybe.bind -(a: Type) -(b: Type) (ma: (Maybe a)) (mb: (_: a) (Maybe b)) : (Maybe b)
(Maybe.bind (Maybe.none) mb) = (Maybe.none)
(Maybe.bind (Maybe.some val) mb) = (mb val)

// Maybe.pure -(a: Type) (x: a) : (Maybe a)
(Maybe.pure x) = (Maybe.some x)

// Char.to_decimal (c: (Char)) : (Maybe U60)
(Char.to_decimal c) = (Bool.if (Char.is_decimal c) (Maybe.some (- c 48)) (Maybe.none))

// Parser.map -(a: Type) -(b: Type) (f: (_: a) b) (prs: (Parser a)) : (Parser b)
(Parser.map f prs) = (Parser.bind prs @r (Parser.pure (f r)))

// Parser.fail_on_none -(a: Type) (prs: (Parser (Maybe a))) : (Parser a)
(Parser.fail_on_none prs) = (Parser.bind prs @ma (Maybe.match ma (Parser.empty) @ma.value (Parser.pure ma.value)))

// List.map -(a: Type) -(b: Type) (xs: (List a)) (f: (_: a) b) : (List b)
(List.map (List.nil) f) = (List.nil)
(List.map (List.cons head tail) f) = (List.cons (f head) (List.map tail f))

// U60.show (n: U60) : (Show)
(U60.show 0) = @str (String.cons 48 str)
(U60.show n) = @str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) @h h @h ((U60.show (/ n 10)) h)); (func next)

// Show : Type
(Show) = 0

// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
(U60.if 0 t f) = f
(U60.if n t f) = t

// Either.left_or -(l: Type) -(r: Type) (either: (Either l r)) (or: l) : l
(Either.left_or (Either.left val) or) = val
(Either.left_or (Either.right val) or) = or

// Nat.equal (n: (Nat)) (m: (Nat)) : (Bool)
(Nat.equal (Nat.zero) (Nat.zero)) = (Bool.true)
(Nat.equal (Nat.succ n) (Nat.succ m)) = (Nat.equal n m)
(Nat.equal n m) = (Bool.false)

// List.all -(a: Type) (xs: (List a)) (cond: (_: a) (Bool)) : (Bool)
(List.all (List.nil) cond) = (Bool.true)
(List.all (List.cons head tail) cond) = (Bool.if (cond head) (List.all tail cond) (Bool.false))

// IO.bind -(a: Type) -(b: Type) (io: (IO a)) (cont: (_: a) (IO b)) : (IO b)
(IO.bind (IO.done val) next) = (next val)
(IO.bind (IO.do_input cont) next) = (IO.do_input @x (IO.bind (cont x) next))
(IO.bind (IO.do_output text cont) next) = (IO.do_output text @x (IO.bind (cont x) next))
(IO.bind (IO.do_load key cont) next) = (IO.do_load key @x (IO.bind (cont x) next))
(IO.bind (IO.do_store key val cont) next) = (IO.do_store key val @x (IO.bind (cont x) next))

// Nat.one : (Nat)
(Nat.one) = (Nat.succ (Nat.zero))

// List.length -(a: Type) (xs: (List a)) : (Nat)
(List.length (List.nil)) = (Nat.zero)
(List.length (List.cons head tail)) = (Nat.succ (List.length tail))

// U60.is_even (n: U60) : (Bool)
(U60.is_even n) = (Bool.not (U60.is_odd n))

// U60.is_odd (n: U60) : (Bool)
(U60.is_odd n) = (U60.to_bool (& n 1))

// Bool.not (a: (Bool)) : (Bool)
(Bool.not (Bool.true)) = (Bool.false)
(Bool.not (Bool.false)) = (Bool.true)

// List.at -(a: Type) (xs: (List a)) (idx: (Nat)) : (Maybe a)
(List.at (List.nil) idx) = (Maybe.none)
(List.at (List.cons head tail) (Nat.zero)) = (Maybe.some head)
(List.at (List.cons head tail) (Nat.succ pred)) = (List.at tail pred)