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;