Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 04:09:48 -0700 (Fri, 04 Jul 2003)
Revision: 4698
Log message:
Implemented the <:con< ... >> quotation that is similar to << ... >>, but allows
anti-quotations, which makes it a very espressive mechanism for term construction.
Currently supported syntax:
Terms:
- $e$ where e is an ML expression of type term
- !t! where t is a traditional term "constant" (allows using input shortcuts)
- '$e$ where e is an ML expression of type string (e.g. creates a variable expr).
- opname[params]{bterm; bterm; ... } - standard format (params and/or bterms can be omited)
Params:
- "str" - string constant
- id[:kind] - (kind is one of s,t,n,l) - meta-variable (kind is "s" by default)
- [0-9]+ - numeric constant
- $e:kind - where e is an ML expression of appropriate type
(string for s,t; Mp_num.num for n, level_exp for l)
Bterm:
- t
- bvar, bvar, ..., bvar. term
Bvar:
- id - constant bvar
- $e$ - where e is an ML expression of type string