(* Exercices de programmation du chapitre 2 *)

(* La syntaxe abstraite des expressions mini-ML (comme au chapitre 1) *)

type expression =
    Var of string
  | Const of int
  | Op of string
  | Fun of string * expression
  | App of expression * expression
  | Paire of expression * expression
  | Fst of expression
  | Snd of expression
  | Let of string * expression * expression

(* Substitution d'une variable x par une expression b dans une expression a
   (comme au chapitre 1) *)

let rec subst a x b =
  match a with
    Var v -> if v = x then b else a
  | Const n -> a
  | Op o -> a
  | Fun(v, a1) -> if v = x then a else Fun(v, subst a1 x b)
  | App(a1, a2) -> App(subst a1 x b, subst a2 x b)
  | Paire(a1, a2) -> Paire(subst a1 x b, subst a2 x b)
  | Fst a1 -> Fst(subst a1 x b)
  | Snd a1 -> Snd(subst a1 x b)
  | Let(v, a1, a2) -> Let(v, subst a1 x b, if v = x then a2 else subst a2 x b)

(* Représentation des contextes par des fonctions Caml *)

let trou = fun (a : expression) -> a   (* le contexte réduit à [] *)

let app_gauche ectx a2 =               (* le contexte (ectx a2) *)
  fun (a : expression) -> App(ectx a, a2)
let app_droite v1 ectx =               (* le contexte (v1 ectx) *)
  fun (a : expression) -> App(v1, ectx a)
let paire_gauche ectx a2 =             (* le contexte (ectx, a2) *)
  fun (a : expression) -> Paire(ectx a, a2)
let paire_droite v1 ectx =             (* le contexte (v1, ectx) *)
  fun (a : expression) -> Paire(v1, ectx a)
let let_gauche x ectx a2 =             (* le contexte (let x = ectx in a2) *)
  fun (a : expression) -> Let(x, ectx a, a2)
let proj_gauche ectx =                 (* le contexte fst ectx *)
  fun (a : expression) -> Fst(ectx a)
let proj_droite ectx =                 (* le contexte snd ectx *)
  fun (a : expression) -> Snd(ectx a)

(* Décompose une expression en un contexte et une sous-expression à évaluer *)

exception Est_une_valeur

