5 This is an incomprehensive list of facts about the new version of the syntax
6 module (the macro system).
9 - Syntax of "translations" section is list of <xrule> where: (metachars: [ | ])
11 <xrule> ::= [(<id>)] <string> [ => | <= | == ] [(<id>)] <string>
13 One such line specifies a parse rule (=>) or a print rule (<=) or both (==).
14 The optional <id> before each <string> specifies the name of the syntactic
15 category to be used for parsing the string; the default is logic. Note that
16 this has no influence on the applicability of rules.
21 (prop) "x:X" == (prop) "|- x:X"
22 "Lam x:A.B" == "Abs(A, %x.B)"
23 "Pi x:A.B" => "Prod(A, %x.B)"
25 All rules of a theory will be shown in their internal (ast * ast) form by
28 - Caveat: rewrite rules know no "context" nor "semantics", e.g. something
29 like "('a, Nil)Cons", "% Nil Cons. Cons(a, Nil)" or "Cons(a, [])" will be
30 rewritten by the rules "[x]" <= "Cons(x, [])", "[]" <= "Nil"; (this is a
31 general problem with macro systems);
33 - syn_of: theory -> Syntax.syntax
35 - Syntax.print_gram shows grammer of syntax
37 - Syntax.print_trans shows translations of syntax
39 - Syntax.print_syntax shows grammer and translations of syntax
41 - Ast.stat_normalize := true enables output of statistics after normalizing;
43 - Ast.trace_normalize := true enables verbose output while normalizing and
46 - eta_contract := false disables eta contraction when printing terms;
48 - asts: (see also Pure/Syntax/ast.ML *)
50 (*Asts come in two flavours:
51 - proper asts representing terms and types: Variables are treated like
53 - patterns used as lhs and rhs in rules: Variables are placeholders for
57 Constant of string | (* "not", "_%", "fun" *)
58 Variable of string | (* x, ?x, 'a, ?'a *)
59 Appl of ast list; (* (f x y z), ("fun" 'a 'b) *)
61 (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
62 there are no empty asts or nullary applications; use mk_appl for convenience*)
67 Appl [ast1, ..., astn] -> (ast1 ... astn)
69 - sext: (see also Pure/Syntax/sextension.ML)
74 op |-> of (string * string) * (string * string) |
75 op <-| of (string * string) * (string * string) |
76 op <-> of (string * string) * (string * string);
81 parse_translation: (string * (term list -> term)) list,
82 print_translation: (string * (term list -> term)) list} |
86 parse_ast_translation: (string * (ast list -> ast)) list,
87 parse_preproc: (ast -> ast) option,
88 parse_postproc: (ast -> ast) option,
89 parse_translation: (string * (term list -> term)) list,
90 print_translation: (string * (term list -> term)) list,
91 print_preproc: (ast -> ast) option,
92 print_postproc: (ast -> ast) option,
93 print_ast_translation: (string * (ast list -> ast)) list};
95 - local (thy, ext) order of rules is preserved, global (merge) order is
98 - read asts contain a mixture of Constant and Variable atoms (some
99 Variables become Const later);
101 - *.thy-file/ML-section: all declarations will be exported, therefore
102 one should use local-in-end constructs where appropriate; especially
103 the examples in Logics/Defining could be better behaved;
105 - [document the asts generated by the standard syntactic categories
106 (idt, idts, args, ...)];
108 - print(_ast)_translation: the constant has to disappear or execption
109 Match raised, otherwise the printer will not terminate;
111 - binders are implemented traditionally, i.e. as parse/print_translations
112 (compatibility, alpha, eta, HOL hack easy);
114 - changes to the term/ast "parsetree" structure: renamed most constants
115 (_args, _idts, ...), unified typ applications, _tapp/_tappl, type atoms
116 no Const rather than Free;
118 - misfeature: eta-contraction before rewriting therefore bounded quantifiers,
119 Collect etc. may fall back to internal form;
121 - changes and fixes to printing of types:
123 "'a => 'b => 'c" now printed as "['a,'b] => 'c";
125 constraints now printed iff not dummyT and show_types enabled, changed
126 internal print_translations accordingly; old translations that intruduce
127 frees may cause printing of constraints at all occurences;
129 constraints of bound vars now printed where bound (i.e. "%x::'a. x" rather
130 than "%x. x::'a") and put in braces if necessary ("%(x::'a) y::'b. f(x,y)");
132 constraints of bound var printed even if a free var in another scope happens
133 to have the same name and type;
135 - [man: toplevel pretty printers for NJ];
137 - (syntactic constants "_..." (e.g. "_idts") are reserved, you may use "@..."
140 - Printer: clash of fun/type constants with concrete syntax type/fun
141 constants causes incorrect printing of of applications;