<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
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
;;
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)
;;
let rec valeur a =
  match a with
  | Const c ->                (* règle 1 *)
      Const c
  | Op o ->                   (* règle 2 *)
      Op o
  | Fun(x, a) ->              (* règle 3 *)
      Fun(x, a)
  | App(a1, a2) ->            (* règles 4, 7, 8, 9 ou 10 *)
      begin match valeur a1 with
      | Fun(x, a) ->          (* règle 4 *)
          valeur (subst a x (valeur a2))
      | Op "+" ->             (* règle 7 *)
          let (Paire(Const n1, Const n2)) = valeur a2 in Const(n1 + n2)
      | Op "fst" ->           (* règle 8 *)
          let (Paire(v1, v2)) = valeur a2 in v1
      | Op "snd" ->           (* règle 9 *)
          let (Paire(v1, v2)) = valeur a2 in v2
      end
  | Paire(a1, a2) ->          (* règle 5 *)
      Paire(valeur a1, valeur a2)
  | Let(x, a1, a2) ->         (* règle 6 *)
      valeur (subst a2 x (valeur a1))
;;
valeur (App(Op "+", Paire(Const 1, Const 2)))
;;
valeur (Paire(App(Op "+", Paire(Const 1, Const 2)),
                App(Op "+", Paire(Const 3, Const 4))))
;;
valeur (App (Fun ("x", App(Op "+", Paire(Var "x", Const 1))), Const 2))
;;
valeur (App (Const 1, Const 2))
;;
let b = Fun("x", App(Var "x", Var "x")) in valeur (App(b, b))
;;
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
;;
exception Forme_normale
;;
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 Forme_normale
;;
type contexte = expression -> expression
;;
let trou = fun (a : expression) -> a    (* le contexte réduit à [] *)
;;
let app_gauche gamma a2 =               (* le contexte (gamma a2) *)
  function (a : expression) -> App(gamma a, a2)
let app_droite v1 gamma =               (* le contexte (v1 gamma) *)
  function (a : expression) -> App(v1, gamma a)
let paire_gauche gamma a2 =             (* le contexte (gamma, a2) *)
  function (a : expression) -> Paire(gamma a, a2)
let paire_droite v1 gamma =             (* le contexte (v1, gamma) *)
  function (a : expression) -> Paire(v1, gamma a)
let let_gauche x gamma a2 =             (* le contexte (let x = gamma in a2) *)
  function (a : expression) -> Let(x, gamma a, a2)
;;
let rec décompose a =
  match a with
  (* Déjà en forme normale *)
  | Var _ | 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
        (* a1 est déjà évaluée, il faut creuser dans a2 *)
        let (gamma, rd) = décompose a2 in
        (paire_droite a1 gamma, rd)
      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)
;;
let réduction a =
  try
    let (gamma, rd) = décompose a in Some(gamma(réduction_tête rd))
  with Forme_normale ->
    None
;;
let rec forme_normale a =
  match réduction a with None -> a | Some a' -> forme_normale a'
;;
forme_normale (App(Op "+", Paire(Const 1, Const 2)))
;;
forme_normale (Paire(App(Op "+", Paire(Const 1, Const 2)),
                     App(Op "+", Paire(Const 3, Const 4))))
;;
forme_normale (App (Fun ("x", App(Op "+", Paire(Var "x", Const 1))), Const 2))
;;
forme_normale (App (Const 1, Const 2))
;;
let b = Fun("x", App(Var "x", Var "x")) in forme_normale (App(b, b))
;;