src/Pure/Syntax/ast.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title:      Pure/Syntax/ast
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Markus Wenzel, TU Muenchen
clasohm@0
     4
clasohm@0
     5
Abstract Syntax Trees, Syntax Rules and translation, matching, normalization
clasohm@0
     6
of asts.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
signature AST =
clasohm@0
    10
sig
clasohm@0
    11
  datatype ast =
clasohm@0
    12
    Constant of string |
clasohm@0
    13
    Variable of string |
clasohm@0
    14
    Appl of ast list
clasohm@0
    15
  val mk_appl: ast -> ast list -> ast
clasohm@0
    16
  exception AST of string * ast list
clasohm@0
    17
  val raise_ast: string -> ast list -> 'a
clasohm@0
    18
  val str_of_ast: ast -> string
clasohm@0
    19
  val head_of_rule: ast * ast -> string
clasohm@0
    20
  val rule_error: ast * ast -> string option
clasohm@0
    21
  val fold_ast: string -> ast list -> ast
clasohm@0
    22
  val fold_ast_p: string -> ast list * ast -> ast
clasohm@0
    23
  val unfold_ast: string -> ast -> ast list
clasohm@0
    24
  val unfold_ast_p: string -> ast -> ast list * ast
clasohm@0
    25
  val trace_norm: bool ref
clasohm@0
    26
  val stat_norm: bool ref
clasohm@0
    27
  val normalize: (string -> (ast * ast) list) option -> ast -> ast
clasohm@0
    28
end;
clasohm@0
    29
clasohm@0
    30
functor AstFun()(*: AST *) =  (* FIXME *)
clasohm@0
    31
struct
clasohm@0
    32
clasohm@0
    33
clasohm@0
    34
(** Abstract Syntax Trees **)
clasohm@0
    35
clasohm@0
    36
(*asts come in two flavours:
clasohm@0
    37
   - proper asts representing terms and types: Variables are treated like
clasohm@0
    38
     Constants;
clasohm@0
    39
   - patterns used as lhs and rhs in rules: Variables are placeholders for
clasohm@0
    40
     proper asts*)
clasohm@0
    41
clasohm@0
    42
datatype ast =
clasohm@0
    43
  Constant of string |    (* "not", "_%", "fun" *)
clasohm@0
    44
  Variable of string |    (* x, ?x, 'a, ?'a *)
clasohm@0
    45
  Appl of ast list;       (* (f x y z), ("fun" 'a 'b) *)
clasohm@0
    46
clasohm@0
    47
clasohm@0
    48
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
clasohm@0
    49
  there are no empty asts or nullary applications; use mk_appl for convenience*)
clasohm@0
    50
clasohm@0
    51
fun mk_appl ast [] = ast
clasohm@0
    52
  | mk_appl ast asts = Appl (ast :: asts);
clasohm@0
    53
clasohm@0
    54
clasohm@0
    55
(*exception for system errors involving asts*)
clasohm@0
    56
clasohm@0
    57
exception AST of string * ast list;
clasohm@0
    58
clasohm@0
    59
fun raise_ast msg asts = raise (AST (msg, asts));
clasohm@0
    60
clasohm@0
    61
clasohm@0
    62
(* print asts in a LISP-like style *)
clasohm@0
    63
clasohm@0
    64
fun str_of_ast (Constant a) = quote a
clasohm@0
    65
  | str_of_ast (Variable x) = x
clasohm@0
    66
  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
clasohm@0
    67
clasohm@0
    68
clasohm@0
    69
(* head_of_ast, head_of_rule *)
clasohm@0
    70
clasohm@0
    71
fun head_of_ast (Constant a) = Some a
clasohm@0
    72
  | head_of_ast (Appl (Constant a :: _)) = Some a
clasohm@0
    73
  | head_of_ast _ = None;
clasohm@0
    74
clasohm@0
    75
fun head_of_rule (lhs, _) = the (head_of_ast lhs);
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
clasohm@0
    79
(** check Syntax Rules **)
clasohm@0
    80
clasohm@0
    81
(*a wellformed rule (lhs, rhs): (ast * ast) has the following properties:
clasohm@0
    82
   - the head of lhs is a constant,
clasohm@0
    83
   - the lhs has unique vars,
clasohm@0
    84
   - vars of rhs is subset of vars of lhs*)
