(* Exercices de programmation du chapitre 5 *)

(* La syntaxe abstraite des expressions mini-ML avec adresses mémoire *)

type adresse = int

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
  | Adr of adresse

(* 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)
  | Adr l -> a

(* 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
  | Adr l -> true

(* Représentation des états mémoire *)
(* Un état mémoire est une fonction des adresses dans les valeurs,
   ainsi que la prochaine adresse libre *)

type état_mémoire = { libre: adresse; contenu: (adresse -> expression) }

exception Mauvaise_adresse of int

let mémoire_vide =
  { libre = 0; contenu = (fun l -> raise(Mauvaise_adresse l)) }

let lire s l =
  s.contenu l
let écrire s l v =
  { libre = s.libre;
    contenu = (fun l' -> if l = l' then v else s.contenu l') }
let allouer s v =
  let l = s.libre in
  (l, { libre = l + 1;
        contenu = (fun l' -> if l = l' then v else s.contenu l') })

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

exception Réduction_en_tête_impossible

let réduction_tête a s =
  match a with
    App(Fun(x, a1), a2) when est_une_valeur a2 -> (* beta_fun *)
      (subst a1 x a2, s)
  | Let(x, a1, a2) when est_une_valeur a1 -> (* beta_let *)
      (subst a2 x a1, s)
  | App(Op "+", Paire(Const n1, Const n2)) -> (* delta_plus *)
      (Const(n1 + n2), s)
  | App(Op "-", Paire(Const n1, Const n2)) -> (* delta_moins *)
      (Const(n1 - n2), s)
  | App(Op "*", Paire(Const n1, Const n2)) -> (* delta_fois *)
      (Const(n1 * n2), s)
  | App(Op "fst", Paire(a1, a2))
    when est_une_valeur a1 && est_une_valeur a2 -> (* delta_fst *)
      (a1, s)
  | App(Op "snd", Paire(a1, a2))
    when est_une_valeur a1 && est_une_valeur a2 -> (* delta_snd *)
      (a2, s)
  | App(Op "fix", Fun(x, a2)) ->        (* delta_fix *)
      (subst a2 x a, s)
  | App(Op "ref", a) when est_une_valeur a -> (* delta_ref *)
      let (l, s') = allouer s a in (Adr l, s')
  | App(Op "!", Adr l) ->
      (lire s l, s)
  | App(Op ":=", Paire(Adr l, a)) when est_une_valeur a ->
      (Const 0, écrire s l a)
  | _ ->
      raise Réduction_en_tête_impossible

(* Représentation des contextes par des fonctions Caml -- comme au chap. 2 *)

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 *)
(* -- comme au chapitre 2 *)

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(_, _) | Adr _ ->
      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 "ref", a1) when est_une_valeur a1 ->
      (trou, a)
  | App(Op "!", Adr l) ->
      (trou, a)
  | App(Op ":=", Paire(Adr l, a1)) when est_une_valeur a1 ->
      (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 /s -> a'/s' et renvoie Some(a', s')
   ou bien renvoie None si a est en forme normale *)

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

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

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

(* Pour tester *)
forme_normale (App(Op "+", Paire(Const 1, Const 2))) mémoire_vide;;
forme_normale (Let("x", Op "+", App(Var "x", Paire(Const 1, Const 2)))) mémoire_vide;;
forme_normale (Paire(App(Op "+", Paire(Const 1, Const 2)),
                     App(Op "+", Paire(Const 3, Const 4))))
              mémoire_vide;;
forme_normale (Let("r", App(Op "ref", Const 1),
               Let("n", App(Op ":=",
                            Paire(Var "r",
                                  App(Op "+",
                                      Paire(App(Op "!", Var "r"),
                                            Const 1)))),
               App(Op "!", Var "r"))))
               mémoire_vide;;