summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/net.ML

changeset 225 | 76f60e6400e8 |

parent 0 | a5a9c433f639 |

child 228 | 4f43430f226e |

1.1 --- a/src/Pure/net.ML Tue Jan 11 12:58:19 1994 +0100 1.2 +++ b/src/Pure/net.ML Fri Jan 14 08:09:07 1994 +0100 1.3 @@ -9,6 +9,9 @@ 1.4 E. Charniak, C. K. Riesbeck, D. V. McDermott. 1.5 Artificial Intelligence Programming. 1.6 (Lawrence Erlbaum Associates, 1980). [Chapter 14] 1.7 + 1.8 +match_term no longer treats abstractions as wildcards but as the constant 1.9 +*Abs*. Requires operands to be beta-eta-normal. 1.10 *) 1.11 1.12 signature NET = 1.13 @@ -33,25 +36,26 @@ 1.14 1.15 datatype key = CombK | VarK | AtomK of string; 1.16 1.17 -(*Only 'loose' bound variables could arise, since Abs nodes are skipped*) 1.18 +(*Bound variables*) 1.19 fun string_of_bound i = "*B*" ^ chr i; 1.20 1.21 (*Keys are preorder lists of symbols -- constants, Vars, bound vars, ... 1.22 - Any term whose head is a Var is regarded entirely as a Var; 1.23 - abstractions are also regarded as Vars (to cover eta-conversion) 1.24 + Any term whose head is a Var is regarded entirely as a Var. 1.25 + Abstractions are also regarded as Vars. This covers eta-conversion 1.26 + and "near" eta-conversions such as %x.P(?f(x)). 1.27 *) 1.28 fun add_key_of_terms (t, cs) = 1.29 let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) 1.30 | rands (Const(c,_), cs) = AtomK c :: cs 1.31 | rands (Free(c,_), cs) = AtomK c :: cs 1.32 - | rands (Bound i, cs) = AtomK (string_of_bound i) :: cs 1.33 + | rands (Bound i, cs) = AtomK (string_of_bound i) :: cs 1.34 in case (head_of t) of 1.35 - Var _ => VarK :: cs 1.36 + Var _ => VarK :: cs 1.37 | Abs (_,_,t) => VarK :: cs 1.38 - | _ => rands(t,cs) 1.39 + | _ => rands(t,cs) 1.40 end; 1.41 1.42 -(*convert a term to a key -- a list of keys*) 1.43 +(*convert a term to a list of keys*) 1.44 fun key_of_term t = add_key_of_terms (t, []); 1.45 1.46 1.47 @@ -173,16 +177,18 @@ 1.48 (*Return the nodes accessible from the term (cons them before nets) 1.49 "unif" signifies retrieval for unification rather than matching. 1.50 Var in net matches any term. 1.51 - Abs in object (and Var if "unif") regarded as wildcard. 1.52 - If not "unif", Var in object only matches a variable in net.*) 1.53 + Abs or Var in object: if "unif", regarded as wildcard, 1.54 + else matches only a variable in net. 1.55 +*) 1.56 fun matching unif t (net,nets) = 1.57 let fun rands _ (Leaf _, nets) = nets 1.58 | rands t (Net{comb,alist,...}, nets) = 1.59 case t of 1.60 - (f$t) => foldr (matching unif t) (rands f (comb,[]), nets) 1.61 - | (Const(c,_)) => look1 (alist, c) nets 1.62 - | (Free(c,_)) => look1 (alist, c) nets 1.63 - | (Bound i) => look1 (alist, string_of_bound i) nets 1.64 + f$t => foldr (matching unif t) (rands f (comb,[]), nets) 1.65 + | Const(c,_) => look1 (alist, c) nets 1.66 + | Free(c,_) => look1 (alist, c) nets 1.67 + | Bound i => look1 (alist, string_of_bound i) nets 1.68 + | Abs _ => look1 (alist, "*Abs*") nets 1.69 in 1.70 case net of 1.71 Leaf _ => nets 1.72 @@ -190,13 +196,16 @@ 1.73 case (head_of t) of 1.74 Var _ => if unif then net_skip (net,nets) 1.75 else var::nets (*only matches Var in net*) 1.76 - | Abs(_,_,u) => net_skip (net,nets) (*could match anything*) 1.77 +(*If "unif" then a var instantiation in the abstraction could allow 1.78 + an eta-reduction, so regard the abstraction as a wildcard.*) 1.79 + | Abs(_,_,u) => if unif then net_skip (net,nets) 1.80 + else rands t (net, var::nets) 1.81 | _ => rands t (net, var::nets) (*var could match also*) 1.82 end; 1.83 1.84 val extract_leaves = flat o map (fn Leaf(xs) => xs); 1.85 1.86 -(*return items whose key could match t*) 1.87 +(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*) 1.88 fun match_term net t = 1.89 extract_leaves (matching false t (net,[])); 1.90