AST translation rules no longer require constant head on LHS;
authorwenzelm
Sun Jul 16 21:00:10 2000 +0200 (2000-07-16)
changeset 93727834e56e2277
parent 9371 2f06293f291a
child 9373 78a11a353473
AST translation rules no longer require constant head on LHS;
src/Pure/Syntax/ast.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/ast.ML	Sun Jul 16 20:59:31 2000 +0200
     1.2 +++ b/src/Pure/Syntax/ast.ML	Sun Jul 16 21:00:10 2000 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4    val fold_ast_p: string -> ast list * ast -> ast
     1.5    val unfold_ast: string -> ast -> ast list
     1.6    val unfold_ast_p: string -> ast -> ast list * ast
     1.7 -  val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
     1.8 -  val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
     1.9 +  val normalize: bool -> bool -> (string -> (ast * ast) list) -> ast -> ast
    1.10 +  val normalize_ast: (string -> (ast * ast) list) -> ast -> ast
    1.11    end;
    1.12  
    1.13  structure Ast : AST =
    1.14 @@ -99,18 +99,17 @@
    1.15  
    1.16  (* head_of_ast, head_of_rule *)
    1.17  
    1.18 -fun head_of_ast (Constant a) = Some a
    1.19 -  | head_of_ast (Appl (Constant a :: _)) = Some a
    1.20 -  | head_of_ast _ = None;
    1.21 +fun head_of_ast (Constant a) = a
    1.22 +  | head_of_ast (Appl (Constant a :: _)) = a
    1.23 +  | head_of_ast _ = "";
    1.24  
    1.25 -fun head_of_rule (lhs, _) = the (head_of_ast lhs);
    1.26 +fun head_of_rule (lhs, _) = head_of_ast lhs;
    1.27  
    1.28  
    1.29  
    1.30  (** check translation rules **)
    1.31  
    1.32  (*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
    1.33 -   - the head of lhs is a constant,
    1.34     - the lhs has unique vars,
    1.35     - vars of rhs is subset of vars of lhs*)
    1.36  
    1.37 @@ -126,8 +125,7 @@
    1.38      val lvars = vars_of lhs;
    1.39      val rvars = vars_of rhs;
    1.40    in
    1.41 -    if is_none (head_of_ast lhs) then Some "lhs has no constant head"
    1.42 -    else if not (unique lvars) then Some "duplicate vars in lhs"
    1.43 +    if not (unique lvars) then Some "duplicate vars in lhs"
    1.44      else if not (rvars subset lvars) then Some "rhs contains extra variables"
    1.45      else None
    1.46    end;
    1.47 @@ -218,13 +216,13 @@
    1.48            | None => (inc failed_matches; try_rules ast pats))
    1.49        | try_rules _ [] = None;
    1.50  
    1.51 -    fun try ast a = (inc lookups; try_rules ast (the get_rules a));
    1.52 +    fun try ast a = (inc lookups; try_rules ast (get_rules a));
    1.53  
    1.54      fun rewrite (ast as Constant a) = try ast a
    1.55        | rewrite (ast as Variable a) = try ast a
    1.56        | rewrite (ast as Appl (Constant a :: _)) = try ast a
    1.57        | rewrite (ast as Appl (Variable a :: _)) = try ast a
    1.58 -      | rewrite _ = None;
    1.59 +      | rewrite ast = try ast "";
    1.60  
    1.61      fun rewrote old_ast new_ast =
    1.62        if trace then
    1.63 @@ -259,7 +257,7 @@
    1.64  
    1.65      val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
    1.66  
    1.67 -    val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
    1.68 +    val post_ast = normal pre_ast;
    1.69    in
    1.70      if trace orelse stat then
    1.71        writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
     2.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 16 20:59:31 2000 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Jul 16 21:00:10 2000 +0200
     2.3 @@ -141,13 +141,7 @@
     2.4  type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
     2.5  
     2.6  fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
     2.7 -
     2.8 -
     2.9 -(* lookup_ruletab *)
    2.10 -
    2.11 -fun lookup_ruletab tab =
    2.12 -  if Symtab.is_empty tab then None
    2.13 -  else Some (fn a => Symtab.lookup_multi (tab, a));
    2.14 +fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
    2.15  
    2.16  
    2.17  (* empty, extend, merge ruletabs *)