1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/MacroHints Tue Nov 09 16:47:38 1993 +0100
1.3 @@ -0,0 +1,142 @@
1.4 +
1.5 +Hints
1.6 +=====
1.7 +
1.8 +This is an incomprehensive list of facts about the new version of the syntax
1.9 +module (the macro system).
1.10 +
1.11 +
1.12 +- Syntax of "translations" section is list of <xrule> where: (metachars: [ | ])
1.13 +
1.14 + <xrule> ::= [(<id>)] <string> [ => | <= | == ] [(<id>)] <string>
1.15 +
1.16 + One such line specifies a parse rule (=>) or a print rule (<=) or both (==).
1.17 + The optional <id> before each <string> specifies the name of the syntactic
1.18 + category to be used for parsing the string; the default is logic. Note that
1.19 + this has no influence on the applicability of rules.
1.20 +
1.21 + Example:
1.22 +
1.23 + translations
1.24 + (prop) "x:X" == (prop) "|- x:X"
1.25 + "Lam x:A.B" == "Abs(A, %x.B)"
1.26 + "Pi x:A.B" => "Prod(A, %x.B)"
1.27 +
1.28 + All rules of a theory will be shown in their internal (ast * ast) form by
1.29 + Syntax.print_trans.
1.30 +
1.31 +- Caveat: rewrite rules know no "context" nor "semantics", e.g. something
1.32 + like "('a, Nil)Cons", "% Nil Cons. Cons(a, Nil)" or "Cons(a, [])" will be
1.33 + rewritten by the rules "[x]" <= "Cons(x, [])", "[]" <= "Nil"; (this is a
1.34 + general problem with macro systems);
1.35 +
1.36 +- syn_of: theory -> Syntax.syntax
1.37 +
1.38 +- Syntax.print_gram shows grammer of syntax
1.39 +
1.40 +- Syntax.print_trans shows translations of syntax
1.41 +
1.42 +- Syntax.print_syntax shows grammer and translations of syntax
1.43 +
1.44 +- Ast.stat_normalize := true enables output of statistics after normalizing;
1.45 +
1.46 +- Ast.trace_normalize := true enables verbose output while normalizing and
1.47 + statistics;
1.48 +
1.49 +- eta_contract := false disables eta contraction when printing terms;
1.50 +
1.51 +- asts: (see also Pure/Syntax/ast.ML *)
1.52 +
1.53 + (*Asts come in two flavours:
1.54 + - proper asts representing terms and types: Variables are treated like
1.55 + Constants;
1.56 + - patterns used as lhs and rhs in rules: Variables are placeholders for
1.57 + proper asts.*)
1.58 +
1.59 + datatype ast =
1.60 + Constant of string | (* "not", "_%", "fun" *)
1.61 + Variable of string | (* x, ?x, 'a, ?'a *)
1.62 + Appl of ast list; (* (f x y z), ("fun" 'a 'b) *)
1.63 +
1.64 + (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
1.65 + there are no empty asts or nullary applications; use mk_appl for convenience*)
1.66 +
1.67 +- ast output style:
1.68 + Constant a -> "a"
1.69 + Variable a -> a
1.70 + Appl [ast1, ..., astn] -> (ast1 ... astn)
1.71 +
1.72 +- sext: (see also Pure/Syntax/sextension.ML)
1.73 +
1.74 + (** datatype sext **)
1.75 +
1.76 + datatype xrule =
1.77 + op |-> of (string * string) * (string * string) |
1.78 + op <-| of (string * string) * (string * string) |
1.79 + op <-> of (string * string) * (string * string);
1.80 +
1.81 + datatype sext =
1.82 + Sext of {
1.83 + mixfix: mixfix list,
1.84 + parse_translation: (string * (term list -> term)) list,
1.85 + print_translation: (string * (term list -> term)) list} |
1.86 + NewSext of {
1.87 + mixfix: mixfix list,
1.88 + xrules: xrule list,
1.89 + parse_ast_translation: (string * (ast list -> ast)) list,
1.90 + parse_preproc: (ast -> ast) option,
1.91 + parse_postproc: (ast -> ast) option,
1.92 + parse_translation: (string * (term list -> term)) list,
1.93 + print_translation: (string * (term list -> term)) list,
1.94 + print_preproc: (ast -> ast) option,
1.95 + print_postproc: (ast -> ast) option,
1.96 + print_ast_translation: (string * (ast list -> ast)) list};
1.97 +
1.98 +- local (thy, ext) order of rules is preserved, global (merge) order is
1.99 + unspecified;
1.100 +
1.101 +- read asts contain a mixture of Constant and Variable atoms (some
1.102 + Variables become Const later);
1.103 +
1.104 +- *.thy-file/ML-section: all declarations will be exported, therefore
1.105 + one should use local-in-end constructs where appropriate; especially
1.106 + the examples in Logics/Defining could be better behaved;
1.107 +
1.108 +- [document the asts generated by the standard syntactic categories
1.109 + (idt, idts, args, ...)];
1.110 +
1.111 +- print(_ast)_translation: the constant has to disappear or execption
1.112 + Match raised, otherwise the printer will not terminate;
1.113 +
1.114 +- binders are implemented traditionally, i.e. as parse/print_translations
1.115 + (compatibility, alpha, eta, HOL hack easy);
1.116 +
1.117 +- changes to the term/ast "parsetree" structure: renamed most constants
1.118 + (_args, _idts, ...), unified typ applications, _tapp/_tappl, type atoms
1.119 + no Const rather than Free;
1.120 +
1.121 +- misfeature: eta-contraction before rewriting therefore bounded quantifiers,
1.122 + Collect etc. may fall back to internal form;
1.123 +
1.124 +- changes and fixes to printing of types:
1.125 +
1.126 + "'a => 'b => 'c" now printed as "['a,'b] => 'c";
1.127 +
1.128 + constraints now printed iff not dummyT and show_types enabled, changed
1.129 + internal print_translations accordingly; old translations that intruduce
1.130 + frees may cause printing of constraints at all occurences;
1.131 +
1.132 + constraints of bound vars now printed where bound (i.e. "%x::'a. x" rather
1.133 + than "%x. x::'a") and put in braces if necessary ("%(x::'a) y::'b. f(x,y)");
1.134 +
1.135 + constraints of bound var printed even if a free var in another scope happens
1.136 + to have the same name and type;
1.137 +
1.138 +- [man: toplevel pretty printers for NJ];
1.139 +
1.140 +- (syntactic constants "_..." (e.g. "_idts") are reserved, you may use "@..."
1.141 + or "*..." instead);
1.142 +
1.143 +- Printer: clash of fun/type constants with concrete syntax type/fun
1.144 + constants causes incorrect printing of of applications;
1.145 +