diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Fri Oct 01 13:26:22 1993 +0100 +++ b/src/Pure/Syntax/ast.ML Mon Oct 04 15:30:49 1993 +0100 @@ -1,71 +1,105 @@ -(* Title: Pure/Syntax/ast +(* Title: Pure/Syntax/ast.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen -Abstract Syntax Trees, Syntax Rules and translation, matching, normalization -of asts. +Abstract syntax trees, translation rules, matching and normalization of asts. *) -signature AST = +signature AST0 = sig + structure Pretty: PRETTY 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 str_of_ast: ast -> string + val pretty_ast: ast -> Pretty.T + val pretty_rule: (ast * ast) -> Pretty.T + val pprint_ast: ast -> pprint_args -> unit + val trace_norm_ast: bool ref + val stat_norm_ast: bool ref +end + +signature AST = +sig + include AST0 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 + val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast + val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast end; -functor AstFun()(*: AST *) = (* FIXME *) +functor AstFun(Pretty: PRETTY): AST = struct +structure Pretty = Pretty; + -(** Abstract Syntax Trees **) +(** abstract syntax trees **) (*asts come in two flavours: - - proper asts representing terms and types: Variables are treated like - Constants; + - ordinary asts representing terms and typs: Variables are (often) 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) *) + Constant of string | (*"not", "_abs", "fun"*) + Variable of string | (*x, ?x, 'a, ?'a*) + Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*) (*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); +fun mk_appl f [] = f + | mk_appl f args = Appl (f :: args); (*exception for system errors involving asts*) exception AST of string * ast list; -fun raise_ast msg asts = raise (AST (msg, asts)); +fun raise_ast msg asts = raise AST (msg, asts); -(* print asts in a LISP-like style *) +(** print asts in a LISP-like style **) + +(* str_of_ast *) 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)) ^ ")"; +(* pretty_ast *) + +fun pretty_ast (Constant a) = Pretty.str (quote a) + | pretty_ast (Variable x) = Pretty.str x + | pretty_ast (Appl asts) = + Pretty.blk (2, (Pretty.str "(") :: + (separate (Pretty.brk 1) (map pretty_ast asts)) @ [Pretty.str ")"]); + + +(* pprint_ast *) + +val pprint_ast = Pretty.pprint o pretty_ast; + + +(* pretty_rule *) + +fun pretty_rule (lhs, rhs) = + Pretty.blk + (2, [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]); + + (* head_of_ast, head_of_rule *) fun head_of_ast (Constant a) = Some a @@ -76,9 +110,9 @@ -(** check Syntax Rules **) +(** check translation rules **) -(*a wellformed rule (lhs, rhs): (ast * ast) has the following properties: +(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions: - the head of lhs is a constant, - the lhs has unique vars, - vars of rhs is subset of vars of lhs*) @@ -103,7 +137,7 @@ -(** translation utilities **) +(** ast translation utilities **) (* fold asts *) @@ -120,10 +154,8 @@ 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) + if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y) | unfold_ast_p _ y = ([], y); @@ -131,6 +163,12 @@ (** normalization of asts **) +(* tracing options *) + +val trace_norm_ast = ref false; +val stat_norm_ast = ref false; + + (* simple env *) structure Env = @@ -163,25 +201,20 @@ end; -(* normalize *) (* FIXME clean *) - -val trace_norm = ref false; -val stat_norm = ref false; +(* normalize *) (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) -fun normalize get_rules pre_ast = +fun normalize trace stat 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 + fun subst _ (ast as Constant _) = ast | subst env (Variable x) = Env.get (env, x) | subst env (Appl asts) = Appl (map (subst env) asts); @@ -189,7 +222,7 @@ (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; + | try_rules _ [] = None; fun try ast a = (inc lookups; try_rules ast (the get_rules a)); @@ -230,11 +263,11 @@ end; - val () = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else (); + 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 + if trace orelse stat then writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^ string_of_int (! passes) ^ " passes, " ^ string_of_int (! lookups) ^ " lookups, " ^ @@ -245,5 +278,11 @@ end; +(* normalize_ast *) + +fun normalize_ast get_rules ast = + normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast; + + end;