src/Pure/Syntax/ast.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2229 64acb485ecce
child 3775 a99fdf465dfb
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
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@18
    25
  val trace_norm_ast: bool ref
wenzelm@18
    26
  val stat_norm_ast: bool ref
paulson@1506
    27
  end;
wenzelm@18
    28
wenzelm@18
    29
signature AST =
paulson@1506
    30
  sig
wenzelm@258
    31
  include AST1
clasohm@0
    32
  val raise_ast: string -> ast list -> 'a
clasohm@0
    33
  val head_of_rule: ast * ast -> string
clasohm@0
    34
  val rule_error: ast * ast -> string option
clasohm@0
    35
  val fold_ast: string -> ast list -> ast
clasohm@0
    36
  val fold_ast_p: string -> ast list * ast -> ast
clasohm@0
    37
  val unfold_ast: string -> ast -> ast list
clasohm@0
    38
  val unfold_ast_p: string -> ast -> ast list * ast
wenzelm@18
    39
  val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
wenzelm@18
    40
  val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
paulson@1506
    41
  end;
clasohm@0
    42
paulson@1506
    43
structure Ast : AST =
clasohm@0
    44
struct
clasohm@0
    45
wenzelm@18
    46
(** abstract syntax trees **)
clasohm@0
    47
clasohm@0
    48
(*asts come in two flavours:
wenzelm@18
    49
   - ordinary asts representing terms and typs: Variables are (often) treated
wenzelm@18
    50
     like Constants;
clasohm@0
    51
   - patterns used as lhs and rhs in rules: Variables are placeholders for
clasohm@0
    52
     proper asts*)
clasohm@0
    53
clasohm@0
    54
datatype ast =
wenzelm@18
    55
  Constant of string |    (*"not", "_abs", "fun"*)
wenzelm@18
    56
  Variable of string |    (*x, ?x, 'a, ?'a*)
wenzelm@18
    57
  Appl of ast list;       (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
clasohm@0
    58
clasohm@0
    59
clasohm@0
    60
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
clasohm@0
    61
  there are no empty asts or nullary applications; use mk_appl for convenience*)
clasohm@0
    62
wenzelm@18
    63
fun mk_appl f [] = f
wenzelm@18
    64
  | mk_appl f args = Appl (f :: args);
clasohm@0
    65
clasohm@0
    66
clasohm@0
    67
(*exception for system errors involving asts*)
clasohm@0
    68
clasohm@0
    69
exception AST of string * ast list;
clasohm@0
    70
wenzelm@18
    71
fun raise_ast msg asts = raise AST (msg, asts);
clasohm@0
    72
clasohm@0
    73
wenzelm@18
    74
(** print asts in a LISP-like style **)
wenzelm@18
    75
wenzelm@18
    76
(* str_of_ast *)
clasohm@0
    77
clasohm@0
    78
fun str_of_ast (Constant a) = quote a
clasohm@0
    79
  | str_of_ast (Variable x) = x
clasohm@0
    80
  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
clasohm@0
    81
clasohm@0
    82
wenzelm@18
    83
(* pretty_ast *)
wenzelm@18
    84
wenzelm@18
    85
fun pretty_ast (Constant a) = Pretty.str (quote a)
wenzelm@18
    86
  | pretty_ast (Variable x) = Pretty.str x
wenzelm@18
    87
  | pretty_ast (Appl asts) =
lcp@513
    88
      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
wenzelm@18
    89
wenzelm@18
    90
wenzelm@18
    91
(* pprint_ast *)
wenzelm@18
    92
wenzelm@18
    93
val pprint_ast = Pretty.pprint o pretty_ast;
wenzelm@18
    94
wenzelm@18
    95
wenzelm@18
    96
(* pretty_rule *)
wenzelm@18
    97
wenzelm@18
    98
fun pretty_rule (lhs, rhs) =
wenzelm@235
    99
  Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
wenzelm@18
   100
wenzelm@18
   101
clasohm@0
   102
(* head_of_ast, head_of_rule *)
clasohm@0
   103
clasohm@0
   104
fun head_of_ast (Constant a) = Some a
clasohm@0
   105
  | head_of_ast (Appl (Constant a :: _)) = Some a
clasohm@0
   106
  | head_of_ast _ = None;
clasohm@0
   107
clasohm@0
   108
fun head_of_rule (lhs, _) = the (head_of_ast lhs);
clasohm@0
   109
clasohm@0
   110
clasohm@0
   111
wenzelm@18
   112
(** check translation rules **)
clasohm@0
   113
wenzelm@18
   114
(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
clasohm@0
   115
   - the head of lhs is a constant,
clasohm@0
   116
   - the lhs has unique vars,
clasohm@0
   117
   - vars of rhs is subset of vars of lhs*)
clasohm@0
   118
clasohm@0
   119
fun rule_error (rule as (lhs, rhs)) =
clasohm@0
   120
  let
clasohm@0
   121
    fun vars_of (Constant _) = []
clasohm@0
   122
      | vars_of (Variable x) = [x]
clasohm@0
   123
      | vars_of (Appl asts) = flat (map vars_of asts);
clasohm@0
   124
clasohm@0
   125
    fun unique (x :: xs) = not (x mem xs) andalso unique xs
clasohm@0
   126
      | unique [] = true;
clasohm@0
   127
clasohm@0
   128
    val lvars = vars_of lhs;
clasohm@0
   129
    val rvars = vars_of rhs;
clasohm@0
   130
  in
clasohm@0
   131
    if is_none (head_of_ast lhs) then Some "lhs has no constant head"
clasohm@0
   132
    else if not (unique lvars) then Some "duplicate vars in lhs"
clasohm@0
   133
    else if not (rvars subset lvars) then Some "rhs contains extra variables"
clasohm@0
   134
    else None
clasohm@0
   135
  end;
clasohm@0
   136
clasohm@0
   137
clasohm@0
   138
wenzelm@18
   139
(** ast translation utilities **)
clasohm@0
   140
clasohm@0
   141
(* fold asts *)
clasohm@0
   142
clasohm@0
   143
fun fold_ast _ [] = raise Match
clasohm@0
   144
  | fold_ast _ [y] = y
clasohm@0
   145
  | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
clasohm@0
   146
clasohm@0
   147
fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
clasohm@0
   148
clasohm@0
   149
clasohm@0
   150
(* unfold asts *)
clasohm@0
   151
clasohm@0
   152