clasohm@0
    85
clasohm@0
    86
fun rule_error (rule as (lhs, rhs)) =
clasohm@0
    87
  let
clasohm@0
    88
    fun vars_of (Constant _) = []
clasohm@0
    89
      | vars_of (Variable x) = [x]
clasohm@0
    90
      | vars_of (Appl asts) = flat (map vars_of asts);
clasohm@0
    91
clasohm@0
    92
    fun unique (x :: xs) = not (x mem xs) andalso unique xs
clasohm@0
    93
      | unique [] = true;
clasohm@0
    94
clasohm@0
    95
    val lvars = vars_of lhs;
clasohm@0
    96
    val rvars = vars_of rhs;
clasohm@0
    97
  in
clasohm@0
    98
    if is_none (head_of_ast lhs) then Some "lhs has no constant head"
clasohm@0
    99
    else if not (unique lvars) then Some "duplicate vars in lhs"
clasohm@0
   100
    else if not (rvars subset lvars) then Some "rhs contains extra variables"
clasohm@0
   101
    else None
clasohm@0
   102
  end;
clasohm@0
   103
clasohm@0
   104
clasohm@0
   105
clasohm@0
   106
(** translation utilities **)
clasohm@0
   107
clasohm@0
   108
(* fold asts *)
clasohm@0
   109
clasohm@0
   110
fun fold_ast _ [] = raise Match
clasohm@0
   111
  | fold_ast _ [y] = y
clasohm@0
   112
  | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
clasohm@0
   113
clasohm@0
   114
fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
clasohm@0
   115
clasohm@0
   116
clasohm@0
   117
(* unfold asts *)
clasohm@0
   118
clasohm@0
   119
fun unfold_ast c (y as Appl [Constant c', x, xs]) =
clasohm@0
   120
      if c = c' then x :: (unfold_ast c xs) else [y]
clasohm@0
   121
  | unfold_ast _ y = [y];
clasohm@0
   122
clasohm@0
   123
fun cons_fst x (xs, y) = (x :: xs, y);
clasohm@0
   124
clasohm@0
   125
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
clasohm@0
   126
      if c = c' then cons_fst x (unfold_ast_p c xs)
clasohm@0
   127
      else ([], y)
clasohm@0
   128
  | unfold_ast_p _ y = ([], y);
clasohm@0
   129
clasohm@0
   130
clasohm@0
   131
clasohm@0
   132
(** normalization of asts **)
clasohm@0
   133
clasohm@0
   134
(* simple env *)
clasohm@0
   135
clasohm@0
   136
structure Env =
clasohm@0
   137
struct
clasohm@0
   138
  val empty = [];
clasohm@0
   139
  val add = op ::;
clasohm@0
   140
  val get = the o assoc;
clasohm@0
   141
end;
clasohm@0
   142
clasohm@0
   143
clasohm@0
   144
(* match *)
clasohm@0
   145
clasohm@0
   146
fun match ast pat =
clasohm@0
   147
  let
clasohm@0
   148
    exception NO_MATCH;
clasohm@0
   149
clasohm@0
   150
    fun mtch (Constant a, Constant b, env) =
clasohm@0
   151
          if a = b then env else raise NO_MATCH
clasohm@0
   152
      | mtch (Variable a, Constant b, env) =
clasohm@0
   153
          if a = b then env else raise NO_MATCH
clasohm@0
   154
      | mtch (ast, Variable x, env) = Env.add ((x, ast), env)
clasohm@0
   155
      | mtch (Appl asts, Appl pats, env) = mtch_lst (asts, pats, env)
clasohm@0
   156
      | mtch _ = raise NO_MATCH
clasohm@0
   157
    and mtch_lst (ast :: asts, pat :: pats, env) =
clasohm@0
   158
          mtch_lst (asts, pats, mtch (ast, pat, env))
clasohm@0
   159
      | mtch_lst ([], [], env) = env
clasohm@0
   160
      | mtch_lst _ = raise NO_MATCH;
clasohm@0
   161
  in
clasohm@0
   162
    Some (mtch (ast, pat, Env.empty)) handle NO_MATCH => None
clasohm@0
   163
  end;
clasohm@0
   164
clasohm@0
   165
clasohm@0
   166
(* normalize *)   (* FIXME clean *)
clasohm@0
   167
clasohm@0
   168
val trace_norm = ref false;
clasohm@0
   169
val stat_norm = ref false;
clasohm@0
   170
clasohm@0
   171
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
clasohm@0
   172
clasohm@0
   173
fun normalize get_rules pre_ast =
clasohm@0
   174
  let
clasohm@0
   175
    val passes = ref 0;
clasohm@0
   176
    val lookups = ref 0;
clasohm@0
   177
    val failed_matches = ref 0;
clasohm@0
   178
    val changes = ref 0;
clasohm@0
   179
clasohm@0
   180
    val trace = ! trace_norm;
clasohm@0
   181
clasohm@0
   182
    fun inc i = i := ! i + 1;
clasohm@0
   183
clasohm@0
   184
    fun subst _ (ast as (Constant _)) = ast
clasohm@0
   185
      | subst env (Variable x) = Env.get (env, x)
clasohm@0
   186
      | subst env (Appl asts) = Appl (map (subst env) asts);
clasohm@0
   187
clasohm@0
   188
    fun try_rules ast ((lhs, rhs) :: pats) =
clasohm@0
   189
          (case match ast lhs of
clasohm@0
   190
            Some env => (inc changes; Some (subst env rhs))
clasohm@0
   191
          | None => (inc failed_matches; try_rules ast pats))
clasohm@0
   192
      | try_rules ast [] = None;
clasohm@0
   193
clasohm@0
   194
    fun try ast a = (inc lookups; try_rules ast (the get_rules a));
clasohm@0
   195
clasohm@0
   196
    fun rewrite (ast as Constant a) = try ast a
clasohm@0
   197
      | rewrite (ast as Variable a) = try ast a
clasohm@0
   198
      | rewrite (ast as Appl (Constant a :: _)) = try ast a
clasohm@0
   199
      | rewrite (ast as Appl (Variable a :: _)) = try ast a
clasohm@0
   200
      | rewrite _ = None;
clasohm@0
   201
clasohm@0
   202
    fun rewrote old_ast new_ast =
clasohm@0
   203
      if trace then
clasohm@0
   204
        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
clasohm@0
   205
      else ();
clasohm@0
   206
clasohm@0
   207
    fun norm_root ast =
clasohm@0
   208
      (case rewrite ast of
clasohm@0
   209
        Some new_ast => (rewrote ast new_ast; norm_root new_ast)
clasohm@0
   210
      | None => ast);
clasohm@0
   211
clasohm@0
   212
    fun norm ast =
clasohm@0
   213
      (case norm_root ast of
clasohm@0
   214
        Appl sub_asts =>
clasohm@0
   215
          let
clasohm@0
   216
            val old_changes = ! changes;
clasohm@0
   217
            val new_ast = Appl (map norm sub_asts);
clasohm@0
   218
          in
clasohm@0
   219
            if old_changes = ! changes then new_ast else norm_root new_ast
clasohm@0
   220
          end
clasohm@0
   221
      | atomic_ast => atomic_ast);
clasohm@0
   222
clasohm@0
   223
    fun normal ast =
clasohm@0
   224
      let
clasohm@0
   225
        val old_changes = ! changes;
clasohm@0
   226
        val new_ast = norm ast;
clasohm@0
   227
      in
clasohm@0
   228
        inc passes;
clasohm@0
   229
        if old_changes = ! changes then new_ast else normal new_ast
clasohm@0
   230
      end;
clasohm@0
   231
clasohm@0
   232
clasohm@0
   233
    val () = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
clasohm@0
   234
clasohm@0
   235
    val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
clasohm@0
   236
  in
clasohm@0
   237
    if trace orelse ! stat_norm then
clasohm@0
   238
      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
clasohm@0
   239
        string_of_int (! passes) ^ " passes, " ^
clasohm@0
   240
        string_of_int (! lookups) ^ " lookups, " ^
clasohm@0
   241
        string_of_int (! changes) ^ " changes, " ^
clasohm@0
   242
        string_of_int (! failed_matches) ^ " matches failed")
clasohm@0
   243
    else ();
clasohm@0
   244
    post_ast
clasohm@0
   245
  end;
clasohm@0
   246
clasohm@0
   247
clasohm@0
   248
end;
clasohm@0
   249