From 56942d07430d4953f50dd59cef0fbf917096e023 Mon Sep 17 00:00:00 2001
From: Christophe Troestler Le module Format des librairies standard de Caml Light et OCaml
propose une méthode d'impression enjolivée. Ce module implémente
@@ -305,7 +310,8 @@
Les boîtes « hov » se subdivisent en deux catégories au comportement
@@ -334,8 +340,8 @@ La différence de comportement entre la boîte « hov » tassante et
la boîte « hov » structurelle (ou « box ») est mise en évidence par la
@@ -519,56 +525,42 @@ Utiliser le module Format
+ Utiliser le module Format
Raffinement sur les boîtes « hov »
-Boîte « hov » tassante et boîte « hov » structurelle
+Boîte « hov » tassante et boîte « hov »
+ structurelle
Boîte « hov » tassante et boîte « hov » structurelle
-Différences entre boîte « hov » tassante et
- boîte « hov » structurelle
+Différences entre boîte « hov » tassante
+ et boîte « hov » structurelle
Un exemple concret
leur application à des arguments.
D'abord, je donne la syntaxe abstraite des lambda-termes : +
D'abord, je donne la syntaxe abstraite des lambda-termes (nous + utilisons le système + interactif pour évaluer ce code) :
--type lambda = - - | Lambda of string * lambda - | Var of string - | Apply of lambda * lambda -;; - ++ type lambda = + | Lambda of string * lambda + | Var of string + | Apply of lambda * lambdaJ'utilise le module format pour imprimer les lambda-termes:
--open Format;; - -let ident = print_string;; -let kwd = print_string;; - -val ident : string -> unit = <fun> -val kwd : string -> unit = <fun> - -let rec print_exp0 = function - - | Var s -> ident s - | lam -> open_hovbox 1; kwd "("; print_lambda lam; kwd ")"; close_box () - -and print_app = function - | e -> open_hovbox 2; print_other_applications e; close_box () - -and print_other_applications f = - match f with - - | Apply (f, arg) -> print_app f; print_space (); print_exp0 arg - | f -> print_exp0 f - -and print_lambda = function - | Lambda (s, lam) -> - open_hovbox 1; - kwd "\\"; ident s; kwd "."; print_space(); print_lambda lam; - close_box() - | e -> print_app e;; - -val print_app : lambda -> unit = <fun> -val print_other_applications : lambda -> unit = <fun> -val print_lambda : lambda -> unit = <fun> - ++ open Format;; + + let ident = print_string + let kwd = print_string;; + + let rec print_exp0 = function + | Var s -> ident s + | lam -> open_hovbox 1; kwd "("; print_lambda lam; kwd ")"; close_box () + and print_app = function + | e -> open_hovbox 2; print_other_applications e; close_box () + and print_other_applications f = + match f with + | Apply (f, arg) -> print_app f; print_space (); print_exp0 arg + | f -> print_exp0 f + and print_lambda = function + | Lambda (s, lam) -> + open_hovbox 1; + kwd "\\"; ident s; kwd "."; print_space(); print_lambda lam; + close_box() + | e -> print_app eEn Caml Light, remplacez la première ligne par : @@ -580,44 +572,6 @@
Un exemple concret
-Utilisation de
- -printf
Cela peut s'écrire de manière équivalente en utilisant -
- -printf
: --open Format;; - -let rec print_exp0 = function - - | Var s -> ident s - | lam -> printf "@[<1>(%a)@]" print_lambda lam - -and print_app = function - - | e -> printf "@[<2>%a@]" print_other_applications e - -and print_other_applications f = - match f with - - | Apply (f, arg) -> printf "%a@ %a" print_app f print_exp0 arg - | f -> print_exp0 f - -and print_lambda = function - - | Lambda (s, lam) -> - printf "@[<1>%a%a%a@ %a@]" kwd "\\" ident s kwd "." print_lambda lam - | e -> print_app e;; - -val print_app : lambda -> unit = <fun> -val print_other_applications : lambda -> unit = <fun> - -val print_lambda : lambda -> unit = <fun> -- - -Impression la plus générale: utilisation de
@@ -638,40 +592,26 @@fprintf
Impression la plus générale: formats d'impression à la
fprintf
. --open Format;; - -let ident ppf s = fprintf ppf "%s" s;; - -let kwd ppf s = fprintf ppf "%s" s;; -val ident : Format.formatter -> string -> unit -val kwd : Format.formatter -> string -> unit - -let rec pr_exp0 ppf = function - | Var s -> fprintf ppf "%a" ident s - | lam -> fprintf ppf "@[<1>(%a)@]" pr_lambda lam - - -and pr_app ppf = function - | e -> fprintf ppf "@[<2>%a@]" pr_other_applications e - -and pr_other_applications ppf f = - - match f with - | Apply (f, arg) -> fprintf ppf "%a@ %a" pr_app f pr_exp0 arg - | f -> pr_exp0 ppf f - - -and pr_lambda ppf = function - | Lambda (s, lam) -> - fprintf ppf "@[<1>%a%a%a@ %a@]" kwd "\\" ident s kwd "." pr_lambda lam - - | e -> pr_app ppf e -;; -val pr_app : Format.formatter -> lambda -> unit -val pr_other_applications : Format.formatter -> lambda -> unit - -val pr_lambda : Format.formatter -> lambda -> unit ++ open Format;; + + let ident ppf s = fprintf ppf "%s" s + let kwd ppf s = fprintf ppf "%s" s;; + + let rec pr_exp0 ppf = function + | Var s -> fprintf ppf "%a" ident s + | lam -> fprintf ppf "@[<1>(%a)@]" pr_lambda lam + and pr_app ppf e = + fprintf ppf "@[<2>%a@]" pr_other_applications e + and pr_other_applications ppf f = + match f with + | Apply (f, arg) -> fprintf ppf "%a@ %a" pr_app f pr_exp0 arg + | f -> pr_exp0 ppf f + and pr_lambda ppf = function + | Lambda (s, lam) -> + fprintf ppf "@[<1>%a%a%a@ %a@]" + kwd "\\" ident s kwd "." pr_lambda lam + | e -> pr_app ppf eArmés de ces fonctions d'impression générales, les procédures @@ -679,11 +619,9 @@
Impression la plus générale: facilement par application partielle:. -
-let print_lambda = pr_lambda std_formatter;; -let eprint_lambda = pr_lambda err_formatter;; -val print_lambda : lambda -> unit -val eprint_lambda : lambda -> unit ++ let print_lambda = pr_lambda std_formatter + let eprint_lambda = pr_lambda err_formatterdiff --git a/src/html/tutorials/format.html b/src/html/tutorials/format.html index 0c2cba4fc..8a5d2d31a 100644 --- a/src/html/tutorials/format.html +++ b/src/html/tutorials/format.html @@ -6,6 +6,12 @@Using the Format module + ++ Table of contents + ++Using the Format module
The
Format
module of Caml Light and OCaml's @@ -290,7 +296,8 @@Indentation of new lines
Refinement on “hov” boxes
-Packing and structural “hov” boxes
+Packing and structural + “hov” boxes
The “hov” box type is refined into two categories.
@@ -312,8 +319,8 @@Packing and structural “hov” boxes
-Differences between a packing and a structural - “hov” box
+Differences between a packing + and a structural “hov” box
The difference between a packing and a structural “hov” box is shown by a routine that closes boxes and @@ -472,7 +479,7 @@
A concrete example
Let me give a full example: the shortest non trivial example - you could imagine, that is the $\lambda-$calculus :) + you could imagine, that is the λ-calculus :)
Thus the problem is to pretty-print the values of a concrete @@ -480,56 +487,42 @@
A concrete example
functions and their applications to arguments. -First, I give the abstract syntax of lambda-terms: +
First, I give the abstract syntax of lambda-terms (we + illustrate is in the + interactive system):
--type lambda = - - | Lambda of string * lambda - | Var of string - | Apply of lambda * lambda -;; - ++ type lambda = + | Lambda of string * lambda + | Var of string + | Apply of lambda * lambdaI use the format library to print the lambda-terms:
--open Format;; - -let ident = print_string;; -let kwd = print_string;; - -val ident : string -> unit = <fun> -val kwd : string -> unit = <fun> - -let rec print_exp0 = function - - | Var s -> ident s - | lam -> open_hovbox 1; kwd "("; print_lambda lam; kwd ")"; close_box () - -and print_app = function - | e -> open_hovbox 2; print_other_applications e; close_box () - -and print_other_applications f = - match f with - - | Apply (f, arg) -> print_app f; print_space (); print_exp0 arg - | f -> print_exp0 f - -and print_lambda = function - | Lambda (s, lam) -> - open_hovbox 1; - kwd "\\"; ident s; kwd "."; print_space(); print_lambda lam; - close_box() - | e -> print_app e;; - -val print_app : lambda -> unit = <fun> -val print_other_applications : lambda -> unit = <fun> -val print_lambda : lambda -> unit = <fun> - ++ open Format;; + + let ident = print_string + let kwd = print_string;; + + let rec print_exp0 = function + | Var s -> ident s + | lam -> open_hovbox 1; kwd "("; print_lambda lam; kwd ")"; close_box () + and print_app = function + | e -> open_hovbox 2; print_other_applications e; close_box () + and print_other_applications f = + match f with + | Apply (f, arg) -> print_app f; print_space (); print_exp0 arg + | f -> print_exp0 f + and print_lambda = function + | Lambda (s, lam) -> + open_hovbox 1; + kwd "\\"; ident s; kwd "."; print_space(); print_lambda lam; + close_box() + | e -> print_app eIn Caml Light, replace the first line by: @@ -541,43 +534,6 @@
A concrete example
-Using
- -printf
This can be equivalently written using
- -printf
: --open Format;; - -let rec print_exp0 = function - - | Var s -> ident s - | lam -> printf "@[<1>(%a)@]" print_lambda lam - -and print_app = function - - | e -> printf "@[<2>%a@]" print_other_applications e - -and print_other_applications f = - match f with - - | Apply (f, arg) -> printf "%a@ %a" print_app f print_exp0 arg - | f -> print_exp0 f - -and print_lambda = function - - | Lambda (s, lam) -> - printf "@[<1>%a%a%a@ %a@]" kwd "\\" ident s kwd "." print_lambda lam - | e -> print_app e;; - -val print_app : lambda -> unit = <fun> -val print_other_applications : lambda -> unit = <fun> - -val print_lambda : lambda -> unit = <fun> -- - -Most general pretty-printing: using
@@ -602,42 +558,26 @@fprintf
routines can be written as follows: -
-open Format;; - - -let ident ppf s = fprintf ppf "%s" s;; -let kwd ppf s = fprintf ppf "%s" s;; -val ident : Format.formatter -> string -> unit - -val kwd : Format.formatter -> string -> unit - -let rec pr_exp0 ppf = function - - | Var s -> fprintf ppf "%a" ident s - | lam -> fprintf ppf "@[<1>(%a)@]" pr_lambda lam - -and pr_app ppf = function - - | e -> fprintf ppf "@[<2>%a@]" pr_other_applications e - -and pr_other_applications ppf f = - match f with - - | Apply (f, arg) -> fprintf ppf "%a@ %a" pr_app f pr_exp0 arg - | f -> pr_exp0 ppf f - -and pr_lambda ppf = function - - | Lambda (s, lam) -> - fprintf ppf "@[<1>%a%a%a@ %a@]" kwd "\\" ident s kwd "." pr_lambda lam - | e -> pr_app ppf e -;; - -val pr_app : Format.formatter -> lambda -> unit -val pr_other_applications : Format.formatter -> lambda -> unit -val pr_lambda : Format.formatter -> lambda -> unit - ++ open Format;; + + let ident ppf s = fprintf ppf "%s" s + let kwd ppf s = fprintf ppf "%s" s;; + + let rec pr_exp0 ppf = function + | Var s -> fprintf ppf "%a" ident s + | lam -> fprintf ppf "@[<1>(%a)@]" pr_lambda lam + and pr_app ppf e = + fprintf ppf "@[<2>%a@]" pr_other_applications e + and pr_other_applications ppf f = + match f with + | Apply (f, arg) -> fprintf ppf "%a@ %a" pr_app f pr_exp0 arg + | f -> pr_exp0 ppf f + and pr_lambda ppf = function + | Lambda (s, lam) -> + fprintf ppf "@[<1>%a%a%a@ %a@]" + kwd "\\" ident s kwd "." pr_lambda lam + | e -> pr_app ppf e@@ -646,11 +586,9 @@
stderr
is just a matter of partial application: --let print_lambda = pr_lambda std_formatter;; -let eprint_lambda = pr_lambda err_formatter;; -val print_lambda : lambda -> unit -val eprint_lambda : lambda -> unit ++ let print_lambda = pr_lambda std_formatter + let eprint_lambda = pr_lambda err_formatter