src/Pure/net.ML
changeset 228 4f43430f226e
parent 225 76f60e6400e8
child 1458 fd510875fb71
     1.1 --- a/src/Pure/net.ML	Fri Jan 14 12:42:49 1994 +0100
     1.2 +++ b/src/Pure/net.ML	Tue Jan 18 07:53:35 1994 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4      Artificial Intelligence Programming.
     1.5      (Lawrence Erlbaum Associates, 1980).  [Chapter 14]
     1.6  
     1.7 -match_term no longer treats abstractions as wildcards but as the constant
     1.8 -*Abs*.  Requires operands to be beta-eta-normal.
     1.9 +match_term no longer treats abstractions as wildcards; instead they match 
    1.10 +only wildcards in patterns.  Requires operands to be beta-eta-normal.
    1.11  *)
    1.12  
    1.13  signature NET = 
    1.14 @@ -39,10 +39,10 @@
    1.15  (*Bound variables*)
    1.16  fun string_of_bound i = "*B*" ^ chr i;
    1.17  
    1.18 -(*Keys are preorder lists of symbols -- constants, Vars, bound vars, ...
    1.19 +(*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
    1.20    Any term whose head is a Var is regarded entirely as a Var.
    1.21 -  Abstractions are also regarded as Vars.  This covers eta-conversion
    1.22 -    and "near" eta-conversions such as %x.P(?f(x)).
    1.23 +  Abstractions are also regarded as Vars;  this covers eta-conversion
    1.24 +    and "near" eta-conversions such as %x.?P(?f(x)).
    1.25  *)
    1.26  fun add_key_of_terms (t, cs) = 
    1.27    let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    1.28 @@ -51,7 +51,7 @@
    1.29  	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    1.30    in case (head_of t) of
    1.31        Var _ => VarK :: cs
    1.32 -    | Abs (_,_,t) => VarK :: cs
    1.33 +    | Abs _ => VarK :: cs
    1.34      | _     => rands(t,cs)
    1.35    end;
    1.36  
    1.37 @@ -188,19 +188,19 @@
    1.38  	      | Const(c,_) => look1 (alist, c) nets
    1.39  	      | Free(c,_)  => look1 (alist, c) nets
    1.40  	      | Bound i    => look1 (alist, string_of_bound i) nets
    1.41 -	      | Abs _      => look1 (alist, "*Abs*") nets
    1.42 +	      | _      	   => nets
    1.43    in 
    1.44       case net of
    1.45  	 Leaf _ => nets
    1.46         | Net{var,...} =>
    1.47  	   case (head_of t) of
    1.48 -	       Var _      => if unif then net_skip (net,nets)
    1.49 -			     else var::nets	   (*only matches Var in net*)
    1.50 +	       Var _ => if unif then net_skip (net,nets)
    1.51 +			else var::nets	   	(*only matches Var in net*)
    1.52  (*If "unif" then a var instantiation in the abstraction could allow
    1.53    an eta-reduction, so regard the abstraction as a wildcard.*)
    1.54 -	     | Abs(_,_,u) => if unif then net_skip (net,nets)
    1.55 -                             else rands t (net, var::nets)
    1.56 -	     | _ => rands t (net, var::nets)	   (*var could match also*)
    1.57 +	     | Abs _ => if unif then net_skip (net,nets)
    1.58 +			else var::nets		(*only a Var can match*)
    1.59 +	     | _ => rands t (net, var::nets)	(*var could match also*)
    1.60    end;
    1.61  
    1.62  val extract_leaves = flat o map (fn Leaf(xs) => xs);