equal
deleted
inserted
replaced
11 (Lawrence Erlbaum Associates, 1980). [Chapter 14] |
11 (Lawrence Erlbaum Associates, 1980). [Chapter 14] |
12 |
12 |
13 match_term no longer treats abstractions as wildcards; instead they match |
13 match_term no longer treats abstractions as wildcards; instead they match |
14 only wildcards in patterns. Requires operands to be beta-eta-normal. |
14 only wildcards in patterns. Requires operands to be beta-eta-normal. |
15 *) |
15 *) |
16 |
|
17 val time_string_of_bound = time_init (); |
|
18 |
16 |
19 signature NET = |
17 signature NET = |
20 sig |
18 sig |
21 type key |
19 type key |
22 type 'a net |
20 type 'a net |
39 |
37 |
40 datatype key = CombK | VarK | AtomK of string; |
38 datatype key = CombK | VarK | AtomK of string; |
41 |
39 |
42 (*Bound variables*) |
40 (*Bound variables*) |
43 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256); |
41 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256); |
44 val string_of_bound = time time_string_of_bound string_of_bound; |
|
45 |
42 |
46 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. |
43 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. |
47 Any term whose head is a Var is regarded entirely as a Var. |
44 Any term whose head is a Var is regarded entirely as a Var. |
48 Abstractions are also regarded as Vars; this covers eta-conversion |
45 Abstractions are also regarded as Vars; this covers eta-conversion |
49 and "near" eta-conversions such as %x.?P(?f(x)). |
46 and "near" eta-conversions such as %x.?P(?f(x)). |