--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/MacroHints Tue Nov 09 16:47:38 1993 +0100
@@ -0,0 +1,142 @@
+
+Hints
+=====
+
+This is an incomprehensive list of facts about the new version of the syntax
+module (the macro system).
+
+
+- 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
+
+- 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.*)
+
+ 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 **)
+
+ 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, ...)];
+
+- 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";
+
+ 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)");
+
+ 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;
+