type ('a,'b) plus = Inl of 'a | Inr of 'b

type 'a next = Later of (unit -> 'a)
type 'a omega = Cons of 'a * 'a omega next
type 'a delta = 'a
type ('a, 'b) arr = 'a -> 'b

type 'a ty =
  Tconst : 'a delta ty
| Tomega : 'a omega ty
| Tnext : 'a ty -> 'a next ty
| Tprod : 'a ty * 'b ty -> ('a * 'b) ty
| Tarr : 'a ty * 'b ty -> ('a, 'b) arr ty
| Tplus : 'a ty * 'b ty -> ('a, 'b) plus ty

type ('a, 'b) tm =
  Id : ('a, 'a) tm
| Pair : ('a, 'b) tm * ('a, 'c) tm -> ('a, 'b * 'c) tm
| Proj1 : ('a * 'b, 'a) tm
| Proj2 : ('a * 'b, 'b) tm
| Delta : ('a -> 'b) -> ('a delta, 'b delta) tm
| Omega : ('a -> 'b) -> ('a omega, 'b omega) tm
| Comp : ('b, 'c) tm * ('a, 'b) tm -> ('a, 'c) tm
| Fold : ('a delta * 'a omega next, 'a omega) tm
| Unfold : ('a omega, 'a delta * 'a omega next) tm
| Fix : (('a next, 'a) arr, 'a) tm
| Lam : ('a * 'b, 'c) tm -> ('a, ('b, 'c) arr) tm
| Nextfun : ('a, 'b) tm -> ('a next, 'b next) tm
| Nextprod : ('a next * 'b next, ('a * 'b) next) tm
| App : (('a, 'b) arr * 'a, 'b) tm
| Tt : ('a, unit delta) tm
| Case : ('a -> ('b, 'c) tm) -> ('b * 'a delta, 'c) tm
| Next : ('a, 'a next) tm (* redondant, mais le typechecker me déteste *)

let next (x : 'a) : 'a next = Later (fun () -> x)

let rec interp : type a b. (a, b) tm -> a -> b = function
  Id -> fun x -> x
| Pair (t, u) -> fun x -> (interp t x, interp u x)
| Proj1 -> fst
| Proj2 -> snd
| Delta f -> f
| Fold -> fun (a, b) -> Cons (a, b)
| Unfold -> (function Cons (a, b) -> (a, b))
| Fix -> let rec fix f =
           f (Later (fun () -> fix f)) in fix
| Lam t -> fun x y -> interp t (x, y)
| App -> fun (f, x) -> f x
| Comp (f, g) -> fun x -> interp f (interp g x)
| Tt -> fun _ -> ()
| Nextprod -> (function (Later f, Later g) -> Later (fun () -> f (), g ()))
| Nextfun t -> (function Later f -> Later (fun () -> interp t (f ())))
| Next -> next

let tm_times : ('a, 'b) tm -> ('c, 'd) tm -> ('a * 'c, 'b * 'd) tm =
  fun t u -> Pair (Comp (t, Proj1), Comp (u, Proj2))

let tm_ilam : type a b c. ((a * b, c) arr, (a, (b, c) arr) arr) tm =
  Lam (Lam (Comp (App, (Pair (Comp (Proj1, Proj1),
                              Pair (Comp (Proj2, Proj1), Proj2))))))

let tm_fixparam : (('a * 'b next, 'b) arr, ('a, 'b) arr) tm =
  Comp (Lam (Comp (Fix, App)), tm_ilam)

let tm_elam (t : (('a,'b) arr, ('c, 'd) arr) tm) (u : ('a, 'b) tm) : ('c, 'd) tm =
  Comp (App, Pair (Comp (t, Lam (Comp (u, Proj2))) , Id))

let tm_Fixparam : type a b. (a * b next, b) tm -> (a, b) tm =
  fun x -> tm_elam tm_fixparam x

(* On simule un compteur c : ω → ω par la fonction synchrone f : Σ^ω → Σ^ω telle que
f(x)(n) = x_{c(n)}

On prend en paramètre un stream bool option omega ≡ 3^omega pour contrôler les
montées/descentes. Le compteur paramétré C : 3^ω × Σ^ω → Σ^ω satisfait les équations suivantes
C(c, x)(0) = x_0
C(c, x)(n+1) = C(c,x)(n) si c(n) = None
C(c, x)(n+1) = C(c,<x)(n) si c(n) = Some true (incrément)
C(c, x)(n+1) = C(c,x_0.x)(n) si c(n) = Some false (décrémentation)

Pour tester l'implèm, on prend Σ ≡ int, mais clairement, Σ ≡ 2 est suffisant pour
fabriquer une machine avec compteurs.
*)

let tm_nextarr : (('a, 'b) arr next, ('a next, 'b next) arr) tm =
  Lam (Comp (Nextfun App, Nextprod))

(*let tm_next : type a. (a omega, a omega next) tm =
  Comp (Proj2, ((tm_Fixparam (Pair (Proj1, Comp (Nextfun Proj1, Proj2)) : (a omega * (a omega * a omega next) next, a omega * a omega next) tm))))
*)

let tm_next = Next

let tm_const (d : 'a) : ('b, 'a delta) tm = Comp (Delta (fun () -> d), Tt)

let tm_ncons (d : 'a) : ('a omega, 'a omega) tm =
  Comp (Fold, Pair (tm_const d, tm_next))

let caseom (f : 'a -> ('b,'c) tm) : ('b * 'a omega, 'c) tm =
  Comp (Case f, tm_times Id (Comp (Proj1, Unfold)))

let tm_tail : ('a omega, 'a omega next) tm = Comp (Proj2, Unfold)

let tm_cmpt (d : 'a) : (bool option omega, ('a omega, 'a omega) arr) tm =
  tm_Fixparam (
        Lam (
        Comp (Fold,
         Pair (Comp (Proj1, Comp (Unfold, Proj2)),
               Comp (Comp (
                      Comp (App,
                            caseom (function None -> tm_times Id tm_next
                                           (* (assert false : ((('a omega next, 'a omega next) arr * 'a omega), ('a omega next, 'a omega next) arr * 'a omega next) tm)*)
                                          | Some true -> tm_times Id tm_tail
                                          | Some false -> tm_times Id (Comp (tm_next, tm_ncons d))
                                 )
                           ),
                            Pair (Pair (Comp (Proj2, Proj1), Proj2), Comp (Proj1, Proj1))
                           )
                     ,
                     tm_times (tm_times Id tm_nextarr) Id)
              )
             )))

let up (l : 'a list) : int -> 'a =
  let rec aux p = function
    [] -> aux [] (List.rev p)
  | h :: t -> function 0 -> h
                     | n -> aux (h :: p) t (n - 1)
  in aux [] l

let listn =
  let rec aux k = function 0 -> [] | n -> k :: (aux (k+1) (n-1)) in
  aux 0

let rec om_of_fun f = Cons (f 0, Later (fun () -> om_of_fun (fun k -> f (k+1))))
let rec fun_of_om (Cons (a, Later f)) = function 0 -> a | k -> fun_of_om (f ()) (k - 1)

let test l =
  let c = interp (tm_cmpt (-1)) in
  let n = List.length l in
  let ln = listn (n+1) in
  List.map (fun_of_om @@ c (om_of_fun (up l)) (om_of_fun (fun n -> n))) ln

let _ = test [None]