diff -r 7a5d207e6151 -r b4a8dabc7313 doc-src/MacroHints --- a/doc-src/MacroHints Thu Nov 11 10:00:43 1993 +0100 +++ b/doc-src/MacroHints Thu Nov 11 10:05:17 1993 +0100 @@ -1,143 +1,26 @@ - Hints ===== -This is an incomprehensive list of facts about the new version of the syntax -module (the macro system). +22-Oct-1993 MMW + +Some things notable, but not (yet?) covered by the manual. -- Syntax of "translations" section is list of where: (metachars: [ | ]) - - ::= [()] [ => | <= | == ] [()] - - One such line specifies a parse rule (=>) or a print rule (<=) or both (==). - The optional before each 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 +- constants of result type prop should always supply concrete 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.*) +- 'Variable --> Constant' possible during rewriting; - 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 **) +- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)"); - 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, ...)]; +- patterns matching any remaining arguments are not possible (i.e. what would + be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros + which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't + match things like Eps(%x. P, a, b, c); -- 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"; +- alpha: the precise manner in which bounds are renamed for printing; - 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)"); +- parsing: applications like f(x)(y)(z) are not parse-ast-translated into + (f x y z); this may cause some problems, when the notation "f x y z" for + applications will be introduced; - 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; -