text:
module Bautzen.Game.Map

import Bautzen.Terrain
import Bautzen.GameUnit

import Data.Nat
import Data.Vect
import Data.List

V : Terrain -> Terrain
V = Village

Wd  : Terrain
Wd = Wood

Cl  : Terrain
Cl = Clear

Rg  : Terrain
Rg = Rough

RW  : Terrain
RW = RoughWood

H : Terrain -> Terrain
H = Hill

SA : Terrain -> Terrain
SA = SupplySource Allies

SX : Terrain -> Terrain
SX = SupplySource Axis

T : Terrain
T = Town

N : Terrain
N = Clear

A : Side
A = Allies

Rd : Connection -> Connection
Rd = Road

Rv : Connection -> Connection
Rv = Road

Pl : Connection
Pl = Plain

Lk : Connection
Lk = Lake

terrains : Vect 13 (Vect 23 Terrain)
terrains = [-- 01      02     03          04    05     06     07     08     09      10     11     12     13     14         15     16     17     18      19     20          21    22      23
 {- 01 -}    [ Cl    , Wd   , Cl        , Wd  , Wd   , V Cl , Cl   , Wd    , Cl   , Wd   , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , Wd    , Cl   , SA (V Wd) , Cl   , Wd   , Cl    ]
 {- 02 -}  , [ Wd    , Wd   , Wd        , Wd  , Wd   , Wd   , Wd   , Wd    , Wd   , V Wd , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , V Wd  , Wd   , V Wd      , V Wd , Wd   , Wd    ]
 {- 03 -}  , [ Wd    , Wd   , Wd        , Wd  , Wd   , Cl   , V Wd , Wd    , Wd   , Cl   , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , Wd    , Wd   , Wd        , Wd   , Wd   , Cl    ]
 {- 04 -}  , [ SX Wd , Cl   , Wd        , Wd  , Wd   , Cl   , V Cl , Cl    , Cl   , V Cl , Cl   , Cl   , V Wd , Wd       , V Wd , Wd   , V Wd , Cl    , Cl   , Cl        , V Cl , Cl   , Cl    ]
 {- 05 -}  , [ Cl    , Wd   , Wd        , Cl  , Cl   , Cl   , Cl   , Cl    , Cl   , Cl   , Cl   , Cl   , Cl   , Cl       , Wd   , Wd   , Wd   , Wd    , V Cl , Cl        , Cl   , Cl   , SA Cl ]
 {- 06 -}  , [ Cl    , Wd   , Wd        , Cl  , Cl   , Cl   , V Cl , Cl    , Cl   , H RW , RW   , Wd   , RW   , H (V RW) , Cl   , V Wd , Wd   , Wd    , V Wd , Wd        , Cl   , T    , SA Cl ]
 {- 07 -}  , [ SX Wd , Wd   , V Wd      , H Rg, Cl   , Cl   , H Rg , T     , Cl   , Cl   , RW   , V Cl , Cl   , V Cl     , Wd   , Cl   , Cl   , Wd    , Cl   , Wd        , V Cl , V Cl , Cl    ]
 {- 08 -}  , [ Wd    , RW   , Wd        , RW  , Cl   , Cl   , V Cl , Rg    , V Cl , Cl   , V Cl , Cl   , Cl   , Cl       , Cl   , Cl   , V Cl , Cl    , Cl   , Cl        , V Cl , Cl   , Cl    ]
 {- 09 -}  , [ Cl    , Rg   , Wd        , Rg  , Cl   , Wd   , Cl   , H RW  , Wd   , V Cl , Cl   , V Cl , Cl   , T        , Cl   , Cl   , Cl   , Cl    , V Cl , Cl        , Cl   , Cl   , Cl    ]
 {- 10 -}  , [ SX Wd , V Cl , V Cl      , Wd  , V Cl , Cl   , Wd   , Cl    , V Rg , Rg   , Wd   , Cl   , Cl   , Cl       , T    , Cl   , Cl   , Cl    , V Cl , Cl        , Cl   , Cl   , Cl    ]
 {- 11 -}  , [ Wd    , V Wd , Cl        , Cl  , Wd   , Cl   , Cl   , Cl    , T    , H Rg , Cl   , RW   , RW   , Rg       , Cl   , H RW , RW   , H Rg  , Cl   , Cl        , Cl   , V Cl , Cl    ]
 {- 12 -}  , [ Wd    , Wd   , V Wd      , Wd  , Cl   , Cl   , Rg   , SX Rg , Rg   , Cl   , RW   , Cl   , Rg   , Cl       , RW   , Cl   , Cl   , SX Cl , T    , Cl        , Cl   , Cl   , Cl    ]
 {- 13 -}  , [ T     , N    , SX (V Cl) , N   , Cl   , N    , Cl   , N     , Cl   , N    , Cl   , N    , Cl   , N        , Cl   , N    , Cl   , N     , Cl   , N         , Cl   , N    , Cl    ]
           ]

