Created
May 18, 2015 10:38
-
-
Save garrigue/603fcb00c8a885dec9a1 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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 -> () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment