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