From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id JAA06608 for caml-redistribution; Mon, 20 Nov 1995 09:34:08 +0100
Received: from peray.inria.fr (peray.inria.fr [128.93.8.98]) by pauillac.inria.fr (8.6.10/8.6.6) with SMTP id RAA00852; Sat, 18 Nov 1995 17:11:49 +0100
Received: by peray.inria.fr; Sat, 18 Nov 1995 17:13:27 +0100
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)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: weis


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