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.33               case head_of t of
    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 **)