links : List (Pos, List (Pos, Connection))
links = [
  (hex 00 00, [(hex 01 00, Pl), (hex 00 01, Pl)]),
  (hex 00 01, [(hex 00 00, Pl), (hex 01 00, Pl), (hex 01 01, Pl), (hex 00 02, Pl)]),
  (hex 00 02, [(hex 00 01, Pl), (hex 01 01, Rd Pl), (hex 01 02, Pl), (hex 00 03, Rd Pl)]),
  (hex 00 03, [(hex 00 02, Rd Pl), (hex 01 02, Pl), (hex 01 03, Rd Pl), (hex 00 04, Pl)]),
  (hex 00 04, [(hex 00 03, Pl), (hex 01 03, Pl), (hex 01 04, Pl), (hex 00 05, Pl)]),
  (hex 00 05, [(hex 00 04, Pl), (hex 01 04, Pl), (hex 01 05, Pl), (hex 00 06, Pl)]),
  (hex 00 06, [(hex 00 05, Pl), (hex 01 05, Rd Pl), (hex 01 06, Pl), (hex 00 07, Pl)]),
  (hex 00 07, [(hex 00 06, Pl), (hex 01 06, Pl), (hex 01 07, Pl), (hex 00 08, Pl)]),
  (hex 00 08, [(hex 00 07, Pl), (hex 01 07, Pl), (hex 01 08, Pl), (hex 00 09, Pl)]),
  (hex 00 09, [(hex 00 08, Pl), (hex 01 08, Pl), (hex 01 09, Rd Pl), (hex 00 10, Pl)]),
  (hex 00 10, [(hex 00 09, Pl), (hex 01 09, Pl), (hex 01 10, Rd Pl), (hex 00 11, Pl)]),
  (hex 00 11, [(hex 00 10, Pl), (hex 01 10, Rd Pl), (hex 01 11, Rd Pl), (hex 00 12, Pl)]),
  (hex 00 12, [(hex 00 11, Pl), (hex 01 11, Rd Pl), (hex 01 12, Pl)]),
  (hex 01 00, [(hex 00 00, Pl), (hex 02 00, Pl), (hex 02 01, Pl), (hex 01 01, Pl), (hex 00 01, Pl)]),
  (hex 01 01, [(hex 00 01, Pl), (hex 01 00, Pl), (hex 02 01, Rd Pl), (hex 02 02, Pl), (hex 01 02, Pl), (hex 00 02, Rd Pl)]),
  (hex 01 02, [(hex 00 02, Pl), (hex 01 01, Pl), (hex 02 02, Pl), (hex 02 03, Pl), (hex 01 03, Pl), (hex 00 03, Pl)]),
  (hex 01 03, [(hex 00 03, Rd Pl), (hex 01 02, Pl), (hex 02 03, Rd Pl), (hex 02 04, Pl), (hex 01 04, Pl), (hex 00 04, Pl)]),
  (hex 01 04, [(hex 00 04, Pl), (hex 01 03, Pl), (hex 02 04, Pl), (hex 02 05, Pl), (hex 01 05, Pl), (hex 00 05, Pl)]),
  (hex 01 05, [(hex 00 05, Pl), (hex 01 04, Pl), (hex 02 05, Pl), (hex 02 06, Rd Pl), (hex 01 06, Pl), (hex 00 06, Rd Pl)]),
  (hex 01 06, [(hex 00 06, Pl), (hex 01 05, Pl), (hex 02 06, Pl), (hex 02 07, Pl), (hex 01 07, Pl), (hex 00 07, Pl)]),
  (hex 01 07, [(hex 00 07, Pl), (hex 01 06, Pl), (hex 02 07, Pl), (hex 02 08, Pl), (hex 01 08, Pl), (hex 00 08, Pl)]),
  (hex 01 08, [(hex 00 08, Pl), (hex 01 07, Pl), (hex 02 08, Pl), (hex 02 09, Pl), (hex 01 09, Pl), (hex 00 09, Pl)]),
  (hex 01 09, [(hex 00 09, Rd Pl), (hex 01 08, Pl), (hex 02 09, Rd Pl), (hex 02 10, Pl), (hex 01 10, Rd Pl), (hex 00 10, Pl)]),
  (hex 01 10, [(hex 00 10, Rd Pl), (hex 01 09, Rd Pl), (hex 02 10, Pl), (hex 02 11, Rd Pl), (hex 01 11, Pl), (hex 00 11, Rd Pl)]),
  (hex 01 11, [(hex 00 11, Rd Pl), (hex 01 10, Pl), (hex 02 11, Pl), (hex 02 12, Pl), (hex 01 12, Pl), (hex 00 12, Rd Pl)]),
  (hex 02 00, [(hex 03 00, Pl), (hex 02 01, Rd Pl), (hex 01 00, Pl)]),
  (hex 02 01, [(hex 01 00, Pl), (hex 02 00, Rd Pl), (hex 03 00, Rd Pl), (hex 03 01, Pl), (hex 02 02, Rd Pl), (hex 01 01, Rd Pl)]),
  (hex 02 02, [(hex 01 01, Pl), (hex 02 01, Rd Pl), (hex 03 01, Pl), (hex 03 02, Rd Pl), (hex 02 03, Pl), (hex 01 02, Pl)]),
  (hex 02 03, [(hex 01 02, Pl), (hex 02 02, Pl), (hex 03 02, Rd Pl), (hex 03 03, Rd Pl), (hex 02 04, Pl), (hex 01 03, Rd Pl)]),
  (hex 02 04, [(hex 01 03, Pl), (hex 02 03, Pl), (hex 03 03, Pl), (hex 03 04, Pl), (hex 02 05, Pl), (hex 01 04, Pl)]),
  (hex 02 05, [(hex 01 04, Pl), (hex 02 04, Pl), (hex 03 04, Rd Pl), (hex 03 05, Pl), (hex 02 06, Rd Pl), (hex 01 05, Pl)]),
  (hex 02 06, [(hex 01 05, Rd Pl), (hex 02 05, Rd Pl), (hex 03 05, Rd Pl), (hex 03 06, Pl), (hex 02 07, Rd Pl), (hex 01 06, Pl)]),
  (hex 02 07, [(hex 01 06, Pl), (hex 02 06, Rd Pl), (hex 03 06, Pl), (hex 03 07, Pl), (hex 02 08, Rd Pl), (hex 01 07, Pl)]),
  (hex 02 08, [(hex 01 07, Pl), (hex 02 07, Rd Pl), (hex 03 07, Pl), (hex 03 08, Pl), (hex 02 09, Rd Pl), (hex 01 08, Pl)]),
  (hex 02 09, [(hex 01 08, Pl), (hex 02 08, Rd Pl), (hex 03 08, Pl), (hex 03 09, Rd Pl), (hex 02 10, Pl), (hex 01 09, Rd Pl)]),
  (hex 02 10, [(hex 01 09, Pl), (hex 02 09, Pl), (hex 03 09, Pl), (hex 03 10, Pl), (hex 02 11, Pl), (hex 01 10, Pl)]),
  (hex 02 11, [(hex 01 10, Rd Pl), (hex 02 10, Pl), (hex 03 10, Rd Pl), (hex 03 11, Pl), (hex 02 12, Rd Pl), (hex 01 11, Pl)]),
  (hex 02 12, [(hex 01 11, Pl), (hex 02 11, Rd Pl), (hex 03 11, Pl), (hex 03 12, Pl), (hex 01 12, Pl)]),
  (hex 03 00, [(hex 02 00, Pl), (hex 04 00, Pl), (hex 04 01, Rd Pl), (hex 03 01, Pl), (hex 02 01, Rd Pl)]),
  (hex 03 01, [(hex 02 01, Pl), (hex 03 00, Pl), (hex 04 01, Pl), (hex 04 02, Pl), (hex 03 02, Pl), (hex 02 02, Pl)]),
  (hex 03 02, [(hex 02 02, Rd Pl), (hex 03 01, Pl), (hex 04 02, Pl), (hex 04 03, Rd Pl), (hex 03 03,Rd Pl), (hex 02 03, Rd Pl)]),
  (hex 03 03, [(hex 02 03, Rd Pl), (hex 03 02, Rd Pl), (hex 04 03, Pl), (hex 04 04, Rd Pl), (hex 03 04, Rd Pl), (hex 02 04, Pl)]),
  (hex 03 04, [(hex 02 04, Pl), (hex 03 03, Rd Pl), (hex 04 04, Rd Pl), (hex 04 05, Rd Pl), (hex 03 05, Pl), (hex 02 05, Rd Pl)]),
  (hex 03 05, [(hex 02 05, Pl), (hex 03 04, Pl), (hex 04 05, Pl), (hex 04 06, Rd Pl), (hex 03 06, Pl), (hex 02 06, Rd Pl)]),
  (hex 03 06, [(hex 02 06, Pl), (hex 03 05, Pl), (hex 04 06, Pl), (hex 04 07, Pl), (hex 03 07, Pl), (hex 02 07, Pl)]),
  (hex 03 07, [(hex 02 07, Pl), (hex 03 06, Pl), (hex 04 07, Pl), (hex 04 08, Pl), (hex 03 08, Pl), (hex 02 08, Pl)]),
  (hex 03 08, [(hex 02 08, Pl), (hex 03 07, Pl), (hex 04 08, Pl), (hex 04 09, Pl), (hex 03 09, Pl), (hex 02 09, Pl)]),
  (hex 03 09, [(hex 02 09, Rd Pl), (hex 03 08, Pl), (hex 04 09, Rd Pl), (hex 04 10, Pl), (hex 03 10, Rd Pl), (hex 02 10, Pl)]),
  (hex 03 10, [(hex 02 10, Pl), (hex 03 09, Rd Pl), (hex 04 10, Pl), (hex 04 11, Rd Pl), (hex 03 11, Pl), (hex 02 11, Rd Pl)]),
  (hex 03 11, [(hex 02 11, Pl), (hex 03 10, Pl), (hex 04 11, Pl), (hex 04 12, Pl), (hex 03 12, Pl), (hex 02 12, Pl)]),
  (hex 04 00, [(hex 05 00, Pl), (hex 04 01, Pl), (hex 03 00, Pl)]),
  (hex 04 01, [(hex 03 00, Rd Pl), (hex 04 00, Pl), (hex 05 00, Rd Pl), (hex 05 01, Pl), (hex 04 02, Pl), (hex 03 01, Pl)]),
  (hex 04 02, [(hex 03 01, Pl), (hex 04 01, Pl), (hex 05 01, Pl), (hex 05 02, Pl), (hex 04 03, Pl), (hex 03 02, Pl)]),
  (hex 04 03, [(hex 03 02, Rd Pl), (hex 04 02, Pl), (hex 05 02, Rd Pl), (hex 05 03, Pl), (hex 04 04, Pl), (hex 03 03, Pl)]),
  (hex 04 04, [(hex 03 03, Rd Pl), (hex 04 03, Pl), (hex 05 03, Rd Pl), (hex 05 04, Rd Pl), (hex 04 05, Pl), (hex 03 04, Rd Pl)]),
  (hex 04 05, [(hex 03 04, Rd Pl), (hex 04 04, Pl), (hex 05 04, Pl), (hex 05 05, Pl), (hex 04 06, Rd Pl), (hex 03 05, Pl)]),
  (hex 04 06, [(hex 03 05, Rd Pl), (hex 04 05, Rd Pl), (hex 05 05, Rd Pl), (hex 05 06, Pl), (hex 04 07, Rd Pl), (hex 03 06, Pl)]),
  (hex 04 07, [(hex 03 06, Pl), (hex 04 06, Rd Pl), (hex 05 06, Pl), (hex 05 07, Rd Pl), (hex 04 08, Pl), (hex 03 07, Pl)]),
  (hex 04 08, [(hex 03 07, Pl), (hex 04 07, Pl), (hex 05 07, Pl), (hex 05 08, Pl), (hex 04 09, Pl), (hex 03 08, Pl)]),
  (hex 04 09, [(hex 03 08, Pl), (hex 04 08, Pl), (hex 05 08, Rd Pl), (hex 05 09, Pl), (hex 04 10, Pl), (hex 03 09, Rd Pl)]),
  (hex 04 10, [(hex 03 09, Pl), (hex 04 09, Pl), (hex 05 09, Pl), (hex 05 10, Pl), (hex 04 11, Pl), (hex 03 10, Pl)]),
  (hex 04 11, [(hex 03 10, Rd Pl), (hex 04 10, Pl), (hex 05 10, Rd Pl), (hex 05 11, Pl), (hex 04 12, Pl), (hex 03 11, Pl)]),
  (hex 04 12, [(hex 03 11, Pl), (hex 04 11, Pl), (hex 05 11, Rd Pl), (hex 05 12, Pl), (hex 03 12, Pl)]),
  (hex 05 00, [(hex 04 00, Pl), (hex 06 00, Pl), (hex 06 01, Rd Pl), (hex 05 01, Pl), (hex 04 01, Rd Pl)]),
  (hex 05 01, [(hex 04 01, Pl), (hex 05 00, Rd Pl), (hex 06 01, Pl), (hex 06 02, Pl), (hex 05 02, Rd Pl), (hex 04 02, Pl)]),
  (hex 05 02, [(hex 04 02, Pl), (hex 05 01, Rd Pl), (hex 06 02, Pl), (hex 06 03, Rd Pl), (hex 05 03, Rd Pl), (hex 04 03, Rd Pl)]),
  (hex 05 03, [(hex 04 03, Pl), (hex 05 02, Rd Pl), (hex 06 03, Rd Pl), (hex 06 04, Rd Pl), (hex 05 04, Pl), (hex 04 04, Rd Pl)]),
  (hex 05 04, [(hex 04 04, Rd Pl), (hex 05 03, Pl), (hex 06 04, Pl), (hex 06 05, Pl), (hex 05 05, Rd Pl), (hex 04 05, Pl)]),
  (hex 05 05, [(hex 04 05, Pl), (hex 05 04, Rd Pl), (hex 06 05, Pl), (hex 06 06, Rd Pl), (hex 05 06, Pl), (hex 04 06, Rd Pl)]),
  (hex 05 06, [(hex 04 06, Pl), (hex 05 05, Pl), (hex 06 06, Pl), (hex 06 07, Pl), (hex 05 07, Pl), (hex 04 07, Pl)]),
  (hex 05 07, [(hex 04 07, Rd Pl), (hex 05 06, Pl), (hex 06 07, Rd Pl), (hex 06 08, Pl), (hex 05 08, Rd Pl), (hex 04 08, Pl)]),
  (hex 05 08, [(hex 04 08, Pl), (hex 05 07, Rd Pl), (hex 06 08, Pl), (hex 06 09, Pl), (hex 05 09, Pl), (hex 04 09, Rd Pl)]),
  (hex 05 09, [(hex 04 09, Pl), (hex 05 08, Pl), (hex 06 09, Pl), (hex 06 10, Pl), (hex 05 10, Pl), (hex 04 10, Pl)]),
  (hex 05 10, [(hex 04 10, Pl), (hex 05 09, Pl), (hex 06 10, Pl), (hex 06 11, Rd Pl), (hex 05 11, Pl), (hex 04 11, Rd Pl)]),
  (hex 05 11, [(hex 04 11, Pl), (hex 05 10, Pl), (hex 06 11, Rd Pl), (hex 06 12, Pl), (hex 05 12, Pl), (hex 04 12, Rd Pl)]),
  (hex 06 00, [(hex 07 00, Rv Pl), (hex 06 01, Pl), (hex 05 00, Pl)]),
  (hex 06 01, [(hex 05 00, Rd Pl), (hex 06 00, Pl), (hex 07 00, Rv Pl), (hex 07 01, Rv (Rd Pl)), (hex 06 02, Pl), (hex 05 01, Pl)]),
  (hex 06 02, [(hex 05 01, Pl), (hex 06 01, Pl), (hex 07 01, Rv Pl), (hex 07 02, Pl), (hex 06 03, Pl), (hex 05 02, Pl)]),
  (hex 06 03, [(hex 05 02, Rd Pl), (hex 06 02, Pl), (hex 07 02, Rd Pl), (hex 07 03, Rd Pl), (hex 06 04, Pl), (hex 05 03, Rd Pl)]),
  (hex 06 04, [(hex 05 03, Rd Pl), (hex 06 03, Pl), (hex 07 03, Pl), (hex 07 04, Pl), (hex 06 05, Rd Pl), (hex 05 04, Pl)]),
  (hex 06 05, [(hex 05 04, Pl), (hex 06 04, Rd Pl), (hex 07 04, Pl), (hex 07 05, Pl), (hex 06 06, Rd Pl), (hex 05 05, Pl)]),
  (hex 06 06, [(hex 05 05, Rd Pl), (hex 06 05, Rd Pl), (hex 07 05, Rd Pl), (hex 07 06, Rd Pl), (hex 06 07, Rd Pl), (hex 05 06, Pl)]),
  (hex 06 07, [(hex 05 06, Pl), (hex 06 06, Rd Pl), (hex 07 06, Pl), (hex 07 07, Pl), (hex 06 08, Pl), (hex 05 07, Rd Pl)]),
  (hex 06 08, [(hex 05 07, Pl), (hex 06 07, Pl), (hex 07 07, Pl), (hex 07 08, Pl), (hex 06 09, Pl), (hex 05 08, Pl)]),
  (hex 06 09, [(hex 05 08, Pl), (hex 06 08, Pl), (hex 07 08, Pl), (hex 07 09, Pl), (hex 06 10, Pl), (hex 05 09, Pl)]),
  (hex 06 10, [(hex 05 09, Pl), (hex 06 09, Pl), (hex 07 09, Pl), (hex 07 10, Pl), (hex 06 11, Pl), (hex 05 10, Pl)]),
  (hex 06 11, [(hex 05 10, Rd Pl), (hex 06 10, Pl), (hex 07 10, Rd Pl), (hex 07 11, Pl), (hex 06 12, Pl), (hex 05 11, Rd Pl)]),
  (hex 06 12, [(hex 05 11, Pl), (hex 06 11, Pl), (hex 07 11, Pl), (hex 07 12, Pl), (hex 05 12, Pl)]),
  (hex 07 00, [(hex 06 00, Rv Pl), (hex 08 00, Pl), (hex 08 01, Pl), (hex 07 01, Pl), (hex 06 01, Rv Pl)]),
  (hex 07 01, [(hex 06 01, Rd (Rv Pl)), (hex 07 00, Pl), (hex 08 01, Pl), (hex 08 02, Rd Pl), (hex 07 02, Rv Pl), (hex 06 02, Rv Pl)]),
  (hex 07 02, [(hex 06 02, Pl), (hex 07 01, Rv Pl), (hex 08 02, Rd (Rv Pl)), (hex 08 03, Pl), (hex 07 03, Pl), (hex 06 03, Rd Pl)]),
  (hex 07 03, [(hex 06 03, Rd Pl), (hex 07 02, Pl), (hex 08 03, Pl), (hex 08 04, Rd Pl), (hex 07 04, Pl), (hex 06 04, Pl)]),
  (hex 07 04, [(hex 06 04, Pl), (hex 07 03, Pl), (hex 08 04, Rd Pl), (hex 08 05, Pl), (hex 07 05, Rd Pl), (hex 06 05, Pl)]),
  (hex 07 05, [(hex 06 05, Pl), (hex 07 04, Rd Pl), (hex 08 05, Pl), (hex 08 06, Rd Pl), (hex 07 06, Lk), (hex 06 06, Rd Pl)]),
  (hex 07 06, [(hex 06 06, Rd Pl), (hex 07 05, Lk), (hex 08 06, Pl), (hex 08 07, Rd Pl), (hex 07 07, Rd Pl), (hex 06 07, Pl)]),
  (hex 07 07, [(hex 06 07, Pl), (hex 07 06, Rd Pl), (hex 08 07, Pl), (hex 08 08, Pl), (hex 07 08, Rd Pl), (hex 06 08, Pl)]),
  (hex 07 08, [(hex 06 08, Pl), (hex 07 07, Rd Pl), (hex 08 08, Pl), (hex 08 09, Rd Pl), (hex 07 09, Rd Pl), (hex 06 09, Pl)]),
  (hex 07 09, [(hex 06 09, Pl), (hex 07 08, Rd Pl), (hex 08 09, Pl), (hex 08 10, Rd Pl), (hex 07 10, Pl), (hex 06 10, Pl)]),
  (hex 07 10, [(hex 06 10, Pl), (hex 07 09, Pl), (hex 08 10, Rd Pl), (hex 08 11, Pl), (hex 07 11, Pl), (hex 06 11, Rd Pl)]),
  (hex 07 11, [(hex 06 11, Pl), (hex 07 10, Pl), (hex 08 11, Rd Pl), (hex 08 12, Pl), (hex 07 12, Pl), (hex 06 12, Pl)]),
  (hex 08 00, [(hex 09 00, Pl), (hex 08 01, Pl), (hex 07 00, Pl)]),
  (hex 08 01, [(hex 07 00, Pl), (hex 08 00, Pl), (hex 09 00, Pl), (hex 09 01, Pl), (hex 08 02, Pl), (hex 07 01, Pl)]),
  (hex 08 02, [(hex 07 01, Rd Pl), (hex 08 01, Pl), (hex 09 01, Rd Pl), (hex 09 02, Pl), (hex 08 03, Rv Pl), (hex 07 02, Rv (Rd Pl))]),
  (hex 08 03, [(hex 07 02, Pl), (hex 08 02, Rv Pl), (hex 09 02, Pl), (hex 09 03, Rd Pl), (hex 08 04, Rd Pl), (hex 07 03, Pl)]),
  (hex 08 04, [(hex 07 03, Rd Pl), (hex 08 03, Rd Pl), (hex 09 03, Pl), (hex 09 04, Pl), (hex 08 05, Lk), (hex 07 04, Rd Pl)]),
  (hex 08 05, [(hex 07 04, Pl), (hex 08 04, Lk), (hex 09 04, Rd Pl), (hex 09 05, Rd Pl), (hex 08 06, Rd Pl), (hex 07 05, Pl)]),
  (hex 08 06, [(hex 07 05, Rd Pl), (hex 08 05, Rd Pl), (hex 09 05, Pl), (hex 09 06, Pl), (hex 08 07, Pl), (hex 07 06, Pl)]),
  (hex 08 07, [(hex 07 06, Rd Pl), (hex 08 06, Pl), (hex 09 06, Rd Pl), (hex 09 07, Rd Pl), (hex 08 08, Pl), (hex 07 07, Pl)]),
  (hex 08 08, [(hex 07 07, Pl), (hex 08 07, Pl), (hex 09 07, Pl), (hex 09 08, Pl), (hex 08 09, Pl), (hex 07 08, Pl)]),
  (hex 08 09, [(hex 07 08, Rd Pl), (hex 08 08, Pl), (hex 09 08, Pl), (hex 09 09, Pl), (hex 08 10, Rd Pl), (hex 07 09, Pl)]),
  (hex 08 10, [(hex 07 09, Rd Pl), (hex 08 09, Rd Pl), (hex 09 09, Rd Pl), (hex 09 10, Pl), (hex 08 11, Rd Pl), (hex 07 10, Rd Pl)]),
  (hex 08 11, [(hex 07 10, Pl), (hex 08 10, Rd Pl), (hex 09 10, Pl), (hex 09 11, Pl), (hex 08 12, Pl), (hex 07 11, Rd Pl)]),
  (hex 08 12, [(hex 07 11, Pl), (hex 08 11, Pl), (hex 09 11, Pl), (hex 09 12, Pl), (hex 07 12, Pl)]),
  --
  (hex 09 00, [(hex 08 00, Pl), (hex 10 00, Pl), (hex 10 01, Pl), (hex 09 01, Pl), (hex 08 01, Pl)]),
  (hex 09 01, [(hex 08 01, Pl), (hex 09 00, Pl), (hex 10 01, Pl), (hex 10 02, Pl), (hex 09 02, Pl), (hex 08 02, Pl)]),
  (hex 09 02, [(hex 08 02, Pl), (hex 09 01, Pl), (hex 10 02, Pl), (hex 10 03, Pl), (hex 09 03, Pl), (hex 08 03, Pl)]),
  (hex 09 03, [(hex 08 03, Pl), (hex 09 02, Pl), (hex 10 03, Pl), (hex 10 04, Pl), (hex 09 04, Pl), (hex 08 04, Pl)]),
  (hex 09 04, [(hex 08 04, Pl), (hex 09 03, Pl), (hex 10 04, Pl), (hex 10 05, Pl), (hex 09 05, Pl), (hex 08 05, Pl)]),
  (hex 09 05, [(hex 08 05, Pl), (hex 09 04, Pl), (hex 10 05, Pl), (hex 10 06, Pl), (hex 09 06, Pl), (hex 08 06, Pl)]),
  (hex 09 06, [(hex 08 06, Pl), (hex 09 05, Pl), (hex 10 06, Pl), (hex 10 07, Pl), (hex 09 07, Pl), (hex 08 07, Pl)]),
  (hex 09 07, [(hex 08 07, Pl), (hex 09 06, Pl), (hex 10 07, Pl), (hex 10 08, Pl), (hex 09 08, Pl), (hex 08 08, Pl)]),
  (hex 09 08, [(hex 08 08, Pl), (hex 09 07, Pl), (hex 10 08, Pl), (hex 10 09, Pl), (hex 09 09, Pl), (hex 08 09, Pl)]),
  (hex 09 09, [(hex 08 09, Pl), (hex 09 08, Pl), (hex 10 09, Pl), (hex 10 10, Pl), (hex 09 10, Pl), (hex 08 10, Pl)]),
  (hex 09 10, [(hex 08 10, Pl), (hex 09 09, Pl), (hex 10 10, Pl), (hex 10 11, Pl), (hex 09 11, Pl), (hex 08 11, Pl)]),
  (hex 09 11, [(hex 08 11, Pl), (hex 09 10, Pl), (hex 10 11, Pl), (hex 10 12, Pl), (hex 09 12, Pl), (hex 08 12, Pl)]),
  (hex 09 12, [(hex 08 12, Pl), (hex 09 11, Pl), (hex 10 12, Pl)]),
  (hex 10 00, [(hex 11 00, Pl), (hex 10 01, Pl), (hex 09 00, Pl)]),
  (hex 10 01, [(hex 09 00, Pl), (hex 10 00, Pl), (hex 11 00, Pl), (hex 11 01, Pl), (hex 10 02, Pl), (hex 09 01, Pl)]),
  (hex 10 02, [(hex 09 01, Pl), (hex 10 01, Pl), (hex 11 01, Pl), (hex 11 02, Pl), (hex 10 03, Pl), (hex 09 02, Pl)]),
  (hex 10 03, [(hex 09 02, Pl), (hex 10 02, Pl), (hex 11 02, Pl), (hex 11 03, Pl), (hex 10 04, Pl), (hex 09 03, Pl)]),
  (hex 10 04, [(hex 09 03, Pl), (hex 10 03, Pl), (hex 11 03, Pl), (hex 11 04, Pl), (hex 10 05, Pl), (hex 09 04, Pl)]),
  (hex 10 05, [(hex 09 04, Pl), (hex 10 04, Pl), (hex 11 04, Pl), (hex 11 05, Pl), (hex 10 06, Pl), (hex 09 05, Pl)]),
  (hex 10 06, [(hex 09 05, Pl), (hex 10 05, Pl), (hex 11 05, Pl), (hex 11 06, Pl), (hex 10 07, Pl), (hex 09 06, Pl)]),
  (hex 10 07, [(hex 09 06, Pl), (hex 10 06, Pl), (hex 11 06, Pl), (hex 11 07, Pl), (hex 10 08, Pl), (hex 09 07, Pl)]),
  (hex 10 08, [(hex 09 07, Pl), (hex 10 07, Pl), (hex 11 07, Pl), (hex 11 08, Pl), (hex 10 09, Pl), (hex 09 08, Pl)]),
  (hex 10 09, [(hex 09 08, Pl), (hex 10 08, Pl), (hex 11 08, Pl), (hex 11 09, Pl), (hex 10 10, Pl), (hex 09 09, Pl)]),
  (hex 10 10, [(hex 09 09, Pl), (hex 10 09, Pl), (hex 11 09, Pl), (hex 11 10, Pl), (hex 10 11, Pl), (hex 09 10, Pl)]),
  (hex 10 11, [(hex 09 10, Pl), (hex 10 10, Pl), (hex 11 10, Pl), (hex 11 11, Pl), (hex 10 12, Pl), (hex 09 11, Pl)]),
  (hex 10 12, [(hex 09 11, Pl), (hex 10 11, Pl), (hex 11 11, Pl), (hex 11 12, Pl), (hex 09 12, Pl)]),
  (hex 11 00, [(hex 10 00, Pl), (hex 12 00, Pl), (hex 12 01, Pl), (hex 11 01, Pl), (hex 10 01, Pl)]),
  (hex 11 01, [(hex 10 01, Pl), (hex 11 00, Pl), (hex 12 01, Pl), (hex 12 02, Pl), (hex 11 02, Pl), (hex 10 02, Pl)]),
  (hex 11 02, [(hex 10 02, Pl), (hex 11 01, Pl), (hex 12 02, Pl), (hex 12 03, Pl), (hex 11 03, Pl), (hex 10 03, Pl)]),
  (hex 11 03, [(hex 10 03, Pl), (hex 11 02, Pl), (hex 12 03, Pl), (hex 12 04, Pl), (hex 11 04, Pl), (hex 10 04, Pl)]),
  (hex 11 04, [(hex 10 04, Pl), (hex 11 03, Pl), (hex 12 04, Pl), (hex 12 05, Pl), (hex 11 05, Pl), (hex 10 05, Pl)]),
  (hex 11 05, [(hex 10 05, Pl), (hex 11 04, Pl), (hex 12 05, Pl), (hex 12 06, Pl), (hex 11 06, Pl), (hex 10 06, Pl)]),
  (hex 11 06, [(hex 10 06, Pl), (hex 11 05, Pl), (hex 12 06, Pl), (hex 12 07, Pl), (hex 11 07, Pl), (hex 10 07, Pl)]),
  (hex 11 07, [(hex 10 07, Pl), (hex 11 06, Pl), (hex 12 07, Pl), (hex 12 08, Pl), (hex 11 08, Pl), (hex 10 08, Pl)]),
  (hex 11 08, [(hex 10 08, Pl), (hex 11 07, Pl), (hex 12 08, Pl), (hex 12 09, Pl), (hex 11 09, Pl), (hex 10 09, Pl)]),
  (hex 11 09, [(hex 10 09, Pl), (hex 11 08, Pl), (hex 12 09, Pl), (hex 12 10, Pl), (hex 11 10, Pl), (hex 10 10, Pl)]),
  (hex 11 10, [(hex 10 10, Pl), (hex 11 09, Pl), (hex 12 10, Pl), (hex 12 11, Pl), (hex 11 11, Pl), (hex 10 11, Pl)]),
  (hex 11 11, [(hex 10 11, Pl), (hex 11 10, Pl), (hex 12 11, Pl), (hex 12 12, Pl), (hex 11 12, Pl), (hex 10 12, Pl)]),
  (hex 11 12, [(hex 10 12, Pl), (hex 11 11, Pl), (hex 12 12, Pl)]),
  (hex 12 00, [(hex 13 00, Pl), (hex 12 01, Pl), (hex 11 00, Pl)]),
  (hex 12 01, [(hex 11 00, Pl), (hex 12 00, Pl), (hex 13 00, Pl), (hex 13 01, Pl), (hex 12 02, Pl), (hex 11 01, Pl)]),
  (hex 12 02, [(hex 11 01, Pl), (hex 12 01, Pl), (hex 13 01, Pl), (hex 13 02, Pl), (hex 12 03, Pl), (hex 11 02, Pl)]),
  (hex 12 03, [(hex 11 02, Pl), (hex 12 02, Pl), (hex 13 02, Pl), (hex 13 03, Pl), (hex 12 04, Pl), (hex 11 03, Pl)]),
  (hex 12 04, [(hex 11 03, Pl), (hex 12 03, Pl), (hex 13 03, Pl), (hex 13 04, Pl), (hex 12 05, Pl), (hex 11 04, Pl)]),
  (hex 12 05, [(hex 11 04, Pl), (hex 12 04, Pl), (hex 13 04, Pl), (hex 13 05, Pl), (hex 12 06, Pl), (hex 11 05, Pl)]),
  (hex 12 06, [(hex 11 05, Pl), (hex 12 05, Pl), (hex 13 05, Pl), (hex 13 06, Pl), (hex 12 07, Pl), (hex 11 06, Pl)]),
  (hex 12 07, [(hex 11 06, Pl), (hex 12 06, Pl), (hex 13 06, Pl), (hex 13 07, Pl), (hex 12 08, Pl), (hex 11 07, Pl)]),
  (hex 12 08, [(hex 11 07, Pl), (hex 12 07, Pl), (hex 13 07, Pl), (hex 13 08, Pl), (hex 12 09, Pl), (hex 11 08, Pl)]),
  (hex 12 09, [(hex 11 08, Pl), (hex 12 08, Pl), (hex 13 08, Pl), (hex 13 09, Pl), (hex 12 10, Pl), (hex 11 09, Pl)]),
  (hex 12 10, [(hex 11 09, Pl), (hex 12 09, Pl), (hex 13 09, Pl), (hex 13 10, Pl), (hex 12 11, Pl), (hex 11 10, Pl)]),
  (hex 12 11, [(hex 11 10, Pl), (hex 12 10, Pl), (hex 13 10, Pl), (hex 13 11, Pl), (hex 12 12, Pl), (hex 11 11, Pl)]),
  (hex 12 12, [(hex 11 11, Pl), (hex 12 11, Pl), (hex 13 11, Pl), (hex 13 12, Pl), (hex 11 12, Pl)]),
  (hex 13 00, [(hex 12 00, Pl), (hex 14 00, Pl), (hex 14 01, Pl), (hex 13 01, Pl), (hex 12 01, Pl)]),
  (hex 13 01, [(hex 12 01, Pl), (hex 13 00, Pl), (hex 14 01, Pl), (hex 14 02, Pl), (hex 13 02, Pl), (hex 12 02, Pl)]),
  (hex 13 02, [(hex 12 02, Pl), (hex 13 01, Pl), (hex 14 02, Pl), (hex 14 03, Pl), (hex 13 03, Pl), (hex 12 03, Pl)]),
  (hex 13 03, [(hex 12 03, Pl), (hex 13 02, Pl), (hex 14 03, Pl), (hex 14 04, Pl), (hex 13 04, Pl), (hex 12 04, Pl)]),
  (hex 13 04, [(hex 12 04, Pl), (hex 13 03, Pl), (hex 14 04, Pl), (hex 14 05, Pl), (hex 13 05, Pl), (hex 12 05, Pl)]),
  (hex 13 05, [(hex 12 05, Pl), (hex 13 04, Pl), (hex 14 05, Pl), (hex 14 06, Pl), (hex 13 06, Pl), (hex 12 06, Pl)]),
  (hex 13 06, [(hex 12 06, Pl), (hex 13 05, Pl), (hex 14 06, Pl), (hex 14 07, Pl), (hex 13 07, Pl), (hex 12 07, Pl)]),
  (hex 13 07, [(hex 12 07, Pl), (hex 13 06, Pl), (hex 14 07, Pl), (hex 14 08, Pl), (hex 13 08, Pl), (hex 12 08, Pl)]),
  (hex 13 08, [(hex 12 08, Pl), (hex 13 07, Pl), (hex 14 08, Pl), (hex 14 09, Pl), (hex 13 09, Pl), (hex 12 09, Pl)]),
  (hex 13 09, [(hex 12 09, Pl), (hex 13 08, Pl), (hex 14 09, Pl), (hex 14 10, Pl), (hex 13 10, Pl), (hex 12 10, Pl)]),
  (hex 13 10, [(hex 12 10, Pl), (hex 13 09, Pl), (hex 14 10, Pl), (hex 14 11, Pl), (hex 13 11, Pl), (hex 12 11, Pl)]),
  (hex 13 11, [(hex 12 11, Pl), (hex 13 10, Pl), (hex 14 11, Pl), (hex 14 12, Pl), (hex 13 12, Pl), (hex 12 12, Pl)]),
  (hex 13 12, [(hex 12 12, Pl), (hex 13 11, Pl), (hex 14 12, Pl)]),
  (hex 14 00, [(hex 15 00, Pl), (hex 14 01, Pl), (hex 13 00, Pl)]),
  (hex 14 01, [(hex 13 00, Pl), (hex 14 00, Pl), (hex 15 00, Pl), (hex 15 01, Pl), (hex 14 02, Pl), (hex 13 01, Pl)]),
  (hex 14 02, [(hex 13 01, Pl), (hex 14 01, Pl), (hex 15 01, Pl), (hex 15 02, Pl), (hex 14 03, Pl), (hex 13 02, Pl)]),
  (hex 14 03, [(hex 13 02, Pl), (hex 14 02, Pl), (hex 15 02, Pl), (hex 15 03, Pl), (hex 14 04, Pl), (hex 13 03, Pl)]),
  (hex 14 04, [(hex 13 03, Pl), (hex 14 03, Pl), (hex 15 03, Pl), (hex 15 04, Pl), (hex 14 05, Pl), (hex 13 04, Pl)]),
  (hex 14 05, [(hex 13 04, Pl), (hex 14 04, Pl), (hex 15 04, Pl), (hex 15 05, Pl), (hex 14 06, Pl), (hex 13 05, Pl)]),
  (hex 14 06, [(hex 13 05, Pl), (hex 14 05, Pl), (hex 15 05, Pl), (hex 15 06, Pl), (hex 14 07, Pl), (hex 13 06, Pl)]),
  (hex 14 07, [(hex 13 06, Pl), (hex 14 06, Pl), (hex 15 06, Pl), (hex 15 07, Pl), (hex 14 08, Pl), (hex 13 07, Pl)]),
  (hex 14 08, [(hex 13 07, Pl), (hex 14 07, Pl), (hex 15 07, Pl), (hex 15 08, Pl), (hex 14 09, Pl), (hex 13 08, Pl)]),
  (hex 14 09, [(hex 13 08, Pl), (hex 14 08, Pl), (hex 15 08, Pl), (hex 15 09, Pl), (hex 14 10, Pl), (hex 13 09, Pl)]),
  (hex 14 10, [(hex 13 09, Pl), (hex 14 09, Pl), (hex 15 09, Pl), (hex 15 10, Pl), (hex 14 11, Pl), (hex 13 10, Pl)]),
  (hex 14 11, [(hex 13 10, Pl), (hex 14 10, Pl), (hex 15 10, Pl), (hex 15 11, Pl), (hex 14 12, Pl), (hex 13 11, Pl)]),
  (hex 14 12, [(hex 13 11, Pl), (hex 14 11, Pl), (hex 15 11, Pl), (hex 15 12, Pl), (hex 13 12, Pl)]),
  (hex 15 00, [(hex 14 00, Pl), (hex 16 00, Pl), (hex 16 01, Pl), (hex 15 01, Pl), (hex 14 01, Pl)]),
  (hex 15 01, [(hex 14 01, Pl), (hex 15 00, Pl), (hex 16 01, Pl), (hex 16 02, Pl), (hex 15 02, Pl), (hex 14 02, Pl)]),
  (hex 15 02, [(hex 14 02, Pl), (hex 15 01, Pl), (hex 16 02, Pl), (hex 16 03, Pl), (hex 15 03, Pl), (hex 14 03, Pl)]),
  (hex 15 03, [(hex 14 03, Pl), (hex 15 02, Pl), (hex 16 03, Pl), (hex 16 04, Pl), (hex 15 04, Pl), (hex 14 04, Pl)]),
  (hex 15 04, [(hex 14 04, Pl), (hex 15 03, Pl), (hex 16 04, Pl), (hex 16 05, Pl), (hex 15 05, Pl), (hex 14 05, Pl)]),
  (hex 15 05, [(hex 14 05, Pl), (hex 15 04, Pl), (hex 16 05, Pl), (hex 16 06, Pl), (hex 15 06, Pl), (hex 14 06, Pl)]),
  (hex 15 06, [(hex 14 06, Pl), (hex 15 05, Pl), (hex 16 06, Pl), (hex 16 07, Pl), (hex 15 07, Pl), (hex 14 07, Pl)]),
  (hex 15 07, [(hex 14 07, Pl), (hex 15 06, Pl), (hex 16 07, Pl), (hex 16 08, Pl), (hex 15 08, Pl), (hex 14 08, Pl)]),
  (hex 15 08, [(hex 14 08, Pl), (hex 15 07, Pl), (hex 16 08, Pl), (hex 16 09, Pl), (hex 15 09, Pl), (hex 14 09, Pl)]),
  (hex 15 09, [(hex 14 09, Pl), (hex 15 08, Pl), (hex 16 09, Pl), (hex 16 10, Pl), (hex 15 10, Pl), (hex 14 10, Pl)]),
  (hex 15 10, [(hex 14 10, Pl), (hex 15 09, Pl), (hex 16 10, Pl), (hex 16 11, Pl), (hex 15 11, Pl), (hex 14 11, Pl)]),
  (hex 15 11, [(hex 14 11, Pl), (hex 15 10, Pl), (hex 16 11, Pl), (hex 16 12, Pl), (hex 15 12, Pl), (hex 14 12, Pl)]),
  (hex 15 12, [(hex 14 12, Pl), (hex 15 11, Pl), (hex 16 12, Pl)]),
  (hex 16 00, [(hex 17 00, Pl), (hex 16 01, Pl), (hex 15 00, Pl)]),
  (hex 16 01, [(hex 15 00, Pl), (hex 16 00, Pl), (hex 17 00, Pl), (hex 17 01, Pl), (hex 16 02, Pl), (hex 15 01, Pl)]),
  (hex 16 02, [(hex 15 01, Pl), (hex 16 01, Pl), (hex 17 01, Pl), (hex 17 02, Pl), (hex 16 03, Pl), (hex 15 02, Pl)]),
  (hex 16 03, [(hex 15 02, Pl), (hex 16 02, Pl), (hex 17 02, Pl), (hex 17 03, Pl), (hex 16 04, Pl), (hex 15 03, Pl)]),
  (hex 16 04, [(hex 15 03, Pl), (hex 16 03, Pl), (hex 17 03, Pl), (hex 17 04, Pl), (hex 16 05, Pl), (hex 15 04, Pl)]),
  (hex 16 05, [(hex 15 04, Pl), (hex 16 04, Pl), (hex 17 04, Pl), (hex 17 05, Pl), (hex 16 06, Pl), (hex 15 05, Pl)]),
  (hex 16 06, [(hex 15 05, Pl), (hex 16 05, Pl), (hex 17 05, Pl), (hex 17 06, Pl), (hex 16 07, Pl), (hex 15 06, Pl)]),
  (hex 16 07, [(hex 15 06, Pl), (hex 16 06, Pl), (hex 17 06, Pl), (hex 17 07, Pl), (hex 16 08, Pl), (hex 15 07, Pl)]),
  (hex 16 08, [(hex 15 07, Pl), (hex 16 07, Pl), (hex 17 07, Pl), (hex 17 08, Pl), (hex 16 09, Pl), (hex 15 08, Pl)]),
  (hex 16 09, [(hex 15 08, Pl), (hex 16 08, Pl), (hex 17 08, Pl), (hex 17 09, Pl), (hex 16 10, Pl), (hex 15 09, Pl)]),
  (hex 16 10, [(hex 15 09, Pl), (hex 16 09, Pl), (hex 17 09, Pl), (hex 17 10, Pl), (hex 16 11, Pl), (hex 15 10, Pl)]),
  (hex 16 11, [(hex 15 10, Pl), (hex 16 10, Pl), (hex 17 10, Pl), (hex 17 11, Pl), (hex 16 12, Pl), (hex 15 11, Pl)]),
  (hex 16 12, [(hex 15 11, Pl), (hex 16 11, Pl), (hex 17 11, Pl), (hex 17 12, Pl), (hex 15 12, Pl)]),
  (hex 17 00, [(hex 16 00, Pl), (hex 18 00, Pl), (hex 18 01, Pl), (hex 17 01, Pl), (hex 16 01, Pl)]),
  (hex 17 01, [(hex 16 01, Pl), (hex 17 00, Pl), (hex 18 01, Pl), (hex 18 02, Pl), (hex 17 02, Pl), (hex 16 02, Pl)]),
  (hex 17 02, [(hex 16 02, Pl), (hex 17 01, Pl), (hex 18 02, Pl), (hex 18 03, Pl), (hex 17 03, Pl), (hex 16 03, Pl)]),
  (hex 17 03, [(hex 16 03, Pl), (hex 17 02, Pl), (hex 18 03, Pl), (hex 18 04, Pl), (hex 17 04, Pl), (hex 16 04, Pl)]),
  (hex 17 04, [(hex 16 04, Pl), (hex 17 03, Pl), (hex 18 04, Pl), (hex 18 05, Pl), (hex 17 05, Pl), (hex 16 05, Pl)]),
  (hex 17 05, [(hex 16 05, Pl), (hex 17 04, Pl), (hex 18 05, Pl), (hex 18 06, Pl), (hex 17 06, Pl), (hex 16 06, Pl)]),
  (hex 17 06, [(hex 16 06, Pl), (hex 17 05, Pl), (hex 18 06, Pl), (hex 18 07, Pl), (hex 17 07, Pl), (hex 16 07, Pl)]),
  (hex 17 07, [(hex 16 07, Pl), (hex 17 06, Pl), (hex 18 07, Pl), (hex 18 08, Pl), (hex 17 08, Pl), (hex 16 08, Pl)]),
  (hex 17 08, [(hex 16 08, Pl), (hex 17 07, Pl), (hex 18 08, Pl), (hex 18 09, Pl), (hex 17 09, Pl), (hex 16 09, Pl)]),
  (hex 17 09, [(hex 16 09, Pl), (hex 17 08, Pl), (hex 18 09, Pl), (hex 18 10, Pl), (hex 17 10, Pl), (hex 16 10, Pl)]),
  (hex 17 10, [(hex 16 10, Pl), (hex 17 09, Pl), (hex 18 10, Pl), (hex 18 11, Pl), (hex 17 11, Pl), (hex 16 11, Pl)]),
  (hex 17 11, [(hex 16 11, Pl), (hex 17 10, Pl), (hex 18 11, Pl), (hex 18 12, Pl), (hex 17 12, Pl), (hex 16 12, Pl)]),
  (hex 17 12, [(hex 16 12, Pl), (hex 17 11, Pl), (hex 18 12, Pl)]),
  (hex 18 00, [(hex 19 00, Pl), (hex 18 01, Pl), (hex 17 00, Pl)]),
  (hex 18 01, [(hex 17 00, Pl), (hex 18 00, Pl), (hex 19 00, Pl), (hex 19 01, Pl), (hex 18 02, Pl), (hex 17 01, Pl)]),
  (hex 18 02, [(hex 17 01, Pl), (hex 18 01, Pl), (hex 19 01, Pl), (hex 19 02, Pl), (hex 18 03, Pl), (hex 17 02, Pl)]),
  (hex 18 03, [(hex 17 02, Pl), (hex 18 02, Pl), (hex 19 02, Pl), (hex 19 03, Pl), (hex 18 04, Pl), (hex 17 03, Pl)]),
  (hex 18 04, [(hex 17 03, Pl), (hex 18 03, Pl), (hex 19 03, Pl), (hex 19 04, Pl), (hex 18 05, Pl), (hex 17 04, Pl)]),
  (hex 18 05, [(hex 17 04, Pl), (hex 18 04, Pl), (hex 19 04, Pl), (hex 19 05, Pl), (hex 18 06, Pl), (hex 17 05, Pl)]),
  (hex 18 06, [(hex 17 05, Pl), (hex 18 05, Pl), (hex 19 05, Pl), (hex 19 06, Pl), (hex 18 07, Pl), (hex 17 06, Pl)]),
  (hex 18 07, [(hex 17 06, Pl), (hex 18 06, Pl), (hex 19 06, Pl), (hex 19 07, Pl), (hex 18 08, Pl), (hex 17 07, Pl)]),
  (hex 18 08, [(hex 17 07, Pl), (hex 18 07, Pl), (hex 19 07, Pl), (hex 19 08, Pl), (hex 18 09, Pl), (hex 17 08, Pl)]),
  (hex 18 09, [(hex 17 08, Pl), (hex 18 08, Pl), (hex 19 08, Pl), (hex 19 09, Pl), (hex 18 10, Pl), (hex 17 09, Pl)]),
  (hex 18 10, [(hex 17 09, Pl), (hex 18 09, Pl), (hex 19 09, Pl), (hex 19 10, Pl), (hex 18 11, Pl), (hex 17 10, Pl)]),
  (hex 18 11, [(hex 17 10, Pl), (hex 18 10, Pl), (hex 19 10, Pl), (hex 19 11, Pl), (hex 18 12, Pl), (hex 17 11, Pl)]),
  (hex 18 12, [(hex 17 11, Pl), (hex 18 11, Pl), (hex 19 11, Pl), (hex 19 12, Pl), (hex 17 12, Pl)]),
  (hex 19 00, [(hex 18 00, Pl), (hex 20 00, Pl), (hex 20 01, Pl), (hex 19 01, Pl), (hex 18 01, Pl)]),
  (hex 19 01, [(hex 18 01, Pl), (hex 19 00, Pl), (hex 20 01, Pl), (hex 20 02, Pl), (hex 19 02, Pl), (hex 18 02, Pl)]),
  (hex 19 02, [(hex 18 02, Pl), (hex 19 01, Pl), (hex 20 02, Pl), (hex 20 03, Pl), (hex 19 03, Pl), (hex 18 03, Pl)]),
  (hex 19 03, [(hex 18 03, Pl), (hex 19 02, Pl), (hex 20 03, Pl), (hex 20 04, Pl), (hex 19 04, Pl), (hex 18 04, Pl)]),
  (hex 19 04, [(hex 18 04, Pl), (hex 19 03, Pl), (hex 20 04, Pl), (hex 20 05, Pl), (hex 19 05, Pl), (hex 18 05, Pl)]),
  (hex 19 05, [(hex 18 05, Pl), (hex 19 04, Pl), (hex 20 05, Pl), (hex 20 06, Pl), (hex 19 06, Pl), (hex 18 06, Pl)]),
  (hex 19 06, [(hex 18 06, Pl), (hex 19 05, Pl), (hex 20 06, Pl), (hex 20 07, Pl), (hex 19 07, Pl), (hex 18 07, Pl)]),
  (hex 19 07, [(hex 18 07, Pl), (hex 19 06, Pl), (hex 20 07, Pl), (hex 20 08, Pl), (hex 19 08, Pl), (hex 18 08, Pl)]),
  (hex 19 08, [(hex 18 08, Pl), (hex 19 07, Pl), (hex 20 08, Pl), (hex 20 09, Pl), (hex 19 09, Pl), (hex 18 09, Pl)]),
  (hex 19 09, [(hex 18 09, Pl), (hex 19 08, Pl), (hex 20 09, Pl), (hex 20 10, Pl), (hex 19 10, Pl), (hex 18 10, Pl)]),
  (hex 19 10, [(hex 18 10, Pl), (hex 19 09, Pl), (hex 20 10, Pl), (hex 20 11, Pl), (hex 19 11, Pl), (hex 18 11, Pl)]),
  (hex 19 11, [(hex 18 11, Pl), (hex 19 10, Pl), (hex 20 11, Pl), (hex 20 12, Pl), (hex 19 12, Pl), (hex 18 12, Pl)]),
  (hex 19 12, [(hex 18 12, Pl), (hex 19 11, Pl), (hex 20 12, Pl)]),
  (hex 20 00, [(hex 21 00, Pl), (hex 20 01, Pl), (hex 19 00, Pl)]),
  (hex 20 01, [(hex 19 00, Pl), (hex 20 00, Pl), (hex 21 00, Pl), (hex 21 01, Pl), (hex 20 02, Pl), (hex 19 01, Pl)]),
  (hex 20 02, [(hex 19 01, Pl), (hex 20 01, Pl), (hex 21 01, Pl), (hex 21 02, Pl), (hex 20 03, Pl), (hex 19 02, Pl)]),
  (hex 20 03, [(hex 19 02, Pl), (hex 20 02, Pl), (hex 21 02, Pl), (hex 21 03, Pl), (hex 20 04, Pl), (hex 19 03, Pl)]),
  (hex 20 04, [(hex 19 03, Pl), (hex 20 03, Pl), (hex 21 03, Pl), (hex 21 04, Pl), (hex 20 05, Pl), (hex 19 04, Pl)]),
  (hex 20 05, [(hex 19 04, Pl), (hex 20 04, Pl), (hex 21 04, Pl), (hex 21 05, Pl), (hex 20 06, Pl), (hex 19 05, Pl)]),
  (hex 20 06, [(hex 19 05, Pl), (hex 20 05, Pl), (hex 21 05, Pl), (hex 21 06, Pl), (hex 20 07, Pl), (hex 19 06, Pl)]),
  (hex 20 07, [(hex 19 06, Pl), (hex 20 06, Pl), (hex 21 06, Pl), (hex 21 07, Pl), (hex 20 08, Pl), (hex 19 07, Pl)]),
  (hex 20 08, [(hex 19 07, Pl), (hex 20 07, Pl), (hex 21 07, Pl), (hex 21 08, Pl), (hex 20 09, Pl), (hex 19 08, Pl)]),
  (hex 20 09, [(hex 19 08, Pl), (hex 20 08, Pl), (hex 21 08, Pl), (hex 21 09, Pl), (hex 20 10, Pl), (hex 19 09, Pl)]),
  (hex 20 10, [(hex 19 09, Pl), (hex 20 09, Pl), (hex 21 09, Pl), (hex 21 10, Pl), (hex 20 11, Pl), (hex 19 10, Pl)]),
  (hex 20 11, [(hex 19 10, Pl), (hex 20 10, Pl), (hex 21 10, Pl), (hex 21 11, Pl), (hex 20 12, Pl), (hex 19 11, Pl)]),
  (hex 20 12, [(hex 19 11, Pl), (hex 20 11, Pl), (hex 21 11, Pl), (hex 21 12, Pl), (hex 19 12, Pl)]),
  (hex 21 00, [(hex 20 00, Pl), (hex 22 00, Pl), (hex 22 01, Pl), (hex 21 01, Pl), (hex 20 01, Pl)]),
  (hex 21 01, [(hex 20 01, Pl), (hex 21 00, Pl), (hex 22 01, Pl), (hex 22 02, Pl), (hex 21 02, Pl), (hex 20 02, Pl)]),
  (hex 21 02, [(hex 20 02, Pl), (hex 21 01, Pl), (hex 22 02, Pl), (hex 22 03, Pl), (hex 21 03, Pl), (hex 20 03, Pl)]),
  (hex 21 03, [(hex 20 03, Pl), (hex 21 02, Pl), (hex 22 03, Pl), (hex 22 04, Pl), (hex 21 04, Pl), (hex 20 04, Pl)]),
  (hex 21 04, [(hex 20 04, Pl), (hex 21 03, Pl), (hex 22 04, Pl), (hex 22 05, Pl), (hex 21 05, Pl), (hex 20 05, Pl)]),
  (hex 21 05, [(hex 20 05, Pl), (hex 21 04, Pl), (hex 22 05, Pl), (hex 22 06, Pl), (hex 21 06, Pl), (hex 20 06, Pl)]),
  (hex 21 06, [(hex 20 06, Pl), (hex 21 05, Pl), (hex 22 06, Pl), (hex 22 07, Pl), (hex 21 07, Pl), (hex 20 07, Pl)]),
  (hex 21 07, [(hex 20 07, Pl), (hex 21 06, Pl), (hex 22 07, Pl), (hex 22 08, Pl), (hex 21 08, Pl), (hex 20 08, Pl)]),
  (hex 21 08, [(hex 20 08, Pl), (hex 21 07, Pl), (hex 22 08, Pl), (hex 22 09, Pl), (hex 21 09, Pl), (hex 20 09, Pl)]),
  (hex 21 09, [(hex 20 09, Pl), (hex 21 08, Pl), (hex 22 09, Pl), (hex 22 10, Pl), (hex 21 10, Pl), (hex 20 10, Pl)]),
  (hex 21 10, [(hex 20 10, Pl), (hex 21 09, Pl), (hex 22 10, Pl), (hex 22 11, Pl), (hex 21 11, Pl), (hex 20 11, Pl)]),
  (hex 21 11, [(hex 20 11, Pl), (hex 21 10, Pl), (hex 22 11, Pl), (hex 22 12, Pl), (hex 21 12, Pl), (hex 20 12, Pl)]),
  (hex 21 12, [(hex 20 12, Pl), (hex 21 11, Pl), (hex 22 12, Pl)]),
  (hex 22 00, [(hex 22 01, Pl), (hex 21 00, Pl)]),
  (hex 22 01, [(hex 21 00, Pl), (hex 22 00, Pl), (hex 22 02, Pl), (hex 21 01, Pl)]),
  (hex 22 02, [(hex 21 01, Pl), (hex 22 01, Pl), (hex 22 03, Pl), (hex 21 02, Pl)]),
  (hex 22 03, [(hex 21 02, Pl), (hex 22 02, Pl), (hex 22 04, Pl), (hex 21 03, Pl)]),
  (hex 22 04, [(hex 21 03, Pl), (hex 22 03, Pl), (hex 22 05, Pl), (hex 21 04, Pl)]),
  (hex 22 05, [(hex 21 04, Pl), (hex 22 04, Pl), (hex 22 06, Pl), (hex 21 05, Pl)]),
  (hex 22 06, [(hex 21 05, Pl), (hex 22 05, Pl), (hex 22 07, Pl), (hex 21 06, Pl)]),
  (hex 22 07, [(hex 21 06, Pl), (hex 22 06, Pl), (hex 22 08, Pl), (hex 21 07, Pl)]),
  (hex 22 08, [(hex 21 07, Pl), (hex 22 07, Pl), (hex 22 09, Pl), (hex 21 08, Pl)]),
  (hex 22 09, [(hex 21 08, Pl), (hex 22 08, Pl), (hex 22 10, Pl), (hex 21 09, Pl)]),
  (hex 22 10, [(hex 21 09, Pl), (hex 22 09, Pl), (hex 22 11, Pl), (hex 21 10, Pl)]),
  (hex 22 11, [(hex 21 10, Pl), (hex 22 10, Pl), (hex 22 12, Pl), (hex 21 11, Pl)]),
  (hex 22 12, [(hex 21 11, Pl), (hex 22 11, Pl), (hex 21 12, Pl)])
      ]

public export
PartialGameMap : Map
PartialGameMap = MkMap positions []
  where
    positions : List (Pos, Terrain)
    positions = [(hex 0 0, Clear),
                 (hex 0 1, Clear),
                 (hex 0 2, Clear),
                 (hex 0 3, SupplySource Axis $ Clear),
                 (hex 0 4, Clear),
                 (hex 1 0, Clear),
                 (hex 1 1, Clear),
                 (hex 1 2, Clear),
                 (hex 1 3, Clear),
                 (hex 1 4, Clear),
                 (hex 2 0, Clear),
                 (hex 2 1, Clear),
                 (hex 2 2, Clear),
                 (hex 2 3, Clear),
                 (hex 2 4, Clear),
                 (hex 3 0, Clear),
                 (hex 3 1, Clear),
                 (hex 3 2, Clear),
                 (hex 3 3, Clear),
                 (hex 3 4, Clear),
                 (hex 4 0, Clear),
                 (hex 4 1, Clear),
                 (hex 4 2, Clear),
                 (hex 4 3, Clear),
                 (hex 4 4, Clear)]

public export
FullGameMap : Map
FullGameMap = MkMap positions links
  where
    mkPosition : (c : Nat) -> (r : Nat) -> Maybe ( Pos, Terrain)
    mkPosition c r with (natToFin c 23, natToFin r 13, isLTE c 22, isLTE r 12)
      mkPosition c r | (Just col, Just row, Yes cprf, Yes rprf) =
           let terrain = index col $ index row terrains
           in Just (hex col row, terrain)
      mkPosition c r | (_, _, _, _) = Nothing

    positions : List (Pos, Terrain)
    positions = catMaybes [ mkPosition c r | c <- [ 0 .. 22 ], r <- [ 0 .. 12 ]]

