(* On ne va pas s'amuser à encoder des machines de Turing; pour aller plus
vite, on va utiliser les combinateurs S K. C'est moralement du λ-calcul un
peu obfusqué.
https://en.wikipedia.org/wiki/SKI_combinator_calculus
*)
type sk =
  App of sk * sk | S | K

(* On implémente une stratégie de réduction call-by-name. Noter qu'on
   donne explicitement un nombre d'étapes de réductions (ce nombre d'étape
   est un poil fantaisiste vu le 3ème sous-cas, mais ce n'est pas très
   important). *)
let rec eval (n : int) (t : sk) =
  if n = 0 then
    t
  else
   match t with
   App (App (K, x), y) -> eval (n-1) y
 | App (App (App (S, x), y), z) -> eval (n-1) (App(App(x, z), App(y, z)))
 | App (x, y) -> eval (n-1) (App (eval n x, eval n y))
 | t -> t

let normal (t : sk) = t = eval 1 t

(* On construit une énumération exhaustive des termes SK en commençant par
   S. (Exercice: prouver que le programme ci-dessous termine et est correct...) *)
let rec succ_sk = function
   S -> K
 | K -> App (S, S)
 | App (S, x) -> App(succ_sk x, S)
 | App (x, y) -> App(pred_sk x, succ_sk y)
and pred_sk = function
 | S -> raise (Invalid_argument "pred_sk undefined on S")
 | K -> S
 | App (S, S) -> K
 | App (x, S) -> App (S, pred_sk x)
 | App (x, y) -> App (succ_sk x, pred_sk y)


(* Avec ce petit bout de formalisme des fonctions calculables, on est prêt!

On définit le type des arbres, et l'arbre de Kleene dans la foulée. *)

type path = bool list
type tree = path -> bool

(* slow est une fonction arbitraire int -> int qui tend vers l'infini.
Je l'ai mise là comme paramètre additionel, car plus on prend quelque chose avec
un taux de croissance faible, plus l'arbre obtenu est feuillu. Pour faire
tourner des exemples, mieux vaut un arbre feuillu!
*)

let slow (n : int) : int =
  let slow_aux n = n+1 |> float_of_int |> log |> int_of_float in
  slow_aux @@ slow_aux @@ slow_aux n

let kleene_tree : tree =
  let rec check n tm =
    function [] -> true
           | h :: t -> let ntm = eval (slow n) tm in
                       ((h && normal ntm) = (ntm = K)) && check n (succ_sk tm) t
  in
  fun l -> check (List.length l) S l

(* Avec cet arbre, on peut donc coder une bijection entre les espaces de Cantor
   et Baire effectif. Pour se faire, on définit d'abord quelque combinateurs sur les
   arbres. *)

let nexttree (b : bool) (t : tree) : tree =
  fun l -> t (b :: l) 

(* Prédicat qui nos donne les chemins minimaux qui sortent d'un arbre. *)
let rec frontier (t : tree) : path -> bool = function
   [] -> not (t [])
 | b :: p' -> t [] && frontier (nexttree b t) p'

(* Énumération naïve des chemins de l'arbre binaire complet. *)
let nextpath (p : path) : path =
   let rec aux acc = function
    [] -> List.rev_map not (true :: acc)
  | true :: p' -> aux (true :: acc) p'
  | false :: p' -> List.rev_append (List.map (fun _ -> false) acc) (true :: p')
   in aux [] p

(* Bijection des chemins sortant minimaux dans ℕ. *)
let kt_of_nat =
  let rec aux c n =
   if frontier kleene_tree c then
     match n with
      0 -> c
    | k -> aux (nextpath c) (n-1)
   else 
    aux (nextpath c) n
  in aux []

let nat_of_kt p =
  let rec aux n =
    if kt_of_nat n = p then n else aux (n + 1)
  in
  aux 0

type cantor = int -> bool
type baire = int -> int

(* D'abord, on construit la fonction Cantor → Baire.

Pour commencer, étant donné f dans Cantor, on cherche le préfixe
minimal sortant de l'arbre de Kleene. *)
let nextoutgoing (f : cantor) : path =
  let rec aux acc t' f =
    if not (t' []) then List.rev acc
    else aux (f 0 :: acc) (nexttree (f 0) t') (fun n -> f (n + 1))
  in aux [] kleene_tree f

(* On itère. *)
let rec outgoingseq (f : cantor) : int -> path = function
   n -> nextoutgoing (fun k -> f (k + outgoingseqlen f (n-1)))
and outgoingseqlen (f : cantor) = function
   -1 -> 0
 | n -> List.length (outgoingseq f n) + outgoingseqlen f (n - 1)

(* Et paf. *)
let baire_of_cantor (f : cantor) : baire =
  fun n -> nat_of_kt (outgoingseq f n)

(* Pour Baire → Cantor, on définit d'abord la concaténation infinie. *)
let rec concat (f : int -> 'a list) (n : int) : 'a =
  let l = f 0 in
  let k = List.length l in
  if n < k then List.nth l n
  else concat (fun m -> f @@ 1 + m) (n - k)

(* Et ensuite on applique point à point kt_of_nat auparavant. *) 
let cantor_of_baire (f : baire) : cantor =
  concat (fun k -> kt_of_nat (f k))