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