summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 18 Jan 1994 07:53:35 +0100 | |

changeset 228 | 4f43430f226e |

parent 227 | 5415c6ad0028 |

child 229 | 4002c4cd450c |

some optimizations of Larry's

src/Pure/net.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/net.ML Fri Jan 14 12:42:49 1994 +0100 +++ b/src/Pure/net.ML Tue Jan 18 07:53:35 1994 +0100 @@ -10,8 +10,8 @@ Artificial Intelligence Programming. (Lawrence Erlbaum Associates, 1980). [Chapter 14] -match_term no longer treats abstractions as wildcards but as the constant -*Abs*. Requires operands to be beta-eta-normal. +match_term no longer treats abstractions as wildcards; instead they match +only wildcards in patterns. Requires operands to be beta-eta-normal. *) signature NET = @@ -39,10 +39,10 @@ (*Bound variables*) fun string_of_bound i = "*B*" ^ chr i; -(*Keys are preorder lists of symbols -- constants, Vars, bound vars, ... +(*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. Any term whose head is a Var is regarded entirely as a Var. - Abstractions are also regarded as Vars. This covers eta-conversion - and "near" eta-conversions such as %x.P(?f(x)). + Abstractions are also regarded as Vars; this covers eta-conversion + and "near" eta-conversions such as %x.?P(?f(x)). *) fun add_key_of_terms (t, cs) = let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) @@ -51,7 +51,7 @@ | rands (Bound i, cs) = AtomK (string_of_bound i) :: cs in case (head_of t) of Var _ => VarK :: cs - | Abs (_,_,t) => VarK :: cs + | Abs _ => VarK :: cs | _ => rands(t,cs) end; @@ -188,19 +188,19 @@ | Const(c,_) => look1 (alist, c) nets | Free(c,_) => look1 (alist, c) nets | Bound i => look1 (alist, string_of_bound i) nets - | Abs _ => look1 (alist, "*Abs*") nets + | _ => nets in case net of Leaf _ => nets | Net{var,...} => case (head_of t) of - Var _ => if unif then net_skip (net,nets) - else var::nets (*only matches Var in net*) + Var _ => if unif then net_skip (net,nets) + else var::nets (*only matches Var in net*) (*If "unif" then a var instantiation in the abstraction could allow an eta-reduction, so regard the abstraction as a wildcard.*) - | Abs(_,_,u) => if unif then net_skip (net,nets) - else rands t (net, var::nets) - | _ => rands t (net, var::nets) (*var could match also*) + | Abs _ => if unif then net_skip (net,nets) + else var::nets (*only a Var can match*) + | _ => rands t (net, var::nets) (*var could match also*) end; val extract_leaves = flat o map (fn Leaf(xs) => xs);