minichess.ml

type x = X
type o = O

type 'a l = 'a * 'a * 'a
type 'a c = 'a * 'a * 'a
type 'a s = 'a l c

type 't lfirst = 'a * 'b * 'c
  constraint 't = 'a * ('b * 'c)

type 't llast = 'a * 'b * 'c
  constraint 't = ('a * 'b) * 'c

type 't cfirst = 'a * 'b * 'c
  constraint 't = 'a * ('b * 'c)

type 't clast = 'a * 'b * 'c
  constraint 't = ('a * 'b) * 'c

type start =
  < ul:x s ; up:x c;      ur:x s ;
    le:x l ; ce:x;      ri: o l;
    ld:x s; dw: o c; dr: o s
  >

type 't fcol =
  ('l1 * 'r1) lfirst
  * ('l2 * 'r2) lfirst
  * ('l3 * 'r3) lfirst
  constraint 't =
    ( 'l1 * 'l2 * 'l3) *
    ( 'r1 * 'r2 * 'r3)

type 't lcol =
  ('l1 * 'r1) llast
  * ('l2 * 'r2) llast
  * ('l3 * 'r3) llast
  constraint 't =
    ( 'l1 * 'l2 *'l3) * ( 'r1 * 'r2 *'r3)

type (_,_) move =
  | Right:(
      < ul:('ul * _) lcol ; up:'up;   ur:('nur * 'ur ) fcol;
        le:('le *_) llast; ce:x;   ri:(o * 'ri) lfirst;
        ld:('ld * _) lcol ; dw:'dw; dr: ('ndr * 'dr) fcol;
      >,
      < ul:('up * 'ul) fcol; up:'nur;  ur:('ur * x c) lcol;
        le:(x * 'le) lfirst; ce:x;  ri:('ri * x) llast;
        ld:('dw * 'ld) fcol; dw:'ndr; dr: ('dr * x c) lcol
      >
    ) move
  | Left:(
      < ul:('nul * 'ul) fcol ; up:'up;   ur:('ur * _ ) lcol;
        le:(o * 'le) lfirst; ce:x;   ri:('ri * _) llast;
        ld:('nld * 'ld) fcol ; dw:'dw; dr: ('dr * _) lcol;
      >,
      < ul:('ul * x c) lcol; up:'nul; ur:('up * 'ur) fcol;
        le:('le * x) llast;   ce:x;   ri:(x * 'ri) lfirst;
        ld:('ld * x c) lcol; dw:'nld; dr: ('dw * 'dr) fcol
      >
    ) move
  | Up:(
      < ul:('nul * 'ul) cfirst; up:(o * 'up ) cfirst;  ur:('nur * 'ur) cfirst;
        le:'le;                ce:x;                   ri:'ri;
        ld:('ld * _) clast;     dw: ('dw * _) clast ;     dr:('dr * _) clast;
      >,
      < ul: ('ul * x l) clast; up:('up * x) clast;  ur: ('ur * x l) clast;
        le:'nul;               ce:x;               ri:'nur;
        ld:('le * 'ld) cfirst;  dw:(x * 'dw) cfirst; dr:('ri * 'dr) cfirst
      >
    ) move
  | Down:(
      < ul:('ul * _ ) clast;     up:('up * _ ) clast;  ur:('ur * _) clast;
        le:'le;                  ce:x;               ri:'ri;
        ld:('nld * 'ld) cfirst;  dw: (o * 'dw) cfirst ; dr:('ndr * 'dr) cfirst;
      >,
      < ul: ('le * 'ul) cfirst ; up: (x * 'up) cfirst; ur: ('ri *'ur) cfirst;
        le:'nld;                ce:x;                ri:'ndr;
        ld:('ld * x l) clast;   dw:('dw * x) clast;   dr:('dr * x l) clast
      >
    ) move



type _ path =
  | []: start path
  | (::) : ('a,'b) move * 'a path -> 'b path


let path: _ path = [Right;Right;Right]

type hamiltonian = <ul: x s; up: x c; ur: x s;
                    le:x l;  ce: x  ; ri: x l;
                    ld: x s; dw: x c; dr: x s
                   >

let check: start path -> unit = function
  | [] -> ()
  | _ :: _ -> .

[@@@warning "@8@56@A"]
(** How to convice the typechecker that wazir's tours don't exist : *)
let there_is_no_wazir_tour: 'a. hamiltonian path -> 'a = function
  | [ _;_;_
     ;_;_;_;_
     ;_;_;_;_
     ;_;_;_;_
     ]-> .
(* ^ this compiles ^ *)

(** Wait a second ... *)
(** v This does not compile v *)
let find_hamiltonian:hamiltonian path -> _ = function
  | [ _;_;_
     ;_;_;_;_
     ;_;_;_;_
     ;Down;Right;Right;Right
     ]-> .
(* The compiler just found a wazir tour. *)