max_stars_repo_name: abailly/hsgames

max_issues_repo_name: abailly/acquire

max_forks_repo_name: abailly/acquire


text:
module FFI
%hide IO
%access public export

data UnsafeRaw;
data Boxed t = MkBoxed t

Unsafe : Type
Unsafe = Boxed UnsafeRaw

mutual

    data QuickTypes : Type -> Type where
        Quick_Unsafe   : QuickTypes Unsafe

    data ForeignName
       = FFunc String
       | FVar String

    FFIQuick : FFI
    FFIQuick = MkFFI QuickTypes ForeignName String

    public export
    IO : Type -> Type
    IO = IO' FFIQuick

FF0 : Type
FF0 = IO Unsafe

FF1 : Type
FF1 = Unsafe -> IO Unsafe

FF2 : Type
FF2 = Unsafe -> Unsafe -> IO Unsafe

FF3 : Type
FF3 = Unsafe -> Unsafe -> Unsafe -> IO Unsafe

||| call foreign language apis
%inline
fcall: (ty : Type) -> (fname : ForeignName) -> {auto fty : FTy FFIQuick [] ty} -> ty
fcall ty fname = foreign FFIQuick fname ty

%inline
fv : String -> IO Unsafe
fv n = fcall (IO Unsafe) (FVar n)

