src/Pure/Syntax/ast.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14599 c3177fffd31a
child 15421 fcf747c0b6b8
permissions -rw-r--r--
Merged in license change from Isabelle2004
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 =
paulson@1506
     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
paulson@1506
    15
  end;
wenzelm@258
    16
wenzelm@258
    17
signature AST1 =
paulson@1506
    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
paulson@1506
    31
  end;
wenzelm@18
    32
wenzelm@18
    33
signature AST =
paulson@1506
    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
paulson@1506
    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
wenzelm@18
    74
(* str_of_ast *)
clasohm@0
    75
clasohm@0
    76
fun str_of_ast (Constant a) = quote a
clasohm@0
    77
  | str_of_ast (Variable x) = x
clasohm@0
    78
  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
clasohm@0
    79
clasohm@0
    80
wenzelm@18
    81
(* pretty_ast *)
wenzelm@18
    82
berghofe@14599
    83
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
wenzelm@18
    84
  | pretty_ast (Variable x) = Pretty.str x
wenzelm@18
    85
  | pretty_ast (Appl asts) =
lcp@513
    86
      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
wenzelm@18
    87
wenzelm@18
    88
wenzelm@18
    89
(* pprint_ast *)
wenzelm@18
    90
wenzelm@18
    91
val pprint_ast = Pretty.pprint o pretty_ast;
wenzelm@18
    92
wenzelm@18
    93
wenzelm@18
    94
(* pretty_rule *)
wenzelm@18
    95
wenzelm@18
    96
fun pretty_rule (lhs, rhs) =
wenzelm@235
    97
  Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
wenzelm@18
    98
wenzelm@18
    99
clasohm@0
   100
(* head_of_ast, head_of_rule *)
clasohm@0
   101
wenzelm@9372
   102
fun head_of_ast (Constant a) = a
wenzelm@9372
   103
  | head_of_ast (Appl (Constant a :: _)) = a
wenzelm@9372
   104
  | head_of_ast _ = "";
clasohm@0
   105
wenzelm@9372
   106
fun head_of_rule (lhs, _) = head_of_ast lhs;
clasohm@0
   107
clasohm@0
   108
clasohm@0
   109
wenzelm@18
   110
(** check translation rules **)
clasohm@0
   111
wenzelm@18
   112
(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
clasohm@0
   113
   - the lhs has unique vars,
clasohm@0
   114
   - vars of rhs is subset of vars of lhs*)
clasohm@0
   115
clasohm@0
   116
fun rule_error (rule as (lhs, rhs)) =
clasohm@0
   117
  let
clasohm@0
   118
    fun vars_of (Constant _) = []
clasohm@0
   119
      | vars_of (Variable x) = [x]
clasohm@0
   120
      | vars_of (Appl asts) = flat (map vars_of asts);
clasohm@0
   121
clasohm@0
   122
    fun unique (x :: xs) = not (x mem xs) andalso unique xs
clasohm@0
   123
      | unique [] = true;
clasohm@0
   124
clasohm@0
   125
    val lvars = vars_of lhs;
clasohm@0
   126
    val rvars = vars_of rhs;
clasohm@0
   127
  in
wenzelm@9372
   128
    if not (unique lvars) then Some "duplicate vars in lhs"
clasohm@0
   129
    else if not (rvars subset lvars) then Some "rhs contains extra variables"
clasohm@0
   130
    else None
clasohm@0
   131
  end;
clasohm@0
   132
clasohm@0
   133
clasohm@0
   134
wenzelm@18
   135
(** ast translation utilities **)
clasohm@0
   136
clasohm@0
   137
(* fold asts *)
clasohm@0
   138
clasohm@0
   139
fun fold_ast _ [] = raise Match
clasohm@0
   140
  | fold_ast _ [y] = y
clasohm@0
   141
  | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
clasohm@0
   142
clasohm@0
   143
fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
clasohm@0
   144
clasohm@0
   145
clasohm@0
   146
(* unfold asts *)
clasohm@0
   147
clasohm@0
   148
