From: Daniel de Rauglaudre <ddr@peray.inria.fr>
Message-Id: <199511181613.AA04092@peray.inria.fr>
Subject: Precisions about quotations
To: caml-list@pauillac.inria.fr, coq@pauillac.inria.fr
Date: Sat, 18 Nov 1995 17:13:26 +0100 (MET)
I was told that my message about quotations was not clear about some
points. First I am sorry to have called them "macros": people told me
that "macro" is not the correct term... Ok, don't let us call them
"macros", they are not "macros", they are "quotations", :-)
Second, my example seemed to show that quotations could just made
"constants" in the langage. This is false: you can generate any piece
of code, not only constants or variable names: you can make functions,
"if then else" constructions, 50 lines of complicated code, etc.
What cpp does, quotations can do it, but quotations can hold any
string and expanders can make any manipulations of this string.
So, let's go to another example, folks.
This example is borrowed from Gerard Huet: manipulations of lambda
terms. The code for the expander is given at the end of this
message. It was just a test for quotations, this code is not the
cleanest of the world, but it works (this code was not written by
Gerard, but by myself: the "borrow" comes from an equivalent program
written by him in Classical CAML, the one before Caml-Light, where
quotations existed already, in another more complicated form).
First we define the type "term" as:
type term = Ref of int | Abs of term | App of term * term;;
Examples of values of type "term":
Abs (Ref 0)
Abs (Abs (Ref 1))
Abs (Abs (Abs (App (App (Ref 2, Ref 0), App (Ref 1, Ref 0)))))
But this representation is not easy to read (I mean for people using
lambda terms). The quotation system allows to make a syntax for such
terms. Thanks to the expander, the 3 above examples can be written:
<< [x]x >>
<< [x,y]x >>
<< [x,y,z](x z (y z)) >>
which are more readable.
Moreover this expander provides an "antiquotation" system to insert
CSL (Caml-Special-Light) variables (or any expression) in the syntax
of terms. For example, after having defined the term "delta" like this:
#let delta = << [x](x x) >>;;
val delta : lambda = Abs (App (Ref 0, Ref 0))
the lambda calculator wants to define "omega" as the application of
"delta" to itself. This can be written using "^":
#let omega = << (^delta ^delta) >>;;
val omega : lambda = App (Abs (App (Ref 0, Ref 0)), Abs (App (Ref 0, Ref 0)))
Another example of antiquotation:
#let abstract t = << [x]^t >>;;
val abstract : term -> term = <fun>
#abstract delta;;
- : term = Abs (Abs (App (Ref 0, Ref 0)))
Note that this syntax with "^" for antiquotations is a decision of the
expander, not a quotation feature.
Finally, the important things to notice are:
* Quotations may hold any syntax, i.e. any string your expander can
parse: it is independant from the syntax of CSL. Only the expander
is responsible for the input syntax. The example of my first message
showed identifiers "MAX", "MIN". This example shows more complicated
syntax: "[x]x", "[x,y,z]^foo", etc. There is no limitation: you can
have your own comments, you own antiquotation system if you need
one, the parenthesis need not balance if you don't want, you can use
CSL keywords as variable identifiers, etc. This is a world diffent
from CSL's.
* The result of an expander can be any piece of CSL code. The first
example was just constants "350", "8". Here they are
values of type "term": "Abs (Ref 0)", "Abs (Abs (Ref 1))", etc. Note
that, in this expander, these strings are builded by concatenations
of strings, resulting from calculus of what "lambda calculators"
call "de_bruijn indices", etc. But you can generate complicated
constructions, like "if ... then ... else" or "match ...", anything,
provided that it is correct CSL syntax. The CSL parser and type
checker are applied afterward. For example:
#let delta = 32;;
val delta : int = 32
#let omega = << (^delta ^delta) >>;;
This expression has type int but is here used with type term
You can perfect and debug your expander by applying it to string
examples. Load and open it (or use the toplevel directive "#use").
Then, test:
#f " (^delta ^delta) ";;
- : string = "App (delta, delta)"
#f "[x,y]x";;
- : string = "Abs (Abs (Ref 1))"
If your expander raises an exception, it is printed and the CSL
parsing stops:
#<<[x]y>>;;
Uncaught exception: Parse_error("y is unbound in lambda term")
Raised while expanding quotation
I would like to precise that a quotation is just a syntactic feature:
it does not slow the execution of your program. If you write:
let abstract t = << [x]^t >>;;
it is exactly as if you wrote:
let abstract t = Abs (t);;
I mean that the string " [x]^t " is *not* evaluated each time the
function "abstract" is applied at run time. It disappears at
compilation time. In others words, the expander is *not* required to
run your program.
I hope that this message made this system of quotations more
understandable. Thank you for having read it.
--------------------------------------------------------------------------
Daniel de RAUGLAUDRE
Projet Cristal - INRIA Rocquencourt
Tel: +33 (1) 39 63 53 51
Email: daniel.de_rauglaudre@inria.fr
Web: http://pauillac.inria.fr:80/~ddr/
--------------------------------------------------------------------------
This is the expander for this example, using parsers (from the version
1.11 of CSL, see the reference manual).
let rec ident str =
parser
[: ''a'..'z'|'A'..'Z' as c; r = ident (str ^ String.make 1 c) :] -> r
| [: :] -> str
;;
let rec lex =
parser
[: ''[' :] -> "["
| [: '']' :] -> "]"
| [: ''(' :] -> "("
| [: '')' :] -> ")"
| [: '',' :] -> ","
| [: ''^' :] -> "^"
| [: ''a'..'z'|'A'..'Z' as c; r = ident (String.make 1 c) :] -> r
| [: ''_' :] -> "_"
| [: '' '; s :] -> lex s
;;
let rec indice x =
function
[] -> raise (Stream.Parse_error (x ^ " is unbound in lambda term"))
| y::l -> if x = y then 0 else (succ (indice x l))
;;
let e_id = "identifier expected";;
let e_rp = "right parenthesis \")\" expected";;
let e_rb = "right bracket \"]\" expected";;
let e_tr = "term expected";;
let e_an = "antiquotation expected";;
let e_es = "end of string expected";;
let rec term env =
parser
[: '"["; 'x?e_id; l = id_list [x]; '"]"?e_rb; e = term (l @ env)?e_tr :] ->
List.fold_right (fun _ e -> "Abs (" ^ e ^ ")") l e
| [: '"("; x = term env?e_tr; a = apply env x?e_rp :] -> a
| [: '"^"; v = antiquot?e_an :] -> v
| [: 'x :] -> "Ref " ^ string_of_int (indice x env)
and id_list l =
parser
[: '","; 'x?e_id; l = id_list (x::l) :] -> l
| [: :] -> l
and apply env x =
parser
[: '")" :] -> x
| [: y = term env; a = apply env ("App (" ^ x ^ ", " ^ y ^ ")")?e_rp :] -> a
and antiquot =
parser
[: '"("; s = antiquot_end :] -> "(" ^ s
| [: 'x :] -> x
and antiquot_end =
parser
[: '")" :] -> ")"
| [: '"("; s1 = antiquot_end; s2 = antiquot_end :] -> "(" ^ s1 ^ s2
| [: 'x; s = antiquot_end :] -> x ^ " " ^ s
;;
let f str =
let cs = Stream.of_string str in
let ts =
Stream.from (fun _ -> try Some (lex cs) with Stream.Parse_failure -> None)
in
match ts with parser [: r = term []; _ = Stream.empty?e_es :] -> r
;;
Quotation.add_expander "term" f;;