Precisions about quotations
 Daniel de Rauglaudre
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  19951120 (08:34) 
From:  Daniel de Rauglaudre <ddr@p...> 
Subject:  Precisions about quotations 
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 CamlLight, 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 (CamlSpecialLight) 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;;