let print = Printf.printf;;
Sys.command "ocaml -version";;

type variable = string;;

type terme =
    | V of variable
    | A of terme * terme
    | F of variable * terme
;;

let identite = F("x", V("x"));;

let identite_2 = F("y", V("y"));;

let omega = A(F("x", A(V("x"), V("x"))), F("x", A(V("x"), V("x"))));;

let u = F("x", A(V("x"), V("x")));;
let omega = A(u, u);

let sprintf = Format.sprintf;;

let rec string_of_terme = function
    | V(s) -> s
    | A(u, v) -> sprintf "(%s)(%s)" (string_of_terme u) (string_of_terme v)
    (* "(" ^ (string_of_terme u) ^ ")" ^ "(" ^ (string_of_terme v) ^ ")" *)
    | F(s, u) -> sprintf "λ %s. (%s)" s (string_of_terme u)
    (* "lambda " ^ s ^ ".(" ^ (string_of_terme u) *)
;;

print_endline (string_of_terme identite);;
print_endline (string_of_terme identite_2);;
print_endline (string_of_terme omega);;

let sprintf = Format.sprintf;;

let rec python_of_terme = function
    | V(s) -> s
    | A(u, v) -> sprintf "(%s)(%s)" (python_of_terme u) (python_of_terme v)
    | F(s, u) -> sprintf "lambda %s: (%s)" s (python_of_terme u)
;;

print_endline (python_of_terme identite);;
print_endline (python_of_terme identite_2);;
print_endline (python_of_terme omega);;

let execute_python_string (s : string) : int =
    Sys.command (sprintf "python -c 'print(%s)'" s)
;;

execute_python_string (python_of_terme identite);;

execute_python_string (python_of_terme omega);;

let none = F("x", V("x"));;

let compose u v = A(u, v);;

let si = F("cond", F("v", F("f", A(A(V("cond"), V("v")), V("f")))));;

print_endline (string_of_terme si);;

let vrai = F("v", F("f", V("v")));;
let faux = F("v", F("f", V("f")));;

print_endline (string_of_terme vrai);;
print_endline (string_of_terme faux);;

let zero = F("f", F("x", V("x")));;
let un = F("f", F("x", A(V("f"), V("x"))));;

let terme_of_int (n : int) : terme =
    let rec aux = function
        | 0 -> V("x")
        | n -> A(V("f"), aux (n-1))
    in
    F("f", F("x", (aux n)))
;;

let deux = terme_of_int 2;;

print_endline (string_of_terme deux);;
execute_python_string (python_of_terme deux);;

let entier_natif_python = "lambda c: c(lambda x: x+1)(0)";;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme deux));;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 10)));;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 100)));;

let successeur = F("n", F("f", F("z", A(V("f"), A(A(V("n"), V("f")), V("z"))))));;

print_endline (string_of_terme successeur);;

let dix = terme_of_int 10;;
let onze = A(successeur, dix);;

let onze2 = terme_of_int 11;;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme dix));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme onze2));;

let somme = F("n", F("m", F("f", F("z", A((A(V("n"), V("f"))), A((A(V("m"), V("f"))), V("z")) )))));;

print_endline (string_of_terme somme);;

let trois = A(A(somme, un), deux);;

let trois2 = terme_of_int 3;;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme trois2));;

let mul = F("n", F("m", F("f", F("z", A(A(V("m"), A(V("n"), V("f"))), V("z"))))));;

let trois = terme_of_int 3 ;;
let six = A(A(mul, trois), deux);;
let six2 = A(A(mul, deux), trois);;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme six2));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (terme_of_int 6)));;

let a = V("a") and b = V("b") and f = V("f");;
let pair = F("a", F("b", F("f", A(A(f, a), b))));;

let gauche = F("f", A(f, vrai));;
let droite = F("f", A(f, faux));;

let exemple_pair = A(A(pair, deux), trois);;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(gauche, exemple_pair))));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme (A(droite, exemple_pair))));;

let constructeur_pair u v = A(A(pair, u), v);;
let pi1 u = A(gauche, u);;
let pi2 u = A(droite, u);;
let constructeur_succ u = A(successeur, u);;

let pair_00 = constructeur_pair zero zero;;

let p = V("p");;
let succ_1 = F("p", constructeur_pair (constructeur_succ(pi1(p))) (pi1(p)));;

let n = V("n");;
let predecesseur = F("n", pi2(A(A(n, succ_1), pair_00)));;

let cinq = A(predecesseur, (terme_of_int 6));;
let cinq2 = terme_of_int 5;;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme cinq2));;

let zero2 = A(predecesseur, zero);;

execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero2));;
execute_python_string (sprintf "(%s)(%s)" entier_natif_python (python_of_terme zero));;