raw_match : hol_type list -> term set -> term -> term -> (term,term) subst * (hol_type,hol_type) subst -> ((term,term) subst * term set) * ((hol_type,hol_type) subst * hol_type list)

- STRUCTURE
- 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 ((TmS,TmID),(TyS,TyID)) such thatwhere TmS' is TmS instantiated by TyS. 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.
aconv (subst TmS' (inst TyS pat)) ob.

The pair (tmS,tyS) is an accumulator argument. This allows raw_match to be folded through lists of terms to be matched. (TmS,TyS) must agree with (tmS,tyS). This means that if there is a {redex,residue} in TmS 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 TyS 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-pair (TmS,TyS) includes (tmS,tyS).

Finally, note that the result also includes a set (resp. a list) of term and type variables, accompanying the substitutions. These represent identity bindings that have occurred in the process of doing the match. If raw_match is to be folded across multiple problems, these output values will need to be merged with avoid_tms and avoid_tys respectively on the next call so that they cannot be instantiated a second time. Because they are identity bindings, they do not need to be referred to in validating the central identity above.

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

- COMMENTS
- Higher level matchers are generally preferable, but raw_match is occasionally useful when programming inference rules.
- SEEALSO

HOL Kananaskis-14