1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
\DOC find_match
\TYPE {find_match: (term -> term -> ((term # term) list # (type # type) list))}
\SYNOPSIS
Determines whether a term matches a subterm of another term.
\DESCRIBE
Recursively destructs its second argument and attempts to match the resulting
subterms with the first term. It returns a list of differing instances of
free variables and types in the matched terms. The search is done in
a depth-first, left-to-right order.
\FAILURE
Fails if the none of the subterms of the second argument match the first.
\EXAMPLE
{
#find_match "a:num" "a:num";;
([], []) : ((term # term) list # (type # type) list)
#find_match "a:*" "T";;
([("T", "a")], [(":bool", ":*")])
: ((term # term) list # (type # type) list)
#find_match "x:num" "n < 2 ==> (a /\ b)";;
([("n", "x")], []) : ((term # term) list # (type # type) list)
#find_match "x:bool" "n < 2 ==> (a /\ b)";;
([("n < 2 ==> a /\ b", "x")], [])
: ((term # term) list # (type # type) list)
#find_match "x /\ y" "1 < 2 ==> (a /\ b)";;
([("b", "y"); ("a", "x")], [])
: ((term # term) list # (type # type) list)
}
\SEEALSO
match, find_term, find_terms
\ENDDOC
|
