src/Pure/net.ML
 changeset 23178 07ba6b58b3d2 parent 20080 1398063aa271 child 29606 fedb8be05f24
```     1.1 --- a/src/Pure/net.ML	Thu May 31 23:02:16 2007 +0200
1.2 +++ b/src/Pure/net.ML	Thu May 31 23:47:36 2007 +0200
1.3 @@ -158,9 +158,9 @@
1.4
1.5
1.6  (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
1.7 -fun net_skip (Leaf _, nets) = nets
1.8 -  | net_skip (Net{comb,var,atoms}, nets) =
1.9 -      foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[]));
1.10 +fun net_skip (Leaf _) nets = nets
1.11 +  | net_skip (Net{comb,var,atoms}) nets =
1.12 +      fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
1.13
1.14
1.15  (** Matching and Unification **)
1.16 @@ -175,11 +175,11 @@
1.17    Abs or Var in object: if "unif", regarded as wildcard,
1.18                                     else matches only a variable in net.
1.19  *)
1.20 -fun matching unif t (net,nets) =
1.21 +fun matching unif t net nets =
1.22    let fun rands _ (Leaf _, nets) = nets
1.23          | rands t (Net{comb,atoms,...}, nets) =
1.24              case t of
1.25 -                f\$t => foldr (matching unif t) nets (rands f (comb,[]))
1.26 +                f\$t => fold_rev (matching unif t) (rands f (comb,[])) nets
1.27                | Const(c,_) => look1 (atoms, c) nets
1.28                | Free(c,_)  => look1 (atoms, c) nets
1.29                | Bound i    => look1 (atoms, Name.bound i) nets
1.30 @@ -189,11 +189,11 @@
1.31           Leaf _ => nets
1.32         | Net{var,...} =>
1.34 -                 Var _ => if unif then net_skip (net,nets)
1.35 +                 Var _ => if unif then net_skip net nets
1.36                            else var::nets           (*only matches Var in net*)
1.37    (*If "unif" then a var instantiation in the abstraction could allow
1.38      an eta-reduction, so regard the abstraction as a wildcard.*)
1.39 -               | Abs _ => if unif then net_skip (net,nets)
1.40 +               | Abs _ => if unif then net_skip net nets
1.41                            else var::nets           (*only a Var can match*)
1.42                 | _ => rands t (net, var::nets)  (*var could match also*)
1.43    end;
1.44 @@ -202,11 +202,11 @@
1.45
1.46  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
1.47  fun match_term net t =
1.48 -    extract_leaves (matching false t (net,[]));
1.49 +    extract_leaves (matching false t net []);
1.50
1.51  (*return items whose key could unify with t*)
1.52  fun unify_term net t =
1.53 -    extract_leaves (matching true t (net,[]));
1.54 +    extract_leaves (matching true t net []);
1.55
1.56
1.57  (** operations on nets **)
```