%inline
callff0 : String -> IO Unsafe
callff0 n = fcall FF0 (FFunc n)

%inline
callff1 : String -> Unsafe -> IO Unsafe
callff1 n src = fcall FF1 (FFunc n) src

%inline
callff2 : String -> Unsafe ->  Unsafe -> IO Unsafe
callff2 n src1 src2 = fcall FF2 (FFunc n) src1 src2

%inline
callff3 : String -> Unsafe ->  Unsafe -> Unsafe -> IO Unsafe
callff3 n src1 src2 src3 = fcall FF3 (FFunc n) src1 src2 src3

unsafe : a -> Unsafe
unsafe = believe_me

ext: idr


text:
module Path

import Basic
import Unit
import Void

||| Type of identities or paths between two points in space.
public export
data Id : (0 a : Type) -> a -> a -> Type where
  Refl : (x : a) -> Id a x x

infix 4 ==

public export
(==) : a -> a -> Type
x == y = Id _ x y

||| Induction principle for paths
public export
J : (p : (x, y : a) -> (x == y) -> Type)
 -> ((x : a) -> p x x (Refl x))
 -> (x, y : a) -> (i : x == y) -> p x y i
J p f x x (Refl x) = f x

-- Another one
public export
H : (x : a) -> (p : (y : a) -> (x == y) -> Type)
 -> p x (Refl x)
 -> (y : a) -> (i : x == y) -> p y i
H x p f x (Refl x) = f

-- J and H agree (no proof here)
-- TODO prove it ?

-- No axiom-K

-- Axiom-K is incompatible with the Univalence Axiom.
-- But unfortunately the former is provable in Idris 2.
-- And there is no option to remove it from the system.

-- In practice this means that we must not pattern match
-- on loops (paths from a point to itself)
-- i.e

-- veryBad : x === x -> ...
-- veryBad Refl = ...

-- but on the other hand, this is ok:
-- noContradiction : x === y -> ...
-- noContradiction Refl = ...

||| Lift a point in the base space `a` to the point in the total
||| space `Sigma a p` via the given path in the base space.
public export
transport : (p : a -> Type) -> {x, y : _} -> x == y -> p x -> p y
-- transport p i = J (\x, y, _ => p x -> p y) (\_ => id) _ _ i
transport p (Refl x) = id

public export
IdFun : {a, b: Type} -> a == b -> a -> b
IdFun = transport id

