doc-src/MacroHints

Initial revision

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;