turing.ml

(* Encoding termination of a Turing machine into a GADT *)

type s0 and s1 and s2 and s3 and s4 and fin
type c0 and c1 and c2 and c3 and blank
type left and right
type endt

type ('st_in, 'head_in, 'st_out, 'head_out, 'lr) transition =
  | Tr1 : (s0, 'a, s1, 'a, left) transition

type ('state, 'head, 'left, 'right) terminates =
  | Tm_fin : (fin, _, _, _) terminates
  | Tm_mv_left :
      ('st_in, 'head_in, 'st_out, 'head_out, left) transition *
      ('st_out, 'head_out, 'left, 'head_out * 'right) terminates ->
      ('st_in, 'head_in, 'head * 'left, 'right) terminates
  | Tm_mv_right :
      ('st_in, 'head_in, 'st_out, 'head_out, right) transition *
      ('st_out, 'head_out, 'head_out * 'left, 'right) terminates ->
      ('st_in, 'head_in, 'left, 'head * 'right) terminates
  | Tm_ext_left :
      ('state, 'head, blank * endt, 'right) terminates ->
      ('state, 'head, endt, 'right) terminates
  | Tm_ext_right :
      ('state, 'head, 'left, blank * endt) terminates ->
      ('state, 'head, 'left, endt) terminates

type goal = (s0, c0, endt, c1 * (c2 * endt)) terminates

(* Now, if the exhaustiveness check were complete, the following should
   only warn when the Turing machine defined by transition terminates *)
   
let f : goal option -> unit = function None -> ()