--- a/doc-src/MacroHints Thu Nov 11 10:00:43 1993 +0100
+++ b/doc-src/MacroHints Thu Nov 11 10:05:17 1993 +0100
@@ -1,143 +1,26 @@
-
Hints
=====
-This is an incomprehensive list of facts about the new version of the syntax
-module (the macro system).
+22-Oct-1993 MMW
+
+Some things notable, but not (yet?) covered by the manual.
-- Syntax of "translations" section is list of <xrule> where: (metachars: [ | ])
-
- <xrule> ::= [(<id>)] <string> [ => | <= | == ] [(<id>)] <string>
-
- One such line specifies a parse rule (=>) or a print rule (<=) or both (==).
- The optional <id> before each <string> specifies the name of the syntactic
- category to be used for parsing the string; the default is logic. Note that
- this has no influence on the applicability of rules.
-
- Example:
-
- translations
- (prop) "x:X" == (prop) "|- x:X"
- "Lam x:A.B" == "Abs(A, %x.B)"
- "Pi x:A.B" => "Prod(A, %x.B)"
-
- All rules of a theory will be shown in their internal (ast * ast) form by
- Syntax.print_trans.
-
-- Caveat: rewrite rules know no "context" nor "semantics", e.g. something
- like "('a, Nil)Cons", "% Nil Cons. Cons(a, Nil)" or "Cons(a, [])" will be
- rewritten by the rules "[x]" <= "Cons(x, [])", "[]" <= "Nil"; (this is a
- general problem with macro systems);
-
-- syn_of: theory -> Syntax.syntax
-
-- Syntax.print_gram shows grammer of syntax
-
-- Syntax.print_trans shows translations of syntax
-
-- Syntax.print_syntax shows grammer and translations of syntax
+- constants of result type prop should always supply concrete syntax;
-- Ast.stat_normalize := true enables output of statistics after normalizing;
-
-- Ast.trace_normalize := true enables verbose output while normalizing and
- statistics;
-
-- eta_contract := false disables eta contraction when printing terms;
-
-- asts: (see also Pure/Syntax/ast.ML *)
-
- (*Asts come in two flavours:
- - proper asts representing terms and types: Variables are treated like
- Constants;
- - patterns used as lhs and rhs in rules: Variables are placeholders for
- proper asts.*)
+- 'Variable --> Constant' possible during rewriting;
- datatype ast =
- Constant of string | (* "not", "_%", "fun" *)
- Variable of string | (* x, ?x, 'a, ?'a *)
- Appl of ast list; (* (f x y z), ("fun" 'a 'b) *)
-
- (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
- there are no empty asts or nullary applications; use mk_appl for convenience*)
-
-- ast output style:
- Constant a -> "a"
- Variable a -> a
- Appl [ast1, ..., astn] -> (ast1 ... astn)
-
-- sext: (see also Pure/Syntax/sextension.ML)
-
- (** datatype sext **)
+- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");
- datatype xrule =
- op |-> of (string * string) * (string * string) |
- op <-| of (string * string) * (string * string) |
- op <-> of (string * string) * (string * string);
-
- datatype sext =
- Sext of {
- mixfix: mixfix list,
- parse_translation: (string * (term list -> term)) list,
- print_translation: (string * (term list -> term)) list} |
- NewSext of {
- mixfix: mixfix list,
- xrules: xrule list,
- parse_ast_translation: (string * (ast list -> ast)) list,
- parse_preproc: (ast -> ast) option,
- parse_postproc: (ast -> ast) option,
- parse_translation: (string * (term list -> term)) list,
- print_translation: (string * (term list -> term)) list,
- print_preproc: (ast -> ast) option,
- print_postproc: (ast -> ast) option,
- print_ast_translation: (string * (ast list -> ast)) list};
-
-- local (thy, ext) order of rules is preserved, global (merge) order is
- unspecified;
-
-- read asts contain a mixture of Constant and Variable atoms (some
- Variables become Const later);
-
-- *.thy-file/ML-section: all declarations will be exported, therefore
- one should use local-in-end constructs where appropriate; especially
- the examples in Logics/Defining could be better behaved;
-
-- [document the asts generated by the standard syntactic categories
- (idt, idts, args, ...)];
+- patterns matching any remaining arguments are not possible (i.e. what would
+ be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros
+ which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't
+ match things like Eps(%x. P, a, b, c);
-- print(_ast)_translation: the constant has to disappear or execption
- Match raised, otherwise the printer will not terminate;
-
-- binders are implemented traditionally, i.e. as parse/print_translations
- (compatibility, alpha, eta, HOL hack easy);
-
-- changes to the term/ast "parsetree" structure: renamed most constants
- (_args, _idts, ...), unified typ applications, _tapp/_tappl, type atoms
- no Const rather than Free;
-
-- misfeature: eta-contraction before rewriting therefore bounded quantifiers,
- Collect etc. may fall back to internal form;
-
-- changes and fixes to printing of types:
-
- "'a => 'b => 'c" now printed as "['a,'b] => 'c";
+- alpha: the precise manner in which bounds are renamed for printing;
- constraints now printed iff not dummyT and show_types enabled, changed
- internal print_translations accordingly; old translations that intruduce
- frees may cause printing of constraints at all occurences;
-
- constraints of bound vars now printed where bound (i.e. "%x::'a. x" rather
- than "%x. x::'a") and put in braces if necessary ("%(x::'a) y::'b. f(x,y)");
+- parsing: applications like f(x)(y)(z) are not parse-ast-translated into
+ (f x y z); this may cause some problems, when the notation "f x y z" for
+ applications will be introduced;
- constraints of bound var printed even if a free var in another scope happens
- to have the same name and type;
-
-- [man: toplevel pretty printers for NJ];
-
-- (syntactic constants "_..." (e.g. "_idts") are reserved, you may use "@..."
- or "*..." instead);
-
-- Printer: clash of fun/type constants with concrete syntax type/fun
- constants causes incorrect printing of of applications;
-