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