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)) ;;