src/Pure/Syntax/ast.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 43347 f18cf88453d6
child 52175 626a757d3c2d
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/Syntax/ast.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Abstract syntax trees, translation rules, matching and normalization of asts.
     5 *)
     6 
     7 signature AST =
     8 sig
     9   datatype ast =
    10     Constant of string |
    11     Variable of string |
    12     Appl of ast list
    13   val mk_appl: ast -> ast list -> ast
    14   exception AST of string * ast list
    15   val pretty_ast: ast -> Pretty.T
    16   val pretty_rule: ast * ast -> Pretty.T
    17   val strip_positions: ast -> ast
    18   val head_of_rule: ast * ast -> string
    19   val rule_error: ast * ast -> string option
    20   val fold_ast: string -> ast list -> ast
    21   val fold_ast_p: string -> ast list * ast -> ast
    22   val unfold_ast: string -> ast -> ast list
    23   val unfold_ast_p: string -> ast -> ast list * ast
    24   val trace_raw: Config.raw
    25   val trace: bool Config.T
    26   val stats_raw: Config.raw
    27   val stats: bool Config.T
    28   val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
    29 end;
    30 
    31 structure Ast: AST =
    32 struct
    33 
    34 (** abstract syntax trees **)
    35 
    36 (*asts come in two flavours:
    37    - ordinary asts representing terms and typs: Variables are (often) treated
    38      like Constants;
    39    - patterns used as lhs and rhs in rules: Variables are placeholders for
    40      proper asts*)
    41 
    42 datatype ast =
    43   Constant of string |    (*"not", "_abs", "fun"*)
    44   Variable of string |    (*x, ?x, 'a, ?'a*)
    45   Appl of ast list;       (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
    46 
    47 (*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
    48   there are no empty asts or nullary applications; use mk_appl for convenience*)
    49 fun mk_appl f [] = f
    50   | mk_appl f args = Appl (f :: args);
    51 
    52 (*exception for system errors involving asts*)
    53 exception AST of string * ast list;
    54 
    55 
    56 
    57 (** print asts in a LISP-like style **)
    58 
    59 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
    60   | pretty_ast (Variable x) =
    61       (case Term_Position.decode x of
    62         SOME pos => Term_Position.pretty pos
    63       | NONE => Pretty.str x)
    64   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
    65 
    66 fun pretty_rule (lhs, rhs) =
    67   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
    68 
    69 
    70 (* strip_positions *)
    71 
    72 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
    73       if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x)
    74       then mk_appl (strip_positions u) (map strip_positions asts)
    75       else Appl (map strip_positions (t :: u :: v :: asts))
    76   | strip_positions (Appl asts) = Appl (map strip_positions asts)
    77   | strip_positions ast = ast;
    78 
    79 
    80 (* head_of_ast and head_of_rule *)
    81 
    82 fun head_of_ast (Constant a) = a
    83   | head_of_ast (Appl (Constant a :: _)) = a
    84   | head_of_ast _ = "";
    85 
    86 fun head_of_rule (lhs, _) = head_of_ast lhs;
    87 
    88 
    89 
    90 (** check translation rules **)
    91 
    92 fun rule_error (lhs, rhs) =
    93   let
    94     fun add_vars (Constant _) = I
    95       | add_vars (Variable x) = cons x
    96       | add_vars (Appl asts) = fold add_vars asts;
    97 
    98     val lvars = add_vars lhs [];
    99     val rvars = add_vars rhs [];
   100   in
   101     if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
   102     else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
   103     else NONE
   104   end;
   105 
   106 
   107 
   108 (** ast translation utilities **)
   109 
   110 (* fold asts *)
   111 
   112 fun fold_ast _ [] = raise Match
   113   | fold_ast _ [y] = y
   114   | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
   115 
   116 fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
   117 
   118 
   119 (* unfold asts *)
   120 
   121 fun unfold_ast c (y as Appl [Constant c', x, xs]) =
   122       if c = c' then x :: unfold_ast c xs else [y]
   123   | unfold_ast _ y = [y];
   124 
   125 fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
   126       if c = c' then apfst (cons x) (unfold_ast_p c xs)
   127       else ([], y)
   128   | unfold_ast_p _ y = ([], y);
   129 
   130 
   131 
   132 (** normalization of asts **)
   133 
   134 (* match *)
   135 
   136 fun match ast pat =
   137   let
   138     exception NO_MATCH;
   139 
   140     fun mtch (Constant a) (Constant b) env =
   141           if a = b then env else raise NO_MATCH
   142       | mtch (Variable a) (Constant b) env =
   143           if a = b then env else raise NO_MATCH
   144       | mtch ast (Variable x) env = Symtab.update (x, ast) env
   145       | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
   146       | mtch _ _ _ = raise NO_MATCH
   147     and mtch_lst (ast :: asts) (pat :: pats) env =
   148           mtch_lst asts pats (mtch ast pat env)
   149       | mtch_lst [] [] env = env
   150       | mtch_lst _ _ _ = raise NO_MATCH;
   151 
   152     val (head, args) =
   153       (case (ast, pat) of
   154         (Appl asts, Appl pats) =>
   155           let val a = length asts and p = length pats in
   156             if a > p then (Appl (take p asts), drop p asts)
   157             else (ast, [])
   158           end
   159       | _ => (ast, []));
   160   in
   161     SOME (mtch head pat Symtab.empty, args) handle NO_MATCH => NONE
   162   end;
   163 
   164 
   165 (* normalize *)
   166 
   167 val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
   168 val trace = Config.bool trace_raw;
   169 
   170 val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
   171 val stats = Config.bool stats_raw;
   172 
   173 fun message head body =
   174   Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
   175 
   176 (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
   177 fun normalize ctxt get_rules pre_ast =
   178   let
   179     val trace = Config.get ctxt trace;
   180     val stats = Config.get ctxt stats;
   181 
   182     val passes = Unsynchronized.ref 0;
   183     val failed_matches = Unsynchronized.ref 0;
   184     val changes = Unsynchronized.ref 0;
   185 
   186     fun subst _ (ast as Constant _) = ast
   187       | subst env (Variable x) = the (Symtab.lookup env x)
   188       | subst env (Appl asts) = Appl (map (subst env) asts);
   189 
   190     fun try_rules ((lhs, rhs) :: pats) ast =
   191           (case match ast lhs of
   192             SOME (env, args) =>
   193               (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args))
   194           | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast))
   195       | try_rules [] _ = NONE;
   196     val try_headless_rules = try_rules (get_rules "");
   197 
   198     fun try ast a =
   199       (case try_rules (get_rules a) ast of
   200         NONE => try_headless_rules ast
   201       | some => some);
   202 
   203     fun rewrite (ast as Constant a) = try ast a
   204       | rewrite (ast as Variable a) = try ast a
   205       | rewrite (ast as Appl (Constant a :: _)) = try ast a
   206       | rewrite (ast as Appl (Variable a :: _)) = try ast a
   207       | rewrite ast = try_headless_rules ast;
   208 
   209     fun rewrote old_ast new_ast =
   210       if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast)))
   211       else ();
   212 
   213     fun norm_root ast =
   214       (case rewrite ast of
   215         SOME new_ast => (rewrote ast new_ast; norm_root new_ast)
   216       | NONE => ast);
   217 
   218     fun norm ast =
   219       (case norm_root ast of
   220         Appl sub_asts =>
   221           let
   222             val old_changes = ! changes;
   223             val new_ast = Appl (map norm sub_asts);
   224           in
   225             if old_changes = ! changes then new_ast else norm_root new_ast
   226           end
   227       | atomic_ast => atomic_ast);
   228 
   229     fun normal ast =
   230       let
   231         val old_changes = ! changes;
   232         val new_ast = norm ast;
   233       in
   234         Unsynchronized.inc passes;
   235         if old_changes = ! changes then new_ast else normal new_ast
   236       end;
   237 
   238 
   239     val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
   240     val post_ast = normal pre_ast;
   241     val _ =
   242       if trace orelse stats then
   243         tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
   244           string_of_int (! passes) ^ " passes, " ^
   245           string_of_int (! changes) ^ " changes, " ^
   246           string_of_int (! failed_matches) ^ " matches failed")
   247       else ();
   248   in post_ast end;
   249 
   250 end;