fun unfold_ast c (y as Appl [Constant c', x, xs]) =
clasohm@0
   149
      if c = c' then x :: (unfold_ast c xs) else [y]
clasohm@0
   150
  | unfold_ast _ y = [y];
clasohm@0
   151
clasohm@0
   152
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
wenzelm@18
   153
      if c = c' then apfst (cons x) (unfold_ast_p c xs)
clasohm@0
   154
      else ([], y)
clasohm@0
   155
  | unfold_ast_p _ y = ([], y);
clasohm@0
   156
clasohm@0
   157
clasohm@0
   158
(** normalization of asts **)
clasohm@0
   159
clasohm@0
   160
(* match *)
clasohm@0
   161
clasohm@0
   162
fun match ast pat =
clasohm@0
   163
  let
clasohm@0
   164
    exception NO_MATCH;
clasohm@0
   165
wenzelm@1127
   166
    fun mtch (Constant a) (Constant b) env =
clasohm@0
   167
          if a = b then env else raise NO_MATCH
wenzelm@1127
   168
      | mtch (Variable a) (Constant b) env =
clasohm@0
   169
          if a = b then env else raise NO_MATCH
wenzelm@5689
   170
      | mtch ast (Variable x) env = Symtab.update ((x, ast), env)
wenzelm@1127
   171
      | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
wenzelm@1127
   172
      | mtch _ _ _ = raise NO_MATCH
wenzelm@1127
   173
    and mtch_lst (ast :: asts) (pat :: pats) env =
wenzelm@1127
   174
          mtch_lst asts pats (mtch ast pat env)
wenzelm@1127
   175
      | mtch_lst [] [] env = env
wenzelm@1127
   176
      | mtch_lst _ _ _ = raise NO_MATCH;
wenzelm@1127
   177
wenzelm@1127
   178
    val (head, args) =
wenzelm@1127
   179
      (case (ast, pat) of
wenzelm@1127
   180
        (Appl asts, Appl pats) =>
wenzelm@1127
   181
          let val a = length asts and p = length pats in
wenzelm@1127
   182
            if a > p then (Appl (take (p, asts)), drop (p, asts))
wenzelm@1127
   183
            else (ast, [])
wenzelm@1127
   184
          end
wenzelm@1127
   185
      | _ => (ast, []));
clasohm@0
   186
  in
wenzelm@5689
   187
    Some (mtch head pat Symtab.empty, args) handle NO_MATCH => None
clasohm@0
   188
  end;
clasohm@0
   189
clasohm@0
   190
wenzelm@18
   191
(* normalize *)
clasohm@0
   192
clasohm@0
   193
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
clasohm@0
   194
wenzelm@18
   195
fun normalize trace stat get_rules pre_ast =
clasohm@0
   196
  let
clasohm@0
   197
    val passes = ref 0;
clasohm@0
   198
    val failed_matches = ref 0;
clasohm@0
   199
    val changes = ref 0;
clasohm@0
   200
wenzelm@18
   201
    fun subst _ (ast as Constant _) = ast
wenzelm@5689
   202
      | subst env (Variable x) = the (Symtab.lookup (env, x))
clasohm@0
   203
      | subst env (Appl asts) = Appl (map (subst env) asts);
clasohm@0
   204
wenzelm@11733
   205
    fun try_rules ((lhs, rhs) :: pats) ast =
clasohm@0
   206
          (case match ast lhs of
wenzelm@1127
   207
            Some (env, args) =>
wenzelm@1127
   208
              (inc changes; Some (mk_appl (subst env rhs) args))
wenzelm@11733
   209
          | None => (inc failed_matches; try_rules pats ast))
wenzelm@11733
   210
      | try_rules [] _ = None;
wenzelm@11733
   211
    val try_headless_rules = try_rules (get_rules "");
clasohm@0
   212
wenzelm@11733
   213
    fun try ast a =
wenzelm@11733
   214
      (case try_rules (get_rules a) ast of
wenzelm@11733
   215
        None => try_headless_rules ast
wenzelm@11733
   216
      | some => some);
clasohm@0
   217
clasohm@0
   218
    fun rewrite (ast as Constant a) = try ast a
clasohm@0
   219
      | rewrite (ast as Variable a) = try ast a
clasohm@0
   220
      | rewrite (ast as Appl (Constant a :: _)) = try ast a
clasohm@0
   221
      | rewrite (ast as Appl (Variable a :: _)) = try ast a
wenzelm@11733
   222
      | rewrite ast = try_headless_rules ast;
clasohm@0
   223
clasohm@0
   224
    fun rewrote old_ast new_ast =
wenzelm@12262
   225
      conditional trace (fn () =>
wenzelm@12262
   226
        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast));
clasohm@0
   227
clasohm@0
   228
    fun norm_root ast =
clasohm@0
   229
      (case rewrite ast of
clasohm@0
   230
        Some new_ast => (rewrote ast new_ast; norm_root new_ast)
clasohm@0
   231
      | None => ast);
clasohm@0
   232
clasohm@0
   233
    fun norm ast =
clasohm@0
   234
      (case norm_root ast of
clasohm@0
   235
        Appl sub_asts =>
clasohm@0
   236
          let
clasohm@0
   237
            val old_changes = ! changes;
clasohm@0
   238
            val new_ast = Appl (map norm sub_asts);
clasohm@0
   239
          in
clasohm@0
   240
            if old_changes = ! changes then new_ast else norm_root new_ast
clasohm@0
   241
          end
clasohm@0
   242
      | atomic_ast => atomic_ast);
clasohm@0
   243
clasohm@0
   244
    fun normal ast =
clasohm@0
   245
      let
clasohm@0
   246
        val old_changes = ! changes;
clasohm@0
   247
        val new_ast = norm ast;
clasohm@0
   248
      in
clasohm@0
   249
        inc passes;
clasohm@0
   250
        if old_changes = ! changes then new_ast else normal new_ast
clasohm@0
   251
      end;
clasohm@0
   252
clasohm@0
   253
wenzelm@12262
   254
    val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
clasohm@0
   255
wenzelm@9372
   256
    val post_ast = normal pre_ast;
clasohm@0
   257
  in
wenzelm@12262
   258
    conditional (trace orelse stat) (fn () =>
wenzelm@12262
   259
      tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
clasohm@0
   260
        string_of_int (! passes) ^ " passes, " ^
clasohm@0
   261
        string_of_int (! changes) ^ " changes, " ^
wenzelm@12262
   262
        string_of_int (! failed_matches) ^ " matches failed"));
clasohm@0
   263
    post_ast
clasohm@0
   264
  end;
clasohm@0
   265
clasohm@0
   266
wenzelm@18
   267
(* normalize_ast *)
wenzelm@18
   268
wenzelm@12262
   269
val trace_ast = ref false;
wenzelm@12262
   270
val stat_ast = ref false;
wenzelm@12262
   271
wenzelm@18
   272
fun normalize_ast get_rules ast =
wenzelm@8997
   273
  normalize (! trace_ast) (! stat_ast) get_rules ast;
wenzelm@18
   274
paulson@1506
   275
end;
wenzelm@18
   276