src/Pure/Syntax/ast.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5689 ffecea547501
child 8997 da290d99d8b2
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/ast.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
Abstract syntax trees, translation rules, matching and normalization of asts.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     8
signature AST0 =
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
     9
  sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  datatype ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    Constant of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    Variable of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
    Appl of ast list
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    14
  exception AST of string * ast list
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    15
  end;
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    16
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    17
signature AST1 =
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    18
  sig
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    19
  include AST0
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val mk_appl: ast -> ast list -> ast
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    21
  val str_of_ast: ast -> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    22
  val pretty_ast: ast -> Pretty.T
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    23
  val pretty_rule: ast * ast -> Pretty.T
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    24
  val pprint_ast: ast -> pprint_args -> unit
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    25
  val trace_norm_ast: bool ref
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    26
  val stat_norm_ast: bool ref
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    27
  end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    28
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    29
signature AST =
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    30
  sig
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 235
diff changeset
    31
  include AST1
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val head_of_rule: ast * ast -> string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val rule_error: ast * ast -> string option
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val fold_ast: string -> ast list -> ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val fold_ast_p: string -> ast list * ast -> ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val unfold_ast: string -> ast -> ast list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val unfold_ast_p: string -> ast -> ast list * ast
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    38
  val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    39
  val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    40
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
    42
