Created
November 3, 2022 13:50
-
-
Save developedby/cd2a02cb05640178d4856e780a35eed4 to your computer and use it in GitHub Desktop.
CLI Tictactoe for HVM
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment