(* 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
  | 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)
  | Let(v, a1, a2) -> Let(v, subst a1 x b, if v = x then a2 else subst a2 x b)

(* Teste si une expression est une valeur *)

let rec est_une_valeur a =
  match a with
    Var v -> false
  | Const n -> true
  | Op o -> true
  | Fun(x, a1) -> true
  | App(a1, a2) -> false
  | Paire(a1, a2) -> est_une_valeur a1 && est_une_valeur a2
  | Let(v, a1, a2) -> false

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

exception Réduction_en_tête_impossible

let réduction_tête a =
  match a with
    App(Fun(x, a1), a2) when est_une_valeur a2 -> (* beta_fun *)
      subst a1 x a2
  | Let(x, a1, a2) when est_une_valeur a1 -> (* beta_let *)
      subst a2 x a1
  | App(Op "+", Paire(Const n1, Const n2)) -> (* delta_plus *)
      Const(n1 + n2)
  | App(Op "-", Paire(Const n1, Const n2)) -> (* delta_moins *)
      Const(n1 - n2)
  | App(Op "*", Paire(Const n1, Const n2)) -> (* delta_fois *)
      Const(n1 * n2)
  | App(Op "fst", Paire(a1, a2))
    when est_une_valeur a1 && est_une_valeur a2 -> (* delta_fst *)
      a1
  | App(Op "snd", Paire(a1, a2))
    when est_une_valeur a1 && est_une_valeur a2 -> (* delta_snd *)
      a2
  | App(Op "fix", Fun(x, a2)) ->        (* delta_fix *)
      subst a2 x a
  | App(Op "ifzero", Paire(Const 0, Paire(a1, a2))) -> (* delta_if *)
      a1
  | App(Op "ifzero", Paire(Const n, Paire(a1, a2))) -> (* delta_if' *)
      a2
  | _ ->
      raise Réduction_en_tête_impossible

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

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

let app_gauche gamma a2 =               (* le contexte (gamma a2) *)
  fun (a : expression) -> App(gamma a, a2)
let app_droite v1 gamma =               (* le contexte (v1 gamma) *)
  fun (a : expression) -> App(v1, gamma a)
let paire_gauche gamma a2 =             (* le contexte (gamma, a2) *)
  fun (a : expression) -> Paire(gamma a, a2)
let paire_droite v1 gamma =             (* le contexte (v1, gamma) *)
  fun (a : expression) -> Paire(v1, gamma a)
let let_gauche x gamma a2 =             (* le contexte (let x = gamma in a2) *)
  fun (a : expression) -> Let(x, gamma a, a2)

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

exception Expression_non_close of string
exception Forme_normale

let rec décompose a =
  match a with
    Var v ->
      raise (Expression_non_close v)
  | Const _ | Op _ | Fun(_, _) ->
      raise Forme_normale
  (* Ici on reconnaît les cas où l'on peut réduire en tête.
     On renvoie alors le contexte trivial [] et l'expression a elle-même. *)
  | App(Fun(x, a1), a2) when est_une_valeur a2 ->
      (trou, a)
  | Let(x, a1, a2) when est_une_valeur a1 ->
      (trou, a)
  | App(Op("+" | "-" | "*"), Paire(Const n1, Const n2)) ->
      (trou, a)
  | App(Op("fst" | "snd"), Paire(a1, a2))
    when est_une_valeur a1 && est_une_valeur a2 ->
      (trou, a)
  | App(Op "fix", Fun(x, a2)) ->
      (trou, a)
  | App(Op "ifzero", Paire(Const n, Paire(a1, a2))) ->
      (trou, a)
  (* Maintenant, on voit si l'on peut réduire dans les sous-expressions *)
  | App(a1, a2) ->
      if est_une_valeur a1 then begin
        (* a1 est déjà évaluée, il faut creuser dans a2 *)
        let (gamma, rd) = décompose a2 in
        (app_droite a1 gamma, rd)
      end else begin
        (* a1 n'est pas encore évalué, c'est là qu'il faut creuser *)
        let (gamma, rd) = décompose a1 in
        (app_gauche gamma a2, rd)
      end
  | Paire(a1, a2) ->
      if est_une_valeur a1 then
        if est_une_valeur a2 then
          raise Forme_normale
        else begin
          (* a1 est déjà évaluée, il faut creuser dans a2 *)
          let (gamma, rd) = décompose a2 in
          (paire_droite a1 gamma, rd)
        end
      else begin
        (* a1 n'est pas encore évalué, c'est là qu'il faut creuser *)
        let (gamma, rd) = décompose a1 in
        (paire_gauche gamma a2, rd)
      end
  | Let(x, a1, a2) ->
      (* On sait que a1 n'est pas une valeur, sinon le cas beta-let ci-dessus
         s'appliquerait.  On va donc creuser dans a1. *)
      let (gamma, rd) = décompose a1 in
      (let_gauche x gamma a2, rd)

(* Effectue une étape de réduction a -> a' et renvoie Some(a')
   ou bien renvoie None si a est en forme normale *)

let réduction a =
  try
    let (gamma, rd) = décompose a in Some(gamma(réduction_tête rd))
  with Forme_normale ->
    None

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

let rec forme_normale a =
  match réduction a with None -> a | Some a' -> forme_normale a';;

(* Pour tester *)
forme_normale (App(Op "+", Paire(Const 1, Const 2)));;
forme_normale (Let("x", Op "+", App(Var "x", Paire(Const 1, Const 2))));;
forme_normale (Paire(App(Op "+", Paire(Const 1, Const 2)),
                     App(Op "+", Paire(Const 3, Const 4))));;
let fact =
  App(Op "fix",
      Fun("fact", Fun("n",
        App(Op "ifzero",
          Paire(Var "n",
                Paire(Const 1,
                      App(Op "*",
                          Paire(Var "n",
                                App(Var "fact",
                                    App(Op "-", Paire(Var "n", Const 1)))))))))));;
forme_normale (App(fact, Const 0));;
forme_normale (App(fact, Const 5));;
forme_normale (App(fact, Const(-1)));;