structure Ast : AST =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    45
(** abstract syntax trees **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*asts come in two flavours:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
   - ordinary asts representing terms and typs: Variables are (often) treated
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
     like Constants;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
   - patterns used as lhs and rhs in rules: Variables are placeholders for
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
     proper asts*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
datatype ast =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    54
  Constant of string |    (*"not", "_abs", "fun"*)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    55
  Variable of string |    (*x, ?x, 'a, ?'a*)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    56
  Appl of ast list;       (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  there are no empty asts or nullary applications; use mk_appl for convenience*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    62
fun mk_appl f [] = f
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    63
  | mk_appl f args = Appl (f :: args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*exception for system errors involving asts*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
exception AST of string * ast list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    72
(** print asts in a LISP-like style **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    73
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    74
(* str_of_ast *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
fun str_of_ast (Constant a) = quote a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
  | str_of_ast (Variable x) = x
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    81
(* pretty_ast *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    82
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    83
fun pretty_ast (Constant a) = Pretty.str (quote a)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    84
  | pretty_ast (Variable x) = Pretty.str x
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    85
  | pretty_ast (Appl asts) =
513
97a879e8d01b updated reference to parents
lcp
parents: 258
diff changeset
    86
      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    87
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    88
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    89
(* pprint_ast *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    90
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    91
val pprint_ast = Pretty.pprint o pretty_ast;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    92
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    93
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    94
(* pretty_rule *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    95
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    96
fun pretty_rule (lhs, rhs) =
235
775dd81a58e5 cosmetic changes;
wenzelm
parents: 18
diff changeset
    97
  Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    98
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    99
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(* head_of_ast, head_of_rule *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
fun head_of_ast (Constant a) = Some a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  | head_of_ast (Appl (Constant a :: _)) = Some a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
  | head_of_ast _ = None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
fun head_of_rule (lhs, _) = the (head_of_ast lhs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   110
(** check translation rules **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   112
(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
   - the head of lhs is a constant,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
   - the lhs has unique vars,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
   - vars of rhs is subset of vars of lhs*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
fun rule_error (rule as (lhs, rhs)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    fun vars_of (Constant _) = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
      | vars_of (Variable x) = [x]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
      | vars_of (Appl asts) = flat (map vars_of asts);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
    fun unique (x :: xs) = not (x mem xs) andalso unique xs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
      | unique [] = true;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
    val lvars = vars_of lhs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
    val rvars = vars_of rhs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
    if is_none (head_of_ast lhs) then Some "lhs has no constant head"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    else if not (unique lvars) then Some "duplicate vars in lhs"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
    else if not (rvars subset lvars) then Some "rhs contains extra variables"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    else None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   137
(** ast translation utilities **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
(* fold asts *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
fun fold_ast _ [] = raise Match
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  | fold_ast _ [y] = y
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
  | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
(* unfold asts *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
fun unfold_ast c (y as Appl [Constant c', x, xs]) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
      if c = c' then x :: (unfold_ast c xs) else [y]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
  | unfold_ast _ y = [y];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   155
      if c = c' then apfst (cons x) (unfold_ast_p c xs)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
      else ([], y)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
  | unfold_ast_p _ y = ([], y);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
(** normalization of asts **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   162
(* tracing options *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   163
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   164
val trace_norm_ast = ref false;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   165
val stat_norm_ast = ref false;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   166
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   167
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
(* match *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
fun match ast pat =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
    exception NO_MATCH;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
1127
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   174
    fun mtch (Constant a) (Constant b) env =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
          if a = b then env else raise NO_MATCH
1127
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   176
      | mtch (Variable a) (Constant b) env =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
          if a = b then env else raise NO_MATCH
5689
ffecea547501 simple Env replaced by Symtab;
wenzelm
parents: 3775
diff changeset
   178
      | mtch ast (Variable x) env = Symtab.update ((x, ast), env)
1127
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   179
      | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   180
      | mtch _ _ _ = raise NO_MATCH
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   181
    and mtch_lst (ast :: asts) (pat :: pats) env =
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   182
          mtch_lst asts pats (mtch ast pat env)
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   183
      | mtch_lst [] [] env = env
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   184
      | mtch_lst _ _ _ = raise NO_MATCH;
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   185
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   186
    val (head, args) =
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   187
      (case (ast, pat) of
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   188
        (Appl asts, Appl pats) =>
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   189
          let val a = length asts and p = length pats in
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   190
            if a > p then (Appl (take (p, asts)), drop (p, asts))
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   191
            else (ast, [])
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   192
          end
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   193
      | _ => (ast, []));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
  in
5689
ffecea547501 simple Env replaced by Symtab;
wenzelm
parents: 3775
diff changeset
   195
    Some (mtch head pat Symtab.empty, args) handle NO_MATCH => None
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   199
(* normalize *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   203
fun normalize trace stat get_rules pre_ast =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
    val passes = ref 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
    val lookups = ref 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
    val failed_matches = ref 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
    val changes = ref 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   210
    fun subst _ (ast as Constant _) = ast
5689
ffecea547501 simple Env replaced by Symtab;
wenzelm
parents: 3775
diff changeset
   211
      | subst env (Variable x) = the (Symtab.lookup (env, x))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
      | subst env (Appl asts) = Appl (map (subst env) asts);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
    fun try_rules ast ((lhs, rhs) :: pats) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
          (case match ast lhs of
1127
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   216
            Some (env, args) =>
42ec82147d83 changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents: 922
diff changeset
   217
              (inc changes; Some (mk_appl (subst env rhs) args))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
          | None => (inc failed_matches; try_rules ast pats))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   219
      | try_rules _ [] = None;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    fun try ast a = (inc lookups; try_rules ast (the get_rules a));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
    fun rewrite (ast as Constant a) = try ast a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
      | rewrite (ast as Variable a) = try ast a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
      | rewrite (ast as Appl (Constant a :: _)) = try ast a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
      | rewrite (ast as Appl (Variable a :: _)) = try ast a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
      | rewrite _ = None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
    fun rewrote old_ast new_ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
      if trace then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
      else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
    fun norm_root ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
      (case rewrite ast of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
        Some new_ast => (rewrote ast new_ast; norm_root new_ast)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
      | None => ast);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
    fun norm ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
      (case norm_root ast of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
        Appl sub_asts =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
            val old_changes = ! changes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
            val new_ast = Appl (map norm sub_asts);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
          in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
            if old_changes = ! changes then new_ast else norm_root new_ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
          end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
      | atomic_ast => atomic_ast);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
    fun normal ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
        val old_changes = ! changes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
        val new_ast = norm ast;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
      in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
        inc passes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
        if old_changes = ! changes then new_ast else normal new_ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   260
    val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
    val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
  in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
    if trace orelse stat then
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
        string_of_int (! passes) ^ " passes, " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
        string_of_int (! lookups) ^ " lookups, " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
        string_of_int (! changes) ^ " changes, " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
        string_of_int (! failed_matches) ^ " matches failed")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
    else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
    post_ast
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   275
(* normalize_ast *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   276
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
fun normalize_ast get_rules ast =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   278
  normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   279
1506
192c48376d25 Elimination of fully-functorial style.
paulson
parents: 1127
diff changeset
   280
end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   281