public export
transportConst : (a, b : Type)
              -> (x, y : a)
              -> (x' : b)
              -> (path : Id a x y)
              -> transport (\_ => b) path x' == x'
transportConst a b x x x' (Refl x) = Refl x'

namespace Id
  public export
  (.) : {x, y, z : a} -> x == y -> y == z -> x == z
  p . q = transport (x ==) q p

  --TODO Vertical composition

||| p <=> p⁻¹
public export
sym : {x, y : a} -> (p : x == y) -> y == x
sym p = transport (== x) p (Refl x)

||| Congruence or f(p)/(ap f p) in the HoTT book
||| p => f(p)
public export
ap : {x, y : a} -> (f : a -> b) -> (p : x == y) -> f x == f y
-- ap f p = transport (\that => f x == f that) p (Refl (f x))
ap f (Refl x) = Refl (f x)

||| Dependent map
public export
apd : (p : a -> Type)
   -> (f : (x : a) -> p x)
   -> (x, y : a)
   -> (path : x == y)
   -> transport p path (f x) == f y
apd p f x x (Refl x) = Refl (f x)


text:
module Bad2

badReturn : (whatever : Int)


text:
module Finmath.Finite

--------------------------------------------------------------------------------
-- Cartesian sums and products of finite sets
--------------------------------------------------------------------------------

||| Map an element of either of two sets, into their Cartesian sum
fSetSum : Either (Fin n) (Fin m) -> Fin (n + m)
fSetSum (Left fZ)               = fZ
fSetSum (Left (fS k))           = fS (fSetSum (Left k))
fSetSum {n=Z} (Right right)     = right
fSetSum {n=(S k)} (Right right) = fS (fSetSum {n=k} (Right right))

||| Map a pair of elements from each of two sets, into their Cartesian product
fSetProduct : (Fin n, Fin m) -> Fin (n * m)
fSetProduct (fZ, right) = fSetSum (Left right)
fSetProduct {n=(S k)} ((fS left), right) = fSetSum (Right (fSetProduct (left, right)))

||| The inverse map of fSetSum
fSetSumInv : Fin (n + m) -> Either (Fin n) (Fin m)
fSetSumInv {n=Z} x      = Right x
fSetSumInv {n=(S k)} fZ = Left fZ
fSetSumInv {n=(S k)} (fS c) with (fSetSumInv {n=k} c)
                                 | Left a = Left (fS a)
                                 | Right b = Right b

--------------------------------------------------------------------------------
-- Misc
--------------------------------------------------------------------------------

||| Functions respect equality
fEq : (f : a -> b) -> (left : a) -> (right : a) -> (p : left = right) -> f left = f right
fEq f left _ refl = refl

--------------------------------------------------------------------------------
-- Proofs about inequality
--------------------------------------------------------------------------------

||| Proof that LTE respects adding a constant to both sides
ltePlus : LTE m l -> (n : Nat) -> LTE (n + m) (n + l)
ltePlus p Z     = p
ltePlus p (S k) = lteSucc (ltePlus p k)

||| Proof that n <= n
lteN : (n : Nat) -> LTE n n
lteN n = (rewrite (fEq (\k => LTE n k) _ _ (plusCommutative 0 n)) in
  (rewrite (fEq (\k => LTE k (n + 0)) _ _ (plusCommutative 0 n)) in
    (ltePlus (lteZero {right=Z}) n)))

||| Proof that if n <= m and m <= l then n <= l
lteTrans : LTE n m -> LTE m l -> LTE n l
lteTrans lteZero _                = lteZero
lteTrans (lteSucc w) (lteSucc w') = lteSucc (lteTrans w w')

||| Dichotomy for lte
lteDichotomy : LTE n m -> Either (n = m) (LT n m)
lteDichotomy (lteZero {right=Z}) = Left refl
lteDichotomy (lteZero {right=(S k)}) = Right (lteSucc lteZero)
lteDichotomy (lteSucc p) = f (lteDichotomy p)
  where f : Either (l = k) (LT l k) -> Either ((S l) = (S k)) (LT (S l) (S k))
        f (Left p) = Left (eqSucc _ _ p)
        f (Right p) = Right (lteSucc p)

||| Dichotomy
dichotomy : (n : Nat) -> (m : Nat) -> Either (LTE n m) (LT m n)
dichotomy Z _ = Left lteZero
dichotomy (S k) Z = Right (lteSucc lteZero)
dichotomy (S l) (S k) = f (dichotomy l k)
  where f : Either (LTE l k) (LT k l) -> Either (LTE (S l) (S k)) (LT (S k) (S l))
        f (Left p) = Left (lteSucc p)
        f (Right p) = Right (lteSucc p)

||| Trichotomy
trichotomy : (n : Nat) -> (m : Nat) -> Either (Either (n = m) (LT n m)) (LT m n)
trichotomy n m with (dichotomy n m)
                                 | Left a = Left (lteDichotomy a)
                                 | Right b = Right b

max_stars_repo_name: silky/idris-finite-math

max_issues_repo_name: silky/idris-finite-math

max_forks_repo_name: silky/idris-finite-math


text:
module Data.List.Extra

import Data.List

%default total

||| Analogous to `map` for `List`, but the function is applied to the index of
||| the element as first argument (counting from 0), and the element itself as
||| second argument.
public export
mapi : ((n : Nat) -> (a -> b))
    -> (xs : List a)
    -> List b
mapi = h 0 where
  h : Nat -> ((n : Nat) -> (a -> b))
   -> (xs : List a)
   -> List b
  h i f [] = []
  h i f (x :: xs) = f i x :: h (S i) f xs

||| Applied to a predicate and a list, returns the list of those elements that
||| satisfy the predicate with corresponding indices in a stand-alone list.
||| See also `Data.List.Extra.filterLoc'`.
public export
filterLoc : (a -> Bool) -> List a -> (List a, List Nat)
filterLoc p = h 0 where
  h : Nat -> List a -> (List a, List Nat)
  h _ [] = ([], [])
  h lvl (x :: xs) = if p x
      then let (ms, ns) = h (S lvl) xs in (x :: ms, lvl :: ns)
      else h (S lvl) xs

||| Applied to a predicate and a list, returns the list of those elements that
||| satisfy the predicate with corresponding indices.
public export
filterLoc' : (a -> Bool) -> List a -> List (a, Nat)
filterLoc' p = h 0 where
  h : Nat -> List a -> List (a, Nat)
  h _ [] = []
  h lvl (x :: xs) = if p x
    then (x, lvl) :: h (S lvl) xs
    else             h (S lvl) xs


text:
import Data.HVect
import System.Info

-- Signature of a %foreign hint:
-- definition|require1(renameRequire1), require2(renameRequire2), ...
-- prefix 'lua:' is optional if there is only one %foreign hint

-- All Idris functions are compiled as curried Lua lambdas, foreign functions are no different.

%foreign "lua:function () end|inspect, extra"
imports : PrimIO ()

-- This function does nothing at runtime
-- But we need to reference it from any runtime relevant function, to make sure idris
-- includes 'imports' definition at runtime
-- otherwise all 'require' statements, like 'inspect' and 'extra', won't be generated
doImports : IO ()
doImports = primIO imports

-- Make sure given names are present in compiled output
%foreign "function (_) return function(_) return function (_) return function(w) return {tag='0'} end end end end"
compile : HVect tyes -> IO ()

%foreign "function(_) return function(x) return idris.inspect(x) end end"
inspect : a -> String

-- Keep in mind that erased arguments are still present in function signatures,
-- though they are always passed as 'nil'
-- I think we should fix this behaviour, but it originates within the Idris compiler
%foreign "function(_) return function(x) return idris.inspect(x) end end"
inspectList : List a -> String

-- 'a : Type' and 'b : Type' are erased, thus two underscores
%foreign "function(_) return function(_) return function(f) return function(x) return idris.extra.apply(f, x) end end end end"
apply : (a -> b) -> a -> b

%foreign "function(_) return function(list) return idris.extra.printList(list) end end"
printList : List a -> String

-- Represents Lua dictionaries
data Dict : Type where [external]

-- Here we silently have another implicit argument of type Nat: length of 'tyes'
%foreign "function(_) return function(_) return function(hv) return idris.extra.hVectToDict(hv, {}) end end end"
toDict : HVect tyes -> Dict
-- toDict : {0 n: Nat} -> {0 tyes : Vect n Type} -> HVect tyes -> Dict

-- for demonstration purposes lets require 'extra' renaming it to 'extras'
%foreign "function(f) return idris.extras.apply(f, 1) end|extra(extras)"
applyTo1 : (Int -> Int) -> Int

%foreign "function(idrisPlus) return idrisPlus(1)(3) end"
four : (Int -> Int -> Int) -> Int

%foreign "function(f) return function(w) f('A string from Lua !')(w); return 'ok' end end"
callIdrisFromLua : (String -> IO String) -> IO String

barePrint : String -> IO ()
barePrint = putStrLn

%foreign "function(w) idris['Main.barePrint']('Another string from Lua !')(w); return 0 end"
callIdrisFromLua' : IO ()

main : IO ()
main = do doImports
          compile [barePrint]
          putStrLn $ inspect "hey"
          putStrLn $ inspectList [1, 2, 3, the Int 4, 5]
          putStrLn $ show $ applyTo1 (* 2)
          putStrLn $ show $ Main.apply (+ 1) (the Int 1)
          putStrLn $ printList [1, the Int 2, 3, the Int 4]
          putStrLn $ inspect $ toDict [("a", the Int 1), ("b", "b"), ("c", the (List Integer) [1, 2, 3])]
          putStrLn $ "is four " ++ show (four (+))
          ok <- callIdrisFromLua (\str => putStrLn str *> pure "ok")
          putStrLn $ "Got " ++ ok ++ " back"
          putStrLn $ inspect codegen
          () <- callIdrisFromLua'
          pure ()


text:
public export
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                         Nothing => Nothing
                         Just prf => Just $ cong prf

-- Ex 8.1 #1
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf
-- Or alternative:
-- same_cons Refl = Refl

-- Ex 8.1 #2
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

-- Ex 8.1 #3
data ThreeEq : a -> b -> c -> Type where
     CreateThreeEq : ThreeEq z z z

-- Ex 8.1 #4
allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z CreateThreeEq = CreateThreeEq


text:
-- Module      : Itea
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

||| Itea top-level module exporting the most commonly used modules
module Itea
import public Itea.Javascript.Types
import public Itea.Html
import public Itea.Html.Attributes
import public Itea.Html.Events
import public Itea.Utils
import public Itea.Program
import public Control.Monad.Trans
import public Control.Monad.Reader

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
f : (Int -> Bool) -> Int

il : Int
il = f \x => x > 0

lc : Int
lc = f $ \case 0 => True ; _ => False

ilc : Int
ilc = f \case 0 => True; _ => False

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Effect.Baseline
import Effect.State
import Effect.StdIO
import Effect.System
import Effects
import Lambdapants.Colors
import Lambdapants.Command
import Lambdapants.Command.Parser
import Lambdapants.Environment
import Lambdapants.Term
import Lambdapants.Term.Nats
import Lambdapants.Term.Parser
import Lambdapants.Term.Reduction
import Lightyear.Strings

ansiPut : String -> String -> Eff () [STDIO]
ansiPut code str = do
  putStr ("\ESC[" ++ code ++ "m")
  putStr str
  putStr "\ESC[0m"

stdEnv : Environment
stdEnv = catMaybes (map f
  [ ("plus"    , "\\m.\\n.\\f.\\x.m f (n f x)")
  , ("succ"    , "\\n.\\f.\\x.f (n f x)")
  , ("pred"    , "\\n.\\f.\\x.n (\\g.\\h.h (g f)) (\\u.x) (\\u.u)")
  , ("mult"    , "\\m.\\n.\\f.m (n f)")
  , ("sub"     , "\\m.\\n.n pred m")
  , ("pow"     , "\\b.\\e.e b")
  , ("id"      , "\\x.x")
  , ("true"    , "\\x.\\y.x")
  , ("false"   , "\\x.\\y.y")
  , ("and"     , "\\p.\\q.p q p")
  , ("or"      , "\\p.\\q.p p q")
  , ("not"     , "\\p.p false true")
  , ("if"      , "\\p.\\a.\\b.p a b")
  , ("is_zero" , "\\n.n (\\x.false) true")
  , ("leq"     , "\\m.\\n.is_zero (sub m n)")
  , ("zero"    , "\\f.\\x.x")
  , ("fact"    , "\\k.k (\\p.p (\\a.\\b.\\g.g (\\f.\\x.f (a f x)) (\\f.a (b f))))(\\g.g (\\h.h) (\\h.h)) (\\a.\\b.b)")

  -- SKI combinators

  , ("I"       , "\\x.x")
  , ("K"       , "\\x.\\y.x")
  , ("S"       , "\\x.\\y.\\z.x z (y z)")
  , ("B"       , "\\x.\\y.\\z.x (y z)")
  , ("C"       , "\\x.\\y.\\z.x z y")
  , ("W"       , "\\x.\\y.x y y")
  , ("U"       , "\\x.\\y.y (x x y)")
  , ("Y"       , "\\g.(\\x.g (x x)) (\\x.g (x x))")
  , ("omega"   , "\\x.x x")
  , ("Omega"   , "omega omega")

  , ("pair"    , "\\x.\\y.\\f.f x y")
  , ("first"   , "\\p.p true")
  , ("second"  , "\\p.p false")
  , ("nil"     , "\\x.true")
  , ("null"    , "\\p.p (\\x.\\y.false)")
  ])

where
  f : (String, String) -> Maybe (String, Term)
  f (s, e) = case parse term e of
                  Left  _ => Nothing
                  Right t => Just (s, t)

partial parseUnsafe : String -> Term
parseUnsafe input =
  case parse term input of
       Right term => term

run_ : Nat -> Term -> Eff () [STATE Repl, STDIO]
run_ count term = do
  when (count > 0) (putStr (okay " \x21d2 ")) -- Right arrow
  putStrLn (pretty term)
  when (not (normal term)) continue
where
  continue : Eff () [STATE Repl, STDIO]
  continue = do
    let maxr = limit !get
    if (count >= maxr)
       then do
         ansiPut "0;91" ("Terminated after " ++ show maxr ++ " reductions. \
           \Use :limit to increase depth.")
         putChar '\n'
       else run_ (succ count) (evaluate (eval !get) term)

runWithEnv : Term -> Eff () [STATE Repl, STDIO]
runWithEnv term = run_ 0 (closed term (dict !get))

exitMsg : Eff () [STDIO]
exitMsg = ansiPut "0;37" "Bye!" *> putChar '\n'

loop : Eff () [STATE Repl, STDIO, SYSTEM, BASELINE]
loop = do
  line <- baseline "\x03bb " -- Lambda sign
  case map trim line of
       Just ""  => loop
       Just ":" => loop
       Just str =>
         if ':' == strHead str
            then do
              case parseCmd (strTail str) of
                   Left err => do
                     putStrLn err
                     loop
                   Right action => do
                     execute action
                     if Quit == action then exitMsg else loop
            else do
              case parse term str of
                   Right t => runWithEnv t
                   otherwise => do
                     putStr (error "Not a valid term. ")
                     putStrLn "Format is \
                       \<term> := <var> | \\<var>.<term> | (<term> <term>)"
              loop
       Nothing => putChar '\n' *> exitMsg

prog : Eff () [STATE Repl, STDIO, SYSTEM, BASELINE]
prog = do
  addDictEntries (map fst (dict !get))
  addDictEntry "normal"
  addDictEntry "applicative"
  ansiPut "1;37" "lambdapants"
  putStrLn " \x03bb_\x03bb version 0.0.1"
  putStrLn "Type :h for help"
  readHistory ".history"
  loop
  writeHistory ".history"

main : IO ()
main = Effects.runInit [ReplState stdEnv 150 Normal, (), (), ()] prog

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
||| Reocurring fragments from the example applications
module Examples.Util

import Data.MSF.Event
import Rhone.JS
import Examples.CSS

public export
MSFEvent : Type -> Type
MSFEvent = Data.MSF.Event.Event

--------------------------------------------------------------------------------
--          Usefule Nodes
--------------------------------------------------------------------------------

export
lbl : (text: String) -> (class : String) -> Node ev
lbl txt cl = label [classes [widgetLabel, cl]] [Text txt]


text:
||| Until Idris2 starts supporting the 'syntax' keyword, here's a
||| poor-man's equational reasoning
module Syntax.PreorderReasoning

infixl 0  ~~
prefix 1  |~
infix  1  ...

|||Slightly nicer syntax for justifying equations:
|||```
||| |~ a
||| ~~ b ...( justification )
|||```
|||and we can think of the `...( justification )` as ASCII art for a thought bubble.
public export
(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
(...) x pf = (x ** pf)

public export
data FastDerivation : (x : a) -> (y : b) -> Type where
  (|~) : (x : a) -> FastDerivation x x
  (~~) : FastDerivation x y -> (step : (z : c ** y ~=~ z)) -> FastDerivation x (fst step)

public export
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y
Calc (|~ x) = Refl
Calc ((~~) {z=_} {y=_} der (_ ** Refl)) = Calc der

{- -- requires import Data.Nat
0
example : (x : Nat) -> (x + 1) + 0 = 1 + x
example x =
  Calc $
   |~ (x + 1) + 0
   ~~ x+1  ...( plusZeroRightNeutral $ x + 1 )
   ~~ 1+x  ...( plusCommutative x 1          )
-}


text:
module Main

import Graphics.Util.Glfw
import Graphics.Util.GlfwConfig

initDisplay : String -> Int -> Int -> IO GlfwWindow
initDisplay title width height = do
  glfw <- glfwInit
  glfwWindowHint GLFW_CONTEXT_VERSION_MAJOR  4
  glfwWindowHint GLFW_CONTEXT_VERSION_MINOR  1
  glfwWindowHint GLFW_OPENGL_FORWARD_COMPAT  1
  glfwWindowHint GLFW_OPENGL_PROFILE         (toInt GLFW_OPENGL_CORE_PROFILE)
  win <- glfwCreateWindow title width height defaultMonitor
  -- now we pretend every thing is going to be ok
  glfwMakeContextCurrent win
  pure win

isKeyPressed : GlfwWindow -> Char -> IO Bool
isKeyPressed win key = do
  ev <- glfwGetKey win key
  if ev == GLFW_PRESS
  then pure True
  else pure False

main : IO ()
main = do win <- initDisplay "Hello Idris" 640 480
          glfwSetInputMode win GLFW_STICKY_KEYS 1
          eventLoop win 0
          glfwDestroyWindow win
          glfwTerminate
          pure ()
       where
         eventLoop : GlfwWindow -> Int -> IO ()
         eventLoop win ticks = do
                      glfwPollEvents
                      key <- glfwGetFunctionKey win GLFW_KEY_ESCAPE
                      shouldClose <- glfwWindowShouldClose win
                      if shouldClose || key == GLFW_PRESS
                      then pure ()
                      else do
                        eventLoop win (ticks+1)

max_stars_repo_name: eckart/glfw-idris

max_issues_repo_name: eckart/glfw-idris

max_forks_repo_name: eckart/glfw-idris


text:
record Album where
    constructor MkAlbum
    artist : String
    title : String
    year : Integer

help : Album
help = MkAlbum "The Beatles" "Help" 1965

rubbersoul : Album
rubbersoul = MkAlbum "The Beatles" "Rubber Soul" 1965

clouds : Album
clouds = MkAlbum "Joni Mitchell" "Clouds" 1969

hunkydory : Album
hunkydory = MkAlbum "David Bowie" "Hunky Dory" 1971

heroes : Album
heroes = MkAlbum "David Bowie" "Heroes" 1977

collection : List Album
collection = [help, rubbersoul, clouds, hunkydory, heroes]

Eq Album where
    (==) (MkAlbum artist title year) (MkAlbum artist' title' year') =
        artist == artist' && title == title' && year == year'

Ord Album where
    compare (MkAlbum artist title year) (MkAlbum artist' title' year') =
        case compare artist artist' of
            EQ => case compare year year' of
                    EQ => compare title title'
                    diff_year => diff_year
            diff_artists => diff_artists

Show Album where
    show (MkAlbum artist title year) =
        title ++ " by " ++ artist ++ " (released " ++ show year ++ ")"


text:
module Learn.Elab4

import Prelude.Strings as S
import Language.Reflection.Utils
-- import Pruviloj.Core
-- import Pruviloj

%language ElabReflection

-- implementation Show TT where
--   show _ = "foo"

-- implementation Show x => Show (Binder x) where
--   show _ = "binder"

implementation Show x => Show (FunDefn x) where
   show ttname = "TTname"

data Foo : Type where
  Fee : Foo

fee : Int -> Int
fee x = x+1

record FnDesc where
  constructor MkFnDesc
  nameType : NameType
  fnType : TT
  fnDef : (FunDefn TT)

implementation Show FnDesc where
  show fd =
    "nameType: " ++ (show (nameType fd)) ++ "\n"
    ++ "fnType: " ++ (show (fnType fd)) ++ "\n"
    ++ "fnDef: " ++ (show (fnDef fd)) ++ "\n"

getTTForFn : TTName -> Elab ()
getTTForFn n =
  do
    (_,nt,t) <- lookupTyExact n
    fnd <- lookupFunDefnExact n
    fill `(MkFnDesc ~(quote nt) ~(quote t) ~(quote fnd))
    --    fill `((~(quote nt)))
    solve

bar : Int -> Int
bar xxx = 42

bar2 : Nat -> Nat
bar2 xxx = S xxx

bar3 : Nat -> Nat
bar3 = \x => S x

bar4 : (n : Nat) -> Nat
bar4 = \x => S x

bar5 : Nat -> Nat
bar5 Z = Z
bar5 (S k) = k

foo' : FnDesc
foo' = %runElab (getTTForFn `{bar})

foo2 : FnDesc
foo2 = %runElab (getTTForFn `{bar2})

foo3 : FnDesc
foo3 = %runElab (getTTForFn `{bar3})

foo4 : FnDesc
foo4 = %runElab (getTTForFn `{bar4})

foo5 : FnDesc
foo5 = %runElab (getTTForFn `{bar5})

bar6 : Nat
bar6 = Z

foo6 : FnDesc
foo6 = %runElab (getTTForFn `{bar6})

-- bar7 : Nat -> x
-- bar7 y = y

-- foo7 : FnDesc
-- foo7 = %runElab (getTTForFn `{bar7})

foo : FnDesc
foo = %runElab (getTTForFn `{fee})
-- foo = %runElab getTT

-- debuggetenv : Elab ()
-- debugGetEnv =
--   do
--     g <- getEnv
--     debugMessage [TextPart (show g)]

-- %runElab debugGetEnv


text:
||| [specification](https://csrc.nist.gov/csrc/media/publications/fips/46/3/archive/1999-10-25/documents/fips46-3.pdf)
module Data.Crypto.Encryption.Block.DEA

-- import Control.Isomorphism
import Data.Bits
import Data.Fin
import Data.Vect

import Data.Crypto.Encryption
import Data.Crypto.Encryption.Block
import Data.Crypto.Util

%default total
%access private

-- utility functions

trim : Bits (1 + n) -> Bits n
trim b = truncate (shiftRightLogical (intToBits 1) b)

-- Plenty of places in the 3DES spec use 1-based indexes, where we would like
-- 0-based indexes. So we embed the same numbers from the spec (for easy
-- eyeball-checking), then use this to correct the difference.
offByOne : Fin (S (S n)) -> Fin (S n)
offByOne FZ     = FZ
offByOne (FS y) = y

selectBits : Vect m (Fin n) -> Bits n -> Bits m
selectBits positions input = foldl (\acc, b => shiftLeft acc (intToBits 1) `and` b)
                                   (intToBits 0)
                                   (map (\x => intToBits (if getBit x input then 1 else 0)) positions)

||| The initial permutation
IP : Bits 64 -> Bits 64
IP = selectBits (map offByOne [58, 50, 42, 34, 26, 18, 10,  2,
                               60, 52, 44, 36, 28, 20, 12,  4,
                               62, 54, 46, 38, 30, 22, 14,  6,
                               64, 56, 48, 40, 32, 24, 16,  8,
                               57, 49, 41, 33, 25, 17,  9,  1,
                               59, 51, 43, 35, 27, 19, 11,  3,
                               61, 53, 45, 37, 29, 21, 13,  5,
                               63, 55, 47, 39, 31, 23, 15,  7])

inverseIP : Bits 64 -> Bits 64
inverseIP = selectBits (map offByOne [40,  8, 48, 16, 56, 24, 64, 32,
                                      39,  7, 47, 15, 55, 23, 63, 31,
                                      38,  6, 46, 14, 54, 22, 62, 30,
                                      37,  5, 45, 13, 53, 21, 61, 29,
                                      36,  4, 44, 12, 52, 20, 60, 28,
                                      35,  3, 43, 11, 51, 19, 59, 27,
                                      34,  2, 42, 10, 50, 18, 58, 26,
                                      33,  1, 41,  9, 49, 17, 57, 25])

-- TODO: prove this
-- permutation : Iso (Bits 64) (Bits 64)
-- permutation = MkIso IP IP'

E : Bits 32 -> Bits 48
E = selectBits (map offByOne [32,  1,  2,  3,  4,  5,
                               4,  5,  6,  7,  8,  9,
                               8,  9, 10, 11, 12, 13,
                              12, 13, 14, 15, 16, 17,
                              16, 17, 18, 19, 20, 21,
                              20, 21, 22, 23, 24, 25,
                              24, 25, 26, 27, 28, 29,
                              28, 29, 30, 31, 32,  1])

P : Bits 32 -> Bits 32
P = selectBits (map offByOne [16,  7, 20, 21,
                              29, 12, 28, 17,
                               1, 15, 23, 26,
                               5, 18, 31, 10,
                               2,  8, 24, 14,
                              32, 27,  3,  9,
                              19, 13, 30,  6,
                              22, 11,  4, 25])

-- TODO: Generalize from `16 in `Fin 16` and `nextPow2 16` to `n`.
select : Vect 4 (Vect 16 (Fin 16)) -> Bits 6 -> Bits (nextPow2 16)
select table bits =
  let row = bitsToFin (truncate {m=4} (or (shiftRightLogical (cast 5) (and bits (intToBits 32))) (and bits (intToBits 1))))
      col = bitsToFin (truncate {m=2} (shiftRightLogical (cast 1) (and bits (intToBits 30))))
  in finToBits (index col (index row table))

S : Vect 8 (Bits 6 -> Bits 4)
S = map select
        --  0   1   2   3   4   5   6   7   8   9  10  11  12  13  14  15
        [[[14,  4, 13,  1,  2, 15, 11,  8,  3, 10,  6, 12,  5,  9,  0,  7],
          [ 0, 15,  7,  4, 14,  2, 13,  1, 10,  6, 12, 11,  9,  5,  3,  8],
          [ 4,  1, 14,  8, 13,  6,  2, 11, 15, 12,  9,  7,  3, 10,  5,  0],
          [15, 12,  8,  2,  4,  9,  1,  7,  5, 11,  3, 14, 10,  0,  6, 13]],
         [[15,  1,  8, 14,  6, 11,  3,  4,  9,  7,  2, 13, 12,  0,  5, 10],
          [ 3, 13,  4,  7, 15,  2,  8, 14, 12,  0,  1, 10,  6,  9, 11,  5],
          [ 0, 14,  7, 11, 10,  4, 13,  1,  5,  8, 12,  6,  9,  3,  2, 15],
          [13,  8, 10,  1,  3, 15,  4,  2, 11,  6,  7, 12,  0,  5, 14,  9]],
         [[10,  0,  9, 14,  6,  3, 15,  5,  1, 13, 12,  7, 11,  4,  2,  8],
          [13,  7,  0,  9,  3,  4,  6, 10,  2,  8,  5, 14, 12, 11, 15,  1],
          [13,  6,  4,  9,  8, 15,  3,  0, 11,  1,  2, 12,  5, 10, 14,  7],
          [ 1, 10, 13,  0,  6,  9,  8,  7,  4, 15, 14,  3, 11,  5,  2, 12]],
         [[ 7, 13, 14,  3,  0,  6,  9, 10,  1,  2,  8,  5, 11, 12,  4, 15],
          [13,  8, 11,  5,  6, 15,  0,  3,  4,  7,  2, 12,  1, 10, 14,  9],
          [10,  6,  9,  0, 12, 11,  7, 13, 15,  1,  3, 14,  5,  2,  8,  4],
          [ 3, 15,  0,  6, 10,  1, 13,  8,  9,  4,  5, 11, 12,  7,  2, 14]],
         [[ 2, 12,  4,  1,  7, 10, 11,  6,  8,  5,  3, 15, 13,  0, 14,  9],
          [14, 11,  2, 12,  4,  7, 13,  1,  5,  0, 15, 10,  3,  9,  8,  6],
          [ 4,  2,  1, 11, 10, 13,  7,  8, 15,  9, 12,  5,  6,  3,  0, 14],
          [11,  8, 12,  7,  1, 14,  2, 13,  6, 15,  0,  9, 10,  4,  5,  3]],
         [[12,  1, 10, 15,  9,  2,  6,  8,  0, 13,  3,  4, 14,  7,  5, 11],
          [10, 15,  4,  2,  7, 12,  9,  5,  6,  1, 13, 14,  0, 11,  3,  8],
          [ 9, 14, 15,  5,  2,  8, 12,  3,  7,  0,  4, 10,  1, 13, 11,  6],
          [ 4,  3,  2, 12,  9,  5, 15, 10, 11, 14,  1,  7,  6,  0,  8, 13]],
         [[ 4, 11,  2, 14, 15,  0,  8, 13,  3, 12,  9,  7,  5, 10,  6,  1],
          [13,  0, 11,  7,  4,  9,  1, 10, 14,  3,  5, 12,  2, 15,  8,  6],
          [ 1,  4, 11, 13, 12,  3,  7, 14, 10, 15,  6,  8,  0,  5,  9,  2],
          [ 6, 11, 13,  8,  1,  4, 10,  7,  9,  5,  0, 15, 14,  2,  3, 12]],
         [[13,  2,  8,  4,  6, 15, 11,  1, 10,  9,  3, 14,  5,  0, 12,  7],
          [ 1, 15, 13,  8, 10,  3,  7,  4, 12,  5,  6, 11,  0, 14,  9,  2],
          [ 7, 11,  4,  1,  9, 12, 14,  2,  0,  6, 10, 13, 15,  3,  5,  8],
          [ 2,  1, 14,  7,  4, 10,  8, 13, 15, 12,  9,  0,  3,  5,  6, 11]]]

f : Bits 32 -> Bits 48 -> Bits 32
f R K = P (concat (zipWith apply S (partition (E R `xor` K))))

iteration : (Bits 32, Bits 32) -> Bits 48 -> (Bits 32, Bits 32)
iteration (L, R) K = (R, L `xor` f R K)

centralDEA : Bits 64 -> Vect 16 (Bits 48) -> Bits 64
centralDEA input keys =
  let [L, R] = the (Vect 2 (Bits 32)) (partition (IP input))
  in inverseIP (uncurry (flip append) (foldl iteration (L, R) keys))

||| permuted choice
PC1 : Bits 64 -> Bits 56
PC1 = selectBits (map offByOne [57, 49, 41, 33, 25, 17,  9,
                                 1, 58, 50, 42, 34, 26, 18,
                                10,  2, 59, 51, 43, 35, 27,
                                19, 11,  3, 60, 52, 44, 36,
                                63, 55, 47, 39, 31, 23, 15,
                                 7, 62, 54, 46, 38, 30, 22,
                                14,  6, 61, 53, 45, 37, 29,
                                21, 13,  5, 28, 20, 12,  4])

||| permuted choice
PC2 : Bits 56 -> Bits 48
PC2 = selectBits (map offByOne [14, 17, 11, 24,  1,  5,
                                 3, 28, 15,  6, 21, 10,
                                23, 19, 12,  4, 26,  8,
                                16,  7, 27, 20, 13,  2,
                                41, 52, 31, 37, 47, 55,
                                30, 40, 51, 45, 33, 48,
                                44, 49, 39, 56, 34, 53,
                                46, 42, 50, 36, 29, 32])

public export
DEAKey : Type
DEAKey = Bits 64

||| INSECURE!
public export
data DataEncryptionAlgorithm : Type where
  DEA : DEAKey -> DataEncryptionAlgorithm

||| key schedule
KS : DEAKey -> Vect 16 (Bits 48)
KS key = map PC2
             (tail (scanl (\prevKey, shift =>
                            concat (map (rotateLeft shift)
                                        (partition {m=28} {n=2} prevKey)))
                          (PC1 key)
                          [1, 1, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 1]))

implementation BlockCipher DataEncryptionAlgorithm 64 0 where
  encryptBlock (DEA key) block = centralDEA block (KS key)
  decryptBlock (DEA key) block = centralDEA block (reverse (KS key))

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> (1 xs : Vect k a) -> Vect (S k) a

partial
append : (1 _ : Vect n a) -> Vect m a -> Vect (n + m) a
append (x :: zs@(y :: ws)) ys = ?foo -- zs usable, y+ws not

cappend : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) $a
cappend xs ys
    = case xs of
           Nil => ys
           x :: zs => ?bar -- zs usable, xs not

cappend2 : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) a
cappend2 xs ys
    = case xs of
           Nil => ys
           x :: zs => let ts = zs in ?baz -- ts usable, xs+zs not


text:
-- Taken and modified from https://github.com/MarcelineVQ/idris2-streaming

||| References:
||| - https://github.com/MarcelineVQ/idris2-streaming
||| - https://hackage.haskell.org/package/streaming
module Utils.Streaming

import Control.Monad.Trans
import Data.List
import Data.Nat

infixl 0 :>

public export
data Of : (a : Type) -> (b : Type) -> Type where
  (:>) : a -> Lazy b -> Of a b

export
Bifunctor Of where
  mapFst f (a :> b) = f a :> b
  mapSnd f (a :> b) = a :> f b
  bimap f g (a :> b) = f a :> g b

export
Functor (Of a) where
  map = mapSnd

||| The `Stream` type
public export
data Stream : (f : Type -> Type) -> (m : Type -> Type) -> (r : Type) -> Type where
  Step : Inf (f (Stream f m r)) -> Stream f m r
  Effect : Inf (m (Stream f m r)) -> Stream f m r
  Return : r -> Stream f m r
  Build : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r

||| Wrap a new layer of a `Stream`
export
wrap : f (Stream f m r) -> Stream f m r
wrap x = Step x

||| Wrap a new effect layer of a `Stream`
export
effect : m (Stream f m r) -> Stream f m r
effect x = Effect x

export
build : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r
build = \phi => phi Return (\x => Effect x) (\x => Step x)

export
fold : (Functor f, Monad m) => (r -> b) -> (m b -> b) -> (f b -> b) -> Stream f m r -> b
fold return effect step (Return x) = return x
fold return effect step (Effect x) = effect (fold return effect step <$> x)
fold return effect step (Step x) = step (fold return effect step <$> x)
fold return effect step (Build g) = g return effect step

export
destroy : (Functor f, Monad m) => (f a -> a) -> (m a -> a) -> (r -> a) -> Stream f m r -> a
destroy step effect return = fold return effect step

||| Unfold a `Stream`
public export
unfold : (Functor f, Monad m) => (a -> m (Either r (f a))) -> a -> Stream f m r
unfold f a = Effect $ do
  Right a' <- f a
  | Left r => pure (Return r)
  pure (Step (unfold f <$> a'))

export
inspect : (Functor f, Monad m) => Stream f m r -> m (Either r (f (Stream f m r)))
inspect = destroy (pure . (Right . map (effect {f} {m} . map (either Return wrap)))) join (pure . Left)

export
hoist : (Functor f, Monad m) => (forall a. m a -> n a) -> Stream f m r -> Stream f n r
hoist f = fold Return (\x => Effect $ f x) (\x => Step x)

public export
(Functor f, Monad m) => Functor (Stream f m) where
  map f x = Build (\return, effect, step => fold (return . f) effect step x)

mutual
  public export
  (Functor f, Monad m) => Applicative (Stream f m) where
    pure = Return
    x <*> y = do
      f <- x
      v <- y
      pure (f v)

  public export
    (Functor f, Monad m) => Monad (Stream f m) where
      x >>= k = assert_total Build (\return, effect, step => fold (fold return effect step . k) effect step x)

public export
MonadTrans (Stream f) where
  lift x = Effect (map Return x)

public export
(HasIO m, Monad (Stream f m)) => HasIO (Stream f m) where
  liftIO x = lift (liftIO x)

export
yield : Monad m => a -> Stream (Of a) m ()
yield x = Step (x :> Return ())

export
run : Monad m => Stream m m r -> m r
run (Return x) = pure x
run (Effect x) = x >>= run
run (Step x) = x >>= run
run (Build g) = run (build g)

||| Turns a `Stream` into a list
public export
toList : Monad m => Stream (Of a) m r -> m (List a, r)
toList = destroy (\(a :> b) => map (mapFst (a ::)) b) join (\x => pure (Nil, x))

||| `toList` but discards the result
public export
toList_ : Monad m => Stream (Of a) m r -> m (List a)
toList_ = destroy (\(a :> b) => map (a ::) b) join (const (pure Nil))

||| Construct a `Stream` from a `List` with a result type
public export
fromList : r -> List a -> Stream (Of a) m r
fromList r Nil = Return r
fromList r (a :: as) = Step (a :> fromList r as)

||| `fromList` but discards the result
public export
fromList_ : List a -> Stream (Of a) m ()
fromList_ = fromList ()

||| Concatenate an element into a `Stream`
public export
cons : a -> Stream (Of a) m r -> Stream (Of a) m r
cons x stream = Step (x :> stream)

export
next : Monad m => Stream (Of a) m r -> m (Either r (a, Stream (Of a) m r))
next stream = inspect stream >>= \case
  Left r => pure (Left r)
  Right (x :> xs) => pure (Right (x, xs))

export
mapf : (Functor f, Monad m) => (forall x. f x -> g x) -> Stream f m r -> Stream g m r
mapf f s = Build (\return, effect, step => fold return effect (step . f) s)

export
mapfM : (Monad m, Functor f) => (forall x. f x -> m (g x)) -> Stream f m r -> Stream g m r
mapfM f stream = Build (\return, effect, step => fold return effect (effect . map step . f) stream)

export
maps : Monad m => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
maps f s = mapf (mapFst f) s

export
mapsM : Monad m => (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r
mapsM f s = mapfM (\(c :> g) => (:> g) <$> f c) s

export
fors : Monad m => (a -> m x) -> Stream (Of a) m r -> m r
fors f = fold pure join (\(x :> act) => ignore (f x) >> act)

export
takeStream : Monad m => Nat -> Stream (Of a) m r -> m (List a, Either r (Stream (Of a) m r))
takeStream n stream = loop [] n stream where
  loop : List a -> Nat -> Stream (Of a) m r -> m (List a, Either r (Stream (Of a) m r))
  loop acc Z stream = pure (acc, Right stream)
  loop acc (S n) stream = do
    Right (elem, rest) <- next stream
    | Left r => pure (acc, Left r)
    loop (snoc acc elem) n rest

||| Split the stream into stream of sublist of length at most n
export
chunksOf : Monad m => (n : Nat) -> {auto 0 ok : NonZero n} -> Stream (Of a) m r -> Stream (Of (List a)) m r
chunksOf n stream = do
  (chunk, Right rest) <- lift $ takeStream n stream
  | (chunk, Left r) => yield chunk >> pure r
  yield chunk *> chunksOf n rest

||| Consume all the content in the stream
export
consume : Monad m => Stream (Of a) m r -> m ()
consume = fold (const $ pure ()) join (\(a :> b) => b)


text:
foo : String
foo = "incomplete: \{ a <+> }"


text:
data DoorState = DoorClosed | DoorOpen

data DoorCmd : Type ->
               DoorState ->
               DoorState ->
               Type where
  Open : DoorCmd () DoorClosed DoorOpen
  Close : DoorCmd () DoorOpen DoorClosed
  RingBell : DoorCmd () DoorClosed DoorClosed

  Pure : ty -> DoorCmd ty state state
  (>>=) : DoorCmd a state1 state2 ->
       (a -> DoorCmd b state2 state3) ->
       DoorCmd b state1 state3

doorProg : DoorCmd () DoorClosed DoorClosed
doorProg = do RingBell
              Open
              Close

{-doorProgBad : DoorCmd ()
doorProgBad = do Open
                 Open
                 RingBell-}


text:
module Language.Elab.Deriving.Newtype

import Language.Reflection

import Language.Elab.Syntax

import Language.Elab.Types

import Util

-- newtype deriving
-- given a datatype name and a list of interface names, determine if it's a
-- newtype, determine if the type it's a newtype of has those instances,
-- generate them for the newtype.

-- Visibility is controlled by the user because this makes it easy enough to
-- have instances that we might want to derive them just for a private use.

%language ElabReflection

-- A more specific List for holding interface identifiers.
-- Interface identifiers are hardly ever going to be simply Type so if we want
-- to collect them we need to hold their type.
data IList : List Type -> Type where
  Nil : IList []
  (::) : (x : r) -> IList rs -> IList (r :: rs)

-- Convert our list of interfaces to qualified Names, vet them at the same time
-- for suitability for deriving. This might be the wrong place to do this check.
collectIList' : IList xs -> Elab (List (Name, (Name, List ArgInfo, TTImp)))
collectIList' [] = pure []
collectIList' (i :: is) = do
    IVar _ w <- quote i
      | _ => fail "Error with reflecting interface name in collectIList."

    -- do a tentative check that we have a valid interface
    -- namely that we're dealing with a one-constructor type and that it has
    -- only one spot let to fill, since our type fills it
    tyinfo <- makeTypeInfo w
    -- (qn,imp) <- lookupName w
    unless (length (filter (isExplicitPi . piInfo) tyinfo.args) == 1)
           $ fail $ (notApro tyinfo.name)
               ++ " It has more than one type argument left to fill."
    [singlecon] <- pure $ tyinfo.cons
      | _ => fail $ (notApro tyinfo.name)
               ++ " It has more than one constructor. " ++
                  "Interfaces are essentialy records of fields."

    pure $ (tyinfo.name, singlecon) :: !(collectIList' is)
  where
    notApro : Name -> String
    notApro n
      = extractNameStr n ++ " is not an appropriate type for newtype deriving."
    oneFillable : TTImp -> Bool
    oneFillable imp = go imp == 1
      where
        go : TTImp -> Int
        go (IPi _ _ ExplicitArg _ _ retTy) = 1 + go retTy
        go (IPi _ _ _ _ _ retTy) = go retTy
        go _ = 0

data Foo : Type where
  MkFoo : Int -> Foo

data Foo2 : Type -> Type where
  MkFoo2 : a -> Foo2 a

interface Fez r where
  fezfo1 : r -> r -> r
  fezfo2 : r -> r

Fez Int where
  fezfo1 x y = y*2
  fezfo2 x = x+1

interface Monad a => Fez2 a (r : Type) where
  constructor Fezfoborbo
  method : a Int
  -- fezfo12 : r -> r -> r
  -- fezfo22 : r -> r

interface Gorp2 a where
  constructor MkGorp2
  fap : a -> (named : Int) -> a -> Bool
  fapo : Bool -> (1 x : a) -> Char -> a
  ofap : (0 _ : a) -> Char
  o : a
  p : Char
  q : Foo2 Bool

interface Gorp3 a (b : Nat) where
  constructor MkGorp3
  p2 : a -> Char

Gorp2 Int where
  fap x i y = x == i
  fapo b a c = a
  ofap a = 'c'
  o = 9
  p = 'p'

record Wok a where
  constructor MkWok
  bopa : a -> Int
  fifw : Int -> Char -> a

record Poo where
  constructor Wup
  bop : Int
  fif : Int -> Char

export
interface MyEq a where
  constructor MkMyEq
  eq : a -> a -> Bool
  neq : a -> a -> Bool

MyEq Int where
  eq x y = x == y
  neq x y = x /= y

%hint
fooMyEq : MyEq Foo
fooMyEq = MkMyEq (\(MkFoo x),(MkFoo y) => eq x y) (\(MkFoo x),(MkFoo y) => neq x y)

interface Gaffer where
  constructor Gaf
-- Gaf : Language.Elab.Deriving.Newtype.Gaffer

-- this is where we accum our parameters, split up the fields
-- collect our arg type names then
-- spider along and make left pi args into fields
-- our return type is the deciding parameter name and a list of fields
separateFields : TTImp -> Elab (Name, List (Name, TTImp))
separateFields (IPi _ _ ImplicitArg (Just det) (IType _) retTy) = do
    fs <- sepFields retTy
    pure $ (det, fs)
  where
    sepFields : TTImp -> Elab (List (Name, TTImp))
    sepFields (IPi _ _ _ name0 argTy retTy) = do
      Just name <- pure name0
        | _ => fail "Unexpected empty field name."
      rest <- sepFields retTy
      pure $ (name,argTy) :: rest
    sepFields retTy = pure []
separateFields _ = fail "Interface has the wrong shape."

-- I'm having issue with taking an arg at a time, take all the args then case
-- one at a time.
-- TODO, this works, so clean it up majorly.
-- NB implicit'' which might be nice to use elsewhere too
ntWrapField : (ntty : TTImp) -> (ntcon : Name) -> (wrappedty : TTImp)
           -> (det : Name) -> (fname : Name) -> (fimp : TTImp) -> Elab TTImp
ntWrapField ntty ntcon wrappedty det fname fimp = mkFun fimp
  where
    isWrappedType : TTImp -> Bool
    isWrappedType (IVar _ n) = n == det
    isWrappedType _ = False

    mkLam : List Name -> TTImp -> Elab TTImp
    mkLam ns (IPi _ c ExplicitArg nam argTy retTy) = do
      argname <- genSym "lam"
      let lamhead = iLam c ExplicitArg (Just argname)
      if  isWrappedType argTy
        then do
          argname' <- readableGenSym "lamc"
          cont <- mkLam (argname' :: ns) retTy
          pure $ lamhead implicit'' $ iCase (iVar argname) implicit''
                [patClause `( ~(iVar ntcon) ~(bindNameVar argname')) cont]
        else pure $ lamhead implicit'' !(mkLam (argname :: ns) retTy)
    mkLam ns (IPi _ _ _ _ _ retTy) = mkLam ns retTy
    -- Apply our field name to our collected args, we check the return
    -- type, since if it is wrapper type we should be wrapping the expression
    mkLam ns retTy = do
      let appedifacecon = IImplicitApp EmptyFC (iVar fname) (Just det) wrappedty
      -- let appedifacecon = (iVar fname)
      let body = foldr (\n,tt => tt `iApp` iVar n) appedifacecon ns
      pure $ if isWrappedType retTy
        then iVar ntcon `iApp` body
        else body
    -- mkCases : List Name -> TTImp
    -- If our field type has no argument, check if we should wrap the result type
    mkFun : TTImp -> Elab TTImp
    mkFun (IVar _ n) = pure $ if n == n then iVar ntcon `iApp` iVar fname else iVar fname
    mkFun pi@(IPi _ _ _ _ _ _) = mkLam [] pi
    mkFun _ = pure $ iVar fname

-- Derive via taking an object and spidering it, we can't get an instance object
-- programatically yet but it's probably a bug that we can't, so let's bet on
-- that changging.
-- We need the ntname, ntcontypimpl, iface name, iface conname, iface objimpl
deriveGeneralImpl : (ntname : Name) -> (nttype : TTImp) -> Visibility
                 -> (ntcon : Name) -> (wrappedtype : TTImp) -> TypeInfo -> Elab ()
deriveGeneralImpl ntname nttype vis ntcon wrappedty tyinfo (iname,icon)  = do
  let defname = UN ("ntImpl_" ++ extractNameStr ntname ++ extractNameStr tyinfo.name)
      hty = mkTy defname (iVar iname `iApp` nttype)
      head = iClaim MW vis [Hint True] hty
  (_,impl) <- lookupName tyinfo.name
  fillty <- makeTypeInfo tyinfo.name
  [arg] <- pure fillty.args
    | _ => fail "badshape"
  (_,conimp) <- lookupName tyinfo.cons.name
    | _ => fail "sdfsdf"
  (det,fields) <- separateFields conimp
  wrappedfs <- traverse (\(fname,imp) => ntWrapField nttype ntcon wrappedty det fname imp) fields

  let cac = foldl (\tt,f => tt `iApp` f) (iVar icon.name) wrappedfs
      def = iDef defname [patClause (iVar defname) cac]

  logDecls 1 "def" [head,def]

  declare [head,def]

  pure ()

-- we determine if we have a newtype constructor ourselves but we could just ask
-- idris as well since that info is in the Context
newtypeDerive : Name -> Visibility -> (ifaces : IList ts) -> Elab ()
newtypeDerive n vis ilist = do
    -- We need to very carefully check ifsomething is a newtype, otherwise we've
    -- lied.
    typeinfo <- makeTypeInfo n
    [con] <- pure $ typeinfo.cons
      | _ => fail notNT
    -- check that our constructor has the right form
    [arg] <- pure $ filter (not . isUse0 . count
                          && isExplicitPi . piInfo) con.args
      | _ => fail notNT

    -- Here we validate our list of interfaces
    ns@(_::_) <- collectIList' ilist
      | [] => fail "Interface list for deriving was empty."

    -- traverse (deriveSpecialImpl ...) ns
    -- ^ things like Show should farm out to Show deriving

    traverse (deriveGeneralImpl n typeinfo.type vis con.name arg.type) ns

    pure ()
  where
    notNT : String
    notNT = extractNameStr n ++ " is not a newtype. A newtype has exactly one
                                  constructor with exactly one used field."

%runElab newtypeDerive `{{Foo}} Private [Eq]
-- %runElab newtypeDerive `{{Foo}} Private [Gorp2, Eq, Ord]
-- %runElab newtypeDerive `{{Foo}} Private [Eq, Ord]

-- ntElim_Foo : (x : Foo) -> MkFoo x = x
-- ntElim_Foo x = ?laf_rhs

-- <int-e> @let ifM b t f = b >>= \b' -> if b' then t else f
-- <int-e> :t ifM even negate (const 0)

lef : Ord Int
lef = %search

rer : Ord Foo
rer = let r = the (Ord Int) %search
      in ?SDFfds

-----------------------------
-- Testing
-----------------------------

data Foo1 : Type where -- newtype, one con, one used field
  MkFoo1 : Int -> Foo1

-- data Foo2 : Type where
  -- MkFoo2 : Char -> Int -> Foo2 -- not nt, two used fields

data Foo3 : Type -> Type where -- newtype
  MkFoo3 : Int -> Foo3 a

data Foo4 : Type -> Type where -- not nt, two cons
  MkFoo4 : a -> Foo4 a
  MkFoo4' : a -> Foo4 a

data Foo5 : Type -> Type -> Type where -- newtype, one used field
  MkFoo5 : a -> (0 _ : b) -> Foo5 a b

-- little ugly here
-- %runElab newtypeDerive `{{Foo1}} [`{{Eq}}, `{{Show}}, `{{Ord}}]

-- Foo2 is not a newtype
-- %runElab newtypeDerive `{{Foo2}} [`{{Eq}}, `{{Show}}, `{{Ord}}]

-- %runElab newtypeDerive `{{Foo3}} [`{{Eq}}, `{{Show}}, `{{Ord}}]

-- Foo4 is not a newtype
-- %runElab newtypeDerive `{{Foo4}} [`{{Eq}}, `{{Show}}, `{{Ord}}]

-- %runElab newtypeDerive `{{Foo5}} [`{{Eq}}, `{{Show}}, `{{Ord}}]

-- Wibble isn't in scope
-- %runElab newtypeDerive `{{Foo1}} [`{{Eq}}, `{{Show}}, `{{Ord}}, `{{Wible}}]


text:
module Main

import Js.ASync

main : JS_IO ()
main = do
  let f = the ((String,String) -> String -> (String, Maybe String ))  (\(_, s),y => (s, Just s))
  case snd $ f ("t", "tst") "cenas" of
    Just z => putStr' z

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Main

import Data.Fin
import Effects
import Effect.StdIO
import Data.Complex
import Graphics.Color
import Graphics.SDL2.SDL
import Graphics.SDL2.Effect
import Graphics.Cairo.Effect
import Graphics.Shape

-- ================================================================
-- Interactive Penrose Tiling
-- ================================================================

%default total

-- ----------------------------------------------------------------
-- a bit of infrastructure
-- ----------------------------------------------------------------

||| Type alias for convenience
C : Type
C = Complex Double

||| Division of Complex Numbers
divC : C -> C -> C
divC (a:+b) (c:+d) = let real = (a*c+b*d) / (c*c+d*d)
                         imag = (b*c-a*d) / (c*c+d*d)
                     in
                        (real:+imag)

||| the golden ratio constant
goldenRatio : Double
goldenRatio = 0.5 * (1 + (sqrt 5))

||| we model a triangle using a triple of complex numbers
Tri : Type
Tri = (C, C, C)

-- ----------------------------------------------------------------
-- Calculate the penrose tiling
-- ----------------------------------------------------------------

data Penrose = Red Tri | Blue Tri

implementation Show Penrose where
    show (Red x)  = "Red " ++ show x
    show (Blue x) = "Blue " ++ show x

||| Penrose subdivide
||| This computes a single step in the tiling
||| see also: http://preshing.com/20110831/penrose-tiling-explained/
penroseSubdivide : Penrose -> List Penrose
penroseSubdivide (Blue (a, b, c)) = let q = b + ((a-b) `divC` (goldenRatio :+ 0))
                                        r = b + ((c-b) `divC` (goldenRatio :+ 0))
                                    in [Blue (r, c, a), Blue (q, r, b), Red (r, q, a)]
penroseSubdivide (Red (a, b, c))  = let p = a + ((b-a) `divC` (goldenRatio :+ 0))
                                    in [Red (c, p, b), Blue (p, c, a)]

||| A Stream of all Tilings for a given initial triangle
||| a single tiliing consists of a list of triangles
penroseTiling : Tri -> Stream (List Penrose)
penroseTiling triangle = penroseTiling' [(Red triangle)]
                         where penroseTiling' : (List Penrose) -> Stream (List Penrose)
                               penroseTiling' triangles = iterate (\tris => tris >>= penroseSubdivide) triangles

||| Creates an initial upside down triangle
initialTriangle : (height: Int) -> (angle: Double) -> Tri
initialTriangle height angle = let rad = 2 * pi * angle / 360
                                   y = (tan (rad / 2)) * (cast height)
                               in ( 0:+0,  (-1) * y :+ (-1) * (cast height), y :+ (-1) * (cast height))

||| computes the full tiling
||| @level number of subdivide iterations
||| @numTriangles the number of symetric triangles
penroseTriangles : (level: Nat) -> (numTriangles: Int) -> List Penrose
penroseTriangles level numTriangles = let angle = 360.0 / (cast numTriangles)
                                          tilings = penroseTiling $ initialTriangle 200 angle
                                      in head (drop level tilings)

-- ----------------------------------------------------------------
-- Cairo Rendering
-- ----------------------------------------------------------------

red : Color
red = RGBA 250 140 89 255

green : Color
green = RGBA 143 206 94 255

||| get the color for drawing each individual triangle
getColor : Penrose -> Color
getColor (Red  _) = red
getColor (Blue _) = green

getTriangle : Penrose -> Tri
getTriangle (Red triangle) = triangle
getTriangle (Blue triangle) = triangle

||| draws a single penrose triangle using the cairo effect
renderTriangle : Penrose -> { [CAIRO_ON] } Eff ()
renderTriangle penrose = with Effects do
  setSourceRGBA $ getColor penrose
  setLineWidth 6
  let (x1:+y1, x2:+y2, x3:+y3) = getTriangle penrose
  triangle (x1, y1) (x2, y2) (x3, y3)
  fill

renderTriangles : List Penrose -> Double -> Nat -> { [CAIRO_ON] } Eff ()
renderTriangles triangles angle Z = pure ()
renderTriangles triangles angle (S k) = with Effects do renderTriangle' triangles
                                                        rotate angle
                                                        renderTriangles triangles angle k
                                                     where
    renderTriangle' : List Penrose -> { [CAIRO_ON] } Eff ()
    renderTriangle' [] = pure ()
    renderTriangle' (t :: ts) = with Effects do
          renderTriangle t
          renderTriangle' ts

-- ----------------------------------------------------------------
-- Setup and Main Loop
-- ----------------------------------------------------------------

||| type synonym for the effectful programm
||| we need at least the SDL and CAIRO effects
||| STDIO is only needed for optional logging
Prog : (sdl: Type) -> (cairo: Type) -> (result : Type) -> Type
Prog sdl cairo t = { [SDL sdl,      -- the SDL effect
                      CAIRO cairo,  -- Cairo effect
                      STDIO]        -- a std io effect
                     } Eff t

||| convenvience shorthand for a running program
Running : Type -> Type
Running t = Prog SDLCtx () t

||| the application state containing the current subdivision level
||| and number of initial triangles
data AppState = MkState Nat Nat

||| draw the current application state
draw : AppState -> Running ()
draw (MkState angles level) =  with Effects do
  renderClear white
  ctx <- getSdlCtx
  getCanvas ctx
  center

  let numTriangles = cast angles + 4
  let solution = penroseTriangles level numTriangles
  let angle = (2 * pi / (cast numTriangles))

  renderTriangles solution angle (cast numTriangles)

  closeCanvas
  render

||| process sdl input events
process : AppState -> Maybe Event -> Maybe AppState
process _                       (Just (KeyDown KeyEsc))        = Nothing
process _                       (Just (AppQuit))               = Nothing
process (MkState angles level)  (Just (KeyDown KeyUpArrow))    = Just (MkState (S angles) level)
process (MkState Z level)       (Just (KeyDown KeyDownArrow))  = Just (MkState Z level)
process (MkState (S k) level)   (Just (KeyDown KeyDownArrow))  = Just (MkState k level)
process (MkState angles level)  (Just (KeyDown KeyRightArrow)) = Just (MkState angles (S level))
process (MkState angles Z)      (Just (KeyDown KeyLeftArrow))  = Just (MkState angles Z)
process (MkState angles (S k))  (Just (KeyDown KeyLeftArrow))  = Just (MkState angles k)
process state                   _                              = Just state

%default partial

||| the effectful main application and loop
emain : Prog () () ()
emain = do putStrLn "Initialising"
           initialise "Penrose" 800 600
           putStrLn "Initialised"
           eventLoop (MkState Z Z)
           quit
           pure ()
        where
          eventLoop : AppState -> Running ()
          eventLoop state = do draw state
                               ev <- poll
                               let res = process state ev
                               case res of
                                 (Just newState) => eventLoop newState
                                 _               => pure ()

main : IO ()
main = runInit [(), -- initial state for the SDL2 effect (nothing needs to go in here)
                (),
                ()  -- initial state for the StdIO effect
                ]
       emain

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


text:
-- ----------------------------------------------------------------- [ Eff.idr ]
-- Module    : Eff.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| XPath but in an effectfull context.
module XML.XPath.Eff

import Effects
import Effect.Exception

import XML.DOM
import XML.XPath

export
queryE : String
      -> Document ty
      -> {auto prf : CanQuery ty}
      -> Eff (Either XPathError (ty' ** XPathResult ty')) xs
queryE qstr doc {ty=ELEMENT} = pure (queryElem qstr doc)
queryE qstr doc {ty=DOCUMENT} = pure (queryDoc qstr doc)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml