Munching squares: Difference between revisions
→{{header|AWK}}
Line 65:
end XorPattern;</syntaxhighlight>
{{out}} [[Image:AdaXorPattern.png|Ada Output|200px]]
=={{header|ATS}}==
<syntaxhighlight lang="ats">
#include "share/atspre_staload.hats"
(* uint2uchar0 seems to have a definition in the prelude, but no
implementation. Such incompletenesses are common, but usually
easily overcome. Here I simply redefine uint2uchar0 locally,
letting C do the casting. *)
extern castfn uint2uchar0 : uint -<> uchar
(* write_pam writes a Portable Arbitrary Map to standard output. It
XORs the positions of colors in a palette of size equal to a power
of two, containing RGB colors in the usual hex format. The palette
is otherwise arbitrary. *)
fn
write_pam {expnt : nat}
{numcolors : nat}
(* The palette size must be proven to be a power of two. *)
(pf : EXP2 (expnt, numcolors) |
palette : &array (uint, numcolors),
numcolors : uint numcolors) : void =
let
fun
loop {x, y : nat | x <= numcolors; y <= numcolors}
.<numcolors - y, numcolors - x>.
(palette : &array (uint, numcolors),
x : uint x,
y : uint y) : void =
if y = numcolors then
()
else if x = numcolors then
loop (palette, 0u, succ y)
else
let
val i = g1ofg0 (x lxor y)
(* Prove that the index is non-negative. *)
prval () = lemma_g1uint_param i
(* Test that the index is not out of bounds high. This could
be proven without a runtime check, but doing that is left
as an exercise for the very, very advanced reader. For
one thing, you will need a more complicated version of
lxor. You will likely want to use an external constraint
solver, as well, or at least a reasonable set of
axioms. *)
val () = assertloc (i < numcolors)
val color = palette[i]
val r = uint2uchar0 (color >> 16)
and g = uint2uchar0 ((color >> 8) land 0xFFu)
and b = uint2uchar0 (color land 0xFFu)
in
print! (r, g, b);
loop (palette, succ x, y)
end
in
println! ("P7");
println! ("WIDTH ", numcolors);
println! ("HEIGHT ", numcolors);
println! ("DEPTH 3");
println! ("MAXVAL 255");
println! ("TUPLTYPE RGB");
println! ("ENDHDR");
loop (palette, 0u, 0u)
end
prfn (* Produces a proof that 2**7 = 128. *)
exp2_of_7_is_128 () :<prf> EXP2 (7, 128) =
EXP2ind (EXP2ind (EXP2ind (EXP2ind
(EXP2ind (EXP2ind (EXP2ind (EXP2bas ())))))))
implement
main0 () =
let
(* 128 RGB colors borrowed from
https://github.com/yeun/open-color *)
var palette : array (uint, 128) =
@[uint][128]
(0xe9ecefu, 0xdee2e6u, 0xced4dau, 0xadb5bdu, 0x868e96u, 0x495057u,
0x343a40u, 0x212529u, 0xfff5f5u, 0xffe3e3u, 0xffc9c9u, 0xffa8a8u,
0xff8787u, 0xff6b6bu, 0xfa5252u, 0xf03e3eu, 0xe03131u, 0xc92a2au,
0xfff0f6u, 0xffdeebu, 0xfcc2d7u, 0xfaa2c1u, 0xf783acu, 0xf06595u,
0xe64980u, 0xd6336cu, 0xc2255cu, 0xa61e4du, 0xf8f0fcu, 0xf3d9fau,
0xeebefau, 0xe599f7u, 0xda77f2u, 0xcc5de8u, 0xbe4bdbu, 0xae3ec9u,
0x9c36b5u, 0x862e9cu, 0xf3f0ffu, 0xe5dbffu, 0xd0bfffu, 0xb197fcu,
0x9775fau, 0x845ef7u, 0x7950f2u, 0x7048e8u, 0x6741d9u, 0x5f3dc4u,
0xedf2ffu, 0xdbe4ffu, 0xbac8ffu, 0x91a7ffu, 0x748ffcu, 0x5c7cfau,
0x4c6ef5u, 0x4263ebu, 0x3b5bdbu, 0x364fc7u, 0xe7f5ffu, 0xd0ebffu,
0xa5d8ffu, 0x74c0fcu, 0x4dabf7u, 0x339af0u, 0x228be6u, 0x1c7ed6u,
0x1971c2u, 0x1864abu, 0xe3fafcu, 0xc5f6fau, 0x99e9f2u, 0x66d9e8u,
0x3bc9dbu, 0x22b8cfu, 0x15aabfu, 0x1098adu, 0x0c8599u, 0x0b7285u,
0xe6fcf5u, 0xc3fae8u, 0x96f2d7u, 0x63e6beu, 0x38d9a9u, 0x20c997u,
0x12b886u, 0x0ca678u, 0x099268u, 0x087f5bu, 0xebfbeeu, 0xd3f9d8u,
0xb2f2bbu, 0x8ce99au, 0x69db7cu, 0x51cf66u, 0x40c057u, 0x37b24du,
0x2f9e44u, 0x2b8a3eu, 0xf4fce3u, 0xe9fac8u, 0xd8f5a2u, 0xc0eb75u,
0xa9e34bu, 0x94d82du, 0x82c91eu, 0x74b816u, 0x66a80fu, 0x5c940du,
0xfff9dbu, 0xfff3bfu, 0xffec99u, 0xffe066u, 0xffd43bu, 0xfcc419u,
0xfab005u, 0xf59f00u, 0xf08c00u, 0xe67700u, 0xfff4e6u, 0xffe8ccu,
0xffd8a8u, 0xffc078u, 0xffa94du, 0xff922bu, 0xfd7e14u, 0xf76707u,
0xe8590cu, 0xd9480fu)
in
write_pam (exp2_of_7_is_128 () | palette, 128u)
end
</syntaxhighlight>
Here I use Netpbm to make a PNG, but you could use, for instance, ImageMagick instead. (Then I generally run my PNGs through optipng before posting them.)
<pre>patscc -std=gnu2x -g -O2 munching_squares.dats && ./a.out | pamtopng > image.png</pre>
{{out}}
[[File:Munching squares ATS.png|alt=A geometric mosaic in 128 arbitrarily chosen colors.]]
=={{header|AWK}}==
| |||