src/Pure/Syntax/ast.ML

Initial revision

(*  Title:      Pure/Syntax/ast
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Abstract Syntax Trees, Syntax Rules and translation, matching, normalization
of asts.
*)

signature AST =
sig
  datatype ast =
    Constant of string |
    Variable of string |
    Appl of ast list
  val mk_appl: ast -> ast list -> ast
  exception AST of string * ast list
  val raise_ast: string -> ast list -> 'a
  val str_of_ast: ast -> string
  val head_of_rule: ast * ast -> string
  val rule_error: ast * ast -> string option
  val fold_ast: string -> ast list -> ast
  val fold_ast_p: string -> ast list * ast -> ast
  val unfold_ast: string -> ast -> ast list
  val unfold_ast_p: string -> ast -> ast list * ast
  val trace_norm: bool ref
  val stat_norm: bool ref
  val normalize: (string -> (ast * ast) list) option -> ast -> ast
end;

functor AstFun()(*: AST *) =  (* FIXME *)
struct


(** Abstract Syntax Trees **)

(*asts come in two flavours:
   - proper asts representing terms and types: Variables are treated like
     Constants;
   - patterns used as lhs and rhs in rules: Variables are placeholders for
     proper asts*)

datatype ast =
  Constant of string |    (* "not", "_%", "fun" *)
  Variable of string |    (* x, ?x, 'a, ?'a *)
  Appl of ast list;       (* (f x y z), ("fun" 'a 'b) *)


(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
  there are no empty asts or nullary applications; use mk_appl for convenience*)

fun mk_appl ast [] = ast
  | mk_appl ast asts = Appl (ast :: asts);


(*exception for system errors involving asts*)

exception AST of string * ast list;

fun raise_ast msg asts = raise (AST (msg, asts));


(* print asts in a LISP-like style *)

fun str_of_ast (Constant a) = quote a
  | str_of_ast (Variable x) = x
  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";


(* head_of_ast, head_of_rule *)

fun head_of_ast (Constant a) = Some a
  | head_of_ast (Appl (Constant a :: _)) = Some a
  | head_of_ast _ = None;

fun head_of_rule (lhs, _) = the (head_of_ast lhs);



(** check Syntax Rules **)

(*a wellformed rule (lhs, rhs): (ast * ast) has the following properties:
   - the head of lhs is a constant,
   - the lhs has unique vars,
   - vars of rhs is subset of vars of lhs*)

fun rule_error (rule as (lhs, rhs)) =
  let
    fun vars_of (Constant _) = []
      | vars_of (Variable x) = [x]
      | vars_of (Appl asts) = flat (map vars_of asts);

    fun unique (x :: xs) = not (x mem xs) andalso unique xs
      | unique [] = true;

    val lvars = vars_of lhs;
    val rvars = vars_of rhs;
  in
    if is_none (head_of_ast lhs) then Some "lhs has no constant head"
    else if not (unique lvars) then Some "duplicate vars in lhs"
    else if not (rvars subset lvars) then Some "rhs contains extra variables"
    else None
  end;



(** translation utilities **)

(* fold asts *)

fun fold_ast _ [] = raise Match
  | fold_ast _ [y] = y
  | fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];

fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);


(* unfold asts *)

fun unfold_ast c (y as Appl [Constant c', x, xs]) =
      if c = c' then x :: (unfold_ast c xs) else [y]
  | unfold_ast _ y = [y];

fun cons_fst x (xs, y) = (x :: xs, y);

fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
      if c = c' then cons_fst x (unfold_ast_p c xs)
      else ([], y)
  | unfold_ast_p _ y = ([], y);



(** normalization of asts **)

(* simple env *)

structure Env =
struct
  val empty = [];
  val add = op ::;
  val get = the o assoc;
end;


(* match *)

fun match ast pat =
  let
    exception NO_MATCH;

    fun mtch (Constant a, Constant b, env) =
          if a = b then env else raise NO_MATCH
      | mtch (Variable a, Constant b, env) =
          if a = b then env else raise NO_MATCH
      | mtch (ast, Variable x, env) = Env.add ((x, ast), env)
      | mtch (Appl asts, Appl pats, env) = mtch_lst (asts, pats, env)
      | mtch _ = raise NO_MATCH
    and mtch_lst (ast :: asts, pat :: pats, env) =
          mtch_lst (asts, pats, mtch (ast, pat, env))
      | mtch_lst ([], [], env) = env
      | mtch_lst _ = raise NO_MATCH;
  in
    Some (mtch (ast, pat, Env.empty)) handle NO_MATCH => None
  end;


(* normalize *)   (* FIXME clean *)

val trace_norm = ref false;
val stat_norm = ref false;

(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)

fun normalize get_rules pre_ast =
  let
    val passes = ref 0;
    val lookups = ref 0;
    val failed_matches = ref 0;
    val changes = ref 0;

    val trace = ! trace_norm;

    fun inc i = i := ! i + 1;

    fun subst _ (ast as (Constant _)) = ast
      | subst env (Variable x) = Env.get (env, x)
      | subst env (Appl asts) = Appl (map (subst env) asts);

    fun try_rules ast ((lhs, rhs) :: pats) =
          (case match ast lhs of
            Some env => (inc changes; Some (subst env rhs))
          | None => (inc failed_matches; try_rules ast pats))
      | try_rules ast [] = None;

    fun try ast a = (inc lookups; try_rules ast (the get_rules a));

    fun rewrite (ast as Constant a) = try ast a
      | rewrite (ast as Variable a) = try ast a
      | rewrite (ast as Appl (Constant a :: _)) = try ast a
      | rewrite (ast as Appl (Variable a :: _)) = try ast a
      | rewrite _ = None;

    fun rewrote old_ast new_ast =
      if trace then
        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
      else ();

    fun norm_root ast =
      (case rewrite ast of
        Some new_ast => (rewrote ast new_ast; norm_root new_ast)
      | None => ast);

    fun norm ast =
      (case norm_root ast of
        Appl sub_asts =>
          let
            val old_changes = ! changes;
            val new_ast = Appl (map norm sub_asts);
          in
            if old_changes = ! changes then new_ast else norm_root new_ast
          end
      | atomic_ast => atomic_ast);

    fun normal ast =
      let
        val old_changes = ! changes;
        val new_ast = norm ast;
      in
        inc passes;
        if old_changes = ! changes then new_ast else normal new_ast
      end;


    val () = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();

    val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
  in
    if trace orelse ! stat_norm then
      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
        string_of_int (! passes) ^ " passes, " ^
        string_of_int (! lookups) ^ " lookups, " ^
        string_of_int (! changes) ^ " changes, " ^
        string_of_int (! failed_matches) ^ " matches failed")
    else ();
    post_ast
  end;


end;