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;