doc-src/MacroHints

-
 
 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: [ | ])
+- constants of result type prop should always supply concrete syntax;
 
-    <xrule> ::= [(<id>)] <string> [ => | <= | == ] [(<id>)] <string>
+- 'Variable --> Constant' possible during rewriting;
 
-  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.
+- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");
 
-  Example:
+- 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);
 
-    translations
-      (prop) "x:X"  == (prop) "|- x:X"
-      "Lam x:A.B"   == "Abs(A, %x.B)"
-      "Pi x:A.B"    => "Prod(A, %x.B)"
+- alpha: the precise manner in which bounds are renamed for printing;
 
-  All rules of a theory will be shown in their internal (ast * ast) form by
-  Syntax.print_trans.
+- 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;
 
-- 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;
-