mirror of
https://github.com/sharkdp/bat
synced 2024-12-18 00:03:05 +00:00
68 lines
2.1 KiB
Text
68 lines
2.1 KiB
Text
import data.matrix.notation
|
||
import data.vector2
|
||
|
||
/-!
|
||
|
||
Helpers that don't currently fit elsewhere...
|
||
|
||
-/
|
||
|
||
lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
|
||
p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
|
||
|
||
-- For `playfield`s, the piece type and/or piece index type.
|
||
variables (X : Type*)
|
||
variables [has_repr X]
|
||
|
||
namespace chess.utils
|
||
|
||
section repr
|
||
|
||
/--
|
||
An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
|
||
for `option`, and rather, output just the value in the `some` and a custom provided
|
||
`string` for `none`.
|
||
-/
|
||
structure option_wrapper :=
|
||
(val : option X)
|
||
(none_s : string)
|
||
|
||
instance wrapped_option_repr : has_repr (option_wrapper X) :=
|
||
⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
|
||
|
||
variables {X}
|
||
/--
|
||
Construct an `option_wrapper` term from a provided `option X` and the `string`
|
||
that will override the `has_repr.repr` for `none`.
|
||
-/
|
||
def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
|
||
|
||
-- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
|
||
variables {m' n' : ℕ}
|
||
|
||
/--
|
||
For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
|
||
the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
|
||
This definition is used for displaying rows of the playfield, when it is defined
|
||
via a `matrix`, likely through notation.
|
||
-/
|
||
def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
|
||
λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
|
||
|
||
instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
|
||
|
||
/--
|
||
For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
|
||
we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
|
||
This definition is used for displaying the playfield, when it is defined
|
||
via a `matrix`, likely through notation.
|
||
-/
|
||
def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
|
||
λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
|
||
|
||
instance matrix_repr_instance :
|
||
has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
|
||
|
||
end repr
|
||
|
||
end chess.utils
|