let rec décompose a =
  match a with
  | Var v ->
      assert false (* l'expression doit être close *)
  | Const _ | Op _ | Fun(_, _) ->
      raise Est_une_valeur
  | App (a1, a2) ->
      begin
	try
	  (* Essayons de décomposer a1 sous la forme ectx1[b1]. Si on arrive,
             alors l'expression complète se décompose en (ectx1 a2)[b1]. *)
	  let ectx1, b1 = décompose a1 in
	  app_gauche ectx1 a2, b1
	with Est_une_valeur ->
	  (* Si on échoue, alors a1 est une valeur, donc on peut essayer de
             décomposer a2 sous la forme ectx2[b2]. Si on arrive, alors
	     l'expression complète se décompose en (a1 ectx2)[b2]. *)
	  try
	    let ectx2, b2 = décompose a2 in
	    app_droite a1 ectx2, b2
	  with Est_une_valeur ->
	    (* Si on échoue, alors a1 et a2 sont des valeurs, donc nous ne
	       pouvons pas décomposer plus loin. Nous avons trouvé une
	       application d'une valeur à une valeur; c'est donc ici qu'il
	       faudrait effectuer une réduction. Le contexte d'évaluation
	       approprié est donc le contexte vide. *)
	    trou, a
      end
  | Paire (a1, a2) ->
      begin
	try
	  let ectx1, b1 = décompose a1 in
	  paire_gauche ectx1 a2, b1
	with Est_une_valeur ->
	  let ectx2, b2 = décompose a2 in
	  paire_droite a1 ectx2, b2
	  (* Si la décomposition de a2 échoue, alors a1 et a2 sont des
             valeurs. Nous avons trouvé une paire de deux valeurs;
             l'expression complète est donc elle-même une valeur. C'est
	     pourquoi nous laissons l'exception s'échapper. *)
      end
  | Fst a1 -> (* similaire au cas de l'application *)
      begin
	try
	  let ectx1, b1 = décompose a1 in
	  proj_gauche ectx1, b1
	with Est_une_valeur ->
	  trou, a
      end
  | Snd a1 ->
      begin
	try
	  let ectx1, b1 = décompose a1 in
	  proj_droite ectx1, b1
	with Est_une_valeur ->
	  trou, a
      end
  | Let (x, a1, a2) ->
      begin
	try
	  let ectx1, b1 = décompose a1 in
	  let_gauche x ectx1 a2, b1
	with Est_une_valeur ->
	  trou, a
      end

(* Une étape de réduction en tête du terme *)

exception RuntimeError

let réduit_en_tête = function
  | App (v1, v2) as a ->
      begin
	match v1 with
	| Fun (x, a1) -> (* beta *)
	    subst a1 x v2
	| Op ("+" | "*" | "-" as op) ->
	    begin
	      match op, v2 with
	      |	"+", Paire (Const n1, Const n2) -> (* delta_plus *)
		  Const(n1 + n2)
	      |	"-", Paire (Const n1, Const n2) -> (* delta_moins *)
		  Const(n1 - n2)
	      |	"*", Paire (Const n1, Const n2) -> (* delta_fois *)
		  Const(n1 * n2)
	      |	_ ->
		  raise RuntimeError (* argument incorrect pour un opérateur arithmétique *)
	    end
	| Op "fix" ->
	    begin
	      match v2 with
	      | Fun (f, e) -> (* fix: return e where f has been replaced by the fixpoint itself *)
		  subst e f a
	      | _ ->
		  raise RuntimeError (* argument incorrect pour l'opérateur fix *)
	    end
	| Op "ifzero"->
	    begin
	      match v2 with
	      |	Const 0 ->
		  Fun ("x", Fun ("y", App (Var "x", Const 0))) (* Un codage de "true" à la Church en call-by-value *)
	      |	Const _ ->
		  Fun ("x", Fun ("y", App (Var "y", Const 0))) (* Un codage de "false" à la Church en call-by-value *)
	      |	_ ->
		  raise RuntimeError (* argument incorrect pour l'opérateur ifzero *)
	    end
	| _ ->
	    raise RuntimeError (* argument incorrect pour l'application *)
      end
  | Let (x, v, a) -> (* let *)
      subst a x v
  | Fst v ->
      begin
	match v with
	| Paire(a1, a2) -> a1 (* fst *)
	| _ -> raise RuntimeError (* argument incorrect pour la projection *)
      end
  | Snd v ->
      begin
	match v with
	| Paire(a1, a2) -> a2 (* snd *)
	| _ -> raise RuntimeError (* argument incorrect pour la projection *)
      end
  | _ ->
      assert false (* aucune autre forme d'expression acceptée par cette fonction *)

(* Réduit jusqu'à obtention d'une valeur *)

let rec évalue a =
  match (

    (* Essayons de décomposer a sous la forme ectx[a1]. Cela peut échouer
       si a est une valeur. On mémorise le résultat sous la forme Some(ectx, a1)
       ou bien None, selon le cas. Les constructeurs Some et None font partie du
       type option défini par la librairie standard de Caml. *)

    try
      Some (décompose a)
    with Est_une_valeur ->
      None

  ) with

  (* Ensuite, on décide quoi faire, selon le cas. Si on a trouvé ectx et a1,
     on réduit a1 par une étape de réduction en tête, on remet ectx autour,
     et on continue à évaluer. Noter que la réduction en tête peut soulever
     une exception RuntimeError. Sinon, on a terminé, donc on renvoie la
     valeur a. *)

  | Some (ectx, a1) ->
      évalue (ectx (réduit_en_tête a1))
  | None ->
      a

(* Pour tester *)
let _ = évalue (App(Op "+", Paire(Const 1, Const 2)))
let _ = évalue (Let("x", Op "+", App(Var "x", Paire(Const 1, Const 2))))
let _ = évalue (Paire(App(Op "+", Paire(Const 1, Const 2)),
                     App(Op "+", Paire(Const 3, Const 4))))

let application_multiple fonction arguments =
  List.fold_left (fun fonction argument -> App (fonction, argument)) fonction arguments

let fonction_multiple lieurs corps =
  List.fold_right (fun lieur corps -> Fun (lieur, corps)) lieurs corps

let délai corps =
  Fun ("_", corps)

(* Voici un codage de la fonction [fact], qui utilise les opérateurs primitifs "fix",
   "+", "-", "*" et "ifzero". Comprenez-vous bien le fonctionnement de "fix" et de
   "ifzero"? Quels sont leurs types? À quoi sert la fonction "délai"? Ces questions
   ne sont pas simples; n'hésitez pas à les soulever en cours si besoin... *)

let fact =
  App(
    Op "fix",
    fonction_multiple ["fact"; "n"] (
      application_multiple (Op "ifzero") [
        Var "n";                        (* si n vaut zéro *)
        délai (Const 1);                (* renvoyer 1 *)
        délai (App(Op "*", Paire(       (* sinon renvoyer n * fact(n-1) *)
                 Var "n",
                 App(Var "fact", App(Op "-", Paire (Var "n", Const 1)))
        )))
      ]
    )
  )

let _ = évalue (App(fact, Const 0))     (* 1 *)
let _ = évalue (App(fact, Const 5))     (* 120 *)
let _ = évalue (App(fact, Const(-1)))   (* boucle *)