raw_match : hol_type list -> term set
    -> term -> term
    -> (term,term) subst *
       ((hol_type,hol_type) subst * hol_type list)
    -> (term,term) subst *
       ((hol_type,hol_type) subst * hol_type list)
STRUCTURE
Term
SYNOPSIS
Primitive term matcher.
DESCRIPTION
The most primitive matching algorithm for HOL terms is raw_match. An invocation raw_match avoid_tys avoid_tms pat ob (tmS,tyS), if it succeeds, returns a substitution pair (S,T) such that 
   aconv (subst S' (inst T pat)) ob.
where S' is S instantiated by T. The arguments avoid_tys and avoid_tms specify type and term variables in pat that are not allowed to become redexes in S and T.

The pair (tmS,tyS) is an accumulator argument. This allows raw_match to be folded through lists of terms to be matched. (S,T) must agree with (tmS,tyS). This means that if there is a {redex,residue} in S and also a {redex,residue} in tmS so that both redex fields are equal, then the residue fields must be alpha-convertible. Similarly for types: if there is a {redex,residue} in T and also a {redex,residue} in tyS so that both redex fields are equal, then the residue fields must also be equal. If these conditions hold, then the result (S,T) includes (tmS,tyS).

FAILURE
raw_match will fail if no S and T meeting the above requirements can be found. If a match (S,T) between pat and ob can be found, but elements of avoid_tys would appear as redexes in T or elements of avoid_tms would appear as redexes in S, then raw_match will also fail.
EXAMPLE
We first perform a match that requires type instantitations, and also alpha-convertibility. 
   - val (S,T) = raw_match [] empty_varset
                    (Term `\x:'a. x = f (y:'b)`)
                    (Term `\a.    a = ~p`) ([],([],[]));
   > val S =
       [{redex = `(f :'b -> 'a)`, residue = `$~`},
        {redex = `(y :'b)`,       residue = `(p :bool)`}] : ...

     val T =
       ([{redex = `:'b`, residue = `:bool`},
         {redex = `:'a`, residue = `:bool`}], []) : ...
One of the main differences between raw_match and more refined derivatives of it, is that the returned substitutions are un-normalized by raw_match. If one naively applied (S,T) to \x:'a. x = f (y:'b), type instantiation with T would be applied first, yielding \x:bool. x = f (y:bool). Then substitution with S would be applied, unsuccessfully, since both f and y in the pattern term have been type instantiated, but the corresponding elements of the substitution haven’t. Thus, higher level operations building on raw_match typically instantiate S by T to get S' before applying (S',T) to the pattern term. This can be achieved by using norm_subst. However, raw_match exposes this level of detail to the programmer.

The returned type substitution T has two components (T1,T2). T1 is a substitution, and T2 is a list of type variables, encountered in the matching process, which have matched to themselves. These identity matches are held in the separate list T2 for obscure reasons. Once matching is finished, they can be ignored (which is why they are held on a separate list).

COMMENTS
Higher level matchers are generally preferable, but raw_match is occasionally useful when programming inference rules.
SEEALSO
match_term, match_terml, norm_subst, subst, inst, raw_match_type, match_type, match_typel, type_subst
HOL  Kananaskis-8