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;