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