fun unfold_ast c (y as Appl [Constant c', x, xs]) =
clasohm@0
   153
      if c = c' then x :: (unfold_ast c xs) else [y]
clasohm@0
   154
  | unfold_ast _ y = [y];
clasohm@0
   155
clasohm@0
   156
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
wenzelm@18
   157
      if c = c' then apfst (cons x) (unfold_ast_p c xs)
clasohm@0
   158
      else ([], y)
clasohm@0
   159
  | unfold_ast_p _ y = ([], y);
clasohm@0
   160
clasohm@0
   161
clasohm@0
   162
(** normalization of asts **)
clasohm@0
   163
wenzelm@18
   164
(* tracing options *)
wenzelm@18
   165
wenzelm@18
   166
val trace_norm_ast = ref false;
wenzelm@18
   167
val stat_norm_ast = ref false;
wenzelm@18
   168
wenzelm@18
   169
clasohm@0
   170
(* simple env *)
clasohm@0
   171
clasohm@0
   172
structure Env =
clasohm@0
   173
struct
clasohm@0
   174
  val empty = [];
clasohm@0
   175
  val add = op ::;
paulson@2229
   176
  fun get (alist,x) = the (assoc (alist,x));
clasohm@0
   177
end;
clasohm@0
   178
clasohm@0
   179
clasohm@0
   180
(* match *)
clasohm@0
   181
clasohm@0
   182
fun match ast pat =
clasohm@0
   183
  let
clasohm@0
   184
    exception NO_MATCH;
clasohm@0
   185
wenzelm@1127
   186
    fun mtch (Constant a) (Constant b) env =
clasohm@0
   187
          if a = b then env else raise NO_MATCH
wenzelm@1127
   188
      | mtch (Variable a) (Constant b) env =
clasohm@0
   189
          if a = b then env else raise NO_MATCH
wenzelm@1127
   190
      | mtch ast (Variable x) env = Env.add ((x, ast), env)
wenzelm@1127
   191
      | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
wenzelm@1127
   192
      | mtch _ _ _ = raise NO_MATCH
wenzelm@1127
   193
    and mtch_lst (ast :: asts) (pat :: pats) env =
wenzelm@1127
   194
          mtch_lst asts pats (mtch ast pat env)
wenzelm@1127
   195
      | mtch_lst [] [] env = env
wenzelm@1127
   196
      | mtch_lst _ _ _ = raise NO_MATCH;
wenzelm@1127
   197
wenzelm@1127
   198
    val (head, args) =
wenzelm@1127
   199
      (case (ast, pat) of
wenzelm@1127
   200
        (Appl asts, Appl pats) =>
wenzelm@1127
   201
          let val a = length asts and p = length pats in
wenzelm@1127
   202
            if a > p then (Appl (take (p, asts)), drop (p, asts))
wenzelm@1127
   203
            else (ast, [])
wenzelm@1127
   204
          end
wenzelm@1127
   205
      | _ => (ast, []));
clasohm@0
   206
  in
wenzelm@1127
   207
    Some (mtch head pat Env.empty, args) handle NO_MATCH => None
clasohm@0
   208
  end;
clasohm@0
   209
clasohm@0
   210
wenzelm@18
   211
(* normalize *)
clasohm@0
   212
clasohm@0
   213
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
clasohm@0
   214
wenzelm@18
   215
fun normalize trace stat get_rules pre_ast =
clasohm@0
   216
  let
clasohm@0
   217
    val passes = ref 0;
clasohm@0
   218
    val lookups = ref 0;
clasohm@0
   219
    val failed_matches = ref 0;
clasohm@0
   220
    val changes = ref 0;
clasohm@0
   221
wenzelm@18
   222
    fun subst _ (ast as Constant _) = ast
clasohm@0
   223
      | subst env (Variable x) = Env.get (env, x)
clasohm@0
   224
      | subst env (Appl asts) = Appl (map (subst env) asts);
clasohm@0
   225
clasohm@0
   226
    fun try_rules ast ((lhs, rhs) :: pats) =
clasohm@0
   227
          (case match ast lhs of
wenzelm@1127
   228
            Some (env, args) =>
wenzelm@1127
   229
              (inc changes; Some (mk_appl (subst env rhs) args))
clasohm@0
   230
          | None => (inc failed_matches; try_rules ast pats))
wenzelm@18
   231
      | try_rules _ [] = None;
clasohm@0
   232
clasohm@0
   233
    fun try ast a = (inc lookups; try_rules ast (the get_rules a));
clasohm@0
   234
clasohm@0
   235
    fun rewrite (ast as Constant a) = try ast a
clasohm@0
   236
      | rewrite (ast as Variable a) = try ast a
clasohm@0
   237
      | rewrite (ast as Appl (Constant a :: _)) = try ast a
clasohm@0
   238
      | rewrite (ast as Appl (Variable a :: _)) = try ast a
clasohm@0
   239
      | rewrite _ = None;
clasohm@0
   240
clasohm@0
   241
    fun rewrote old_ast new_ast =
clasohm@0
   242
      if trace then
clasohm@0
   243
        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
clasohm@0
   244
      else ();
clasohm@0
   245
clasohm@0
   246
    fun norm_root ast =
clasohm@0
   247
      (case rewrite ast of
clasohm@0
   248
        Some new_ast => (rewrote ast new_ast; norm_root new_ast)
clasohm@0
   249
      | None => ast);
clasohm@0
   250
clasohm@0
   251
    fun norm ast =
clasohm@0
   252
      (case norm_root ast of
clasohm@0
   253
        Appl sub_asts =>
clasohm@0
   254
          let
clasohm@0
   255
            val old_changes = ! changes;
clasohm@0
   256
            val new_ast = Appl (map norm sub_asts);
clasohm@0
   257
          in
clasohm@0
   258
            if old_changes = ! changes then new_ast else norm_root new_ast
clasohm@0
   259
          end
clasohm@0
   260
      | atomic_ast => atomic_ast);
clasohm@0
   261
clasohm@0
   262
    fun normal ast =
clasohm@0
   263
      let
clasohm@0
   264
        val old_changes = ! changes;
clasohm@0
   265
        val new_ast = norm ast;
clasohm@0
   266
      in
clasohm@0
   267
        inc passes;
clasohm@0
   268
        if old_changes = ! changes then new_ast else normal new_ast
clasohm@0
   269
      end;
clasohm@0
   270
clasohm@0
   271
wenzelm@18
   272
    val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
clasohm@0
   273
clasohm@0
   274
    val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
clasohm@0
   275
  in
wenzelm@18
   276
    if trace orelse stat then
clasohm@0
   277
      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
clasohm@0
   278
        string_of_int (! passes) ^ " passes, " ^
clasohm@0
   279
        string_of_int (! lookups) ^ " lookups, " ^
clasohm@0
   280
        string_of_int (! changes) ^ " changes, " ^
clasohm@0
   281
        string_of_int (! failed_matches) ^ " matches failed")
clasohm@0
   282
    else ();
clasohm@0
   283
    post_ast
clasohm@0
   284
  end;
clasohm@0
   285
clasohm@0
   286
wenzelm@18
   287
(* normalize_ast *)
wenzelm@18
   288
wenzelm@18
   289
fun normalize_ast get_rules ast =
wenzelm@18
   290
  normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
wenzelm@18
   291
paulson@1506
   292
end;
wenzelm@18
   293